diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCache.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCache.lean
new file mode 100644
index 000000000..f0d7f3a3d
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCache.lean
@@ -0,0 +1,32 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCalls
+
+/-! Cache one address block per 128 segment positions. Frame offset eight holds
+its one-based counter; initializing it to zero forces generation even when the
+first filled index is two. Only public counters control regeneration.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressCache
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def check : List Instr := [
+  .mov .rax (.reg .r15), .shift .shr .rax 7, .alu .add .rax (.imm 1),
+  .alu .cmp .rax (.mem (at_ .rbp 8))]
+
+def save : List Instr := [.store (at_ .rbp 8) .rax]
+
+def select : Prog isa := .seq (.block check)
+  (.ite .e (.block []) (.seq (.block save) AddressCalls.code))
+
+def wordArgs : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)), .mov .rax (.reg .r15), .alu .and .rax (.imm 127)]
+
+def wordRead : List Instr := [
+  .mov .rdi (.mem { base := .rcx, index := some .rax, scale := 8, disp := 6144 })]
+
+def word : Prog isa := .seq (.block wordArgs) (.block wordRead)
+
+def code : Prog isa := .seq select word
+
+end VG.Impl.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCache.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCache.lean
new file mode 100644
index 000000000..1ed6dcf14
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCache.lean
@@ -0,0 +1,49 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheSelect
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheWord
+
+/-! Complete cached random-word selection against RFC 9106's address block. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+structure Done (s t : State) (p : Params) (pass lane slice : Nat) : Prop where
+  selected : Selected s t p pass lane slice
+  random : t.gpr .rdi =
+    (addressBlock p pass lane slice (wanted s))[(s.gpr .r15).toNat % 128]'(Nat.mod_lt _ (by decide))
+
+theorem code_ok (p : Params) (pass lane slice old : Nat) (s : State)
+    (h : Ready p pass lane slice old s) :
+    WP isa code s (Done s · p pass lane slice) := by
+  unfold code
+  refine WP.seq ((selected_ok p pass lane slice old s h).mono ?_)
+  intro a selected
+  refine (word_ok a selected.layout).mono ?_
+  rintro t ⟨random, keeps⟩
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r := by
+    intro r hr
+    have ne : r ∉ [Reg.rcx, .rax, .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 (keeps.regs r ne).trans (selected.regs r hr)
+  have bp := keeps.regs .rbp (by decide)
+  have sp := keeps.regs .rsp (by decide)
+  have work' : AddressCalls.work t = AddressCalls.work a := by
+    unfold AddressCalls.work; rw [bp, keeps.mem]
+  have layout : AddressCalls.Ready t := by
+    constructor
+    · rw [keeps.rd, keeps.wr, bp]; exact selected.layout.frameRead
+    · rw [work', keeps.wr]; exact selected.layout.workWrite
+    · rw [bp, work']; exact selected.layout.frameWork
+    · rw [bp, sp]; exact selected.layout.frameStack
+    · rw [sp, work']; exact selected.layout.stackWork
+  refine ⟨⟨?_, layout, work'.trans selected.work_eq, regs,
+    keeps.rd.trans selected.rd, keeps.wr.trans selected.wr, ?_,
+    keeps.mxcsr.trans selected.mxcsr, ?_⟩, ?_⟩
+  · rw [keeps.mem]; exact selected.block
+  · rw [keeps.mem]; exact selected.frame
+  · rw [bp, keeps.mem]; exact selected.counterWord
+  · rw [selected.work_eq, selected.regs .r15 (by simp [calleeSaved]), selected.block] at random
+    exact random
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMeta.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMeta.lean
new file mode 100644
index 000000000..5a2664356
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMeta.lean
@@ -0,0 +1,77 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceStart
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCache
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsPrepare
+
+/-! Public cache counters and indexed-word arguments. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCache
+
+def counter (index : Addr) : Addr := (index >>> 7) + 1
+
+theorem check_ok (s : State)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 8) 8) :
+    WP isa (.block check) s fun t => t.gpr .rax = counter (s.gpr .r15) ∧
+      t.zf = decide (counter (s.gpr .r15) = s.mem.readW (off (s.gpr .rbp) 8) 64) ∧
+      Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [check, counter, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    execShift, execAlu, State.load64, ea_at, hr, RegUpd.gpr_setReg, RegUpd.gpr_setFlags,
+    RegUpd.gpr_arithFlags, RegUpd.mem_setReg, RegUpd.mem_setFlags, RegUpd.mem_arithFlags,
+    RegUpd.rd_setReg, RegUpd.rd_setFlags, RegUpd.rd_arithFlags,
+    RegUpd.wr_setReg, RegUpd.wr_setFlags, RegUpd.wr_arithFlags,
+    RegUpd.zf_arithFlags, reduceCtorEq, ite_true, ite_false, and_self,
+    show 1 ≤ (7 : Nat) ∧ (7 : Nat) ≤ 63 from by decide,
+    show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl,
+    Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, ?_, ?_⟩
+  · apply Bool.eq_iff_iff.mpr
+    simp only [beq_iff_eq, ReferenceStart.sub_zero_iff]
+    exact ⟨fun h => decide_eq_true h, of_decide_eq_true⟩
+  · constructor
+    · intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      simp only [RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags, hr, ite_false]
+    all_goals rfl
+
+theorem counter_nat (index : Addr) : counter index = BitVec.ofNat 64 (index.toNat / 128 + 1) := by
+  have shifted : index >>> 7 = BitVec.ofNat 64 (index.toNat / 128) := by
+    apply BitVec.eq_of_toNat_eq
+    rw [BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, BitVec.toNat_ofNat,
+      Nat.mod_eq_of_lt (by have := index.isLt; omega)]
+  unfold counter
+  rw [shifted]
+  exact (BitVec.ofNat_add _ _).symm
+
+theorem counter_ne_zero (index : Addr) : counter index ≠ 0 := by
+  have bound : index.toNat / 128 + 1 < 2 ^ 64 := by have := index.isLt; omega
+  intro h
+  have nat := congrArg BitVec.toNat h
+  rw [counter_nat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt bound] at nat
+  change index.toNat / 128 + 1 = 0 at nat
+  omega
+
+theorem wordArgs_ok (s : State)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block wordArgs) s fun t => t.gpr .rcx = AddressCalls.work s ∧
+      t.gpr .rax = s.gpr .r15 &&& 127 ∧ Divide.Keeps [.rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [wordArgs, AddressCalls.work, 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,
+    show BitVec.signExtend 64 (127 : BitVec 32) = (127 : Addr) from rfl,
+    Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+    simp only [RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, hr.1, hr.2, ite_false]
+  all_goals rfl
+
+theorem index_nat (index : Addr) : index &&& 127 = BitVec.ofNat 64 (index.toNat % 128) := by
+  apply BitVec.eq_of_toNat_eq
+  rw [BitVec.toNat_and, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)]
+  exact Nat.and_two_pow_sub_one_eq_mod index.toNat 7
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSave.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSave.lean
new file mode 100644
index 000000000..f69d79251
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSave.lean
@@ -0,0 +1,65 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheMeta
+
+/-! Save the public cache counter without disturbing scratch or header fields. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+theorem save_ok (s : State) (hw : InRegions s.wr (off (s.gpr .rbp) 8) 8) :
+    WP isa (.block save) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rbp) 8) (s.gpr .rax) ∧
+      t.gpr = s.gpr ∧ t.rd = s.rd ∧ t.wr = s.wr ∧ t.mxcsr = s.mxcsr := by
+  apply WP.of_runBlock
+  simp only [save, runBlock_cons, runStep_some, runBlock_nil, exec, State.store64,
+    ea_at, hw, ite_true, Option.some.injEq, exists_eq_left']
+  exact ⟨trivial, trivial, trivial, trivial, trivial⟩
+
+structure Saved (s t : State) : Prop where
+  mem : t.mem = s.mem.writeW (off (s.gpr .rbp) 8) (s.gpr .rax)
+  regs : t.gpr = s.gpr
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  mxcsr : t.mxcsr = s.mxcsr
+  ready : AddressCalls.Ready t
+  work_eq : AddressCalls.work t = AddressCalls.work s
+  frame : Frame [⟨off (s.gpr .rbp) 8, 8⟩] s.mem t.mem
+
+theorem save_ready (s : State) (h : AddressCalls.Ready s)
+    (hw : InRegions s.wr (off (s.gpr .rbp) 8) 8) : WP isa (.block save) s (Saved s) := by
+  refine (save_ok s hw).mono ?_
+  rintro t ⟨mem, regs, rd, wr, mx⟩
+  have work' : AddressCalls.work t = AddressCalls.work s := by
+    unfold AddressCalls.work
+    rw [regs, mem, Mem.readW_writeW_sep (Offset.sep _ (by decide) (by decide) (by decide)) (by decide)]
+  have ready : AddressCalls.Ready t := by
+    constructor
+    · rw [rd, wr, regs]; exact h.frameRead
+    · rw [work', wr]; exact h.workWrite
+    · rw [regs, work']; exact h.frameWork
+    · rw [regs]; exact h.frameStack
+    · rw [regs, work']; exact h.stackWork
+  refine ⟨mem, regs, rd, wr, mx, ready, work', ?_⟩
+  rw [mem]
+  exact (Frame.refl _ _).writeW (r := ⟨off (s.gpr .rbp) 8, 8⟩) (by simp) _
+    (Region.contains_self _ _)
+
+theorem Saved.read {s t : State} (h : Saved s t) (d : Nat)
+    (hd : d + 8 ≤ 8 ∨ 16 ≤ d) (bound : d + 8 ≤ 272) :
+    t.mem.readW (off (t.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 := by
+  rw [h.regs, h.mem]
+  exact Mem.readW_writeW_sep (Offset.sep _ hd (by omega) (by decide)) (by decide)
+
+theorem Saved.words {s t : State} {p : Params} {pass lane slice old counter : Nat}
+    (h : Saved s t) (words : AddressHeader.Words p pass lane slice old s)
+    (value : s.gpr .rax = BitVec.ofNat 64 counter) :
+    AddressHeader.Words p pass lane slice counter t := by
+  refine ⟨(h.read 0 (by decide) (by decide)).trans words.passWord,
+    ?_, ?_, (h.read 240 (by decide) (by decide)).trans words.blocksWord,
+    (h.read 72 (by decide) (by decide)).trans words.passesWord,
+    (h.read 112 (by decide) (by decide)).trans words.variantWord, ?_⟩
+  · rw [h.regs]; exact words.laneWord
+  · rw [h.regs]; exact words.sliceWord
+  · rw [h.regs, h.mem, Mem.readW_writeW_self64, value]
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelect.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelect.lean
new file mode 100644
index 000000000..2426c91d0
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelect.lean
@@ -0,0 +1,114 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheSave
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressGeneration
+
+/-! Regenerate only when the public one-based block counter changes. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+def wanted (s : State) : Nat := (s.gpr .r15).toNat / 128 + 1
+
+def writes (s : State) : List Region :=
+  [⟨AddressCalls.work s, 8192⟩, below (s.gpr .rsp) 8, ⟨off (s.gpr .rbp) 8, 8⟩]
+
+structure Ready (p : Params) (pass lane slice old : Nat) (s : State) : Prop where
+  layout : AddressCalls.Ready s
+  reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8
+  write : InRegions s.wr (off (s.gpr .rbp) 8) 8
+  words : AddressHeader.Words p pass lane slice old s
+  cached : counter (s.gpr .r15) = s.mem.readW (off (s.gpr .rbp) 8) 64 →
+    blockAt s.mem (off (AddressCalls.work s) 6144) = addressBlock p pass lane slice (wanted s)
+
+theorem ready_zero (p : Params) (pass lane slice : Nat) (s : State)
+    (layout : AddressCalls.Ready s)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (write : InRegions s.wr (off (s.gpr .rbp) 8) 8)
+    (words : AddressHeader.Words p pass lane slice 0 s) : Ready p pass lane slice 0 s :=
+  ⟨layout, reads, write, words, fun same => False.elim
+    (counter_ne_zero _ (same.trans words.counterWord))⟩
+
+structure Selected (s t : State) (p : Params) (pass lane slice : Nat) : Prop where
+  block : blockAt t.mem (off (AddressCalls.work s) 6144) = addressBlock p pass lane slice (wanted s)
+  layout : AddressCalls.Ready t
+  work_eq : AddressCalls.work t = AddressCalls.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
+  mxcsr : t.mxcsr = s.mxcsr
+  counterWord : t.mem.readW (off (t.gpr .rbp) 8) 64 = counter (s.gpr .r15)
+
+theorem check_stable {s a : State} (h : AddressCalls.Ready s) (k : Divide.Keeps [.rax] s a) :
+    AddressCalls.Stable s a := by
+  apply AddressCalls.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 selected_ok (p : Params) (pass lane slice old : Nat) (s : State)
+    (h : Ready p pass lane slice old s) :
+    WP isa select s (Selected s · p pass lane slice) := by
+  unfold select
+  refine WP.seq ((check_ok s (h.reads 8 (by simp))).mono ?_)
+  rintro a ⟨value, flag, keeps⟩
+  have stableA := check_stable h.layout keeps
+  refine WP.ite (decide (counter (s.gpr .r15) = s.mem.readW (off (s.gpr .rbp) 8) 64))
+    (by simp only [eval, flag]) ?_ ?_
+  · intro same
+    have equal := of_decide_eq_true same
+    apply WP.of_runBlock
+    simp only [runBlock_nil, Option.some.injEq, exists_eq_left']
+    refine ⟨?_, stableA.ready, stableA.work_eq, stableA.regs, keeps.rd, keeps.wr,
+      ?_, keeps.mxcsr, ?_⟩
+    · rw [keeps.mem]; exact h.cached equal
+    · rw [keeps.mem]; exact Frame.refl _ _
+    · rw [stableA.regs .rbp (by simp [calleeSaved]), keeps.mem]; exact equal.symm
+  · intro _
+    have write : InRegions a.wr (off (a.gpr .rbp) 8) 8 := by
+      rw [keeps.wr, stableA.regs .rbp (by simp [calleeSaved])]; exact h.write
+    refine WP.seq ((save_ready a stableA.ready write).mono ?_)
+    intro b saved
+    have words : AddressHeader.Words p pass lane slice (wanted s) b := by
+      apply saved.words (stableA.words h.layout h.words)
+      rw [value, counter_nat]; rfl
+    have reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (b.rd ++ b.wr) (off (b.gpr .rbp) d) 8 := by
+      rw [saved.rd, saved.wr, saved.regs]; exact stableA.reads h.reads
+    refine (AddressCalls.code_ok p pass lane slice (wanted s) b saved.ready reads words).mono ?_
+    rintro t ⟨generated, mx⟩
+    have workB : AddressCalls.work b = AddressCalls.work s := saved.work_eq.trans stableA.work_eq
+    have regsB (r : Reg) (hr : r ∈ calleeSaved) : b.gpr r = s.gpr r :=
+      (congrFun saved.regs r).trans (stableA.regs r hr)
+    have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r :=
+      fun r hr => (generated.regs r hr).trans (regsB r hr)
+    have firstFrame : Frame (writes s) s.mem b.mem := by
+      have frame := saved.frame
+      rw [stableA.regs .rbp (by simp [calleeSaved]), keeps.mem] at frame
+      exact frame.mono (by intro r hr; simp only [List.mem_singleton] at hr; subst r; simp [writes])
+    have finalFrame : Frame (writes s) b.mem t.mem := by
+      have frame := generated.frame
+      rw [AddressCalls.writes, workB, regsB .rsp (by simp [calleeSaved])] at frame
+      exact frame.mono (by
+        intro r hr
+        simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+        rcases hr with rfl | rfl <;> simp [writes])
+    refine ⟨?_, generated.ready, generated.work.trans workB, regs,
+      generated.rd.trans (saved.rd.trans keeps.rd), generated.wr.trans (saved.wr.trans keeps.wr),
+      firstFrame.trans finalFrame, mx.trans (saved.mxcsr.trans keeps.mxcsr), ?_⟩
+    · have block := generated.block
+      rw [workB] at block
+      exact block
+    · have preserved : t.mem.readW (off (b.gpr .rbp) 8) 64 = b.mem.readW (off (b.gpr .rbp) 8) 64 :=
+        generated.frame.readW (r := ⟨b.gpr .rbp, 272⟩)
+          (Offset.contains_base _ (by decide) (by decide)) (by
+            intro r hr
+            simp only [AddressCalls.writes, List.mem_cons, List.not_mem_nil, or_false] at hr
+            rcases hr with rfl | rfl
+            · exact saved.ready.frameWork
+            · exact saved.ready.frameStack) (by decide)
+      rw [generated.regs .rbp (by simp [calleeSaved]), preserved, saved.regs, saved.mem,
+        Mem.readW_writeW_self64, value]
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelectCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelectCT.lean
new file mode 100644
index 000000000..5652b3b09
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelectCT.lean
@@ -0,0 +1,118 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheSelect
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheWordCT
+
+/-! Cache regeneration branches only on public counters. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCache
+
+structure CacheRelated (s t : State) : Prop where
+  prepare : AddressCalls.PrepareRelated s t
+  indices : s.gpr .r15 = t.gpr .r15
+  counters : s.mem.readW (off (s.gpr .rbp) 8) 64 = t.mem.readW (off (t.gpr .rbp) 8) 64
+  leftWrite : InRegions s.wr (off (s.gpr .rbp) 8) 8
+  rightWrite : InRegions t.wr (off (t.gpr .rbp) 8) 8
+
+structure CheckedRelated (s t : State) : Prop where
+  related : CacheRelated s t
+  values : s.gpr .rax = t.gpr .rax
+  flags : s.zf = t.zf
+
+theorem check_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.rbp, .r15], s.gpr r = t.gpr r)
+    (.block check) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp, .r15])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+theorem check_public_rel : RelCT isa CacheRelated (.block check) CheckedRelated := by
+  have trace := check_rel.mono (P' := CacheRelated) (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.prepare.related.bases
+    · exact h.indices) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨check_ok s (h.prepare.leftReads 8 (by simp)), check_ok t (h.prepare.rightReads 8 (by simp))⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ⟨va, fa, ka⟩, ⟨vb, fb, kb⟩⟩ := h
+  have sa := check_stable hp.prepare.related.left ka
+  have sb := check_stable hp.prepare.related.right kb
+  have index : a.gpr .r15 = b.gpr .r15 := (sa.regs .r15 (by simp [calleeSaved])).trans
+    (hp.indices.trans (sb.regs .r15 (by simp [calleeSaved])).symm)
+  have counters : a.mem.readW (off (a.gpr .rbp) 8) 64 = b.mem.readW (off (b.gpr .rbp) 8) 64 := by
+    rw [ka.mem, kb.mem, sa.regs .rbp (by simp [calleeSaved]), sb.regs .rbp (by simp [calleeSaved])]
+    exact hp.counters
+  refine ⟨⟨⟨hp.prepare.related.of_stable sa sb, sa.reads hp.prepare.leftReads,
+    sb.reads hp.prepare.rightReads⟩, index, counters, ?_, ?_⟩, ?_, ?_⟩
+  · rw [ka.wr, sa.regs .rbp (by simp [calleeSaved])]; exact hp.leftWrite
+  · rw [kb.wr, sb.regs .rbp (by simp [calleeSaved])]; exact hp.rightWrite
+  · rw [va, vb, hp.indices]
+  · rw [fa, fb, hp.indices, hp.counters]
+
+theorem save_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block save) (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 save_public_rel : RelCT isa CheckedRelated (.block save) AddressCalls.PrepareRelated := by
+  have trace := save_rel.mono (P' := CheckedRelated)
+    (fun _ _ h => h.related.prepare.related.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨save_ready s h.related.prepare.related.left h.related.leftWrite,
+      save_ready t h.related.prepare.related.right h.related.rightWrite⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨⟨ha.ready, hb.ready, ?_, ?_, ha.work_eq.trans
+    (hp.related.prepare.related.work.trans hb.work_eq.symm)⟩, ?_, ?_⟩
+  · rw [ha.regs, hb.regs]; exact hp.related.prepare.related.bases
+  · rw [ha.regs, hb.regs]; exact hp.related.prepare.related.stacks
+  · rw [ha.rd, ha.wr, ha.regs]; exact hp.related.prepare.leftReads
+  · rw [hb.rd, hb.wr, hb.regs]; exact hp.related.prepare.rightReads
+
+theorem select_trace : RelCT isa CacheRelated select (fun _ _ => True) := by
+  have noop : RelCT isa (fun _ _ : State => True) (.block []) (fun _ _ => True) :=
+    RelCT.taint (A := taint) (Taint.ofRegs [])
+      (fun _ _ _ => Taint.agree_ofRegs (by intro r hr; simp at hr)) (by taint_decide)
+  have branches : RelCT isa CheckedRelated
+      (.ite .e (.block []) (.seq (.block save) Impl.Argon2.X86_64.AddressCalls.code))
+      (fun _ _ => True) :=
+    RelCT.ite (by intro s t h; simp only [eval, h.flags])
+      (noop.mono (fun _ _ _ => trivial) (fun _ _ h => h))
+      ((save_public_rel.seq AddressCalls.code_rel).mono (fun _ _ h => h.1) (fun _ _ _ => trivial))
+  exact check_public_rel.seq branches
+
+structure ReadyRelated (p : Spec.Argon2.Params) (pass lane slice old : Nat) (s t : State) : Prop where
+  left : Ready p pass lane slice old s
+  right : Ready p pass lane slice old t
+  pubs : CacheRelated s t
+
+theorem select_public_rel (p : Spec.Argon2.Params) (pass lane slice old : Nat) :
+    RelCT isa (ReadyRelated p pass lane slice old) select WordRelated := by
+  have trace := select_trace.mono (P' := ReadyRelated p pass lane slice old)
+    (fun _ _ h => h.pubs) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨selected_ok p pass lane slice old s h.left, selected_ok p pass lane slice old t h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨⟨ha.layout, hb.layout, ?_, ?_, ha.work_eq.trans
+    (hp.pubs.prepare.related.work.trans hb.work_eq.symm)⟩, ?_⟩
+  · exact (ha.regs .rbp (by simp [calleeSaved])).trans
+      (hp.pubs.prepare.related.bases.trans (hb.regs .rbp (by simp [calleeSaved])).symm)
+  · exact (ha.regs .rsp (by simp [calleeSaved])).trans
+      (hp.pubs.prepare.related.stacks.trans (hb.regs .rsp (by simp [calleeSaved])).symm)
+  · exact (ha.regs .r15 (by simp [calleeSaved])).trans
+      (hp.pubs.indices.trans (hb.regs .r15 (by simp [calleeSaved])).symm)
+
+theorem code_rel (p : Spec.Argon2.Params) (pass lane slice old : Nat) :
+    RelCT isa (ReadyRelated p pass lane slice old) code (fun _ _ => True) :=
+  (select_public_rel p pass lane slice old).seq word_rel
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheWord.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheWord.lean
new file mode 100644
index 000000000..095983bc2
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheWord.lean
@@ -0,0 +1,61 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheMeta
+
+/-! Read exactly the public indexed word of the cached address block. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+def wordAddress (s : State) : Addr :=
+  s.gpr .rcx + s.gpr .rax * BitVec.ofNat 64 8 + BitVec.ofInt 64 6144
+
+theorem wordRead_ok (s : State) (hr : InRegions (s.rd ++ s.wr) (wordAddress s) 8) :
+    WP isa (.block wordRead) s fun t => t.gpr .rdi = s.mem.readW (wordAddress s) 64 ∧
+      Divide.Keeps [.rdi] s t := by
+  dsimp only [wordAddress] at hr
+  apply WP.of_runBlock
+  simp only [wordRead, wordAddress, runBlock_cons, runStep_some, runBlock_nil,
+    exec, readSrc, State.load64, State.ea, hr, Option.map_some,
+    Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg, ite_true]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    simp only [RegUpd.gpr_setReg, hr, ite_false]
+  all_goals rfl
+
+theorem wordAddress_args {s a : State}
+    (scratch : a.gpr .rcx = AddressCalls.work s)
+    (index : a.gpr .rax = s.gpr .r15 &&& 127) :
+    wordAddress a = off (off (AddressCalls.work s) 6144) (8 * ((s.gpr .r15).toNat % 128)) := by
+  unfold wordAddress off
+  rw [scratch, index, index_nat, ← BitVec.ofNat_mul, Nat.mul_comm]
+  change AddressCalls.work s + BitVec.ofNat 64 (8 * ((s.gpr .r15).toNat % 128)) +
+    BitVec.ofNat 64 6144 = _
+  rw [BitVec.add_assoc, BitVec.add_comm (BitVec.ofNat 64 (8 * ((s.gpr .r15).toNat % 128)))
+    (BitVec.ofNat 64 6144), ← BitVec.add_assoc]
+
+theorem word_ok (s : State) (h : AddressCalls.Ready s) :
+    WP isa Impl.Argon2.X86_64.AddressCache.word s fun t => t.gpr .rdi =
+      (blockAt s.mem (off (AddressCalls.work s) 6144))[(s.gpr .r15).toNat % 128]'(Nat.mod_lt _ (by decide)) ∧
+      Divide.Keeps [.rcx, .rax, .rdi] s t := by
+  unfold Impl.Argon2.X86_64.AddressCache.word
+  refine WP.seq ((wordArgs_ok s h.frameRead).mono ?_)
+  rintro a ⟨scratch, index, keeps⟩
+  have address := wordAddress_args scratch index
+  have read : InRegions (a.rd ++ a.wr) (wordAddress a) 8 := by
+    rw [address, keeps.rd, keeps.wr]
+    have cover := AddressCalls.work_cover s h 6144 1024 (by decide)
+    have writable := cover _ _ ⟨⟨off (AddressCalls.work s) 6144, 1024⟩, by simp,
+      Offset.contains_base _ (d := 8 * ((s.gpr .r15).toNat % 128)) (n := 8) (k := 1024)
+        (by have := Nat.mod_lt (s.gpr .r15).toNat (by decide : 0 < 128); omega) (by omega)⟩
+    obtain ⟨r, hr, hc⟩ := writable
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  refine (wordRead_ok a read).mono ?_
+  rintro t ⟨value, tail⟩
+  refine ⟨?_, (keeps.mono (by decide)).trans (tail.mono (by decide))⟩
+  rw [value, address, keeps.mem]
+  change s.mem.readW _ 64 = (blockAt _ _)[(⟨_, Nat.mod_lt _ (by decide)⟩ : Fin 128)]
+  rw [blockAt_get]
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheWordCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheWordCT.lean
new file mode 100644
index 000000000..dd5e7ad90
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheWordCT.lean
@@ -0,0 +1,45 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheWord
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressGenerationCT
+
+/-! The cached random word is secret; its read address is public. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCache
+
+structure WordRelated (s t : State) : Prop where
+  layout : AddressCalls.Related s t
+  indices : s.gpr .r15 = t.gpr .r15
+
+theorem wordArgs_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.rbp, .r15], s.gpr r = t.gpr r)
+    (.block wordArgs) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp, .r15])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+theorem wordRead_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.rcx, .rax], s.gpr r = t.gpr r)
+    (.block wordRead) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rcx, .rax])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+theorem word_rel : RelCT isa WordRelated Impl.Argon2.X86_64.AddressCache.word (fun _ _ => True) := by
+  have trace := wordArgs_rel.mono (P' := WordRelated) (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.layout.bases
+    · exact h.indices) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨wordArgs_ok s h.layout.left.frameRead, wordArgs_ok t h.layout.right.frameRead⟩)
+  have args : RelCT isa WordRelated (.block wordArgs)
+      (fun s t => ∀ r ∈ [Reg.rcx, .rax], s.gpr r = t.gpr r) := full.mono (fun _ _ h => h) (by
+    intro a b h r hr
+    obtain ⟨_, s, t, hp, ⟨sa, ia, _⟩, ⟨sb, ib, _⟩⟩ := h
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl
+    · exact sa.trans (hp.layout.work.trans sb.symm)
+    · exact ia.trans ((congrArg (· &&& 127) hp.indices).trans ib.symm))
+  exact args.seq wordRead_rel
+
+end VG.Proof.Argon2.X86_64.AddressCache