From 811799a8361df2ab80d4f66edf211a464982d2e4 Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 14:25:43 +0000
Subject: [PATCH 1/4] Assemble Argon2 reference mapping and prove its argument
 setup

---
 .../Impl/Argon2/X86_64/FirstLane.lean         | 20 ++++++
 .../Impl/Argon2/X86_64/ReferenceMap.lean      | 42 +++++++++++
 .../Proof/Argon2/X86_64/FirstLane.lean        | 61 ++++++++++++++++
 .../Proof/Argon2/X86_64/FirstLaneCT.lean      | 21 ++++++
 .../Proof/Argon2/X86_64/FirstLaneLit.lean     | 10 +++
 .../Proof/Argon2/X86_64/ReferenceMapArgs.lean | 70 +++++++++++++++++++
 6 files changed, 224 insertions(+)
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/FirstLane.lean
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLane.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneLit.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapArgs.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/FirstLane.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FirstLane.lean
new file mode 100644
index 000000000..3cad23882
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FirstLane.lean
@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Force the current lane on the first slice of the first pass.
+
+The pass and slice are public in `r9` and `r14`. The current lane is in
+`rbx`; `r8` initially contains J₂ modulo the lane count. Only the public
+position controls a branch.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FirstLane
+
+open VG.X86_64
+
+def test : List Instr := [.mov .rax (.reg .r9), .alu .or .rax (.reg .r14)]
+
+def current : List Instr := [.mov .r8 (.reg .rbx)]
+
+def code : Prog isa := .seq (.block test) (.ite .e (.block current) (.block []))
+
+end VG.Impl.Argon2.X86_64.FirstLane
diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
new file mode 100644
index 000000000..3e51d9b7b
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
@@ -0,0 +1,42 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceLane
+import VerifiedGarbage.Impl.Argon2.X86_64.FirstLane
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceStart
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceCount
+import VerifiedGarbage.Impl.Argon2.X86_64.Relative
+import VerifiedGarbage.Impl.Argon2.X86_64.Wrap
+
+/-! Complete mapping of J₁ and J₂ to a reference lane and column.
+
+`rdi` contains the random word and `rsi` the lane count. The current
+lane is in `rbx`, lane and segment lengths in `r12` and `r13`, slice and
+index in `r14` and `r15`. The pass counter is at the frame base `rbp`:
+H₀'s first word is reused after memory initialization. `r9` and `rdi`
+receive the reference lane and column. The input word is retained in `r11`.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ReferenceMap
+
+open VG.X86_64
+
+def loadPass : List Instr := [.mov .r9 (.mem { base := .rbp })]
+
+def laneArgs : List Instr := [.mov .rdi (.reg .r8), .mov .rsi (.reg .rbx)]
+
+def relativeArgs : List Instr := [
+  .mov .r9 (.reg .rdi), .mov .rdi (.reg .r11), .mov .rsi (.reg .r8)]
+
+def wrapArgs : List Instr := [
+  .mov .rdi (.reg .rax), .alu .add .rdi (.reg .r10), .mov .rsi (.reg .r12)]
+
+def code : Prog isa :=
+  .seq ReferenceLane.code
+  (.seq (.block loadPass)
+  (.seq FirstLane.code
+  (.seq (.block laneArgs)
+  (.seq ReferenceStart.code
+  (.seq ReferenceCount.code
+  (.seq (.block relativeArgs)
+  (.seq Relative.code
+  (.seq (.block wrapArgs) Wrap.code))))))))
+
+end VG.Impl.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLane.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLane.lean
new file mode 100644
index 000000000..4d3c83efe
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLane.lean
@@ -0,0 +1,61 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FirstLane
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! The first reference window stays in the current lane. -/
+
+namespace VG.Proof.Argon2.X86_64.FirstLane
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FirstLane
+
+theorem test_ok (s : State) : WP isa (.block test) s fun t =>
+    t.zf = decide (s.gpr .r9 = 0 ∧ s.gpr .r14 = 0) ∧ Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [test, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.gpr_setReg, RegUpd.zf_setReg, RegUpd.zf_arithFlags,
+    reduceCtorEq, ite_true, Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨?_, ?_⟩
+  · apply Bool.eq_iff_iff.mpr
+    simp only [beq_iff_eq, decide_eq_true_eq]
+    change (s.gpr .r9 ||| s.gpr .r14) = 0#64 ↔ _
+    exact BitVec.or_eq_zero_iff
+  · constructor
+    · intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      simp only [RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, hr, ite_false]
+    all_goals rfl
+
+theorem current_ok (s : State) : WP isa (.block current) s fun t =>
+    t.gpr .r8 = s.gpr .rbx ∧ Divide.Keeps [.r8] s t := by
+  apply WP.of_runBlock
+  simp only [current, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    RegUpd.gpr_setReg, ite_true, Option.map_some, Option.some.injEq, exists_eq_left']
+  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) : WP isa code s fun t =>
+    t.gpr .r8 = (if s.gpr .r9 = 0 ∧ s.gpr .r14 = 0 then s.gpr .rbx else s.gpr .r8) ∧
+    Divide.Keeps [.rax, .r8] s t := by
+  unfold code
+  refine WP.seq ((test_ok s).mono ?_)
+  rintro a ⟨flag, keeps⟩
+  refine WP.ite (decide (s.gpr .r9 = 0 ∧ s.gpr .r14 = 0))
+    (by simp only [eval, flag]) ?_ ?_
+  · intro h
+    have position := of_decide_eq_true h
+    refine (current_ok a).mono ?_
+    rintro t ⟨out, tail⟩
+    refine ⟨?_, (keeps.mono (by decide)).trans (tail.mono (by decide))⟩
+    simpa only [position, and_self, ite_true, keeps.regs .rbx (by decide)] using out
+  · intro h
+    have position := of_decide_eq_false h
+    apply WP.of_runBlock
+    simp only [runBlock_nil, Option.some.injEq, exists_eq_left']
+    refine ⟨?_, keeps.mono (by decide)⟩
+    simp only [position, ite_false]
+    exact keeps.regs .r8 (by decide)
+
+end VG.Proof.Argon2.X86_64.FirstLane
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneCT.lean
new file mode 100644
index 000000000..f9094a469
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneCT.lean
@@ -0,0 +1,21 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FirstLaneLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! The first-slice override branches only on the public position. -/
+
+namespace VG.Proof.Argon2.X86_64.FirstLane
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FirstLane
+
+theorem code_rel : RelCT isa
+    (fun s t => s.gpr .r9 = t.gpr .r9 ∧ s.gpr .r14 = t.gpr .r14) code
+    (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.r9, .r14])
+    (fun _ _ h => Taint.agree_ofRegs (by
+      intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl
+      · exact h.1
+      · exact h.2)) (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.FirstLane
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneLit.lean
new file mode 100644
index 000000000..c128ec479
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FirstLaneLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FirstLane
+
+/-! A checked literal for the public first-slice lane override. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FirstLane.code
+
+end VG
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapArgs.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapArgs.lean
new file mode 100644
index 000000000..d1987e655
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapArgs.lean
@@ -0,0 +1,70 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceMap
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! Register preparation for the reference-index stages. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+theorem pass_ea (s : State) : s.ea { base := .rbp } = s.gpr .rbp := by
+  change s.gpr .rbp + 0#64 = s.gpr .rbp
+  exact BitVec.add_zero _
+
+theorem loadPass_ok (s : State) (read : InRegions (s.rd ++ s.wr) (s.gpr .rbp) 8) :
+    WP isa (.block loadPass) s fun t =>
+      t.gpr .r9 = s.mem.readW (s.gpr .rbp) 64 ∧ Divide.Keeps [.r9] s t := by
+  apply WP.of_runBlock
+  simp only [loadPass, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    pass_ea, State.load64, read, ite_true, Option.map_some, RegUpd.gpr_setReg,
+    Option.some.injEq, exists_eq_left']
+  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 laneArgs_ok (s : State) : WP isa (.block laneArgs) s fun t =>
+    t.gpr .rdi = s.gpr .r8 ∧ t.gpr .rsi = s.gpr .rbx ∧
+    Divide.Keeps [.rdi, .rsi] s t := by
+  apply WP.of_runBlock
+  simp only [laneArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, RegUpd.gpr_setReg, reduceCtorEq, ite_true, ite_false,
+    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 relativeArgs_ok (s : State) : WP isa (.block relativeArgs) s fun t =>
+    t.gpr .r9 = s.gpr .rdi ∧ t.gpr .rdi = s.gpr .r11 ∧ t.gpr .rsi = s.gpr .r8 ∧
+    Divide.Keeps [.r9, .rdi, .rsi] s t := by
+  apply WP.of_runBlock
+  simp only [relativeArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, RegUpd.gpr_setReg, reduceCtorEq, ite_true, ite_false,
+    Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, 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.1, hr.2.2, ite_false]
+  all_goals rfl
+
+theorem wrapArgs_ok (s : State) : WP isa (.block wrapArgs) s fun t =>
+    t.gpr .rdi = s.gpr .rax + s.gpr .r10 ∧ t.gpr .rsi = s.gpr .r12 ∧
+    Divide.Keeps [.rdi, .rsi] s t := by
+  apply WP.of_runBlock
+  simp only [wrapArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    Option.map_some, Option.bind_some, RegUpd.gpr_setReg, RegUpd.gpr_arithFlags,
+    reduceCtorEq, ite_true, ite_false, 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, RegUpd.gpr_arithFlags, hr.1, hr.2, ite_false]
+  all_goals rfl
+
+end VG.Proof.Argon2.X86_64.ReferenceMap

From 2dfbee9c130db9323916d308d37751aae3b8c330 Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 14:51:42 +0000
Subject: [PATCH 2/4] Prove complete Argon2 reference-lane selection and its
 dimension bounds

---
 .../Impl/Argon2/X86_64/ReferenceMap.lean      |  17 +-
 .../Proof/Argon2/X86_64/ReferenceMapLane.lean |  83 +++++++++
 .../Argon2/X86_64/ReferenceMapState.lean      | 172 ++++++++++++++++++
 3 files changed, 265 insertions(+), 7 deletions(-)
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLane.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
index 3e51d9b7b..3fbdae5f5 100644
--- a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
@@ -28,15 +28,18 @@ def relativeArgs : List Instr := [
 def wrapArgs : List Instr := [
   .mov .rdi (.reg .rax), .alu .add .rdi (.reg .r10), .mov .rsi (.reg .r12)]
 
+def chooseLane : Prog isa :=
+  .seq ReferenceLane.code (.seq (.block loadPass) FirstLane.code)
+
+def prepareLanes : Prog isa := .seq chooseLane (.block laneArgs)
+
+def window : Prog isa := .seq ReferenceStart.code ReferenceCount.code
+
 def code : Prog isa :=
-  .seq ReferenceLane.code
-  (.seq (.block loadPass)
-  (.seq FirstLane.code
-  (.seq (.block laneArgs)
-  (.seq ReferenceStart.code
-  (.seq ReferenceCount.code
+  .seq prepareLanes
+  (.seq window
   (.seq (.block relativeArgs)
   (.seq Relative.code
-  (.seq (.block wrapArgs) Wrap.code))))))))
+  (.seq (.block wrapArgs) Wrap.code))))
 
 end VG.Impl.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLane.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLane.lean
new file mode 100644
index 000000000..884bbfe01
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLane.lean
@@ -0,0 +1,83 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapState
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceLane
+import VerifiedGarbage.Proof.Argon2.X86_64.FirstLane
+
+/-! Choose the reference lane, restore the pass and prepare the window inputs. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+structure Chosen (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  selected : t.gpr .r8 = BitVec.ofNat 64 (chosenLane p pass lane slice (s.gpr .rdi))
+  pass : t.gpr .r9 = BitVec.ofNat 64 pass
+  original : t.gpr .r11 = s.gpr .rdi
+  position : Position p lane slice index t
+  keeps : Divide.Keeps changed s t
+
+theorem chooseLane_ok (s : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) :
+    WP isa chooseLane s (Chosen p pass lane slice index s) := by
+  have lanesNat : (s.gpr .rsi).toNat = p.lanes := by
+    rw [ready.lanes, word_nat _ (by have := ready.bounds.lanesBound; omega)]
+  unfold chooseLane
+  refine WP.seq ((ReferenceLane.code_ok s
+    (by rw [lanesNat]; exact ready.bounds.lanesPositive)
+    (by rw [lanesNat]; exact ready.bounds.lanesBound)).mono ?_)
+  rintro a ⟨laneNat, original, ka⟩
+  have ka' : Divide.Keeps changed s a := ka.mono (by decide)
+  have readA : InRegions (a.rd ++ a.wr) (a.gpr .rbp) 8 := by
+    rw [ka'.rd, ka'.wr, ka'.regs .rbp (by decide)]
+    exact ready.passRead
+  have laneWord : a.gpr .r8 = BitVec.ofNat 64 ((s.gpr .rdi >>> 32).toNat % p.lanes) := by
+    calc
+      a.gpr .r8 = BitVec.ofNat 64 (a.gpr .r8).toNat := by simp only [BitVec.ofNat_toNat, BitVec.setWidth_eq]
+      _ = _ := by rw [laneNat, lanesNat]
+  refine WP.seq ((loadPass_ok a readA).mono ?_)
+  rintro b ⟨loaded, kb⟩
+  have kb' : Divide.Keeps changed a b := kb.mono (by decide)
+  have kab := ka'.trans kb'
+  have pb := ready.position.of_keeps kab
+  have passWord : b.gpr .r9 = BitVec.ofNat 64 pass := by
+    rw [loaded, ka'.mem, ka'.regs .rbp (by decide)]
+    exact ready.passWord
+  have passZero : b.gpr .r9 = 0 ↔ pass = 0 := by
+    rw [passWord]
+    exact word_zero _ (by have := ready.bounds.passBound; omega)
+  have sliceZero : b.gpr .r14 = 0 ↔ slice = 0 := by
+    rw [pb.slice]
+    exact word_zero _ (by have := ready.bounds.sliceBound; omega)
+  refine (FirstLane.code_ok b).mono ?_
+  rintro t ⟨out, kt⟩
+  have kt' : Divide.Keeps changed b t := kt.mono (by decide)
+  refine ⟨?_, ?_, ?_, ready.position.of_keeps (kab.trans kt'), kab.trans kt'⟩
+  · rw [out]
+    by_cases position : pass = 0 ∧ slice = 0 <;>
+      simp only [passZero, sliceZero, pb.current, kb.regs .r8 (by decide), laneWord,
+        chosenLane, position, and_self, ite_true, ite_false]
+  · exact (kt.regs .r9 (by decide)).trans passWord
+  · exact (kt.regs .r11 (by decide)).trans ((kb.regs .r11 (by decide)).trans original)
+
+structure Prepared (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  selected : t.gpr .rdi = BitVec.ofNat 64 (chosenLane p pass lane slice (s.gpr .rdi))
+  current : t.gpr .rsi = BitVec.ofNat 64 lane
+  pass : (t.gpr .r9).toNat = pass
+  original : t.gpr .r11 = s.gpr .rdi
+  position : Position p lane slice index t
+  keeps : Divide.Keeps changed s t
+
+theorem prepareLanes_ok (s : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) :
+    WP isa prepareLanes s (Prepared p pass lane slice index s) := by
+  unfold prepareLanes
+  refine WP.seq ((chooseLane_ok s p pass lane slice index ready).mono ?_)
+  intro a ha
+  refine (laneArgs_ok a).mono ?_
+  rintro t ⟨laneOut, currentOut, kt⟩
+  have kt' : Divide.Keeps changed a t := kt.mono (by decide)
+  refine ⟨laneOut.trans ha.selected, currentOut.trans ha.position.current, ?_,
+    (kt.regs .r11 (by decide)).trans ha.original,
+    ha.position.of_keeps kt', ha.keeps.trans kt'⟩
+  rw [kt.regs .r9 (by decide), ha.pass, word_nat _ (by have := ready.bounds.passBound; omega)]
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean
new file mode 100644
index 000000000..3885fc12e
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean
@@ -0,0 +1,172 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceCount
+
+/-! Parameters and register invariants for the complete reference mapping. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64
+
+/-- Every stage preserves the enclosing loop's callee-saved registers. -/
+def changed : List Reg := [.rax, .rdx, .rcx, .r8, .r9, .r10, .r11, .rdi, .rsi]
+
+structure Bounds (p : Spec.Argon2.Params) (pass lane slice index : Nat) : Prop where
+  lanesPositive : 0 < p.lanes
+  lanesBound : p.lanes < 2 ^ 32
+  memoryMinimum : 8 * p.lanes ≤ p.memory
+  memoryBound : p.memory < 2 ^ 32
+  passBound : pass < 2 ^ 32
+  laneBound : lane < p.lanes
+  sliceBound : slice < 4
+  indexBound : index < p.segmentLen
+  active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index
+
+structure Position (p : Spec.Argon2.Params) (lane slice index : Nat) (s : State) : Prop where
+  current : s.gpr .rbx = BitVec.ofNat 64 lane
+  laneLength : s.gpr .r12 = BitVec.ofNat 64 p.laneLen
+  segmentLength : s.gpr .r13 = BitVec.ofNat 64 p.segmentLen
+  slice : s.gpr .r14 = BitVec.ofNat 64 slice
+  index : s.gpr .r15 = BitVec.ofNat 64 index
+
+theorem Position.of_keeps {s t : State} {p : Spec.Argon2.Params} {lane slice index : Nat}
+    (h : Position p lane slice index s) (k : Divide.Keeps changed s t) :
+    Position p lane slice index t :=
+  ⟨(k.regs .rbx (by decide)).trans h.current,
+    (k.regs .r12 (by decide)).trans h.laneLength,
+    (k.regs .r13 (by decide)).trans h.segmentLength,
+    (k.regs .r14 (by decide)).trans h.slice,
+    (k.regs .r15 (by decide)).trans h.index⟩
+
+structure Ready (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s : State) : Prop where
+  bounds : Bounds p pass lane slice index
+  position : Position p lane slice index s
+  lanes : s.gpr .rsi = BitVec.ofNat 64 p.lanes
+  passRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp) 8
+  passWord : s.mem.readW (s.gpr .rbp) 64 = BitVec.ofNat 64 pass
+
+def chosenLane (p : Spec.Argon2.Params) (pass lane slice : Nat) (random : Addr) : Nat :=
+  if pass = 0 ∧ slice = 0 then lane else (random >>> 32).toNat % p.lanes
+
+theorem chosenLane_bound (p : Spec.Argon2.Params) (pass lane slice : Nat) (random : Addr)
+    (positive : 0 < p.lanes) (bound : lane < p.lanes) :
+    chosenLane p pass lane slice random < p.lanes := by
+  unfold chosenLane
+  split
+  · exact bound
+  · exact Nat.mod_lt _ positive
+
+theorem word_nat (n : Nat) (bound : n < 2 ^ 64) : (BitVec.ofNat 64 n).toNat = n := by
+  rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt bound]
+
+theorem word_zero (n : Nat) (bound : n < 2 ^ 64) : BitVec.ofNat 64 n = (0 : Addr) ↔ n = 0 := by
+  constructor
+  · intro h
+    have hn := congrArg BitVec.toNat h
+    rw [word_nat n bound] at hn
+    exact hn
+  · intro h; rw [h]; rfl
+
+theorem word_eq (x y : Nat) (hx : x < 2 ^ 64) (hy : y < 2 ^ 64) :
+    BitVec.ofNat 64 x = BitVec.ofNat 64 y ↔ x = y := by
+  constructor
+  · intro h
+    have hn := congrArg BitVec.toNat h
+    rw [word_nat x hx, word_nat y hy] at hn
+    exact hn
+  · intro h; rw [h]
+
+theorem Bounds.laneLength_bound {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) : p.laneLen < 2 ^ 32 := by
+  have hb : p.laneLen ≤ p.blocks := by
+    rw [Proof.Argon2.blocks_lanes p h.lanesPositive]
+    exact Nat.le_mul_of_pos_left _ h.lanesPositive
+  exact Nat.lt_of_le_of_lt (Nat.le_trans hb (Proof.Argon2.blocks_le_memory p)) h.memoryBound
+
+theorem Bounds.window_positive {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) :
+    0 < ReferenceCount.windowBase p pass slice + index ∧
+      (index = 0 → 0 < ReferenceCount.windowBase p pass slice) := by
+  have hp := Proof.Argon2.reference_count_positive p h.lanesPositive h.memoryMinimum
+    pass slice index true h.active (by intro _ _; rfl)
+  rw [ReferenceCount.spec_count] at hp
+  change 0 < ReferenceCount.windowBase p pass slice + index - 1 at hp
+  constructor
+  · omega
+  · intro zero; rw [zero, Nat.add_zero] at hp; omega
+
+def windowSize (p : Spec.Argon2.Params) (pass lane slice index : Nat) (random : Addr) : Nat :=
+  Spec.Argon2.referenceCount p pass slice index (chosenLane p pass lane slice random == lane)
+
+def windowStart (p : Spec.Argon2.Params) (pass slice : Nat) : Nat :=
+  if pass = 0 then 0 else (slice + 1) * p.segmentLen % p.laneLen
+
+def relativeValue (p : Spec.Argon2.Params) (pass lane slice index : Nat) (random : Addr) : Nat :=
+  let count := windowSize p pass lane slice index random
+  let j := (random &&& 0xffffffff).toNat
+  count - 1 - count * (j * j / 2 ^ 32) / 2 ^ 32
+
+theorem Bounds.segment_le_lane {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) : p.segmentLen ≤ p.laneLen := by
+  have segments := Proof.Argon2.laneLen_segments p h.lanesPositive
+  omega
+
+theorem Bounds.index_bound64 {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) : index < 2 ^ 64 :=
+  Nat.lt_trans (Nat.lt_of_lt_of_le h.indexBound h.segment_le_lane)
+    (Nat.lt_trans h.laneLength_bound (by decide))
+
+theorem Bounds.chosenLane_bound64 {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) (random : Addr) :
+    chosenLane p pass lane slice random < 2 ^ 64 :=
+  Nat.lt_trans (chosenLane_bound p pass lane slice random h.lanesPositive h.laneBound)
+    (Nat.lt_trans h.lanesBound (by decide))
+
+theorem Bounds.lane_bound64 {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) : lane < 2 ^ 64 :=
+  Nat.lt_trans h.laneBound (Nat.lt_trans h.lanesBound (by decide))
+
+theorem Bounds.windowSize_positive {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) (random : Addr) :
+    0 < windowSize p pass lane slice index random := by
+  apply Proof.Argon2.reference_count_positive p h.lanesPositive h.memoryMinimum
+    pass slice index _ h.active
+  intro firstPass firstSlice
+  simp only [chosenLane, firstPass, firstSlice, and_self, ite_true]
+  exact beq_iff_eq.mpr rfl
+
+theorem Bounds.windowSize_bound32 {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) (random : Addr) :
+    windowSize p pass lane slice index random < 2 ^ 32 :=
+  Proof.Argon2.reference_count_32 p h.lanesPositive h.memoryMinimum h.memoryBound
+    pass slice index _ h.sliceBound h.indexBound
+
+theorem Bounds.windowSize_lt_lane {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) (random : Addr) :
+    windowSize p pass lane slice index random < p.laneLen :=
+  Proof.Argon2.reference_count_lt_lane p h.lanesPositive h.memoryMinimum
+    pass slice index _ h.sliceBound h.indexBound
+
+theorem Bounds.laneLength_positive {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) : 0 < p.laneLen := by
+  have seg := Proof.Argon2.segmentLen_ge_two p h.lanesPositive h.memoryMinimum
+  have len := Proof.Argon2.laneLen_segments p h.lanesPositive
+  omega
+
+theorem Bounds.windowStart_lt_lane {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) : windowStart p pass slice < p.laneLen := by
+  unfold windowStart
+  split
+  · exact h.laneLength_positive
+  · exact Nat.mod_lt _ h.laneLength_positive
+
+theorem Bounds.sum_bound {p : Spec.Argon2.Params} {pass lane slice index : Nat}
+    (h : Bounds p pass lane slice index) (random : Addr) :
+    windowStart p pass slice + relativeValue p pass lane slice index random < 2 * p.laneLen := by
+  have start := h.windowStart_lt_lane
+  have relative := Proof.Argon2.reference_relative_bound _ (random &&& 0xffffffff).toNat
+    (h.windowSize_positive random)
+  have count := h.windowSize_lt_lane random
+  change relativeValue p pass lane slice index random < windowSize p pass lane slice index random at relative
+  omega
+
+end VG.Proof.Argon2.X86_64.ReferenceMap

From 92344dbcd99275fbff18be5b4cbec2fb8c1e0b19 Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 15:42:15 +0000
Subject: [PATCH 3/4] Prove the complete Argon2 reference mapping and its fixed
 execution trace

---
 .../Impl/Argon2/X86_64/ReferenceMap.lean      |  11 +-
 .../Proof/Argon2/X86_64/ReferenceMap.lean     |  39 ++++++
 .../Proof/Argon2/X86_64/ReferenceMapCT.lean   |  30 +++++
 .../Argon2/X86_64/ReferenceMapFinish.lean     |  48 ++++++++
 .../Argon2/X86_64/ReferenceMapLaneCT.lean     | 115 ++++++++++++++++++
 .../Proof/Argon2/X86_64/ReferenceMapLit.lean  |  10 ++
 .../Argon2/X86_64/ReferenceMapRelative.lean   |  55 +++++++++
 .../Argon2/X86_64/ReferenceMapState.lean      |  13 ++
 .../Argon2/X86_64/ReferenceMapWindow.lean     |  52 ++++++++
 .../Argon2/X86_64/ReferenceMapWindowCT.lean   |  24 ++++
 10 files changed, 391 insertions(+), 6 deletions(-)
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMap.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapFinish.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLaneCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLit.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapRelative.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindow.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindowCT.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
index 3fbdae5f5..512a4e087 100644
--- a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean
@@ -35,11 +35,10 @@ def prepareLanes : Prog isa := .seq chooseLane (.block laneArgs)
 
 def window : Prog isa := .seq ReferenceStart.code ReferenceCount.code
 
-def code : Prog isa :=
-  .seq prepareLanes
-  (.seq window
-  (.seq (.block relativeArgs)
-  (.seq Relative.code
-  (.seq (.block wrapArgs) Wrap.code))))
+def relative : Prog isa := .seq (.block relativeArgs) Relative.code
+
+def finish : Prog isa := .seq (.block wrapArgs) Wrap.code
+
+def code : Prog isa := .seq prepareLanes (.seq window (.seq relative finish))
 
 end VG.Impl.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMap.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMap.lean
new file mode 100644
index 000000000..45f203cf3
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMap.lean
@@ -0,0 +1,39 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapFinish
+
+/-! Complete reference mapping against the reviewed RFC specification. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+theorem code_ok (s : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) :
+    WP isa code s (Result p pass lane slice index s) := by
+  unfold code
+  refine WP.seq ((prepareLanes_ok s p pass lane slice index ready).mono ?_)
+  intro a ha
+  refine WP.seq ((window_ok s a p pass lane slice index ready.bounds ha).mono ?_)
+  intro b hb
+  refine WP.seq ((relative_ok s b p pass lane slice index ready.bounds hb).mono ?_)
+  intro c hc
+  exact finish_ok s c p pass lane slice index ready.bounds hc
+
+theorem spec_lane (p : Spec.Argon2.Params) (pass lane slice index : Nat) (random : Addr) :
+    (Spec.Argon2.reference p pass lane slice index random).1 = chosenLane p pass lane slice random := rfl
+
+theorem spec_column (p : Spec.Argon2.Params) (pass lane slice index : Nat) (random : Addr) :
+    (Spec.Argon2.reference p pass lane slice index random).2 =
+      (windowStart p pass slice + relativeValue p pass lane slice index random) % p.laneLen := rfl
+
+theorem code_spec_ok (s : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) :
+    WP isa code s fun t =>
+      t.gpr .r9 = BitVec.ofNat 64 (Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)).1 ∧
+      t.gpr .rdi = BitVec.ofNat 64 (Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)).2 ∧
+      t.gpr .r11 = s.gpr .rdi ∧ Divide.Keeps changed s t := by
+  refine (code_ok s p pass lane slice index ready).mono ?_
+  intro t h
+  rw [spec_lane, spec_column]
+  exact ⟨h.selected, h.column, h.original, h.keeps⟩
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapCT.lean
new file mode 100644
index 000000000..dd93d0306
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapCT.lean
@@ -0,0 +1,30 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapLaneCT
+import VerifiedGarbage.Proof.Argon2.X86_64.Relative
+import VerifiedGarbage.Proof.Argon2.X86_64.Wrap
+
+/-! Complete reference mapping has no secret-dependent execution trace. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+theorem relativeArgs_secret_rel :
+    RelCT isa (fun _ _ => True) (.block relativeArgs) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide)
+
+theorem wrapArgs_secret_rel :
+    RelCT isa (fun _ _ => True) (.block wrapArgs) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide)
+
+theorem tail_secret_rel :
+    RelCT isa (fun _ _ => True) (.seq relative finish) (fun _ _ => True) :=
+  (relativeArgs_secret_rel.seq Relative.code_secret_rel).seq
+    (wrapArgs_secret_rel.seq Wrap.code_secret_rel)
+
+theorem code_rel (p : Spec.Argon2.Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) code (fun _ _ => True) :=
+  (prepareLanes_rel p pass lane slice index).seq (window_rel.seq tail_secret_rel)
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapFinish.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapFinish.lean
new file mode 100644
index 000000000..3ef35cc99
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapFinish.lean
@@ -0,0 +1,48 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapRelative
+import VerifiedGarbage.Proof.Argon2.X86_64.Wrap
+
+/-! Wrap the selected relative position into the lane's columns. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+structure Result (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  selected : t.gpr .r9 = BitVec.ofNat 64 (chosenLane p pass lane slice (s.gpr .rdi))
+  column : t.gpr .rdi = BitVec.ofNat 64
+    ((windowStart p pass slice + relativeValue p pass lane slice index (s.gpr .rdi)) % p.laneLen)
+  original : t.gpr .r11 = s.gpr .rdi
+  position : Position p lane slice index t
+  keeps : Divide.Keeps changed s t
+
+theorem finish_ok (s a : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (bounds : Bounds p pass lane slice index) (mapped : Mapped p pass lane slice index s a) :
+    WP isa finish a (Result p pass lane slice index s) := by
+  unfold finish
+  refine WP.seq ((wrapArgs_ok a).mono ?_)
+  rintro b ⟨sum, length, kb⟩
+  have sumWord : b.gpr .rdi = BitVec.ofNat 64
+      (windowStart p pass slice + relativeValue p pass lane slice index (s.gpr .rdi)) := by
+    rw [sum, mapped.relative, mapped.start, ← BitVec.ofNat_add, Nat.add_comm]
+  have sumBound : windowStart p pass slice + relativeValue p pass lane slice index (s.gpr .rdi)
+      < 2 ^ 64 := by
+    have small := bounds.sum_bound (s.gpr .rdi)
+    have q := bounds.laneLength_bound
+    omega
+  have sumNat : (b.gpr .rdi).toNat =
+      windowStart p pass slice + relativeValue p pass lane slice index (s.gpr .rdi) := by
+    rw [sumWord, word_nat _ sumBound]
+  have lengthNat : (b.gpr .rsi).toNat = p.laneLen := by
+    rw [length, mapped.position.laneLength,
+      word_nat _ (Nat.lt_trans bounds.laneLength_bound (by decide))]
+  refine (Wrap.code_nat_ok b (by rw [sumNat, lengthNat]; exact bounds.sum_bound _)).mono ?_
+  rintro t ⟨out, kt⟩
+  have kb' : Divide.Keeps changed a b := kb.mono (by decide)
+  have kt' : Divide.Keeps changed b t := kt.mono (by decide)
+  refine ⟨?_, ?_, ?_, mapped.position.of_keeps (kb'.trans kt'),
+    mapped.keeps.trans (kb'.trans kt')⟩
+  · exact (kt.regs .r9 (by decide)).trans ((kb.regs .r9 (by decide)).trans mapped.selected)
+  · rw [out, sumNat, lengthNat]
+  · exact (kt.regs .r11 (by decide)).trans ((kb.regs .r11 (by decide)).trans mapped.original)
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLaneCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLaneCT.lean
new file mode 100644
index 000000000..a22007d7c
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLaneCT.lean
@@ -0,0 +1,115 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapLane
+import VerifiedGarbage.Proof.Argon2.X86_64.FirstLaneCT
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapWindowCT
+
+/-! Recover the public pass from the frame without exposing the secret word. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+def Related (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop :=
+  Ready p pass lane slice index s ∧ Ready p pass lane slice index t ∧ s.gpr .rbp = t.gpr .rbp
+
+theorem division_keeps (s : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) :
+    WP isa VG.Impl.Argon2.X86_64.ReferenceLane.code s fun t =>
+      Ready p pass lane slice index t ∧ Divide.Keeps changed s t := by
+  refine (ReferenceLane.code_ok s
+    (by rw [ready.lanes_nat]; exact ready.bounds.lanesPositive)
+    (by rw [ready.lanes_nat]; exact ready.bounds.lanesBound)).mono ?_
+  rintro t ⟨_, _, keeps⟩
+  have k : Divide.Keeps changed s t := keeps.mono (by decide)
+  exact ⟨ready.of_keeps k (keeps.regs .rsi (by decide)), k⟩
+
+theorem division_rel (p : Spec.Argon2.Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index)
+      VG.Impl.Argon2.X86_64.ReferenceLane.code (Related p pass lane slice index) := by
+  have full := (ReferenceLane.code_secret_rel.mono
+    (P' := Related p pass lane slice index) (fun _ _ _ => trivial)
+    (fun _ _ h => h)).wpDep (fun s t hp =>
+      ⟨division_keeps s p pass lane slice index hp.1,
+        division_keeps t p pass lane slice index hp.2.1⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact ⟨ha.1, hb.1, (ha.2.regs .rbp (by decide)).trans
+    (hp.2.2.trans (hb.2.regs .rbp (by decide)).symm)⟩
+
+theorem loadPass_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block loadPass) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp])
+    (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)
+
+def Loaded (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop :=
+  Related p pass lane slice index s t ∧
+    s.gpr .r9 = BitVec.ofNat 64 pass ∧ t.gpr .r9 = BitVec.ofNat 64 pass
+
+theorem loadPass_public (s : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (ready : Ready p pass lane slice index s) : WP isa (.block loadPass) s fun t =>
+      Ready p pass lane slice index t ∧ t.gpr .r9 = BitVec.ofNat 64 pass ∧
+        Divide.Keeps changed s t := by
+  refine (loadPass_ok s ready.passRead).mono ?_
+  rintro t ⟨loaded, keeps⟩
+  have k : Divide.Keeps changed s t := keeps.mono (by decide)
+  exact ⟨ready.of_keeps k (keeps.regs .rsi (by decide)), loaded.trans ready.passWord, k⟩
+
+theorem loadPass_public_rel (p : Spec.Argon2.Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) (.block loadPass)
+      (Loaded p pass lane slice index) := by
+  have full := (loadPass_rel.mono (P' := Related p pass lane slice index)
+    (fun _ _ h => h.2.2) (fun _ _ h => h)).wpDep (fun s t hp =>
+      ⟨loadPass_public s p pass lane slice index hp.1,
+        loadPass_public t p pass lane slice index hp.2.1⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact ⟨⟨ha.1, hb.1, (ha.2.2.regs .rbp (by decide)).trans
+    (hp.2.2.trans (hb.2.2.regs .rbp (by decide)).symm)⟩, ha.2.1, hb.2.1⟩
+
+theorem firstLane_loaded_rel (p : Spec.Argon2.Params) (pass lane slice index : Nat) :
+    RelCT isa (Loaded p pass lane slice index) VG.Impl.Argon2.X86_64.FirstLane.code
+      (Loaded p pass lane slice index) := by
+  have trace := FirstLane.code_rel.mono (P' := Loaded p pass lane slice index)
+    (fun _ _ hp => ⟨hp.2.1.trans hp.2.2.symm,
+      hp.1.1.position.slice.trans hp.1.2.1.position.slice.symm⟩) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t _ => ⟨FirstLane.code_ok s, FirstLane.code_ok t⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  have ka : Divide.Keeps changed s a := ha.2.mono (by decide)
+  have kb : Divide.Keeps changed t b := hb.2.mono (by decide)
+  refine ⟨⟨hp.1.1.of_keeps ka (ha.2.regs .rsi (by decide)),
+    hp.1.2.1.of_keeps kb (hb.2.regs .rsi (by decide)),
+    (ka.regs .rbp (by decide)).trans (hp.1.2.2.trans (kb.regs .rbp (by decide)).symm)⟩, ?_, ?_⟩
+  · exact (ha.2.regs .r9 (by decide)).trans hp.2.1
+  · exact (hb.2.regs .r9 (by decide)).trans hp.2.2
+
+theorem laneArgs_secret_rel : RelCT isa (fun _ _ => True) (.block laneArgs) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide)
+
+theorem prepareLanes_rel (p : Spec.Argon2.Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) prepareLanes PublicPosition := by
+  have head := (division_rel p pass lane slice index).seq
+    ((loadPass_public_rel p pass lane slice index).seq (firstLane_loaded_rel p pass lane slice index))
+  have trace := head.seq (laneArgs_secret_rel.mono (fun _ _ _ => trivial) (fun _ _ h => h))
+  have full := trace.wpDep (fun s t hp =>
+    ⟨prepareLanes_ok s p pass lane slice index hp.1,
+      prepareLanes_ok t p pass lane slice index hp.2.1⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, _, _, _, ha, hb⟩ := h
+  intro r hr
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl
+  · apply BitVec.eq_of_toNat_eq
+    exact ha.pass.trans hb.pass.symm
+  · exact ha.position.slice.trans hb.position.slice.symm
+  · exact ha.position.segmentLength.trans hb.position.segmentLength.symm
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLit.lean
new file mode 100644
index 000000000..d146119a0
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceMap
+
+/-! A checked literal for complete reference-index mapping. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.ReferenceMap.code
+
+end VG
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapRelative.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapRelative.lean
new file mode 100644
index 000000000..6052f06fe
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapRelative.lean
@@ -0,0 +1,55 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapWindow
+import VerifiedGarbage.Proof.Argon2.X86_64.Relative
+import VerifiedGarbage.Proof.Framework.X86_64.Abi
+
+/-! Apply the squared J₁ mapping while retaining the lane and window start. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+theorem relativeWord_ok (s : State) (positive : 0 < (s.gpr .rsi).toNat)
+    (bound : (s.gpr .rsi).toNat < 2 ^ 32) :
+    WP isa VG.Impl.Argon2.X86_64.Relative.code s fun t =>
+      t.gpr .rax = BitVec.ofNat 64
+        ((s.gpr .rsi).toNat - 1 - (s.gpr .rsi).toNat *
+          ((s.gpr .rdi &&& 0xffffffff).toNat * (s.gpr .rdi &&& 0xffffffff).toNat / 2 ^ 32) /
+          2 ^ 32) ∧ Divide.Keeps [.rax, .rdx, .rcx] s t := by
+  refine WP.mono_mx (by decide +kernel) (Relative.code_nat_ok s positive bound) ?_
+  rintro t ⟨out, other, mem, rd, wr⟩ mx
+  refine ⟨out, ⟨?_, mem, rd, wr, mx⟩⟩
+  intro r hr
+  simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+  exact other r hr.1 hr.2.1 hr.2.2
+
+structure Mapped (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  selected : t.gpr .r9 = BitVec.ofNat 64 (chosenLane p pass lane slice (s.gpr .rdi))
+  relative : t.gpr .rax = BitVec.ofNat 64 (relativeValue p pass lane slice index (s.gpr .rdi))
+  start : t.gpr .r10 = BitVec.ofNat 64 (windowStart p pass slice)
+  original : t.gpr .r11 = s.gpr .rdi
+  position : Position p lane slice index t
+  keeps : Divide.Keeps changed s t
+
+theorem relative_ok (s a : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (bounds : Bounds p pass lane slice index) (counted : Counted p pass lane slice index s a) :
+    WP isa relative a (Mapped p pass lane slice index s) := by
+  unfold relative
+  refine WP.seq ((relativeArgs_ok a).mono ?_)
+  rintro b ⟨selected, random, count, kb⟩
+  have countNat : (b.gpr .rsi).toNat = windowSize p pass lane slice index (s.gpr .rdi) := by
+    rw [count, counted.count, word_nat _ (Nat.lt_trans (bounds.windowSize_bound32 _) (by decide))]
+  have randomWord : b.gpr .rdi = s.gpr .rdi := random.trans counted.original
+  refine (relativeWord_ok b
+    (by rw [countNat]; exact bounds.windowSize_positive _)
+    (by rw [countNat]; exact bounds.windowSize_bound32 _)).mono ?_
+  rintro t ⟨out, kt⟩
+  have kb' : Divide.Keeps changed a b := kb.mono (by decide)
+  have kt' : Divide.Keeps changed b t := kt.mono (by decide)
+  refine ⟨?_, ?_, ?_, ?_, counted.position.of_keeps (kb'.trans kt'),
+    counted.keeps.trans (kb'.trans kt')⟩
+  · exact (kt.regs .r9 (by decide)).trans (selected.trans counted.selected)
+  · simpa only [relativeValue, countNat, randomWord] using out
+  · exact (kt.regs .r10 (by decide)).trans ((kb.regs .r10 (by decide)).trans counted.start)
+  · exact (kt.regs .r11 (by decide)).trans ((kb.regs .r11 (by decide)).trans counted.original)
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean
index 3885fc12e..593f7b09c 100644
--- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapState.lean
@@ -44,6 +44,19 @@ structure Ready (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s : Stat
   passRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp) 8
   passWord : s.mem.readW (s.gpr .rbp) 64 = BitVec.ofNat 64 pass
 
+theorem Ready.lanes_nat {p : Spec.Argon2.Params} {pass lane slice index : Nat} {s : State}
+    (h : Ready p pass lane slice index s) : (s.gpr .rsi).toNat = p.lanes := by
+  rw [h.lanes, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (Nat.lt_trans h.bounds.lanesBound (by decide))]
+
+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 changed s t)
+    (lanes : t.gpr .rsi = s.gpr .rsi) : Ready p pass lane slice index t := by
+  refine ⟨h.bounds, h.position.of_keeps k, lanes.trans h.lanes, ?_, ?_⟩
+  · rw [k.rd, k.wr, k.regs .rbp (by decide)]
+    exact h.passRead
+  · rw [k.mem, k.regs .rbp (by decide)]
+    exact h.passWord
+
 def chosenLane (p : Spec.Argon2.Params) (pass lane slice : Nat) (random : Addr) : Nat :=
   if pass = 0 ∧ slice = 0 then lane else (random >>> 32).toNat % p.lanes
 
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindow.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindow.lean
new file mode 100644
index 000000000..705491c15
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindow.lean
@@ -0,0 +1,52 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapLane
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceStart
+
+/-! The selected eligible window and its chronological starting column. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+structure Counted (p : Spec.Argon2.Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  selected : t.gpr .rdi = BitVec.ofNat 64 (chosenLane p pass lane slice (s.gpr .rdi))
+  current : t.gpr .rsi = BitVec.ofNat 64 lane
+  count : t.gpr .r8 = BitVec.ofNat 64 (windowSize p pass lane slice index (s.gpr .rdi))
+  start : t.gpr .r10 = BitVec.ofNat 64 (windowStart p pass slice)
+  original : t.gpr .r11 = s.gpr .rdi
+  position : Position p lane slice index t
+  keeps : Divide.Keeps changed s t
+
+theorem window_ok (s a : State) (p : Spec.Argon2.Params) (pass lane slice index : Nat)
+    (bounds : Bounds p pass lane slice index) (prepared : Prepared p pass lane slice index s a) :
+    WP isa window a (Counted p pass lane slice index s) := by
+  have segmentPositive : 0 < p.segmentLen :=
+    Nat.lt_of_lt_of_le (by decide : 0 < 2)
+      (Proof.Argon2.segmentLen_ge_two p bounds.lanesPositive bounds.memoryMinimum)
+  unfold window
+  refine WP.seq ((ReferenceStart.code_nat_ok a p pass slice bounds.lanesPositive
+    segmentPositive bounds.sliceBound prepared.pass prepared.position.slice
+    prepared.position.segmentLength).mono ?_)
+  rintro b ⟨startWord, kb⟩
+  have kb' : Divide.Keeps changed a b := kb.mono (by decide)
+  have pb := prepared.position.of_keeps kb'
+  have passB : (b.gpr .r9).toNat = pass := by
+    rw [kb.regs .r9 (by decide), prepared.pass]
+  have same : decide (b.gpr .rdi = b.gpr .rsi) =
+      (chosenLane p pass lane slice (s.gpr .rdi) == lane) := by
+    apply Bool.eq_iff_iff.mpr
+    simp only [decide_eq_true_eq, beq_iff_eq]
+    rw [kb.regs .rdi (by decide), kb.regs .rsi (by decide), prepared.selected, prepared.current]
+    exact word_eq _ _ (bounds.chosenLane_bound64 _) bounds.lane_bound64
+  refine (ReferenceCount.code_nat_ok b p pass slice index passB pb.laneLength
+    pb.segmentLength pb.slice pb.index bounds.segment_le_lane bounds.index_bound64
+    bounds.window_positive.1 bounds.window_positive.2).mono ?_
+  rintro t ⟨countWord, kt⟩
+  have kt' : Divide.Keeps changed b t := kt.mono (by decide)
+  refine ⟨?_, ?_, ?_, ?_, ?_, pb.of_keeps kt', prepared.keeps.trans (kb'.trans kt')⟩
+  · exact (kt.regs .rdi (by decide)).trans ((kb.regs .rdi (by decide)).trans prepared.selected)
+  · exact (kt.regs .rsi (by decide)).trans ((kb.regs .rsi (by decide)).trans prepared.current)
+  · simpa only [windowSize, same] using countWord
+  · exact (kt.regs .r10 (by decide)).trans startWord
+  · exact (kt.regs .r11 (by decide)).trans ((kb.regs .r11 (by decide)).trans prepared.original)
+
+end VG.Proof.Argon2.X86_64.ReferenceMap
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindowCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindowCT.lean
new file mode 100644
index 000000000..84f7f741e
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceMapWindowCT.lean
@@ -0,0 +1,24 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapState
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceStart
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceStartCT
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceCount
+
+/-! The chronological window branches only on the public pass and slice. -/
+
+namespace VG.Proof.Argon2.X86_64.ReferenceMap
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceMap
+
+def PublicPosition (s t : State) : Prop :=
+  ∀ r ∈ [Reg.r9, .r14, .r13], s.gpr r = t.gpr r
+
+theorem window_rel : RelCT isa PublicPosition window (fun _ _ => True) := by
+  have start := ReferenceStart.code_rel.wpDep (fun s t _ =>
+    ⟨ReferenceStart.code_ok s, ReferenceStart.code_ok t⟩)
+  refine start.seq (ReferenceCount.code_rel.mono ?_ (fun _ _ h => h))
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact (ha.2.regs .r9 (by decide)).trans
+    ((hp .r9 (by simp)).trans (hb.2.regs .r9 (by decide)).symm)
+
+end VG.Proof.Argon2.X86_64.ReferenceMap

From a2202ce4b50d895b3a45bade43f484549283d661 Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 16:31:53 +0000
Subject: [PATCH 4/4] Prove Argon2 filling columns and lane-major block
 addresses

---
 .../Impl/Argon2/X86_64/BlockAddress.lean      |  20 +++
 .../Impl/Argon2/X86_64/FillColumn.lean        |  26 +++
 .../Proof/Argon2/FillPositions.lean           |  55 ++++++
 .../Proof/Argon2/X86_64/BlockAddress.lean     |  81 +++++++++
 .../Proof/Argon2/X86_64/BlockAddressLit.lean  |  10 ++
 .../Proof/Argon2/X86_64/FillColumn.lean       | 160 ++++++++++++++++++
 .../Proof/Argon2/X86_64/FillColumnCT.lean     |  16 ++
 .../Proof/Argon2/X86_64/FillColumnLit.lean    |  10 ++
 8 files changed, 378 insertions(+)
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/BlockAddress.lean
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/FillColumn.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/FillPositions.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddress.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddressLit.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnLit.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/BlockAddress.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/BlockAddress.lean
new file mode 100644
index 000000000..a259440e0
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/BlockAddress.lean
@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Lane-major matrix addressing. The matrix base is in `r8`, the lane
+in `rax`, the column in `rcx`, and the lane length in `r12`. The resulting
+block pointer is returned in `rax`. Scalar multiplication and ten doublings
+work on the baseline ISA, including when the reference coordinates are secret.
+-/
+
+namespace VG.Impl.Argon2.X86_64.BlockAddress
+
+open VG.X86_64
+
+def flatten : List Instr := [.mul .r12, .alu .add .rax (.reg .rcx)]
+
+def scale : List Instr := List.replicate 10 (.alu .add .rax (.reg .rax))
+
+def code : Prog isa :=
+  .seq (.block flatten) (.seq (.block scale) (.block [.alu .add .rax (.reg .r8)]))
+
+end VG.Impl.Argon2.X86_64.BlockAddress
diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillColumn.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillColumn.lean
new file mode 100644
index 000000000..0eb460e65
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillColumn.lean
@@ -0,0 +1,26 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Current and preceding columns in the filling loop. The public slice,
+segment length and offset are in `r14`, `r13` and `r15`, and the lane length
+is in `r12`. `rcx` receives the current column; `rdi` receives its cyclic
+predecessor. Only the public column-zero test controls a branch.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillColumn
+
+open VG.X86_64
+
+def current : List Instr := [
+  .mov .rax (.reg .r14), .mul .r13, .mov .rcx (.reg .rax),
+  .alu .add .rcx (.reg .r15)]
+
+def select : Prog isa := .ite .e
+  (.block [.mov .rdi (.reg .r12)]) (.block [.mov .rdi (.reg .rcx)])
+
+def previous : Prog isa :=
+  .seq (.block [.alu .cmp .rcx (.imm 0)])
+    (.seq select (.block [.alu .sub .rdi (.imm 1)]))
+
+def code : Prog isa := .seq (.block current) previous
+
+end VG.Impl.Argon2.X86_64.FillColumn
diff --git a/lean/VerifiedGarbage/Proof/Argon2/FillPositions.lean b/lean/VerifiedGarbage/Proof/Argon2/FillPositions.lean
new file mode 100644
index 000000000..850534bf1
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/FillPositions.lean
@@ -0,0 +1,55 @@
+import VerifiedGarbage.Proof.Argon2.Dimensions
+import VerifiedGarbage.Proof.Framework.Offset
+
+/-! Bounds for every block address used by the filling loop. -/
+
+namespace VG.Proof.Argon2
+
+open VG.Spec.Argon2
+
+theorem previous_column_lt (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (column : Nat) :
+    (column + p.laneLen - 1) % p.laneLen < p.laneLen := by
+  have seg := segmentLen_ge_two p hl hm
+  have lanes := laneLen_segments p hl
+  exact Nat.mod_lt _ (by omega)
+
+theorem cell_bytes (p : Params) (hl : 0 < p.lanes) {lane column : Nat}
+    (hlane : lane < p.lanes) (hcolumn : column < p.laneLen) :
+    (lane * p.laneLen + column) * 1024 + 1024 ≤ p.blocks * 1024 := by
+  have cell := cell_lt p hl hlane hcolumn
+  have scaled := Nat.mul_le_mul_right 1024 (show lane * p.laneLen + column + 1 ≤ p.blocks by omega)
+  simpa only [Nat.add_mul, Nat.one_mul] using scaled
+
+theorem current_cell_lt (p : Params) (hl : 0 < p.lanes) {lane slice index : Nat}
+    (hlane : lane < p.lanes) (hslice : slice < 4) (hindex : index < p.segmentLen) :
+    lane * p.laneLen + (slice * p.segmentLen + index) < p.blocks :=
+  cell_lt p hl hlane (column_lt p hl hslice hindex)
+
+theorem previous_cell_lt (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) {lane column : Nat} (hlane : lane < p.lanes) :
+    lane * p.laneLen + ((column + p.laneLen - 1) % p.laneLen) < p.blocks :=
+  cell_lt p hl hlane (previous_column_lt p hl hm column)
+
+theorem reference_cell_lt (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (pass lane slice index : Nat) (random : Word)
+    (hlane : lane < p.lanes) :
+    let ref := reference p pass lane slice index random
+    ref.1 * p.laneLen + ref.2 < p.blocks := by
+  obtain ⟨laneBound, columnBound⟩ := reference_bounds p hl hm pass lane slice index random hlane
+  exact cell_lt p hl laneBound columnBound
+
+theorem cell_contains (base : VG.Addr) (p : Params) (hl : 0 < p.lanes)
+    (hm : p.memory < 2 ^ 32) {lane column : Nat}
+    (hlane : lane < p.lanes) (hcolumn : column < p.laneLen) :
+    (⟨base, p.blocks * 1024⟩ : VG.Region).Contains
+      (base + BitVec.ofNat 64 ((lane * p.laneLen + column) * 1024)) 1024 := by
+  have bytes := cell_bytes p hl hlane hcolumn
+  have blocks : p.blocks < 2 ^ 32 := Nat.lt_of_le_of_lt (blocks_le_memory p) hm
+  have total : p.blocks * 1024 < 2 ^ 64 :=
+    Nat.lt_trans (Nat.mul_lt_mul_of_pos_right blocks (by decide : 0 < 1024)) (by decide +kernel)
+  exact VG.Offset.contains_base base
+    (d := (lane * p.laneLen + column) * 1024) (n := 1024) (k := p.blocks * 1024)
+    bytes (Nat.lt_of_le_of_lt (Nat.le_trans (Nat.le_add_right _ _) bytes) total)
+
+end VG.Proof.Argon2
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddress.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddress.lean
new file mode 100644
index 000000000..66b63e638
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddress.lean
@@ -0,0 +1,81 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.BlockAddress
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitScale
+import VerifiedGarbage.Proof.Framework.X86_64.Abi
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Fault-free matrix pointer calculation, with no memory accesses. -/
+
+namespace VG.Proof.Argon2.X86_64.BlockAddress
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.BlockAddress
+
+theorem flatten_ok (s : State) : WP isa (.block flatten) s fun t =>
+    t.gpr .rax = s.gpr .rax * s.gpr .r12 + s.gpr .rcx ∧
+    Divide.Keeps [.rax, .rdx] s t := by
+  apply WP.of_runBlock
+  simp only [flatten, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    execMul, execAlu, RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags,
+    reduceCtorEq, ite_true, ite_false, Option.bind_some, Option.some.injEq,
+    exists_eq_left', BitVec.ofNat_mul, BitVec.ofNat_toNat, BitVec.setWidth_eq]
+  refine ⟨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, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags,
+      hr.1, hr.2, ite_false]
+  all_goals rfl
+
+theorem scale_ok (s : State) : WP isa (.block scale) s fun t =>
+    t.gpr .rax = s.gpr .rax * 1024 ∧ Divide.Keeps [.rax] s t := by
+  refine WP.mono_mx (by decide +kernel) (MemoryInit.scale_ok s .rax 10) ?_
+  intro t h mx
+  refine ⟨h.value, ?_, h.mem, h.rd, h.wr, mx⟩
+  intro r hr
+  exact h.other r (by simpa only [List.mem_cons, List.not_mem_nil, or_false] using hr)
+
+theorem base_ok (s : State) : WP isa (.block [.alu .add .rax (.reg .r8)]) s fun t =>
+    t.gpr .rax = s.gpr .rax + s.gpr .r8 ∧ Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, Option.bind_some,
+    Option.some.injEq, exists_eq_left']
+  refine ⟨by simp only [ite_true], ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    exact ite_eq_right hr
+  all_goals rfl
+
+theorem code_ok (s : State) : WP isa code s fun t =>
+    t.gpr .rax = (s.gpr .rax * s.gpr .r12 + s.gpr .rcx) * 1024 + s.gpr .r8 ∧
+    Divide.Keeps [.rax, .rdx] s t := by
+  unfold code
+  refine WP.seq ((flatten_ok s).mono ?_)
+  rintro a ⟨flat, ka⟩
+  refine WP.seq ((scale_ok a).mono ?_)
+  rintro b ⟨scaled, kb⟩
+  refine (base_ok b).mono ?_
+  rintro t ⟨result, kt⟩
+  refine ⟨?_, ka.trans ((kb.mono (by simp)).trans (kt.mono (by simp)))⟩
+  rw [result, scaled, flat, kb.regs .r8 (by decide), ka.regs .r8 (by decide)]
+
+theorem code_nat_ok (s : State) (lane column q : Nat)
+    (hl : s.gpr .rax = BitVec.ofNat 64 lane)
+    (hc : s.gpr .rcx = BitVec.ofNat 64 column)
+    (hq : s.gpr .r12 = BitVec.ofNat 64 q) :
+    WP isa code s fun t =>
+      t.gpr .rax = s.gpr .r8 + BitVec.ofNat 64 ((lane * q + column) * 1024) ∧
+      Divide.Keeps [.rax, .rdx] s t := by
+  refine (code_ok s).mono ?_
+  rintro t ⟨h, k⟩
+  refine ⟨?_, k⟩
+  rw [h, hl, hc, hq, ← BitVec.ofNat_mul, ← BitVec.ofNat_add]
+  change BitVec.ofNat 64 (lane * q + column) * BitVec.ofNat 64 1024 + s.gpr .r8 = _
+  rw [← BitVec.ofNat_mul, BitVec.add_comm]
+
+theorem code_secret_rel : RelCT isa (fun _ _ => True) code (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.BlockAddress
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddressLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddressLit.lean
new file mode 100644
index 000000000..af28ce7cd
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddressLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.BlockAddress
+
+/-! A checked literal for lane-major matrix block addressing. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.BlockAddress.code
+
+end VG
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean
new file mode 100644
index 000000000..e1e0f5a5b
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean
@@ -0,0 +1,160 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillColumn
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+import VerifiedGarbage.Proof.Argon2.Dimensions
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Current-column arithmetic and the cyclic predecessor, preserving the
+matrix, enclosing loop registers and MXCSR. -/
+
+namespace VG.Proof.Argon2.X86_64.FillColumn
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillColumn
+
+theorem current_ok (s : State) : WP isa (.block current) s fun t =>
+    t.gpr .rcx = s.gpr .r14 * s.gpr .r13 + s.gpr .r15 ∧
+    Divide.Keeps [.rax, .rdx, .rcx] s t := by
+  apply WP.of_runBlock
+  simp only [current, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    execMul, execAlu, RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags,
+    reduceCtorEq, ite_true, ite_false, Option.map_some, Option.bind_some,
+    Option.some.injEq, exists_eq_left', BitVec.ofNat_mul, BitVec.ofNat_toNat, BitVec.setWidth_eq]
+  refine ⟨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, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags,
+      hr.1, hr.2.1, hr.2.2, ite_false]
+  all_goals rfl
+
+theorem compare_ok (s : State) : WP isa (.block [.alu .cmp .rcx (.imm 0)]) s
+    fun t => t.zf = decide (s.gpr .rcx = 0) ∧ Divide.Keeps [] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.zf_arithFlags, Option.bind_some, Option.some.injEq, exists_eq_left',
+    show BitVec.signExtend 64 (0 : BitVec 32) = (0 : Addr) from rfl]
+  refine ⟨?_, ?_⟩
+  · change (s.gpr .rcx - 0#64 == 0#64) = decide (s.gpr .rcx = 0#64)
+    rw [BitVec.sub_zero]
+    exact Bool.eq_iff_iff.mpr (by simp only [beq_iff_eq, decide_eq_true_eq])
+  constructor
+  · intro r _; exact congrFun (RegUpd.gpr_arithFlags _ _ _ _) r
+  all_goals rfl
+
+theorem move_ok (s : State) (r : Reg) : WP isa (.block [.mov .rdi (.reg r)]) s
+    fun t => t.gpr .rdi = s.gpr r ∧ Divide.Keeps [.rdi] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg, ite_true]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro q hq
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hq
+    exact ite_eq_right hq
+  all_goals rfl
+
+theorem decrement_ok (s : State) : WP isa (.block [.alu .sub .rdi (.imm 1)]) s
+    fun t => t.gpr .rdi = s.gpr .rdi - 1 ∧ Divide.Keeps [.rdi] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, Option.bind_some,
+    Option.some.injEq, exists_eq_left', ite_true,
+    show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    exact ite_eq_right hr
+  all_goals rfl
+
+theorem previous_ok (s : State) : WP isa previous s fun t =>
+    t.gpr .rdi = (if s.gpr .rcx = 0 then s.gpr .r12 else s.gpr .rcx) - 1 ∧
+    Divide.Keeps [.rdi] s t := by
+  unfold previous
+  refine WP.seq ((compare_ok s).mono ?_)
+  rintro a ⟨flag, ka⟩
+  have selected : WP isa select a fun b =>
+      b.gpr .rdi = (if s.gpr .rcx = 0 then s.gpr .r12 else s.gpr .rcx) ∧
+      Divide.Keeps [.rdi] s b := by
+    unfold select
+    refine WP.ite (decide (s.gpr .rcx = 0)) (by simp only [eval, flag]) ?_ ?_
+    · intro h
+      have zero := of_decide_eq_true h
+      refine (move_ok a .r12).mono ?_
+      rintro b ⟨value, kb⟩
+      exact ⟨by rw [value, ka.regs .r12 (by simp), ite_eq_left zero],
+        (ka.mono (by simp)).trans kb⟩
+    · intro h
+      have nonzero := of_decide_eq_false h
+      refine (move_ok a .rcx).mono ?_
+      rintro b ⟨value, kb⟩
+      exact ⟨by rw [value, ka.regs .rcx (by simp), ite_eq_right nonzero],
+        (ka.mono (by simp)).trans kb⟩
+  refine WP.seq (selected.mono ?_)
+  rintro b ⟨value, kb⟩
+  refine (decrement_ok b).mono ?_
+  rintro t ⟨result, kt⟩
+  exact ⟨by rw [result, value], kb.trans kt⟩
+
+theorem code_ok (s : State) : WP isa code s fun t =>
+    let column := s.gpr .r14 * s.gpr .r13 + s.gpr .r15
+    t.gpr .rcx = column ∧
+    t.gpr .rdi = (if column = 0 then s.gpr .r12 else column) - 1 ∧
+    Divide.Keeps [.rax, .rdx, .rcx, .rdi] s t := by
+  unfold code
+  refine WP.seq ((current_ok s).mono ?_)
+  rintro a ⟨column, ka⟩
+  refine (previous_ok a).mono ?_
+  rintro t ⟨previous, kt⟩
+  refine ⟨(kt.regs .rcx (by decide)).trans column, ?_,
+    (ka.mono (by simp)).trans (kt.mono (by simp))⟩
+  rw [previous, column, ka.regs .r12 (by decide)]
+
+theorem previous_nat (column q : Nat) (positive : 0 < q) (bound : column < q) :
+    (if column = 0 then q else column) - 1 = (column + q - 1) % q := by
+  by_cases zero : column = 0
+  · simp only [zero, ite_true, Nat.zero_add]
+    exact (Nat.mod_eq_of_lt (by omega : q - 1 < q)).symm
+  · simp only [zero, ite_false]
+    have sub : column + q - 1 - q = column - 1 := by omega
+    rw [Nat.mod_eq_sub_mod (by omega : q ≤ column + q - 1), sub,
+      Nat.mod_eq_of_lt (by omega : column - 1 < q)]
+
+theorem code_nat_ok (s : State) (slice segment index q : Nat)
+    (hs : s.gpr .r14 = BitVec.ofNat 64 slice)
+    (hg : s.gpr .r13 = BitVec.ofNat 64 segment)
+    (hi : s.gpr .r15 = BitVec.ofNat 64 index)
+    (hq : s.gpr .r12 = BitVec.ofNat 64 q)
+    (positive : 0 < q) (qBound : q < 2 ^ 64)
+    (bound : slice * segment + index < q) :
+    WP isa code s fun t =>
+      t.gpr .rcx = BitVec.ofNat 64 (slice * segment + index) ∧
+      t.gpr .rdi = BitVec.ofNat 64 ((slice * segment + index + q - 1) % q) ∧
+      Divide.Keeps [.rax, .rdx, .rcx, .rdi] s t := by
+  refine (code_ok s).mono ?_
+  rintro t ⟨column, previous, keeps⟩
+  have word : s.gpr .r14 * s.gpr .r13 + s.gpr .r15 =
+      BitVec.ofNat 64 (slice * segment + index) := by
+    rw [hs, hg, hi, ← BitVec.ofNat_mul, ← BitVec.ofNat_add]
+  refine ⟨column.trans word, ?_, keeps⟩
+  have zero : BitVec.ofNat 64 (slice * segment + index) = 0#64 ↔
+      slice * segment + index = 0 := by
+    constructor
+    · intro h
+      have hn := congrArg BitVec.toNat h
+      rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (Nat.lt_trans bound qBound)] at hn
+      exact hn
+    · intro h; rw [h]
+  rw [previous, word, hq]
+  change (if BitVec.ofNat 64 (slice * segment + index) = 0#64 then
+    BitVec.ofNat 64 q else BitVec.ofNat 64 (slice * segment + index)) - 1 = _
+  simp only [zero]
+  by_cases h : slice * segment + index = 0
+  · simp only [h, ite_true]
+    rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl,
+      Offset.ofNat_sub_ofNat positive, Nat.zero_add, Nat.mod_eq_of_lt (by omega : q - 1 < q)]
+  · simp only [h, ite_false]
+    rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl,
+      Offset.ofNat_sub_ofNat (by omega : 1 ≤ slice * segment + index),
+      ← previous_nat _ q positive bound, ite_eq_right h]
+
+end VG.Proof.Argon2.X86_64.FillColumn
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnCT.lean
new file mode 100644
index 000000000..b142465e6
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnCT.lean
@@ -0,0 +1,16 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillColumnLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Public loop coordinates determine both columns and their branch trace. -/
+
+namespace VG.Proof.Argon2.X86_64.FillColumn
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillColumn
+
+theorem code_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.r14, .r13, .r15, .r12], s.gpr r = t.gpr r) code
+    (fun s t => ∀ r ∈ [Reg.rcx, .rdi], s.gpr r = t.gpr r) :=
+  RelCT.taintRegs (τ := Taint.ofRegs [.r14, .r13, .r15, .r12])
+    (fun _ _ h => Taint.agree_ofRegs h) [Reg.rcx, .rdi] (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.FillColumn
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnLit.lean
new file mode 100644
index 000000000..6d12ca925
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumnLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FillColumn
+
+/-! A checked literal for current and cyclic predecessor column calculation. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FillColumn.code
+
+end VG