From fe528eb1a9a9d2269d111e1c9c75ef5b4f62970f Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 18:51:27 +0000
Subject: [PATCH] Prove Argon2 dependent random-word selection on x86-64

---
 .../Impl/Argon2/X86_64/DependentWord.lean     | 21 ++++++
 .../Proof/Argon2/X86_64/DependentWord.lean    | 68 +++++++++++++++++++
 .../Proof/Argon2/X86_64/DependentWordCT.lean  | 53 +++++++++++++++
 .../Proof/Argon2/X86_64/DependentWordLit.lean | 10 +++
 .../Argon2/X86_64/DependentWordPointer.lean   | 52 ++++++++++++++
 .../Argon2/X86_64/DependentWordState.lean     | 25 +++++++
 .../Proof/Argon2/X86_64/FillKernelStable.lean | 16 +++++
 7 files changed, 245 insertions(+)
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/DependentWord.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWord.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordLit.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordPointer.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordState.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelStable.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/DependentWord.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/DependentWord.lean
new file mode 100644
index 000000000..726cfc16d
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/DependentWord.lean
@@ -0,0 +1,21 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillKernel
+
+/-! Read the previous cell's first word for data-dependent addressing. Only the
+public loop position and matrix base determine the read address.
+-/
+
+namespace VG.Impl.Argon2.X86_64.DependentWord
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def args : List Instr := [.mov .rcx (.reg .rdi), .mov .rax (.reg .rbx)]
+
+def pointer : Prog isa := .seq (.block FillKernel.matrix)
+  (.seq FillColumn.code (.seq (.block args) BlockAddress.code))
+
+def read : List Instr := [.mov .rdi (.mem (at_ .rax 0))]
+
+def code : Prog isa := .seq pointer (.block read)
+
+end VG.Impl.Argon2.X86_64.DependentWord
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWord.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWord.lean
new file mode 100644
index 000000000..4125b3273
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWord.lean
@@ -0,0 +1,68 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.DependentWordPointer
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelSpec
+
+/-! Select the specified secret random word from the public previous-cell address. -/
+
+namespace VG.Proof.Argon2.X86_64.DependentWord
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.DependentWord
+
+theorem read_ok (s : State) (hr : InRegions (s.rd ++ s.wr) (s.gpr .rax) 8) :
+    WP isa (.block Impl.Argon2.X86_64.DependentWord.read) s fun t => t.gpr .rdi = s.mem.readW (s.gpr .rax) 64 ∧ Divide.Keeps [.rdi] s t := by
+  apply WP.of_runBlock
+  simp only [Impl.Argon2.X86_64.DependentWord.read, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, State.load64,
+    ea_at, BitVec.add_zero, hr, Option.map_some,
+    Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg, ite_true]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    simp only [RegUpd.gpr_setReg, hr, ite_false]
+  all_goals rfl
+
+theorem code_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : FillKernel.Ready p pass lane slice index s) : WP isa code s fun t =>
+      t.gpr .rdi = (blockAt s.mem (FillKernel.previous s p lane slice index))[0] ∧
+      Divide.Keeps ReferenceMap.changed s t := by
+  unfold code
+  refine WP.seq ((pointer_ok s p pass lane slice index h).mono ?_)
+  rintro a ⟨pointer, keeps⟩
+  have bound := Proof.Argon2.previous_column_lt p h.bounds.lanesPositive h.bounds.memoryMinimum
+    (slice * p.segmentLen + index)
+  have cover := h.layout.cell_cover h.bounds.lanesPositive h.bounds.laneBound bound
+  have hr : InRegions (a.rd ++ a.wr) (a.gpr .rax) 8 := by
+    rw [keeps.rd, keeps.wr, pointer]
+    have contains : (⟨FillKernel.previous s p lane slice index, 1024⟩ : Region).Contains
+        (FillKernel.previous s p lane slice index) 8 :=
+      by simpa only [BitVec.add_zero] using (Offset.contains_base
+        (FillKernel.previous s p lane slice index) (d := 0) (n := 8) (k := 1024) (by decide) (by decide))
+    obtain ⟨r, hr, hc⟩ := cover _ _ ⟨⟨FillKernel.previous s p lane slice index, 1024⟩,
+      by simp [FillKernel.previous, FillKernel.previousColumn, FillKernel.currentColumn], contains⟩
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  refine (read_ok a hr).mono ?_
+  rintro t ⟨random, tail⟩
+  refine ⟨?_, keeps.trans (tail.mono (by decide))⟩
+  rw [random, pointer, keeps.mem]
+  change s.mem.readW _ 64 = (blockAt _ _)[(⟨0, by decide⟩ : Fin 128)]
+  rw [blockAt_get]
+  change s.mem.readW _ 64 = s.mem.readW (_ + 0#64) 64
+  rw [BitVec.add_zero]
+
+theorem code_spec_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : FillKernel.Ready p pass lane slice index s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory)
+    (dependent : independent p pass slice = false) : WP isa code s fun t =>
+      t.gpr .rdi = Proof.Argon2.FillStep.random p pass lane slice index state.memory ∧
+      Divide.Keeps ReferenceMap.changed s t := by
+  refine (code_ok s p pass lane slice index h).mono ?_
+  rintro t ⟨random, keeps⟩
+  have bound := Proof.Argon2.previous_cell_lt p h.bounds.lanesPositive h.bounds.memoryMinimum
+    h.bounds.laneBound (column := FillKernel.currentColumn p slice index)
+  have block := represented.block (FillKernel.previousIndex p lane slice index) bound
+  change blockAt s.mem (FillKernel.previous s p lane slice index) = _ at block
+  rw [block] at random
+  refine ⟨?_, keeps⟩
+  simpa only [Proof.Argon2.FillStep.random, dependent, Bool.false_eq_true, ite_false, FillKernel.previousIndex, FillKernel.previousColumn,
+    FillKernel.currentColumn] using random
+
+end VG.Proof.Argon2.X86_64.DependentWord
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordCT.lean
new file mode 100644
index 000000000..408e40078
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordCT.lean
@@ -0,0 +1,53 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.DependentWord
+import VerifiedGarbage.Proof.Argon2.X86_64.DependentWordLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! The previous cell is read at an address determined by public parameters. -/
+
+namespace VG.Proof.Argon2.X86_64.DependentWord
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.DependentWord
+
+structure Related (p : Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  left : FillKernel.Ready p pass lane slice index s
+  right : FillKernel.Ready p pass lane slice index t
+  bases : s.gpr .rbp = t.gpr .rbp
+  matrices : FillKernel.matrix s = FillKernel.matrix t
+
+theorem pointer_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.rbp, .r12, .r13, .r14, .r15], s.gpr r = t.gpr r)
+    pointer (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp, .r12, .r13, .r14, .r15])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+theorem read_rel : RelCT isa (fun s t => s.gpr .rax = t.gpr .rax) (.block Impl.Argon2.X86_64.DependentWord.read) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rax])
+    (fun _ _ h => Taint.agree_ofRegs (by
+      intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      subst r
+      exact h)) (by taint_decide)
+
+theorem code_rel (p : Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) code (fun _ _ => True) := by
+  have trace := pointer_rel.mono (P' := Related p pass lane slice index) (by
+    intro s t h r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl | rfl
+    · exact h.bases
+    · exact h.left.position.laneLength.trans h.right.position.laneLength.symm
+    · exact h.left.position.segmentLength.trans h.right.position.segmentLength.symm
+    · exact h.left.position.slice.trans h.right.position.slice.symm
+    · exact h.left.position.index.trans h.right.position.index.symm) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨pointer_ok s p pass lane slice index h.left, pointer_ok t p pass lane slice index h.right⟩)
+  have publicTrace : RelCT isa (Related p pass lane slice index) pointer
+      (fun s t => s.gpr .rax = t.gpr .rax) := full.mono (fun _ _ h => h) (by
+    intro a b h
+    obtain ⟨_, s, t, hp, ⟨pa, _⟩, ⟨pb, _⟩⟩ := h
+    have equal : FillKernel.previous s p lane slice index = FillKernel.previous t p lane slice index := by
+      unfold FillKernel.previous; rw [hp.matrices]
+    exact pa.trans (equal.trans pb.symm))
+  exact publicTrace.seq read_rel
+
+end VG.Proof.Argon2.X86_64.DependentWord
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordLit.lean
new file mode 100644
index 000000000..e0d6657f7
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.DependentWord
+
+/-! Checked literal of the public predecessor-address computation. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.DependentWord.pointer
+
+end VG
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordPointer.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordPointer.lean
new file mode 100644
index 000000000..222bc410b
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordPointer.lean
@@ -0,0 +1,52 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.DependentWord
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelPrepare
+
+/-! The data-dependent word's address is the specification's cyclic predecessor. -/
+
+namespace VG.Proof.Argon2.X86_64.DependentWord
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.DependentWord
+
+theorem args_ok (s : State) : WP isa (.block args) s fun t =>
+    t.gpr .rcx = s.gpr .rdi ∧ t.gpr .rax = s.gpr .rbx ∧ Divide.Keeps [.rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [args, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    RegUpd.gpr_setReg, reduceCtorEq, ite_true, ite_false, Option.map_some,
+    Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+    simp only [RegUpd.gpr_setReg, hr.1, hr.2, ite_false]
+  all_goals rfl
+
+theorem pointer_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : FillKernel.Ready p pass lane slice index s) : WP isa pointer s fun t =>
+      t.gpr .rax = FillKernel.previous s p lane slice index ∧ Divide.Keeps ReferenceMap.changed s t := by
+  unfold pointer
+  refine WP.seq ((FillKernel.load_ok s .r8 232 (h.layout.frameRead 232 (by simp))).mono ?_)
+  rintro a ⟨base, ka⟩
+  have k : Divide.Keeps ReferenceMap.changed s a := ka.mono (by decide)
+  have pos := h.position.of_keeps k
+  have columnBound := Proof.Argon2.column_lt p h.bounds.lanesPositive h.bounds.sliceBound h.bounds.indexBound
+  have segment := Proof.Argon2.segmentLen_ge_two p h.bounds.lanesPositive h.bounds.memoryMinimum
+  have q := Proof.Argon2.laneLen_segments p h.bounds.lanesPositive
+  refine WP.seq ((FillColumn.code_nat_ok a slice p.segmentLen index p.laneLen
+    pos.slice pos.segmentLength pos.index pos.laneLength (by omega)
+    (Nat.lt_trans h.bounds.laneLength_bound (by decide)) columnBound).mono ?_)
+  rintro b ⟨_, prev, kb⟩
+  refine WP.seq ((args_ok b).mono ?_)
+  rintro c ⟨col, laneReg, kc⟩
+  have col' := col.trans prev
+  have lane' : c.gpr .rax = BitVec.ofNat 64 lane := laneReg.trans ((kb.regs .rbx (by decide)).trans pos.current)
+  have length : c.gpr .r12 = BitVec.ofNat 64 p.laneLen :=
+    (kc.regs .r12 (by decide)).trans ((kb.regs .r12 (by decide)).trans pos.laneLength)
+  refine (BlockAddress.code_nat_ok c lane
+    ((slice * p.segmentLen + index + p.laneLen - 1) % p.laneLen) p.laneLen lane' col' length).mono ?_
+  rintro t ⟨address, kt⟩
+  refine ⟨?_, ((k.trans (kb.mono (by decide))).trans (kc.mono (by decide))).trans (kt.mono (by decide))⟩
+  rw [address, kc.regs .r8 (by decide), kb.regs .r8 (by decide), base]
+  rfl
+
+end VG.Proof.Argon2.X86_64.DependentWord
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordState.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordState.lean
new file mode 100644
index 000000000..33d7648fe
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/DependentWordState.lean
@@ -0,0 +1,25 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.DependentWord
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelStable
+
+/-! The dependent source hands the filling step its random word and unchanged matrix. -/
+
+namespace VG.Proof.Argon2.X86_64.DependentWord
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.DependentWord
+
+theorem state_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : FillKernel.Ready p pass lane slice index s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory)
+    (dependent : independent p pass slice = false) : WP isa code s fun t =>
+      t.gpr .rdi = Proof.Argon2.FillStep.random p pass lane slice index state.memory ∧
+      FillKernel.Ready p pass lane slice index t ∧
+      Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks state.memory ∧
+      Divide.Keeps ReferenceMap.changed s t := by
+  refine (code_spec_ok s p pass lane slice index h state represented dependent).mono ?_
+  rintro t ⟨random, keeps⟩
+  refine ⟨random, h.of_keeps keeps, ?_, keeps⟩
+  have base : FillKernel.matrix t = FillKernel.matrix s := by
+    unfold FillKernel.matrix; rw [keeps.mem, keeps.regs .rbp (by decide)]
+  rw [keeps.mem, base]; exact represented
+
+end VG.Proof.Argon2.X86_64.DependentWord
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelStable.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelStable.lean
new file mode 100644
index 000000000..007196a70
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelStable.lean
@@ -0,0 +1,16 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelArgs
+
+/-! Register-only helpers retain the filling allocation and position invariants. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64
+
+theorem Ready.of_keeps {p : Spec.Argon2.Params} {pass lane slice index : Nat} {s t : State}
+    (h : Ready p pass lane slice index s) (k : Divide.Keeps ReferenceMap.changed s t) :
+    Ready p pass lane slice index t := by
+  refine ⟨h.layout.of_keeps k, h.bounds, h.position.of_keeps k, ?_, ?_⟩
+  · rw [k.mem, k.regs .rbp (by decide)]; exact h.passWord
+  · rw [k.mem, k.regs .rbp (by decide)]; exact h.lanesWord
+
+end VG.Proof.Argon2.X86_64.FillKernel