Argon2 on x86-64: prove the filling matrix state transition

lean/VerifiedGarbage/Proof/Argon2/FillStep.lean

@@ -0,0 +1,41 @@
+import VerifiedGarbage.Spec.Argon2
+
+/-! Expose the reviewed filling step's random word, matrix update and leakage log. -/
+
+namespace VG.Proof.Argon2.FillStep
+
+open VG.Spec.Argon2
+
+def random (p : Params) (pass lane slice index : Nat) (blocks : Array Block) : Word :=
+  if independent p pass slice then
+    (addressBlock p pass lane slice (index / 128 + 1))[index % 128]'(Nat.mod_lt _ (by decide))
+  else
+    (blocks[lane * p.laneLen + (slice * p.segmentLen + index + p.laneLen - 1) % p.laneLen]?.getD zeroBlock)[0]
+
+def update (p : Params) (pass lane slice index : Nat) (blocks : Array Block) (word : Word) : Array Block :=
+  let column := slice * p.segmentLen + index
+  let current := lane * p.laneLen + column
+  let prev := blocks[lane * p.laneLen + (column + p.laneLen - 1) % p.laneLen]?.getD zeroBlock
+  let ref := reference p pass lane slice index word
+  let other := blocks[ref.1 * p.laneLen + ref.2]?.getD zeroBlock
+  let next := compress prev other
+  blocks.set! current (if pass = 0 then next else xorBlock next (blocks[current]?.getD zeroBlock))
+
+theorem not_skipped (pass slice index : Nat) (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index) :
+    ¬(pass = 0 ∧ slice = 0 ∧ index < 2) := by omega
+
+theorem memory (p : Params) (pass lane slice index : Nat) (s : FillState)
+    (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index) :
+    (fillBlock p pass slice lane index s).memory =
+      update p pass lane slice index s.memory (random p pass lane slice index s.memory) := by
+  rw [fillBlock, ite_eq_right (not_skipped pass slice index active)]
+  rfl
+
+theorem indices (p : Params) (pass lane slice index : Nat) (s : FillState)
+    (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index) :
+    (fillBlock p pass slice lane index s).indices = if independent p pass slice then s.indices
+      else reference p pass lane slice index (random p pass lane slice index s.memory) :: s.indices := by
+  rw [fillBlock, ite_eq_right (not_skipped pass slice index active)]
+  rfl
+
+end VG.Proof.Argon2.FillStep

lean/VerifiedGarbage/Proof/Argon2/Matrix.lean

@@ -0,0 +1,39 @@
+import VerifiedGarbage.Spec.Argon2.Contract
+import VerifiedGarbage.Proof.Framework.Offset
+
+/-! Relate the lane-major assembly allocation to the specification's block array. -/
+
+namespace VG.Proof.Argon2
+
+open VG VG.Spec.Argon2
+
+def matrixCell (base : Addr) (k : Nat) : Addr := base + BitVec.ofNat 64 (k * 1024)
+
+structure Represents (m : Mem) (base : Addr) (n : Nat) (blocks : Array Block) : Prop where
+  size : blocks.size = n
+  block : ∀ k < n, blockAt m (matrixCell base k) = blocks[k]?.getD zeroBlock
+
+theorem Represents.update {m m' : Mem} {base : Addr} {n : Nat} {blocks : Array Block}
+    (h : Represents m base n blocks) (k : Nat) (hk : k < n) (value : Block)
+    (written : blockAt m' (matrixCell base k) = value)
+    (kept : ∀ j < n, j ≠ k → blockAt m' (matrixCell base j) = blockAt m (matrixCell base j)) :
+    Represents m' base n (blocks.set! k value) := by
+  refine ⟨(Array.size_set! _ _ _).trans h.size, ?_⟩
+  intro j hj
+  rw [Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds]
+  by_cases equal : k = j
+  · rw [ite_eq_left equal, ite_eq_left (by rw [h.size]; exact hk), Option.getD_some]
+    rw [← equal]; exact written
+  · rw [ite_eq_right equal]
+    exact (kept j hj (Ne.symm equal)).trans (h.block j hj)
+
+theorem matrixCell_sub (base : Addr) (n k : Nat) (hk : k < n) :
+    Region.Sub ⟨matrixCell base k, 1024⟩ ⟨base, n * 1024⟩ :=
+  Offset.sub_base base (by omega)
+
+theorem matrixCell_disjoint (base : Addr) (n i j : Nat) (bound : n * 1024 < 2 ^ 64)
+    (hi : i < n) (hj : j < n) (different : i ≠ j) :
+    (⟨matrixCell base i, 1024⟩ : Region).Disjoint ⟨matrixCell base j, 1024⟩ :=
+  Offset.disjoint base (by omega) (by omega) (by omega)
+
+end VG.Proof.Argon2

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelInvariant.lean

@@ -0,0 +1,53 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernel
+
+/-! Each active-cell update retains the frame and matrix allocation invariant. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+theorem Done.frame_word {s t : State} {p : Params} {pass lane slice index : Nat}
+    (h : Ready p pass lane slice index s) (done : Done s t p pass lane slice index)
+    (d : Nat) (bound : d + 8 ≤ 272) (separate : d + 8 ≤ 16 ∨ 24 ≤ d) :
+    t.mem.readW (off (t.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 := by
+  rw [done.regs .rbp (by simp [calleeSaved])]
+  have sub : Region.Sub ⟨off (s.gpr .rbp) d, 8⟩ ⟨s.gpr .rbp, 272⟩ := Offset.sub_base _ bound
+  have currentSub : Region.Sub ⟨current s p lane slice index, 1024⟩ ⟨matrix s, p.blocks * 1024⟩ :=
+    cell_sub p _ h.bounds.lanesPositive h.bounds.laneBound
+      (Proof.Argon2.column_lt p h.bounds.lanesPositive h.bounds.sliceBound h.bounds.indexBound)
+  exact done.frame.readW (r := ⟨off (s.gpr .rbp) d, 8⟩) (Region.contains_self _ _) (by
+    intro r hr
+    simp only [writes, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl
+    · exact ((h.layout.matrixFrame.sub_left currentSub).symm).sub_left sub
+    · exact h.layout.frameWork.sub_left sub
+    · exact h.layout.frameStack.sub_left sub
+    · exact Offset.disjoint _ separate (by omega) (by decide)) (by decide)
+
+theorem Done.retains {s t : State} {p : Params} {pass lane slice index : Nat}
+    (h : Ready p pass lane slice index s) (done : Done s t p pass lane slice index) :
+    Ready p pass lane slice index t := by
+  have bp := done.regs .rbp (by simp [calleeSaved])
+  have sp := done.regs .rsp (by simp [calleeSaved])
+  have matrix' : matrix t = matrix s := done.frame_word h 232 (by decide) (by decide)
+  have work' : work t = work s := done.frame_word h 248 (by decide) (by decide)
+  refine ⟨?_, h.bounds, ?_, (done.frame_word h 0 (by decide) (by decide)).trans h.passWord,
+    (done.frame_word h 184 (by decide) (by decide)).trans h.lanesWord⟩
+  · constructor
+    · rw [done.rd, done.wr, bp]; exact h.layout.frameRead
+    · rw [done.wr, bp]; exact h.layout.frameWrite
+    · rw [matrix', done.wr]; exact h.layout.matrixWrite
+    · rw [work', done.wr]; exact h.layout.workWrite
+    · rw [matrix', work']; exact h.layout.matrixWork
+    · rw [matrix', bp]; exact h.layout.matrixFrame
+    · rw [matrix', sp]; exact h.layout.matrixStack
+    · rw [bp, work']; exact h.layout.frameWork
+    · rw [bp, sp]; exact h.layout.frameStack
+    · rw [sp, work']; exact h.layout.stackWork
+  · exact ⟨(done.regs .rbx (by simp [calleeSaved])).trans h.position.current,
+      (done.regs .r12 (by simp [calleeSaved])).trans h.position.laneLength,
+      (done.regs .r13 (by simp [calleeSaved])).trans h.position.segmentLength,
+      (done.regs .r14 (by simp [calleeSaved])).trans h.position.slice,
+      (done.regs .r15 (by simp [calleeSaved])).trans h.position.index⟩
+
+end VG.Proof.Argon2.X86_64.FillKernel

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelMatrix.lean

@@ -0,0 +1,60 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernel
+import VerifiedGarbage.Proof.Argon2.Matrix
+
+/-! The filling step updates exactly one cell of the specification's block array. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+def currentIndex (p : Params) (lane slice index : Nat) : Nat :=
+  lane * p.laneLen + currentColumn p slice index
+
+def previousIndex (p : Params) (lane slice index : Nat) : Nat :=
+  lane * p.laneLen + previousColumn p slice index
+
+def referenceIndex (s : State) (p : Params) (pass lane slice index : Nat) : Nat :=
+  let ref := Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)
+  ref.1 * p.laneLen + ref.2
+
+def nextBlock (s : State) (p : Params) (pass lane slice index : Nat) (blocks : Array Block) : Block :=
+  let next := Spec.Argon2.compress (blocks[previousIndex p lane slice index]?.getD zeroBlock)
+    (blocks[referenceIndex s p pass lane slice index]?.getD zeroBlock)
+  if pass = 0 then next else xorBlock next (blocks[currentIndex p lane slice index]?.getD zeroBlock)
+
+theorem Done.represents {s t : State} {p : Params} {pass lane slice index : Nat}
+    (ready : Ready p pass lane slice index s) (done : Done s t p pass lane slice index)
+    (blocks : Array Block) (represented : Proof.Argon2.Represents s.mem (matrix s) p.blocks blocks) :
+    Proof.Argon2.Represents t.mem (matrix s) p.blocks
+      (blocks.set! (currentIndex p lane slice index) (nextBlock s p pass lane slice index blocks)) := by
+  have currentBound := Proof.Argon2.current_cell_lt p ready.bounds.lanesPositive
+    ready.bounds.laneBound ready.bounds.sliceBound ready.bounds.indexBound
+  have previousBound := Proof.Argon2.previous_cell_lt p ready.bounds.lanesPositive
+    ready.bounds.memoryMinimum ready.bounds.laneBound (column := currentColumn p slice index)
+  have referenceBound := Proof.Argon2.reference_cell_lt p ready.bounds.lanesPositive
+    ready.bounds.memoryMinimum pass lane slice index (s.gpr .rdi) ready.bounds.laneBound
+  apply represented.update (currentIndex p lane slice index) currentBound (nextBlock s p pass lane slice index blocks)
+  · have block := done.block
+    change blockAt t.mem (Proof.Argon2.matrixCell (matrix s) (currentIndex p lane slice index)) = _ at block
+    have prev := represented.block (previousIndex p lane slice index) previousBound
+    have other := represented.block (referenceIndex s p pass lane slice index) referenceBound
+    have old := represented.block (currentIndex p lane slice index) currentBound
+    change blockAt s.mem (previous s p lane slice index) = _ at prev
+    change blockAt s.mem (referenced s p pass lane slice index) = _ at other
+    change blockAt s.mem (current s p lane slice index) = _ at old
+    rw [prev, other, old] at block
+    exact block
+  · intro j hj different
+    apply FillCompress.block_frame done.frame
+    intro r hr
+    simp only [writes, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl
+    · have blocksBound := Nat.lt_of_le_of_lt (Proof.Argon2.blocks_le_memory p) ready.bounds.memoryBound
+      exact Proof.Argon2.matrixCell_disjoint _ p.blocks j (currentIndex p lane slice index)
+        (Nat.lt_trans (Nat.mul_lt_mul_of_pos_right blocksBound (by decide)) (by decide)) hj currentBound different
+    · exact ready.layout.matrixWork.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hj)
+    · exact ready.layout.matrixStack.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hj)
+    · exact (ready.layout.matrixFrame.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hj)).sub_right
+        (Offset.sub_base _ (by decide))
+
+end VG.Proof.Argon2.X86_64.FillKernel

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelSpec.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelMatrix
+import VerifiedGarbage.Proof.Argon2.FillStep
+
+/-! Relate the complete assembly step to the reviewed filling-state transition. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+theorem update_spec (s : State) (p : Params) (pass lane slice index : Nat) (state : FillState)
+    (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index)
+    (random : s.gpr .rdi = Proof.Argon2.FillStep.random p pass lane slice index state.memory) :
+    state.memory.set! (currentIndex p lane slice index) (nextBlock s p pass lane slice index state.memory) =
+      (fillBlock p pass slice lane index state).memory := by
+  rw [Proof.Argon2.FillStep.memory p pass lane slice index state active]
+  unfold nextBlock referenceIndex
+  rw [random]
+  rfl
+
+theorem code_spec_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (matrix s) p.blocks state.memory)
+    (random : s.gpr .rdi = Proof.Argon2.FillStep.random p pass lane slice index state.memory) :
+    WP isa Impl.Argon2.X86_64.FillKernel.code s fun t => Done s t p pass lane slice index ∧
+      Proof.Argon2.Represents t.mem (matrix s) p.blocks (fillBlock p pass slice lane index state).memory := by
+  refine (code_ok s p pass lane slice index ready).mono ?_
+  intro t done
+  have represented' := done.represents ready state.memory represented
+  rw [update_spec s p pass lane slice index state ready.bounds.active random] at represented'
+  exact ⟨done, represented'⟩
+
+end VG.Proof.Argon2.X86_64.FillKernel

lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitRepresent.lean

@@ -0,0 +1,21 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInit
+import VerifiedGarbage.Proof.Argon2.Matrix
+
+/-! Memory initialization establishes the shared matrix representation invariant. -/
+
+namespace VG.Proof.Argon2.X86_64.MemoryInit
+
+open VG VG.Spec.Argon2
+
+theorem Initialized.represents {m : Mem} {base : Addr} {p : Params} {h0 : List Byte}
+    (positive : 0 < p.lanes) (lanePositive : 0 < p.laneLen)
+    (h : Initialized m base p.lanes p.laneLen p.lanes h0) :
+    Proof.Argon2.Represents m base p.blocks (initMemory p h0).memory := by
+  refine ⟨Proof.Argon2.initMemory_size p h0, ?_⟩
+  intro k hk
+  rw [Array.getElem?_eq_getElem (by rw [Proof.Argon2.initMemory_size]; exact hk), Option.getD_some]
+  unfold Proof.Argon2.matrixCell
+  rw [Nat.mul_comm k 1024]
+  exact h.spec positive lanePositive k hk
+
+end VG.Proof.Argon2.X86_64.MemoryInit