From fcd58dc1105706ea209a5c0290a6aa5bcf81e708 Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 19:21:53 +0000
Subject: [PATCH] Prove Argon2 address cache retains filling state and matrix

---
 .../Argon2/X86_64/AddressCacheInvariant.lean  | 87 +++++++++++++++++++
 .../Argon2/X86_64/AddressCacheMatrix.lean     | 59 +++++++++++++
 .../Argon2/X86_64/AddressCacheState.lean      | 53 +++++++++++
 3 files changed, 199 insertions(+)
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheInvariant.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMatrix.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheState.lean

diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheInvariant.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheInvariant.lean
new file mode 100644
index 0000000000..19fdec209c
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheInvariant.lean
@@ -0,0 +1,87 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheState
+
+/-! Cache validity does not depend on the current index, so advancing an index
+retains it. Counter zero requires no cached contents; every other counter
+identifies its specified independent-address block.
+-/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+structure Invariant (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
+  bound : old < 2 ^ 64
+  cached : old = 0 ∨ blockAt s.mem (off (AddressCalls.work s) 6144) = addressBlock p pass lane slice old
+
+theorem wanted_bound (s : State) : wanted s < 2 ^ 64 := by
+  unfold wanted
+  have := (s.gpr .r15).isLt
+  omega
+
+theorem Invariant.ready {p : Params} {pass lane slice old : Nat} {s : State}
+    (h : Invariant p pass lane slice old s) : Ready p pass lane slice old s := by
+  refine ⟨h.layout, h.reads, h.write, h.words, ?_⟩
+  intro same
+  have word : BitVec.ofNat 64 (wanted s) = BitVec.ofNat 64 old := by
+    unfold wanted
+    rw [← counter_nat]; exact same.trans h.words.counterWord
+  have equal := (ReferenceMap.word_eq _ _ (wanted_bound s) h.bound).mp word
+  rcases h.cached with zero | cached
+  · exfalso
+    exact counter_ne_zero _ (same.trans (h.words.counterWord.trans (by rw [zero]; rfl)))
+  · rw [← equal] at cached
+    exact cached
+
+theorem Selected.invariant {s t : State} {p : Params} {pass lane slice old : Nat}
+    (ready : Ready p pass lane slice old s) (h : Selected s t p pass lane slice) :
+    Invariant p pass lane slice (wanted s) t := by
+  have bp := h.regs .rbp (by simp [calleeSaved])
+  refine ⟨h.layout, ?_, ?_, h.words ready, wanted_bound s, Or.inr ?_⟩
+  · rw [h.rd, h.wr, bp]; exact ready.reads
+  · rw [h.wr, bp]; exact ready.write
+  · rw [h.work_eq]; exact h.block
+
+theorem Invariant.zero {p : Params} {pass lane slice : Nat} {s : State}
+    (h : Ready p pass lane slice 0 s) : Invariant p pass lane slice 0 s :=
+  ⟨h.layout, h.reads, h.write, h.words, by decide, Or.inl rfl⟩
+
+theorem Invariant.of_state {p : Params} {pass lane slice old : Nat} {s t : State}
+    (h : Invariant p pass lane slice old s)
+    (regs : ∀ r ∈ [Reg.rsp, .rbp, .rbx, .r14], t.gpr r = s.gpr r)
+    (mem : t.mem = s.mem) (rd : t.rd = s.rd) (wr : t.wr = s.wr) :
+    Invariant p pass lane slice old t := by
+  have bp := regs .rbp (by simp)
+  have sp := regs .rsp (by simp)
+  have work : AddressCalls.work t = AddressCalls.work s := by
+    unfold AddressCalls.work; rw [mem, bp]
+  refine ⟨?_, ?_, ?_, ?_, h.bound, ?_⟩
+  · constructor
+    · rw [rd, wr, bp]; exact h.layout.frameRead
+    · rw [wr, work]; exact h.layout.workWrite
+    · rw [bp, work]; exact h.layout.frameWork
+    · rw [bp, sp]; exact h.layout.frameStack
+    · rw [sp, work]; exact h.layout.stackWork
+  · rw [rd, wr, bp]; exact h.reads
+  · rw [wr, bp]; exact h.write
+  · exact ⟨by rw [mem, bp]; exact h.words.passWord,
+      (regs .rbx (by simp)).trans h.words.laneWord,
+      (regs .r14 (by simp)).trans h.words.sliceWord,
+      by rw [mem, bp]; exact h.words.blocksWord,
+      by rw [mem, bp]; exact h.words.passesWord,
+      by rw [mem, bp]; exact h.words.variantWord,
+      by rw [mem, bp]; exact h.words.counterWord⟩
+  · rw [mem, work]; exact h.cached
+
+theorem Invariant.of_keeps {p : Params} {pass lane slice old : Nat} {s t : State}
+    (h : Invariant p pass lane slice old s) (k : Divide.Keeps ReferenceMap.changed s t) :
+    Invariant p pass lane slice old t := by
+  apply h.of_state _ k.mem k.rd k.wr
+  intro r hr
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl <;> exact k.regs _ (by decide)
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMatrix.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMatrix.lean
new file mode 100644
index 0000000000..bb635e73eb
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMatrix.lean
@@ -0,0 +1,59 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheState
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelInvariant
+import VerifiedGarbage.Proof.Argon2.Matrix
+
+/-! Independent-address generation leaves every matrix cell intact. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+theorem Selected.filling_ready {s t : State} {p : Params} {pass lane slice index : Nat}
+    (cacheLayout : AddressCalls.Ready s) (h : FillKernel.Ready p pass lane slice index s)
+    (done : Selected s t p pass lane slice) : FillKernel.Ready p pass lane slice index t := by
+  have bp := done.regs .rbp (by simp [calleeSaved])
+  have sp := done.regs .rsp (by simp [calleeSaved])
+  have matrix' : FillKernel.matrix t = FillKernel.matrix s := done.frame_word cacheLayout 232 (by decide) (by decide)
+  have work' : FillKernel.work t = FillKernel.work s := done.frame_word cacheLayout 248 (by decide) (by decide)
+  refine ⟨?_, h.bounds, ?_, (done.frame_word cacheLayout 0 (by decide) (by decide)).trans h.passWord,
+    (done.frame_word cacheLayout 184 (by decide) (by decide)).trans h.lanesWord⟩
+  · constructor
+    · rw [done.rd, done.wr, bp]; exact h.layout.frameRead
+    · rw [done.wr, bp]; exact h.layout.frameWrite
+    · rw [matrix', done.wr]; exact h.layout.matrixWrite
+    · rw [work', done.wr]; exact h.layout.workWrite
+    · rw [matrix', work']; exact h.layout.matrixWork
+    · rw [matrix', bp]; exact h.layout.matrixFrame
+    · rw [matrix', sp]; exact h.layout.matrixStack
+    · rw [bp, work']; exact h.layout.frameWork
+    · rw [bp, sp]; exact h.layout.frameStack
+    · rw [sp, work']; exact h.layout.stackWork
+  · exact ⟨(done.regs .rbx (by simp [calleeSaved])).trans h.position.current,
+      (done.regs .r12 (by simp [calleeSaved])).trans h.position.laneLength,
+      (done.regs .r13 (by simp [calleeSaved])).trans h.position.segmentLength,
+      (done.regs .r14 (by simp [calleeSaved])).trans h.position.slice,
+      (done.regs .r15 (by simp [calleeSaved])).trans h.position.index⟩
+
+theorem Selected.represents {s t : State} {p : Params} {pass lane slice index : Nat}
+    (cacheLayout : AddressCalls.Ready s) (h : FillKernel.Ready p pass lane slice index s)
+    (matrixWork : (⟨FillKernel.matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨AddressCalls.work s, 8192⟩)
+    (done : Selected s t p pass lane slice) (blocks : Array Block)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks blocks) :
+    Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks blocks := by
+  have base : FillKernel.matrix t = FillKernel.matrix s := done.frame_word cacheLayout 232 (by decide) (by decide)
+  rw [base]
+  refine ⟨represented.size, ?_⟩
+  intro k hk
+  have kept : blockAt t.mem (Proof.Argon2.matrixCell (FillKernel.matrix s) k) =
+      blockAt s.mem (Proof.Argon2.matrixCell (FillKernel.matrix s) k) := by
+    apply FillCompress.block_frame done.frame
+    intro r hr
+    simp only [writes, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl
+    · exact matrixWork.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hk)
+    · exact h.layout.matrixStack.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hk)
+    · exact (h.layout.matrixFrame.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hk)).sub_right
+        (Offset.sub_base _ (by decide))
+  exact kept.trans (represented.block k hk)
+
+end VG.Proof.Argon2.X86_64.AddressCache
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheState.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheState.lean
new file mode 100644
index 0000000000..fbed7f0c3a
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheState.lean
@@ -0,0 +1,53 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCache
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelStable
+
+/-! Retain the filling header and allocation across independent-address regeneration. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+theorem Selected.frame_word {s t : State} {p : Params} {pass lane slice : Nat}
+    (layout : AddressCalls.Ready s) (h : Selected s t p pass lane slice)
+    (d : Nat) (bound : d + 8 ≤ 272) (separate : d + 8 ≤ 8 ∨ 16 ≤ d) :
+    t.mem.readW (off (t.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 := by
+  rw [h.regs .rbp (by simp [calleeSaved])]
+  have sub : Region.Sub ⟨off (s.gpr .rbp) d, 8⟩ ⟨s.gpr .rbp, 272⟩ := Offset.sub_base _ bound
+  exact h.frame.readW (r := ⟨off (s.gpr .rbp) d, 8⟩) (Region.contains_self _ _) (by
+    intro r hr
+    simp only [writes, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl
+    · exact layout.frameWork.sub_left sub
+    · exact layout.frameStack.sub_left sub
+    · exact Offset.disjoint _ separate (by omega) (by decide)) (by decide)
+
+theorem Selected.words {s t : State} {p : Params} {pass lane slice old : Nat}
+    (ready : Ready p pass lane slice old s) (h : Selected s t p pass lane slice) :
+    AddressHeader.Words p pass lane slice (wanted s) t := by
+  exact ⟨(h.frame_word ready.layout 0 (by decide) (by decide)).trans ready.words.passWord,
+    (h.regs .rbx (by simp [calleeSaved])).trans ready.words.laneWord,
+    (h.regs .r14 (by simp [calleeSaved])).trans ready.words.sliceWord,
+    (h.frame_word ready.layout 240 (by decide) (by decide)).trans ready.words.blocksWord,
+    (h.frame_word ready.layout 72 (by decide) (by decide)).trans ready.words.passesWord,
+    (h.frame_word ready.layout 112 (by decide) (by decide)).trans ready.words.variantWord,
+    h.counterWord.trans (counter_nat _)⟩
+
+theorem Ready.of_keeps {p : Params} {pass lane slice old : Nat} {s t : State}
+    (h : Ready p pass lane slice old s) (k : Divide.Keeps ReferenceMap.changed s t) :
+    Ready p pass lane slice old t := by
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r := by
+    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
+  have stable := AddressCalls.stable_of_frame h.layout regs k.rd k.wr
+    (by rw [k.mem]; exact Frame.refl _ _) k.mxcsr
+  refine ⟨stable.ready, stable.reads h.reads, ?_, stable.words h.layout h.words, ?_⟩
+  · rw [k.wr, k.regs .rbp (by decide)]; exact h.write
+  · intro same
+    have wanted' : wanted t = wanted s := by unfold wanted; rw [k.regs .r15 (by decide)]
+    rw [k.mem, k.regs .rbp (by decide), k.regs .r15 (by decide)] at same
+    rw [k.mem, stable.work_eq, wanted']
+    exact h.cached same
+
+end VG.Proof.Argon2.X86_64.AddressCache