diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillPointers.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillPointers.lean
new file mode 100644
index 000000000..9fdfcf4a3
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillPointers.lean
@@ -0,0 +1,35 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.BlockAddress
+import VerifiedGarbage.Impl.Argon2.X86_64.FillColumn
+
+/-! Prepare the block pointers for one filling operation. `r8` is the matrix
+base; `rbx`, `r12`–`r15` retain the loop position. Reference mapping supplied
+the reference lane and column in `r9` and `rdi`. The current pointer is saved
+in `r10`, with the previous and reference pointers in `rdi` and `rsi`.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillPointers
+
+open VG.X86_64
+
+def saveReference : List Instr := [.mov .rsi (.reg .rdi)]
+
+def currentArgs : List Instr := [.mov .rax (.reg .rbx)]
+
+def previousArgs : List Instr := [
+  .mov .r10 (.reg .rax), .mov .rcx (.reg .rdi), .mov .rax (.reg .rbx)]
+
+def referenceArgs : List Instr := [
+  .mov .r11 (.reg .rax), .mov .rcx (.reg .rsi), .mov .rax (.reg .r9)]
+
+def finishArgs : List Instr := [.mov .rsi (.reg .rax), .mov .rdi (.reg .r11)]
+
+def current : Prog isa := .seq (.block currentArgs) BlockAddress.code
+
+def previous : Prog isa := .seq (.block previousArgs) BlockAddress.code
+
+def reference : Prog isa := .seq (.block referenceArgs) BlockAddress.code
+
+def code : Prog isa := .seq (.block saveReference) (.seq FillColumn.code
+  (.seq current (.seq previous (.seq reference (.block finishArgs)))))
+
+end VG.Impl.Argon2.X86_64.FillPointers
diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillWrite.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillWrite.lean
new file mode 100644
index 000000000..f6d62956d
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillWrite.lean
@@ -0,0 +1,24 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Write the compression result into the current matrix block. `rsi` points
+to the temporary result and `rdi` to the matrix destination; `r9` is the public
+pass number. Pass zero copies the result, and later passes XOR the old cell.
+Both paths visit every word in ascending order.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillWrite
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def word (xorOld : Bool) (i : Nat) : List Instr :=
+  [.mov .rax (.mem (at_ .rsi (8 * i)))] ++
+    (if xorOld then [.alu .xor .rax (.mem (at_ .rdi (8 * i)))] else []) ++
+    [.store (at_ .rdi (8 * i)) .rax]
+
+def words (xorOld : Bool) (n : Nat) : List Instr := (List.range n).flatMap (word xorOld)
+
+def code : Prog isa := .seq (.block [.alu .cmp .r9 (.imm 0)])
+  (.ite .e (.block (words false 128)) (.block (words true 128)))
+
+end VG.Impl.Argon2.X86_64.FillWrite
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointers.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointers.lean
new file mode 100644
index 000000000..346b12d82
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointers.lean
@@ -0,0 +1,99 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointersArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.FillColumn
+import VerifiedGarbage.Proof.Argon2.X86_64.BlockAddress
+
+/-! Compose the matrix addresses while retaining the enclosing loop position. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+def address (base lane column q : Addr) : Addr := (lane * q + column) * 1024 + base
+
+def column (s : State) : Addr := s.gpr .r14 * s.gpr .r13 + s.gpr .r15
+
+def predecessor (s : State) : Addr :=
+  (if column s = 0 then s.gpr .r12 else column s) - 1
+
+def changed : List Reg := [.rax, .rdx, .rcx, .rdi, .rsi, .r10, .r11]
+
+theorem current_ok (s : State) : WP isa current s fun t =>
+    t.gpr .rax = address (s.gpr .r8) (s.gpr .rbx) (s.gpr .rcx) (s.gpr .r12) ∧
+    Divide.Keeps [.rax, .rdx] s t := by
+  unfold current
+  refine WP.seq ((currentArgs_ok s).mono ?_)
+  rintro a ⟨lane, ka⟩
+  refine (BlockAddress.code_ok a).mono ?_
+  rintro t ⟨pointer, kt⟩
+  refine ⟨?_, (ka.mono (by simp)).trans kt⟩
+  rw [pointer, lane, ka.regs .r12 (by decide), ka.regs .rcx (by decide), ka.regs .r8 (by decide), address]
+
+theorem previous_ok (s : State) : WP isa previous s fun t =>
+    t.gpr .r10 = s.gpr .rax ∧
+    t.gpr .rax = address (s.gpr .r8) (s.gpr .rbx) (s.gpr .rdi) (s.gpr .r12) ∧
+    Divide.Keeps [.rax, .rdx, .rcx, .r10] s t := by
+  unfold previous
+  refine WP.seq ((previousArgs_ok s).mono ?_)
+  rintro a ⟨saved, col, lane, ka⟩
+  refine (BlockAddress.code_ok a).mono ?_
+  rintro t ⟨pointer, kt⟩
+  refine ⟨(kt.regs .r10 (by decide)).trans saved, ?_,
+    (ka.mono (by simp)).trans (kt.mono (by simp))⟩
+  rw [pointer, lane, col, ka.regs .r12 (by decide), ka.regs .r8 (by decide), address]
+
+theorem reference_ok (s : State) : WP isa reference s fun t =>
+    t.gpr .r11 = s.gpr .rax ∧
+    t.gpr .rax = address (s.gpr .r8) (s.gpr .r9) (s.gpr .rsi) (s.gpr .r12) ∧
+    Divide.Keeps [.rax, .rdx, .rcx, .r11] s t := by
+  unfold reference
+  refine WP.seq ((referenceArgs_ok s).mono ?_)
+  rintro a ⟨saved, col, lane, ka⟩
+  refine (BlockAddress.code_ok a).mono ?_
+  rintro t ⟨pointer, kt⟩
+  refine ⟨(kt.regs .r11 (by decide)).trans saved, ?_,
+    (ka.mono (by simp)).trans (kt.mono (by simp))⟩
+  rw [pointer, lane, col, ka.regs .r12 (by decide), ka.regs .r8 (by decide), address]
+
+theorem code_ok (s : State) : WP isa code s fun t =>
+    t.gpr .r10 = address (s.gpr .r8) (s.gpr .rbx) (column s) (s.gpr .r12) ∧
+    t.gpr .rdi = address (s.gpr .r8) (s.gpr .rbx) (predecessor s) (s.gpr .r12) ∧
+    t.gpr .rsi = address (s.gpr .r8) (s.gpr .r9) (s.gpr .rdi) (s.gpr .r12) ∧
+    Divide.Keeps changed s t := by
+  unfold code
+  refine WP.seq ((saveReference_ok s).mono ?_)
+  rintro a ⟨refColumn, ka⟩
+  refine WP.seq ((FillColumn.code_ok a).mono ?_)
+  rintro b ⟨curColumn, prevColumn, kb⟩
+  refine WP.seq ((current_ok b).mono ?_)
+  rintro c ⟨curPointer, kc⟩
+  refine WP.seq ((previous_ok c).mono ?_)
+  rintro d ⟨savedCurrent, prevPointer, kd⟩
+  refine WP.seq ((reference_ok d).mono ?_)
+  rintro e ⟨savedPrevious, refPointer, ke⟩
+  refine (finishArgs_ok e).mono ?_
+  rintro t ⟨referenceResult, previousResult, kt⟩
+  have coords : column a = column s := by
+    unfold column
+    rw [ka.regs .r14 (by decide), ka.regs .r13 (by decide), ka.regs .r15 (by decide)]
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · rw [kt.regs .r10 (by decide), ke.regs .r10 (by decide), savedCurrent, curPointer,
+      kb.regs .r8 (by decide), ka.regs .r8 (by decide), kb.regs .rbx (by decide),
+      ka.regs .rbx (by decide), kb.regs .r12 (by decide), ka.regs .r12 (by decide), curColumn]
+    exact congrArg (fun col => address (s.gpr .r8) (s.gpr .rbx) col (s.gpr .r12)) coords
+  · rw [previousResult, savedPrevious, prevPointer, kc.regs .r8 (by decide),
+      kc.regs .rbx (by decide), kc.regs .rdi (by decide), kc.regs .r12 (by decide),
+      kb.regs .r8 (by decide), ka.regs .r8 (by decide), kb.regs .rbx (by decide),
+      ka.regs .rbx (by decide), kb.regs .r12 (by decide), ka.regs .r12 (by decide), prevColumn]
+    change address _ _ ((if column a = 0 then a.gpr .r12 else column a) - 1) _ = _
+    rw [coords, ka.regs .r12 (by decide), predecessor]
+  · rw [referenceResult, refPointer, kd.regs .r8 (by decide), kd.regs .r9 (by decide),
+      kd.regs .rsi (by decide), kd.regs .r12 (by decide), kc.regs .r8 (by decide),
+      kc.regs .r9 (by decide), kc.regs .rsi (by decide), kc.regs .r12 (by decide),
+      kb.regs .r8 (by decide), kb.regs .r9 (by decide), kb.regs .rsi (by decide),
+      kb.regs .r12 (by decide), ka.regs .r8 (by decide), ka.regs .r9 (by decide),
+      ka.regs .r12 (by decide), refColumn]
+  · exact (((((ka.mono (by simp [changed])).trans (kb.mono (by simp [changed]))).trans
+      (kc.mono (by simp [changed]))).trans (kd.mono (by simp [changed]))).trans
+      (ke.mono (by simp [changed]))).trans (kt.mono (by simp [changed]))
+
+end VG.Proof.Argon2.X86_64.FillPointers
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersArgs.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersArgs.lean
new file mode 100644
index 000000000..f55ec4160
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersArgs.lean
@@ -0,0 +1,76 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillPointers
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! Short register-setup steps for the filling pointers. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+theorem saveReference_ok (s : State) : WP isa (.block saveReference) s fun t =>
+    t.gpr .rsi = s.gpr .rdi ∧ Divide.Keeps [.rsi] s t := by
+  apply WP.of_runBlock
+  simp only [saveReference, 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 r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    exact ite_eq_right hr
+  all_goals rfl
+
+theorem currentArgs_ok (s : State) : WP isa (.block currentArgs) s fun t =>
+    t.gpr .rax = s.gpr .rbx ∧ Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [currentArgs, 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 r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    exact ite_eq_right hr
+  all_goals rfl
+
+theorem previousArgs_ok (s : State) : WP isa (.block previousArgs) s fun t =>
+    t.gpr .r10 = s.gpr .rax ∧ t.gpr .rcx = s.gpr .rdi ∧ t.gpr .rax = s.gpr .rbx ∧
+    Divide.Keeps [.r10, .rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [previousArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg,
+    reduceCtorEq, ite_true, ite_false]
+  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 referenceArgs_ok (s : State) : WP isa (.block referenceArgs) s fun t =>
+    t.gpr .r11 = s.gpr .rax ∧ t.gpr .rcx = s.gpr .rsi ∧ t.gpr .rax = s.gpr .r9 ∧
+    Divide.Keeps [.r11, .rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [referenceArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg,
+    reduceCtorEq, ite_true, ite_false]
+  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 finishArgs_ok (s : State) : WP isa (.block finishArgs) s fun t =>
+    t.gpr .rsi = s.gpr .rax ∧ t.gpr .rdi = s.gpr .r11 ∧
+    Divide.Keeps [.rsi, .rdi] s t := by
+  apply WP.of_runBlock
+  simp only [finishArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg,
+    reduceCtorEq, ite_true, ite_false]
+  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
+
+end VG.Proof.Argon2.X86_64.FillPointers
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersCT.lean
new file mode 100644
index 000000000..b531c5cc2
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersCT.lean
@@ -0,0 +1,17 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointersLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! The pointer setup only branches on the public current column.
+Reference coordinates may differ without changing its execution trace. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+theorem code_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.r8, .rbx, .r12, .r13, .r14, .r15], s.gpr r = t.gpr r) code
+    (fun s t => ∀ r ∈ [Reg.r10], s.gpr r = t.gpr r) :=
+  RelCT.taintRegs (τ := Taint.ofRegs [.r8, .rbx, .r12, .r13, .r14, .r15])
+    (fun _ _ h => Taint.agree_ofRegs h) [Reg.r10] (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.FillPointers
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersLit.lean
new file mode 100644
index 000000000..6b85e3f1f
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FillPointers
+
+/-! Checked literal of the complete filling pointer setup. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FillPointers.code
+
+end VG
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWrite.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWrite.lean
new file mode 100644
index 000000000..ba86b63da
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWrite.lean
@@ -0,0 +1,52 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillWritePrefix
+import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidates
+
+/-! Whole-block first-pass copying and later-pass XOR, with a frame proof. -/
+
+namespace VG.Proof.Argon2.X86_64.FillWrite
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillWrite
+
+theorem code_ok (s : State)
+    (hs : (⟨s.gpr .rsi, 1024⟩ : Region) ∈ s.rd ++ s.wr)
+    (hw : (⟨s.gpr .rdi, 1024⟩ : Region) ∈ s.wr)
+    (hd : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩) :
+    WP isa code s fun t =>
+      blockAt t.mem (s.gpr .rdi) =
+        (if s.gpr .r9 = 0 then blockAt s.mem (s.gpr .rsi)
+          else xorBlock (blockAt s.mem (s.gpr .rsi)) (blockAt s.mem (s.gpr .rdi))) ∧
+      Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by
+  unfold code
+  refine WP.seq ((CountCandidates.compare_ok s).mono ?_)
+  rintro a ⟨flag, ka⟩
+  have src : a.gpr .rsi = s.gpr .rsi := ka.regs .rsi (by simp)
+  have dest : a.gpr .rdi = s.gpr .rdi := ka.regs .rdi (by simp)
+  have hs' : (⟨a.gpr .rsi, 1024⟩ : Region) ∈ a.rd ++ a.wr := by
+    rw [src, ka.rd, ka.wr]; exact hs
+  have hw' : (⟨a.gpr .rdi, 1024⟩ : Region) ∈ a.wr := by
+    rw [dest, ka.wr]; exact hw
+  have hd' : (⟨a.gpr .rsi, 1024⟩ : Region).Disjoint ⟨a.gpr .rdi, 1024⟩ := by
+    rw [src, dest]; exact hd
+  refine WP.ite (decide (s.gpr .r9 = 0)) (by simp only [eval, flag]) ?_ ?_
+  · intro h
+    have zero := of_decide_eq_true h
+    refine (prefix_ok false 128 (by decide) a hs' hw' hd').mono ?_
+    rintro t ⟨written, frame, keeps, mx⟩
+    refine ⟨?_, ?_, ?_, mx.trans ka.mxcsr⟩
+    · rw [dest] at written
+      rw [ite_eq_left zero, written_block written]
+      simp only [result, Bool.false_eq_true, ite_false, ka.mem, src]
+    · rw [dest, ka.mem] at frame; exact frame
+    · exact (show CopyKeeps s a from ⟨fun r _ => ka.regs r (by simp), ka.rd, ka.wr⟩).trans keeps
+  · intro h
+    have nonzero := of_decide_eq_false h
+    refine (prefix_ok true 128 (by decide) a hs' hw' hd').mono ?_
+    rintro t ⟨written, frame, keeps, mx⟩
+    refine ⟨?_, ?_, ?_, mx.trans ka.mxcsr⟩
+    · rw [dest] at written
+      rw [ite_eq_right nonzero, written_block written]
+      simp only [result, ite_true, ka.mem, src]
+    · rw [dest, ka.mem] at frame; exact frame
+    · exact (show CopyKeeps s a from ⟨fun r _ => ka.regs r (by simp), ka.rd, ka.wr⟩).trans keeps
+
+end VG.Proof.Argon2.X86_64.FillWrite
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCT.lean
new file mode 100644
index 000000000..0f85f3962
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCT.lean
@@ -0,0 +1,16 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillWriteLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Both write paths have a public, fixed sequence of memory accesses. -/
+
+namespace VG.Proof.Argon2.X86_64.FillWrite
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillWrite
+
+theorem code_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.r9, .rdi, .rsi], s.gpr r = t.gpr r) code
+    (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.r9, .rdi, .rsi])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.FillWrite
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteLit.lean
new file mode 100644
index 000000000..d869cc860
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteLit.lean
@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FillWrite
+
+/-! Checked literal of the complete copy/XOR block write. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FillWrite.code
+
+end VG
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWritePrefix.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWritePrefix.lean
new file mode 100644
index 000000000..71ba91432
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWritePrefix.lean
@@ -0,0 +1,90 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillWriteWord
+import VerifiedGarbage.Proof.Argon2.X86_64.Finish
+
+/-! Compose the word writes without re-executing a long load/store block. -/
+
+namespace VG.Proof.Argon2.X86_64.FillWrite
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillWrite
+
+def result (xorOld : Bool) (m : Mem) (src dest : Addr) : Block :=
+  if xorOld then xorBlock (blockAt m src) (blockAt m dest) else blockAt m src
+
+theorem result_get (xorOld : Bool) (m : Mem) (src dest : Addr) (i : Fin 128) :
+    (result xorOld m src dest)[i] = value xorOld m src dest i.val := by
+  cases xorOld <;> simp only [result, value, Bool.false_eq_true, ite_false, ite_true,
+    xorBlock_get, blockAt_get]
+
+theorem frame_extend {m m' : Mem} {dest : Addr} {n k : Nat}
+    (hf : Frame [⟨dest, 8 * n⟩] m m') (h : n ≤ k) : Frame [⟨dest, 8 * k⟩] m m' := by
+  apply hf.sub
+  intro r hr
+  simp only [List.mem_singleton] at hr
+  subst r
+  exact ⟨_, by simp, Region.sub_prefix (Nat.mul_le_mul_left 8 h)⟩
+
+theorem source_read {m m' : Mem} {src dest : Addr} {n : Nat}
+    (hf : Frame [⟨dest, 8 * n⟩] m m') (hn : n ≤ 128)
+    (hd : (⟨src, 1024⟩ : Region).Disjoint ⟨dest, 1024⟩) (i : Fin 128) :
+    m'.readW (off src (8 * i.val)) 64 = m.readW (off src (8 * i.val)) 64 := by
+  have full := frame_extend hf hn
+  exact full.readW (r := ⟨src, 1024⟩)
+    (Offset.contains_base src (by omega) (by omega))
+    (by intro r hr; simp only [List.mem_singleton] at hr; subst r; exact hd) (by decide)
+
+theorem old_read {m m' : Mem} {dest : Addr} {n : Nat}
+    (hf : Frame [⟨dest, 8 * n⟩] m m') (hn : n < 128) :
+    m'.readW (off dest (8 * n)) 64 = m.readW (off dest (8 * n)) 64 :=
+  hf.readW (r := ⟨off dest (8 * n), 8⟩) (Region.contains_self _ _)
+    (by
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      exact Offset.disjoint_base dest (Nat.le_refl _) (by omega)) (by decide)
+
+theorem prefix_ok (xorOld : Bool) (n : Nat) (hn : n ≤ 128) (s : State)
+    (hs : (⟨s.gpr .rsi, 1024⟩ : Region) ∈ s.rd ++ s.wr)
+    (hw : (⟨s.gpr .rdi, 1024⟩ : Region) ∈ s.wr)
+    (hd : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩) :
+    WP isa (.block (words xorOld n)) s fun t =>
+      Written t.mem (s.gpr .rdi) (result xorOld s.mem (s.gpr .rsi) (s.gpr .rdi)) n ∧
+      Frame [⟨s.gpr .rdi, 8 * n⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by
+  induction n with
+  | zero => exact WP.block_nil ⟨fun i hi => by omega, Frame.refl _ _, CopyKeeps.refl s, rfl⟩
+  | succ n ih =>
+    simp only [words, List.range_succ, List.flatMap_append, List.flatMap_cons,
+      List.flatMap_nil, List.append_nil]
+    apply WP.block_append
+    refine (ih (by omega)).mono ?_
+    rintro t ⟨written, frame, keeps, mx⟩
+    have hn' : n < 128 := by omega
+    have src : t.gpr .rsi = s.gpr .rsi := keeps.1 .rsi (by decide)
+    have dest : t.gpr .rdi = s.gpr .rdi := keeps.1 .rdi (by decide)
+    have write : InRegions t.wr (off (t.gpr .rdi) (8 * n)) 8 := by
+      rw [dest, keeps.2.2]
+      exact ⟨_, hw, Offset.contains_base _ (by omega) (by omega)⟩
+    have read : InRegions (t.rd ++ t.wr) (off (t.gpr .rsi) (8 * n)) 8 := by
+      rw [src, keeps.2.1, keeps.2.2]
+      exact ⟨_, hs, Offset.contains_base _ (by omega) (by omega)⟩
+    have old : InRegions (t.rd ++ t.wr) (off (t.gpr .rdi) (8 * n)) 8 := by
+      obtain ⟨r, hr, hc⟩ := write
+      exact ⟨r, List.mem_append_right _ hr, hc⟩
+    refine (word_ok xorOld t n read write old).mono ?_
+    rintro u ⟨mem, regs, rd, wr, mx'⟩
+    have v : value xorOld t.mem (t.gpr .rsi) (t.gpr .rdi) n =
+        (result xorOld s.mem (s.gpr .rsi) (s.gpr .rdi))[(⟨n, hn'⟩ : Fin 128)] := by
+      rw [result_get, src, dest]
+      unfold value
+      rw [source_read frame (by omega) hd ⟨n, hn'⟩]
+      cases xorOld
+      · rfl
+      · rw [old_read frame hn']
+    refine ⟨?_, ?_, keeps.trans ⟨regs, rd, wr⟩, mx'.trans mx⟩
+    · rw [mem, v, dest]
+      exact written_step hn' written
+    · rw [mem, dest]
+      exact (frame_extend frame (Nat.le_succ n)).writeW
+        (r := ⟨s.gpr .rdi, 8 * (n + 1)⟩) (by simp) _
+        (Offset.contains_base _ (by omega) (by omega))
+
+end VG.Proof.Argon2.X86_64.FillWrite
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteWord.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteWord.lean
new file mode 100644
index 000000000..ce2f39452
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteWord.lean
@@ -0,0 +1,40 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillWrite
+import VerifiedGarbage.Proof.Argon2.X86_64.Memory
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! One output word, keeping register writes folded during execution. -/
+
+namespace VG.Proof.Argon2.X86_64.FillWrite
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillWrite
+
+def value (xorOld : Bool) (m : Mem) (src dest : Addr) (i : Nat) : Addr :=
+  let next := m.readW (off src (8 * i)) 64
+  if xorOld then next ^^^ m.readW (off dest (8 * i)) 64 else next
+
+/-- The source is readable and the destination writable; its old contents
+are read only on later passes. -/
+theorem word_ok (xorOld : Bool) (s : State) (i : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rsi) (8 * i)) 8)
+    (hw : InRegions s.wr (off (s.gpr .rdi) (8 * i)) 8)
+    (ho : InRegions (s.rd ++ s.wr) (off (s.gpr .rdi) (8 * i)) 8) :
+    WP isa (.block (Impl.Argon2.X86_64.FillWrite.word xorOld i)) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rdi) (8 * i))
+        (value xorOld s.mem (s.gpr .rsi) (s.gpr .rdi) i) ∧
+      (∀ r, r ≠ .rax → t.gpr r = s.gpr r) ∧
+      t.rd = s.rd ∧ t.wr = s.wr ∧ t.mxcsr = s.mxcsr := by
+  cases xorOld <;> apply WP.of_runBlock <;>
+    simp only [Impl.Argon2.X86_64.FillWrite.word, value, Bool.false_eq_true, ite_false, ite_true,
+      List.cons_append, List.nil_append,
+      runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+      State.load64, State.store64, execAlu, ea_at, hr, hw, ho,
+      RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg,
+      RegUpd.gpr_arithFlags, RegUpd.mem_arithFlags, RegUpd.rd_arithFlags,
+      RegUpd.wr_arithFlags, reduceCtorEq, ite_true, ite_false,
+      Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  all_goals
+    refine ⟨trivial, ?_, trivial, trivial, rfl⟩
+    intro r hr
+    simp only [hr, ite_false]
+
+end VG.Proof.Argon2.X86_64.FillWrite