From 6e086a63b5b715c9a5afc151e8223941155ddf65 Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 18:02:03 +0000
Subject: [PATCH] Prove complete Argon2 independent-address generation on
 x86-64

---
 .../Impl/Argon2/X86_64/AddressCalls.lean      |  37 ++++
 .../Proof/Argon2/X86_64/AddressCalls.lean     |  64 +++++++
 .../Proof/Argon2/X86_64/AddressCallsArgs.lean |  49 ++++++
 .../Proof/Argon2/X86_64/AddressCallsCT.lean   |  94 +++++++++++
 .../Argon2/X86_64/AddressCallsClear.lean      |  64 +++++++
 .../Argon2/X86_64/AddressCallsLayout.lean     |  79 +++++++++
 .../Proof/Argon2/X86_64/AddressCallsMx.lean   |  32 ++++
 .../Argon2/X86_64/AddressCallsPrepare.lean    | 159 ++++++++++++++++++
 .../Argon2/X86_64/AddressCallsStage.lean      |  76 +++++++++
 .../Argon2/X86_64/AddressGeneration.lean      |  39 +++++
 .../Argon2/X86_64/AddressGenerationCT.lean    |  95 +++++++++++
 11 files changed, 788 insertions(+)
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCalls.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCalls.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsArgs.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsClear.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsLayout.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsMx.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsPrepare.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsStage.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGeneration.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGenerationCT.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCalls.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCalls.lean
new file mode 100644
index 000000000..df34e03ec
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCalls.lean
@@ -0,0 +1,37 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressHeader
+import VerifiedGarbage.Impl.Argon2.X86_64.ClearBlock
+import VerifiedGarbage.Spec.Argon2.Contract
+
+/-! Independent-address generation in the shared 16 KiB scratch allocation.
+G uses `[0,4096)`, temporary output `[4096,5120)`, input `[5120,6144)`,
+address output `[6144,7168)`, and the zero block `[7168,8192)`. Every stage
+reloads the scratch pointer from frame offset 248 after a compression call.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressCalls
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def pointer (offset : Nat) : List Instr := [
+  .mov .rdi (.mem (at_ .rbp 248)), .alu .add .rdi (.imm (BitVec.ofNat 32 offset))]
+
+def args (x y out : Nat) : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)),
+  .mov .rdi (.reg .rcx), .alu .add .rdi (.imm (BitVec.ofNat 32 x)),
+  .mov .rsi (.reg .rcx), .alu .add .rsi (.imm (BitVec.ofNat 32 y)),
+  .mov .rdx (.reg .rcx), .alu .add .rdx (.imm (BitVec.ofNat 32 out))]
+
+def stage (x y out : Nat) : Prog isa := .seq (.block (args x y out))
+  (.call Spec.Argon2.compressApi.name VG.Impl.Argon2.X86_64.compress)
+
+def calls : Prog isa := .seq (stage 7168 5120 4096) (stage 7168 4096 6144)
+
+def clearAt (offset : Nat) : Prog isa := .seq (.block (pointer offset)) ClearBlock.code
+
+def prepare : Prog isa := .seq (clearAt 5120) (.seq (clearAt 7168)
+  (.seq (.block (pointer 5120)) AddressHeader.code))
+
+def code : Prog isa := .seq prepare calls
+
+end VG.Impl.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCalls.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCalls.lean
new file mode 100644
index 000000000..9018d7867
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCalls.lean
@@ -0,0 +1,64 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsStage
+import VerifiedGarbage.Proof.Argon2.AddressInput
+
+/-! Both compression calls produce exactly the reviewed independent-address block. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+def writes (s : State) : List Region := [⟨work s, 8192⟩, below (s.gpr .rsp) 8]
+
+structure Generated (s t : State) (p : Params) (pass lane slice counter : Nat) : Prop where
+  block : blockAt t.mem (off (work s) 6144) = addressBlock p pass lane slice counter
+  ready : Ready t
+  work : work t = work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (writes s) s.mem t.mem
+
+theorem stage_frame_full {s t : State} {out : Nat} (bound : out + 1024 ≤ 8192)
+    (hf : Frame (stageWrites s out) s.mem t.mem) : Frame (writes s) s.mem t.mem := by
+  apply hf.sub
+  intro r hr
+  simp only [stageWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl
+  · exact ⟨⟨work s, 8192⟩, by simp [writes], Offset.sub_base _ bound⟩
+  · exact ⟨⟨work s, 8192⟩, by simp [writes], Region.sub_prefix (by decide)⟩
+  · exact ⟨_, by simp [writes], fun _ h => h⟩
+
+theorem zero_preserved {s t : State} (h : Ready s)
+    (hf : Frame (stageWrites s 4096) s.mem t.mem) :
+    blockAt t.mem (off (work s) 7168) = blockAt s.mem (off (work s) 7168) := by
+  apply FillCompress.block_frame hf
+  intro r hr
+  simp only [stageWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl
+  · exact Offset.disjoint _ (by decide) (by decide) (by decide)
+  · exact Offset.disjoint_base _ (by decide) (by decide)
+  · exact (h.stackWork.sub_right (Offset.sub_base _ (by decide))).symm
+
+theorem calls_ok (p : Params) (pass lane slice counter : Nat) (s : State) (h : Ready s)
+    (zero : blockAt s.mem (off (work s) 7168) = zeroBlock)
+    (input : blockAt s.mem (off (work s) 5120) = Proof.Argon2.addressInput p pass lane slice counter) :
+    WP isa calls s (Generated s · p pass lane slice counter) := by
+  unfold calls
+  refine WP.seq ((stage_ok s h 7168 5120 4096 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide)).mono ?_)
+  intro a first
+  refine (stage_ok a first.ready 7168 4096 6144 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide)).mono ?_
+  intro t second
+  refine ⟨?_, second.ready, second.work.trans first.work,
+    fun r hr => (second.regs r hr).trans (first.regs r hr),
+    second.rd.trans first.rd, second.wr.trans first.wr, ?_⟩
+  · have result := second.result
+    rw [first.work, zero_preserved h first.frame, zero, first.result, zero, input] at result
+    rw [Proof.Argon2.addressBlock_eq]
+    exact result
+  · have next := stage_frame_full (by decide) second.frame
+    simp only [writes, first.work, first.regs .rsp (by simp [calleeSaved])] at next
+    exact (stage_frame_full (by decide) first.frame).trans next
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsArgs.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsArgs.lean
new file mode 100644
index 000000000..1794c8b57
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsArgs.lean
@@ -0,0 +1,49 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCalls
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressHeaderWords
+
+/-! Independent-address compression arguments from one fixed frame read. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCalls
+
+def work (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 248) 64
+
+def displacement (n : Nat) : Addr := BitVec.signExtend 64 (BitVec.ofNat 32 n)
+
+theorem pointer_ok (s : State) (offset : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block (pointer offset)) s fun t =>
+      t.gpr .rdi = work s + displacement offset ∧ Divide.Keeps [.rdi] s t := by
+  apply WP.of_runBlock
+  simp only [pointer, work, displacement, runBlock_cons, runStep_some, runBlock_nil,
+    exec, readSrc, State.load64, ea_at, hr, execAlu, RegUpd.gpr_setReg,
+    RegUpd.gpr_arithFlags, ite_true, Option.map_some,
+    Option.bind_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, RegUpd.gpr_arithFlags, hr, ite_false]
+  all_goals rfl
+
+theorem args_ok (s : State) (x y out : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block (args x y out)) s fun t =>
+      t.gpr .rcx = work s ∧ t.gpr .rdi = work s + displacement x ∧
+      t.gpr .rsi = work s + displacement y ∧ t.gpr .rdx = work s + displacement out ∧
+      Divide.Keeps [.rcx, .rdi, .rsi, .rdx] s t := by
+  apply WP.of_runBlock
+  simp only [args, work, displacement, runBlock_cons, runStep_some, runBlock_nil,
+    exec, readSrc, State.load64, ea_at, hr, execAlu, RegUpd.gpr_setReg,
+    RegUpd.gpr_arithFlags, reduceCtorEq, ite_true, ite_false, Option.map_some,
+    Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, 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, RegUpd.gpr_arithFlags, hr.1, hr.2.1,
+      hr.2.2.1, hr.2.2.2, ite_false]
+  all_goals rfl
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsCT.lean
new file mode 100644
index 000000000..35a0234b3
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsCT.lean
@@ -0,0 +1,94 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCalls
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCallCT
+
+/-! The two address-generation compression calls have public fixed addresses. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCalls
+
+structure Related (s t : State) : Prop where
+  left : Ready s
+  right : Ready t
+  bases : s.gpr .rbp = t.gpr .rbp
+  stacks : s.gpr .rsp = t.gpr .rsp
+  work : work s = work t
+
+structure CallRelated (s t : State) : Prop where
+  left : FillCompress.CallReady s
+  right : FillCompress.CallReady t
+  args : ∀ r ∈ [Reg.rdi, .rsi, .rdx, .rcx, .rsp], s.gpr r = t.gpr r
+
+theorem first_args_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block (args 7168 5120 4096)) (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)
+
+theorem second_args_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block (args 7168 4096 6144)) (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)
+
+theorem args_public_rel (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192)
+    (argTrace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+      (.block (args x y out)) (fun _ _ => True)) :
+    RelCT isa Related (.block (args x y out)) CallRelated := by
+  have trace := argTrace.mono (P' := Related) (fun _ _ hp => hp.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t hp =>
+    ⟨args_nat_ok s hp.left x y out (by omega) (by omega) (by omega),
+      args_nat_ok t hp.right x y out (by omega) (by omega) (by omega)⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨args_call_ready s a hp.left x y out hx hy ho bx by_ bo ha,
+    args_call_ready t b hp.right x y out hx hy ho bx by_ bo hb, ?_⟩
+  intro r hr
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl | rfl
+  · exact ha.left.trans ((congrArg (fun p => off p x) hp.work).trans hb.left.symm)
+  · exact ha.right.trans ((congrArg (fun p => off p y) hp.work).trans hb.right.symm)
+  · exact ha.output.trans ((congrArg (fun p => off p out) hp.work).trans hb.output.symm)
+  · exact ha.scratch.trans (hp.work.trans hb.scratch.symm)
+  · exact (ha.keeps.regs .rsp (by decide)).trans
+      (hp.stacks.trans (hb.keeps.regs .rsp (by decide)).symm)
+
+theorem stage_rel (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192)
+    (argTrace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+      (.block (args x y out)) (fun _ _ => True)) :
+    RelCT isa Related (stage x y out) Related := by
+  have call := FillCompress.call_rel Spec.Argon2.compressApi.name (P := CallRelated)
+    (fun _ _ hp => ⟨hp.left, hp.right, hp.args .rdi (by simp), hp.args .rsi (by simp),
+      hp.args .rdx (by simp), hp.args .rcx (by simp), hp.args .rsp (by simp)⟩)
+  have trace := (args_public_rel x y out hx hy ho bx by_ bo argTrace).seq call
+  have full := trace.wpDep (fun s t hp =>
+    ⟨stage_ok s hp.left x y out hx hy ho bx by_ bo,
+      stage_ok t hp.right x y out hx hy ho bx by_ bo⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact ⟨ha.ready, hb.ready,
+    (ha.regs .rbp (by simp [calleeSaved])).trans
+      (hp.bases.trans (hb.regs .rbp (by simp [calleeSaved])).symm),
+    (ha.regs .rsp (by simp [calleeSaved])).trans
+      (hp.stacks.trans (hb.regs .rsp (by simp [calleeSaved])).symm),
+    ha.work.trans (hp.work.trans hb.work.symm)⟩
+
+theorem calls_rel : RelCT isa Related calls Related :=
+  (stage_rel 7168 5120 4096 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide) first_args_rel).seq
+  (stage_rel 7168 4096 6144 (by decide) (by decide) (by decide)
+    (by decide) (by decide) (by decide) second_args_rel)
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsClear.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsClear.lean
new file mode 100644
index 000000000..33149882b
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsClear.lean
@@ -0,0 +1,64 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsStage
+import VerifiedGarbage.Proof.Argon2.X86_64.ClearBlock
+
+/-! Clear an address-generation block, retaining the allocation invariants. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+structure Cleared (s t : State) (offset : Nat) : Prop where
+  block : blockAt t.mem (off (work s) offset) = zeroBlock
+  ready : Ready t
+  work_eq : work t = work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame [⟨off (work s) offset, 1024⟩] s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+
+theorem clearAt_ok (s : State) (h : Ready s) (offset : Nat) (bound : offset + 1024 ≤ 8192) :
+    WP isa (clearAt offset) s (Cleared s · offset) := by
+  unfold clearAt
+  refine WP.seq ((pointer_ok s offset h.frameRead).mono ?_)
+  rintro a ⟨dest, keeps⟩
+  rw [displacement_eq offset (by omega)] at dest
+  have write : Covers [⟨a.gpr .rdi, 1024⟩] a.wr := by
+    rw [dest, keeps.wr]; exact work_cover s h offset 1024 bound
+  refine (ClearBlock.code_ok a write).mono ?_
+  rintro t ⟨zero, frame, tk, mx⟩
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r := by
+    intro r hr
+    have ne : r ≠ .rax ∧ r ≠ .rdi := by
+      simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+    exact (tk.1 r ne.1).trans (keeps.regs r (by simpa only [List.mem_cons, List.not_mem_nil, or_false] using ne.2))
+  have rd := tk.2.1.trans keeps.rd
+  have wr := tk.2.2.trans keeps.wr
+  have hf : Frame [⟨off (work s) offset, 1024⟩] s.mem t.mem := by
+    rw [dest, keeps.mem] at frame; exact frame
+  have bigger : Frame (stageWrites s offset) s.mem t.mem :=
+    hf.mono (by
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      simp [stageWrites])
+  obtain ⟨ready, work'⟩ := ready_of_frame h offset bound regs rd wr bigger
+  rw [dest] at zero
+  exact ⟨zero, ready, work', regs, rd, wr, hf, mx.trans keeps.mxcsr⟩
+
+theorem Cleared.full_frame {s t : State} {offset : Nat} (h : Cleared s t offset)
+    (bound : offset + 1024 ≤ 8192) : Frame [⟨work s, 8192⟩] s.mem t.mem := by
+  apply h.frame.sub
+  intro r hr
+  simp only [List.mem_singleton] at hr
+  subst r
+  exact ⟨⟨work s, 8192⟩, by simp, Offset.sub_base _ bound⟩
+
+theorem frame_word {s t : State} (h : Ready s) (frame : Frame [⟨work s, 8192⟩] s.mem t.mem)
+    (d : Nat) (bound : d + 8 ≤ 272) :
+    t.mem.readW (off (s.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 :=
+  frame.readW (r := ⟨s.gpr .rbp, 272⟩) (Offset.contains_base _ bound (by omega))
+    (by intro r hr; simp only [List.mem_singleton] at hr; subst r; exact h.frameWork) (by decide)
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsLayout.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsLayout.lean
new file mode 100644
index 000000000..81cc0442b
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsLayout.lean
@@ -0,0 +1,79 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCall
+
+/-! Permissions and separation for either address-generation compression call. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64
+
+structure Ready (s : State) : Prop where
+  frameRead : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8
+  workWrite : Covers [⟨work s, 8192⟩] s.wr
+  frameWork : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨work s, 8192⟩
+  frameStack : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint (below (s.gpr .rsp) 8)
+  stackWork : (below (s.gpr .rsp) 8).Disjoint ⟨work s, 8192⟩
+
+theorem displacement_eq (n : Nat) (bound : n ≤ 8192) : displacement n = BitVec.ofNat 64 n := by
+  have n32 : n < 2 ^ 32 := by omega
+  have msb : (BitVec.ofNat 32 n).msb = false := by
+    rw [BitVec.msb_eq_false_iff_two_mul_lt, BitVec.toNat_ofNat, Nat.mod_eq_of_lt n32]
+    omega
+  unfold displacement
+  rw [BitVec.signExtend_eq_setWidth_of_msb_false msb,
+    BitVec.setWidth_ofNat_of_le_of_lt (by decide) n32]
+
+theorem work_cover (s : State) (h : Ready s) (d n : Nat) (hd : d + n ≤ 8192) :
+    Covers [⟨off (work s) d, n⟩] s.wr := by
+  have sub : Covers [⟨off (work s) d, n⟩] [⟨work s, 8192⟩] := by
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.mem_singleton] at hr
+    subst r
+    exact ⟨⟨work s, 8192⟩, by simp, d, rfl, hd⟩
+  exact fun p n hp => h.workWrite p n (sub p n hp)
+
+structure Args (s a : State) (x y out : Nat) : Prop where
+  scratch : a.gpr .rcx = work s
+  left : a.gpr .rdi = off (work s) x
+  right : a.gpr .rsi = off (work s) y
+  output : a.gpr .rdx = off (work s) out
+  keeps : Divide.Keeps [.rcx, .rdi, .rsi, .rdx] s a
+
+theorem args_nat_ok (s : State) (h : Ready s) (x y out : Nat)
+    (hx : x ≤ 8192) (hy : y ≤ 8192) (ho : out ≤ 8192) :
+    WP isa (.block (Impl.Argon2.X86_64.AddressCalls.args x y out)) s (Args s · x y out) := by
+  refine (args_ok s x y out h.frameRead).mono ?_
+  rintro a ⟨scratch, left, right, output, keeps⟩
+  rw [displacement_eq x hx] at left
+  rw [displacement_eq y hy] at right
+  rw [displacement_eq out ho] at output
+  exact ⟨scratch, left, right, output, keeps⟩
+
+theorem args_call_ready (s a : State) (h : Ready s) (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192)
+    (args : Args s a x y out) : FillCompress.CallReady a := by
+  have read (d : Nat) (hd : d + 1024 ≤ 8192) :
+      Covers [⟨off (work s) d, 1024⟩] (a.rd ++ a.wr) := by
+    rw [args.keeps.rd, args.keeps.wr]
+    intro p n hp
+    obtain ⟨r, hr, hc⟩ := work_cover s h d 1024 hd p n hp
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  have sp : a.gpr .rsp = s.gpr .rsp := args.keeps.regs .rsp (by decide)
+  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · rw [args.left]; exact read x bx
+  · rw [args.right]; exact read y by_
+  · rw [args.output, args.keeps.wr]; exact work_cover s h out 1024 bo
+  · rw [args.scratch, args.keeps.wr]
+    simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero]
+      using work_cover s h 0 4096 (by decide)
+  · rw [args.left, args.scratch]; exact Offset.disjoint_base _ hx (by omega)
+  · rw [args.right, args.scratch]; exact Offset.disjoint_base _ hy (by omega)
+  · rw [args.output, args.scratch]; exact Offset.disjoint_base _ ho (by omega)
+  · rw [sp, args.left]; exact h.stackWork.sub_right (Offset.sub_base _ bx)
+  · rw [sp, args.right]; exact h.stackWork.sub_right (Offset.sub_base _ by_)
+  · rw [sp, args.output]; exact h.stackWork.sub_right (Offset.sub_base _ bo)
+  · rw [sp, args.scratch]; exact h.stackWork.sub_right (Region.sub_prefix (by decide))
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsMx.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsMx.lean
new file mode 100644
index 000000000..faed3e606
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsMx.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCalls
+
+/-! The baseline independent-address calls preserve all MXCSR bits. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCalls
+
+theorem compression_noMx : VG.Impl.Argon2.X86_64.compress.allInstrs (fun i => !loadsMxcsr i) = true :=
+  by lit_decide
+
+theorem stage_noMx (x y out : Nat) : (stage x y out).allInstrs (fun i => !loadsMxcsr i) = true := by
+  change ((Code.block (args x y out) : Prog isa).allInstrs (fun i => !loadsMxcsr i) &&
+    VG.Impl.Argon2.X86_64.compress.allInstrs (fun i => !loadsMxcsr i)) = true
+  rw [compression_noMx]
+  rfl
+
+theorem calls_noMx : calls.allInstrs (fun i => !loadsMxcsr i) = true := by
+  change ((stage 7168 5120 4096).allInstrs (fun i => !loadsMxcsr i) &&
+    (stage 7168 4096 6144).allInstrs (fun i => !loadsMxcsr i)) = true
+  rw [stage_noMx, stage_noMx]
+  rfl
+
+theorem calls_mx_ok (p : Spec.Argon2.Params) (pass lane slice counter : Nat) (s : State) (h : Ready s)
+    (zero : Spec.Argon2.blockAt s.mem (off (work s) 7168) = Spec.Argon2.zeroBlock)
+    (input : Spec.Argon2.blockAt s.mem (off (work s) 5120) =
+      Proof.Argon2.addressInput p pass lane slice counter) :
+    WP isa calls s fun t => Generated s t p pass lane slice counter ∧ t.mxcsr = s.mxcsr :=
+  WP.mono_mx calls_noMx (calls_ok p pass lane slice counter s h zero input)
+    (fun _ generated mx => ⟨generated, mx⟩)
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsPrepare.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsPrepare.lean
new file mode 100644
index 000000000..ef17576d0
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsPrepare.lean
@@ -0,0 +1,159 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsClear
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressHeaderCorrect
+
+/-! Prepare the independent-address input and zero block from arbitrary scratch. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+structure Stable (s t : State) : Prop where
+  ready : Ready t
+  work_eq : work t = work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame [⟨work s, 8192⟩] s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+
+theorem Stable.trans {s a t : State} (h : Stable s a) (k : Stable a t) : Stable s t := by
+  have hf := k.frame
+  rw [h.work_eq] at hf
+  exact ⟨k.ready, k.work_eq.trans h.work_eq, fun r hr => (k.regs r hr).trans (h.regs r hr),
+    k.rd.trans h.rd, k.wr.trans h.wr, h.frame.trans hf, k.mxcsr.trans h.mxcsr⟩
+
+theorem Cleared.stable {s t : State} {offset : Nat} (h : Cleared s t offset)
+    (bound : offset + 1024 ≤ 8192) : Stable s t :=
+  ⟨h.ready, h.work_eq, h.regs, h.rd, h.wr, h.full_frame bound, h.mxcsr⟩
+
+theorem stable_of_frame {s t : State} (h : Ready s)
+    (regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r) (rd : t.rd = s.rd) (wr : t.wr = s.wr)
+    (frame : Frame [⟨work s, 8192⟩] s.mem t.mem) (mx : t.mxcsr = s.mxcsr) : Stable s t := by
+  have bp := regs .rbp (by simp [calleeSaved])
+  have sp := regs .rsp (by simp [calleeSaved])
+  have work' : work t = work s := by
+    unfold work
+    rw [bp, frame_word h frame 248 (by decide)]
+  refine ⟨⟨?_, ?_, ?_, ?_, ?_⟩, work', regs, rd, wr, frame, mx⟩
+  · rw [rd, wr, bp]; exact h.frameRead
+  · rw [work', wr]; exact h.workWrite
+  · rw [bp, work']; exact h.frameWork
+  · rw [bp, sp]; exact h.frameStack
+  · rw [sp, work']; exact h.stackWork
+
+theorem Stable.reads {s t : State} (h : Stable s t)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8) :
+    ∀ d ∈ [0, 8, 72, 112, 240], InRegions (t.rd ++ t.wr) (off (t.gpr .rbp) d) 8 := by
+  rw [h.rd, h.wr, h.regs .rbp (by simp [calleeSaved])]
+  exact reads
+
+theorem Stable.words {s t : State} {p : Params} {pass lane slice counter : Nat} (ready : Ready s) (h : Stable s t)
+    (words : AddressHeader.Words p pass lane slice counter s) :
+    AddressHeader.Words p pass lane slice counter t := by
+  have bp := h.regs .rbp (by simp [calleeSaved])
+  have read (d : Nat) (hd : d + 8 ≤ 272) :
+      t.mem.readW (off (t.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 := by
+    rw [bp]; exact frame_word ready h.frame d hd
+  exact ⟨(read 0 (by decide)).trans words.passWord,
+    (h.regs .rbx (by simp [calleeSaved])).trans words.laneWord,
+    (h.regs .r14 (by simp [calleeSaved])).trans words.sliceWord,
+    (read 240 (by decide)).trans words.blocksWord,
+    (read 72 (by decide)).trans words.passesWord,
+    (read 112 (by decide)).trans words.variantWord,
+    (read 8 (by decide)).trans words.counterWord⟩
+
+theorem pointer_stable {s a : State} (h : Ready s)
+    (k : Divide.Keeps [.rdi] s a) : Stable s a := by
+  apply stable_of_frame h _ k.rd k.wr _ k.mxcsr
+  · intro r hr
+    apply k.regs
+    simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+  · rw [k.mem]; exact Frame.refl _ _
+
+theorem Stable.input {s t : State} (ready : Ready s) (h : Stable s t) :
+    AddressHeader.input t = AddressHeader.input s := by
+  have value (i : Nat) (hi : i < 7) : AddressHeader.value t i = AddressHeader.value s i := by
+    unfold AddressHeader.value
+    rw [h.regs .rbx (by simp [calleeSaved]), h.regs .r14 (by simp [calleeSaved]),
+      h.regs .rbp (by simp [calleeSaved]),
+      frame_word ready h.frame (Impl.Argon2.X86_64.AddressHeader.frameOffset i)
+        (AddressHeader.offset_bound i hi)]
+  unfold AddressHeader.input
+  rw [value 0 (by decide), value 1 (by decide), value 2 (by decide), value 3 (by decide),
+    value 4 (by decide), value 5 (by decide), value 6 (by decide)]
+
+structure PreparedInput (s t : State) : Prop where
+  stable : Stable s t
+  zero : blockAt t.mem (off (work s) 7168) = zeroBlock
+  input : blockAt t.mem (off (work s) 5120) = AddressHeader.input s
+
+structure Prepared (s t : State) (p : Params) (pass lane slice counter : Nat) : Prop where
+  stable : Stable s t
+  zero : blockAt t.mem (off (work s) 7168) = zeroBlock
+  input : blockAt t.mem (off (work s) 5120) = Proof.Argon2.addressInput p pass lane slice counter
+
+theorem prepare_layout_ok (s : State) (h : Ready s)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    : WP isa prepare s (PreparedInput s) := by
+  unfold prepare
+  refine WP.seq ((clearAt_ok s h 5120 (by decide)).mono ?_)
+  intro a inputClear
+  refine WP.seq ((clearAt_ok a inputClear.ready 7168 (by decide)).mono ?_)
+  intro b zeroClear
+  have stableB := (inputClear.stable (by decide)).trans (zeroClear.stable (by decide))
+  have inputZero : blockAt b.mem (off (work s) 5120) = zeroBlock := by
+    have kept := FillCompress.block_frame zeroClear.frame (p := off (work s) 5120) (by
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      rw [inputClear.work_eq]
+      exact Offset.disjoint _ (by decide) (by decide) (by decide))
+    exact kept.trans inputClear.block
+  refine WP.seq ((pointer_ok b 5120 zeroClear.ready.frameRead).mono ?_)
+  rintro c ⟨dest, keeps⟩
+  rw [displacement_eq 5120 (by decide)] at dest
+  have stableC := stableB.trans (pointer_stable zeroClear.ready keeps)
+  have dest' : c.gpr .rdi = off (work s) 5120 := by rw [dest, stableB.work_eq]
+  have write : Covers [⟨c.gpr .rdi, 1024⟩] c.wr := by
+    rw [dest, keeps.wr]; exact work_cover b zeroClear.ready 5120 1024 (by decide)
+  have sep : (⟨c.gpr .rbp, 272⟩ : Region).Disjoint ⟨c.gpr .rdi, 1024⟩ := by
+    rw [dest', stableC.regs .rbp (by simp [calleeSaved])]
+    exact h.frameWork.sub_right (Offset.sub_base _ (by decide))
+  have zero : blockAt c.mem (c.gpr .rdi) = zeroBlock := by rw [dest', keeps.mem]; exact inputZero
+  refine (AddressHeader.code_ok c (stableC.reads reads) write sep zero).mono ?_
+  rintro t ⟨input, frame, tk, mx⟩
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = c.gpr r := by
+    intro r hr
+    apply tk.1
+    simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+  have frame' : Frame [⟨work c, 8192⟩] c.mem t.mem := by
+    apply frame.sub
+    intro r hr
+    simp only [List.mem_singleton] at hr
+    subst r
+    refine ⟨⟨work c, 8192⟩, by simp, ?_⟩
+    rw [dest', stableC.work_eq]
+    exact Offset.sub_base _ (by decide)
+  have stableT := stableC.trans (stable_of_frame stableC.ready regs tk.2.1 tk.2.2 frame' mx)
+  refine ⟨stableT, ?_, ?_⟩
+  · have kept := FillCompress.block_frame frame (p := off (work s) 7168) (by
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      rw [dest']
+      exact Offset.disjoint _ (by decide) (by decide) (by decide))
+    rw [kept, keeps.mem, ← inputClear.work_eq]
+    exact zeroClear.block
+  · rw [dest'] at input
+    exact input.trans (stableC.input h)
+
+theorem prepare_ok (p : Params) (pass lane slice counter : Nat) (s : State) (h : Ready s)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (words : AddressHeader.Words p pass lane slice counter s) :
+    WP isa prepare s (Prepared s · p pass lane slice counter) :=
+  (prepare_layout_ok s h reads).mono (fun _ k =>
+    ⟨k.stable, k.zero, k.input.trans (AddressHeader.input_spec p pass lane slice counter s words)⟩)
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsStage.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsStage.lean
new file mode 100644
index 000000000..a675ced48
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCallsStage.lean
@@ -0,0 +1,76 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsLayout
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressSetup
+
+/-! One verified G call within the independent-address scratch layout. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+def stageWrites (s : State) (out : Nat) : List Region :=
+  [⟨off (work s) out, 1024⟩, ⟨work s, 4096⟩, below (s.gpr .rsp) 8]
+
+structure StageDone (s t : State) (x y out : Nat) : Prop where
+  result : blockAt t.mem (off (work s) out) = Spec.Argon2.compress
+    (blockAt s.mem (off (work s) x)) (blockAt s.mem (off (work s) y))
+  ready : Ready t
+  work : work t = work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (stageWrites s out) s.mem t.mem
+
+theorem Args.callee {s a : State} {x y out : Nat} (h : Args s a x y out)
+    (r : Reg) (hr : r ∈ calleeSaved) : a.gpr r = s.gpr r := by
+  apply h.keeps.regs
+  simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+
+theorem ready_of_frame {s t : State} (h : Ready s) (out : Nat) (ho : out + 1024 ≤ 8192)
+    (regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r) (rd : t.rd = s.rd) (wr : t.wr = s.wr)
+    (frame : Frame (stageWrites s out) s.mem t.mem) : Ready t ∧ work t = work s := by
+  have bp := regs .rbp (by simp [calleeSaved])
+  have sp := regs .rsp (by simp [calleeSaved])
+  have safe : ∀ r ∈ stageWrites s out, (⟨s.gpr .rbp, 272⟩ : Region).Disjoint r := by
+    intro r hr
+    simp only [stageWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl
+    · exact h.frameWork.sub_right (Offset.sub_base _ ho)
+    · exact h.frameWork.sub_right (Region.sub_prefix (by decide))
+    · exact h.frameStack
+  have read : t.mem.readW (off (s.gpr .rbp) 248) 64 = s.mem.readW (off (s.gpr .rbp) 248) 64 :=
+    frame.readW (r := ⟨s.gpr .rbp, 272⟩)
+      (Offset.contains_base _ (by decide) (by decide)) safe (by decide)
+  have work' : work t = work s := by unfold work; rw [bp, read]
+  refine ⟨⟨?_, ?_, ?_, ?_, ?_⟩, work'⟩
+  · rw [rd, wr, bp]; exact h.frameRead
+  · rw [work', wr]; exact h.workWrite
+  · rw [bp, work']; exact h.frameWork
+  · rw [bp, sp]; exact h.frameStack
+  · rw [sp, work']; exact h.stackWork
+
+theorem stage_ok (s : State) (h : Ready s) (x y out : Nat)
+    (hx : 4096 ≤ x) (hy : 4096 ≤ y) (ho : 4096 ≤ out)
+    (bx : x + 1024 ≤ 8192) (by_ : y + 1024 ≤ 8192) (bo : out + 1024 ≤ 8192) :
+    WP isa (stage x y out) s (StageDone s · x y out) := by
+  unfold stage
+  refine WP.seq ((args_nat_ok s h x y out (by omega) (by omega) (by omega)).mono ?_)
+  intro a args
+  have callReady := args_call_ready s a h x y out hx hy ho bx by_ bo args
+  refine (FillCompress.call_ok _ a callReady).mono ?_
+  intro t called
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r :=
+    fun r hr => (called.regs r hr).trans (args.callee r hr)
+  have rd := called.rd.trans args.keeps.rd
+  have wr := called.wr.trans args.keeps.wr
+  have frame : Frame (stageWrites s out) s.mem t.mem := by
+    have hf := called.frame
+    rw [args.output, args.scratch, args.callee .rsp (by simp [calleeSaved]), args.keeps.mem] at hf
+    exact hf
+  obtain ⟨ready, work'⟩ := ready_of_frame h out bo regs rd wr frame
+  refine ⟨?_, ready, work', regs, rd, wr, frame⟩
+  have result := called.result
+  rw [args.output, args.left, args.right, args.keeps.mem] at result
+  exact result
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGeneration.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGeneration.lean
new file mode 100644
index 000000000..ad97eb8d3
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGeneration.lean
@@ -0,0 +1,39 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsPrepare
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsMx
+
+/-! Complete independent-address generation against the reviewed algorithm. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCalls
+
+theorem code_ok (p : Params) (pass lane slice counter : Nat) (s : State) (h : Ready s)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (words : AddressHeader.Words p pass lane slice counter s) :
+    WP isa code s fun t => Generated s t p pass lane slice counter ∧ t.mxcsr = s.mxcsr := by
+  unfold code
+  refine WP.seq ((prepare_ok p pass lane slice counter s h reads words).mono ?_)
+  intro a prepared
+  have zero : blockAt a.mem (off (work a) 7168) = zeroBlock := by
+    rw [prepared.stable.work_eq]; exact prepared.zero
+  have input : blockAt a.mem (off (work a) 5120) = Proof.Argon2.addressInput p pass lane slice counter := by
+    rw [prepared.stable.work_eq]; exact prepared.input
+  refine (calls_mx_ok p pass lane slice counter a prepared.stable.ready zero input).mono ?_
+  rintro t ⟨generated, mx⟩
+  have frame := generated.frame
+  rw [writes, prepared.stable.work_eq, prepared.stable.regs .rsp (by simp [calleeSaved])] at frame
+  have firstFrame : Frame (writes s) s.mem a.mem :=
+    prepared.stable.frame.mono (by
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      simp [writes])
+  refine ⟨⟨?_, generated.ready, generated.work.trans prepared.stable.work_eq,
+    fun r hr => (generated.regs r hr).trans (prepared.stable.regs r hr),
+    generated.rd.trans prepared.stable.rd, generated.wr.trans prepared.stable.wr,
+    firstFrame.trans frame⟩, mx.trans prepared.stable.mxcsr⟩
+  have block := generated.block
+  rw [prepared.stable.work_eq] at block
+  exact block
+
+end VG.Proof.Argon2.X86_64.AddressCalls
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGenerationCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGenerationCT.lean
new file mode 100644
index 000000000..fe611aec5
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressGenerationCT.lean
@@ -0,0 +1,95 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsCT
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsPrepare
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressInputCT
+
+/-! Independent-address generation keeps its entire trace independent of secrets. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCalls
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCalls
+
+theorem Related.of_stable {s t a b : State} (h : Related s t)
+    (ha : Stable s a) (hb : Stable t b) : Related a b :=
+  ⟨ha.ready, hb.ready,
+    (ha.regs .rbp (by simp [calleeSaved])).trans
+      (h.bases.trans (hb.regs .rbp (by simp [calleeSaved])).symm),
+    (ha.regs .rsp (by simp [calleeSaved])).trans
+      (h.stacks.trans (hb.regs .rsp (by simp [calleeSaved])).symm),
+    ha.work_eq.trans (h.work.trans hb.work_eq.symm)⟩
+
+theorem input_pointer_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block (pointer 5120)) (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)
+
+theorem zero_pointer_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block (pointer 7168)) (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)
+
+structure PointRelated (s t : State) : Prop where
+  related : Related s t
+  pointer : s.gpr .rdi = t.gpr .rdi
+
+theorem pointer_public_rel (offset : Nat)
+    (trace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+      (.block (pointer offset)) (fun _ _ => True)) :
+    RelCT isa Related (.block (pointer offset)) PointRelated := by
+  have publicTrace := trace.mono (P' := Related) (fun _ _ h => h.bases) (fun _ _ h => h)
+  have full := publicTrace.wpDep (fun s t h =>
+    ⟨pointer_ok s offset h.left.frameRead, pointer_ok t offset h.right.frameRead⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ⟨pa, ka⟩, ⟨pb, kb⟩⟩ := h
+  exact ⟨hp.of_stable (pointer_stable hp.left ka) (pointer_stable hp.right kb),
+    pa.trans ((congrArg (· + displacement offset) hp.work).trans pb.symm)⟩
+
+theorem clearAt_rel (offset : Nat) (bound : offset + 1024 ≤ 8192)
+    (trace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+      (.block (pointer offset)) (fun _ _ => True)) :
+    RelCT isa Related (clearAt offset) Related := by
+  have clear := ClearBlock.code_rel.mono (P' := PointRelated)
+    (fun _ _ h => h.pointer) (fun _ _ h => h)
+  have blocks := (pointer_public_rel offset trace).seq clear
+  have full := blocks.wpDep (fun s t h =>
+    ⟨clearAt_ok s h.left offset bound, clearAt_ok t h.right offset bound⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact hp.of_stable (ha.stable bound) (hb.stable bound)
+
+structure PrepareRelated (s t : State) : Prop where
+  related : Related s t
+  leftReads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8
+  rightReads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (t.rd ++ t.wr) (off (t.gpr .rbp) d) 8
+
+theorem prepare_rel : RelCT isa PrepareRelated prepare Related := by
+  have header := AddressHeader.code_rel.mono (P' := PointRelated) (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
+    · exact h.pointer
+    · exact h.related.bases) (fun _ _ h => h)
+  have trace := (clearAt_rel 5120 (by decide) input_pointer_rel).seq
+    ((clearAt_rel 7168 (by decide) zero_pointer_rel).seq
+      ((pointer_public_rel 5120 input_pointer_rel).seq header))
+  have narrowed := trace.mono (P' := PrepareRelated) (fun _ _ h => h.related) (fun _ _ h => h)
+  have full := narrowed.wpDep (fun s t h =>
+    ⟨prepare_layout_ok s h.related.left h.leftReads,
+      prepare_layout_ok t h.related.right h.rightReads⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact hp.related.of_stable ha.stable hb.stable
+
+theorem code_rel : RelCT isa PrepareRelated code Related := prepare_rel.seq calls_rel
+
+end VG.Proof.Argon2.X86_64.AddressCalls