diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillKernel.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillKernel.lean
new file mode 100644
index 000000000..958ad44d8
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillKernel.lean
@@ -0,0 +1,27 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceMap
+import VerifiedGarbage.Impl.Argon2.X86_64.FillPointers
+import VerifiedGarbage.Impl.Argon2.X86_64.FillCompress
+
+/-! Map the random word, prepare matrix pointers, and update one active cell.
+The enclosing loops provide the position in callee-saved registers and the
+frame; `rdi` contains either the cached independent word or the previous cell's
+first word. The lane count and matrix base are reloaded after volatile calls.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillKernel
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def lanes : List Instr := [.mov .rsi (.mem (at_ .rbp 184))]
+def matrix : List Instr := [.mov .r8 (.mem (at_ .rbp 232))]
+
+def mapping : Prog isa := .seq (.block lanes) ReferenceMap.code
+
+def pointers : Prog isa := .seq (.block matrix) FillPointers.code
+
+def prepare : Prog isa := .seq mapping pointers
+
+def code : Prog isa := .seq prepare FillCompress.code
+
+end VG.Impl.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean
index e1e0f5a5b..a146c8fae 100644
--- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillColumn.lean
@@ -119,6 +119,28 @@ theorem previous_nat (column q : Nat) (positive : 0 < q) (bound : column < q) :
     rw [Nat.mod_eq_sub_mod (by omega : q ≤ column + q - 1), sub,
       Nat.mod_eq_of_lt (by omega : column - 1 < q)]
 
+theorem previous_word_nat (column q : Nat) (positive : 0 < q) (qBound : q < 2 ^ 64)
+    (bound : column < q) :
+    (if BitVec.ofNat 64 column = 0#64 then BitVec.ofNat 64 q else BitVec.ofNat 64 column) - 1 =
+      BitVec.ofNat 64 ((column + q - 1) % q) := by
+  have zero : BitVec.ofNat 64 column = 0#64 ↔
+      column = 0 := by
+    constructor
+    · intro h
+      have hn := congrArg BitVec.toNat h
+      rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (Nat.lt_trans bound qBound)] at hn
+      exact hn
+    · intro h; rw [h]
+  simp only [zero]
+  by_cases h : column = 0
+  · simp only [h, ite_true]
+    rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl,
+      Offset.ofNat_sub_ofNat positive, Nat.zero_add, Nat.mod_eq_of_lt (by omega : q - 1 < q)]
+  · simp only [h, ite_false]
+    rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl,
+      Offset.ofNat_sub_ofNat (by omega : 1 ≤ column),
+      ← previous_nat _ q positive bound, ite_eq_right h]
+
 theorem code_nat_ok (s : State) (slice segment index q : Nat)
     (hs : s.gpr .r14 = BitVec.ofNat 64 slice)
     (hg : s.gpr .r13 = BitVec.ofNat 64 segment)
@@ -136,25 +158,7 @@ theorem code_nat_ok (s : State) (slice segment index q : Nat)
       BitVec.ofNat 64 (slice * segment + index) := by
     rw [hs, hg, hi, ← BitVec.ofNat_mul, ← BitVec.ofNat_add]
   refine ⟨column.trans word, ?_, keeps⟩
-  have zero : BitVec.ofNat 64 (slice * segment + index) = 0#64 ↔
-      slice * segment + index = 0 := by
-    constructor
-    · intro h
-      have hn := congrArg BitVec.toNat h
-      rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (Nat.lt_trans bound qBound)] at hn
-      exact hn
-    · intro h; rw [h]
   rw [previous, word, hq]
-  change (if BitVec.ofNat 64 (slice * segment + index) = 0#64 then
-    BitVec.ofNat 64 q else BitVec.ofNat 64 (slice * segment + index)) - 1 = _
-  simp only [zero]
-  by_cases h : slice * segment + index = 0
-  · simp only [h, ite_true]
-    rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl,
-      Offset.ofNat_sub_ofNat positive, Nat.zero_add, Nat.mod_eq_of_lt (by omega : q - 1 < q)]
-  · simp only [h, ite_false]
-    rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl,
-      Offset.ofNat_sub_ofNat (by omega : 1 ≤ slice * segment + index),
-      ← previous_nat _ q positive bound, ite_eq_right h]
+  exact previous_word_nat _ q positive qBound bound
 
 end VG.Proof.Argon2.X86_64.FillColumn
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernel.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernel.lean
new file mode 100644
index 000000000..8f271cd07
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernel.lean
@@ -0,0 +1,67 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelPrepare
+
+/-! Complete active-cell update from a random word and the matrix allocation. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+def writes (s : State) (p : Params) (lane slice index : Nat) : List Region :=
+  [⟨current s p lane slice index, 1024⟩, ⟨work s, 5120⟩,
+    below (s.gpr .rsp) 8, ⟨off (s.gpr .rbp) 16, 8⟩]
+
+structure Done (s t : State) (p : Params) (pass lane slice index : Nat) : Prop where
+  block : blockAt t.mem (current s p lane slice index) =
+    let next := Spec.Argon2.compress (blockAt s.mem (previous s p lane slice index))
+      (blockAt s.mem (referenced s p pass lane slice index))
+    if pass = 0 then next else xorBlock next (blockAt s.mem (current s p lane slice index))
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (writes s p lane slice index) s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+
+theorem code_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : Ready p pass lane slice index s) :
+    WP isa Impl.Argon2.X86_64.FillKernel.code s (Done s · p pass lane slice index) := by
+  unfold Impl.Argon2.X86_64.FillKernel.code
+  refine WP.seq ((prepare_ok s p pass lane slice index h).mono ?_)
+  intro b prepared
+  have keeps := prepared.keeps
+  have cur := prepared.currentPtr
+  have prev := prepared.previousPtr
+  have other := prepared.referencePtr
+  refine (FillCompress.code_mx_ok b prepared.ready).mono ?_
+  rintro t ⟨done, mx⟩
+  have counter : FillCompress.pass b = BitVec.ofNat 64 pass := by
+    unfold FillCompress.pass
+    rw [keeps.mem, keeps.regs .rbp (by decide)]
+    exact h.passWord
+  refine ⟨?_, ?_, done.rd.trans keeps.rd, done.wr.trans keeps.wr, ?_, mx.trans keeps.mxcsr⟩
+  · have block := done.block
+    rw [cur, prev, other, keeps.mem, counter] at block
+    simp only [ReferenceMap.word_zero pass (Nat.lt_trans h.bounds.passBound (by decide))] at block
+    exact block
+  · intro r hr
+    have ne : r ∉ ReferenceMap.changed := 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 (done.regs r hr).trans (keeps.regs r ne)
+  · have workB : FillCompress.work b = work s := by
+      unfold FillCompress.work work
+      rw [keeps.regs .rbp (by decide), keeps.mem]
+    have frame := done.frame
+    rw [FillCompress.writes, workB, cur, keeps.regs .rsp (by decide), keeps.regs .rbp (by decide), keeps.mem] at frame
+    change Frame [⟨current s p lane slice index, 1024⟩, ⟨work s + 4096, 1024⟩,
+      ⟨work s, 4096⟩, below (s.gpr .rsp) 8, ⟨off (s.gpr .rbp) 16, 8⟩] s.mem t.mem at frame
+    apply frame.sub
+    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 ⟨_, by simp [writes], fun _ h => h⟩
+    · exact ⟨⟨work s, 5120⟩, by simp [writes], Offset.sub_base _ (by decide)⟩
+    · exact ⟨⟨work s, 5120⟩, by simp [writes], Region.sub_prefix (by decide)⟩
+    · exact ⟨_, by simp [writes], fun _ h => h⟩
+    · exact ⟨_, by simp [writes], fun _ h => h⟩
+
+end VG.Proof.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelArgs.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelArgs.lean
new file mode 100644
index 000000000..b2afb6895
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelArgs.lean
@@ -0,0 +1,80 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelLayout
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMap
+
+/-! Reload frame arguments and compose reference mapping with matrix addresses. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+theorem load_ok (s : State) (r : Reg) (d : Nat)
+    (read : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8) :
+    WP isa (.block [.mov r (.mem (Impl.Argon2.X86_64.at_ .rbp d))]) s fun t =>
+      t.gpr r = s.mem.readW (off (s.gpr .rbp) d) 64 ∧ Divide.Keeps [r] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, State.load64,
+    ea_at, read, Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg, ite_true]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro q hq
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hq
+    exact ite_eq_right hq
+  all_goals rfl
+
+structure Ready (p : Params) (pass lane slice index : Nat) (s : State) : Prop where
+  layout : Layout p s
+  bounds : ReferenceMap.Bounds p pass lane slice index
+  position : ReferenceMap.Position p lane slice index s
+  passWord : s.mem.readW (off (s.gpr .rbp) 0) 64 = BitVec.ofNat 64 pass
+  lanesWord : s.mem.readW (off (s.gpr .rbp) 184) 64 = BitVec.ofNat 64 p.lanes
+
+structure Mapped (s t : State) (p : Params) (pass lane slice index : Nat) : Prop where
+  selected : t.gpr .r9 = BitVec.ofNat 64 (Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)).1
+  column : t.gpr .rdi = BitVec.ofNat 64 (Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)).2
+  original : t.gpr .r11 = s.gpr .rdi
+  keeps : Divide.Keeps ReferenceMap.changed s t
+
+theorem mapping_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : Ready p pass lane slice index s) :
+    WP isa Impl.Argon2.X86_64.FillKernel.mapping s (Mapped s · p pass lane slice index) := by
+  unfold Impl.Argon2.X86_64.FillKernel.mapping
+  refine WP.seq ((load_ok s .rsi 184 (h.layout.frameRead 184 (by simp))).mono ?_)
+  rintro a ⟨lanes, keeps⟩
+  have k : Divide.Keeps ReferenceMap.changed s a := keeps.mono (by decide)
+  have ready : ReferenceMap.Ready p pass lane slice index a := by
+    refine ⟨h.bounds, h.position.of_keeps k, lanes.trans h.lanesWord, ?_, ?_⟩
+    · rw [k.rd, k.wr, k.regs .rbp (by decide)]
+      simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero]
+        using h.layout.frameRead 0 (by simp)
+    · rw [k.mem, k.regs .rbp (by decide)]
+      simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero] using h.passWord
+  refine (ReferenceMap.code_spec_ok a p pass lane slice index ready).mono ?_
+  rintro t ⟨lane, column, original, tail⟩
+  rw [keeps.regs .rdi (by decide)] at lane column original
+  exact ⟨lane, column, original, k.trans tail⟩
+
+structure Pointers (s t : State) (p : Params) (lane slice index refLane refColumn : Nat) : Prop where
+  current : t.gpr .r10 = FillPointers.cell (matrix s) p lane (slice * p.segmentLen + index)
+  previous : t.gpr .rdi = FillPointers.cell (matrix s) p lane
+    ((slice * p.segmentLen + index + p.laneLen - 1) % p.laneLen)
+  reference : t.gpr .rsi = FillPointers.cell (matrix s) p refLane refColumn
+  keeps : Divide.Keeps ReferenceMap.changed s t
+
+theorem pointers_ok (s : State) (p : Params) (pass lane slice index refLane refColumn : Nat)
+    (layout : Layout p s) (bounds : ReferenceMap.Bounds p pass lane slice index)
+    (position : ReferenceMap.Position p lane slice index s)
+    (laneWord : s.gpr .r9 = BitVec.ofNat 64 refLane) (columnWord : s.gpr .rdi = BitVec.ofNat 64 refColumn) :
+    WP isa Impl.Argon2.X86_64.FillKernel.pointers s (Pointers s · p lane slice index refLane refColumn) := by
+  unfold Impl.Argon2.X86_64.FillKernel.pointers
+  refine WP.seq ((load_ok s .r8 232 (layout.frameRead 232 (by simp))).mono ?_)
+  rintro a ⟨base, keeps⟩
+  have k : Divide.Keeps ReferenceMap.changed s a := keeps.mono (by decide)
+  have lane' : a.gpr .r9 = BitVec.ofNat 64 refLane := (keeps.regs .r9 (by decide)).trans laneWord
+  have col' : a.gpr .rdi = BitVec.ofNat 64 refColumn := (keeps.regs .rdi (by decide)).trans columnWord
+  refine (FillPointers.code_nat_ok a p pass lane slice index refLane refColumn bounds
+    (position.of_keeps k) lane' col').mono ?_
+  rintro t ⟨current, previous, reference, tail⟩
+  rw [base] at current previous reference
+  exact ⟨current, previous, reference, k.trans (tail.mono (by decide))⟩
+
+end VG.Proof.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelCT.lean
new file mode 100644
index 000000000..e5b41c53d
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelCT.lean
@@ -0,0 +1,57 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelMappingCT
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCT
+
+/-! Equal permitted references give equal compression and block-update traces. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+theorem prepared_public {p : Params} {pass lane slice index : Nat} {s t a b : State}
+    (h : Related p pass lane slice index s t)
+    (ha : Prepared s a p pass lane slice index) (hb : Prepared t b p pass lane slice index) :
+    FillCompress.CodeRelated a b := by
+  have currentEq : current s p lane slice index = current t p lane slice index := by
+    unfold current; rw [h.matrices]
+  have previousEq : previous s p lane slice index = previous t p lane slice index := by
+    unfold previous; rw [h.matrices]
+  have referenceEq : referenced s p pass lane slice index = referenced t p pass lane slice index := by
+    unfold referenced; rw [h.references, h.matrices]
+  have workA : FillCompress.work a = work s := by
+    unfold FillCompress.work work; rw [ha.keeps.regs .rbp (by decide), ha.keeps.mem]
+  have workB : FillCompress.work b = work t := by
+    unfold FillCompress.work work; rw [hb.keeps.regs .rbp (by decide), hb.keeps.mem]
+  have passA : FillCompress.pass a = BitVec.ofNat 64 pass := by
+    unfold FillCompress.pass
+    rw [ha.keeps.regs .rbp (by decide), ha.keeps.mem]
+    exact h.left.passWord
+  have passB : FillCompress.pass b = BitVec.ofNat 64 pass := by
+    unfold FillCompress.pass
+    rw [hb.keeps.regs .rbp (by decide), hb.keeps.mem]
+    exact h.right.passWord
+  refine ⟨ha.ready, hb.ready, ?_, workA.trans (h.scratch.trans workB.symm), passA.trans passB.symm⟩
+  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.previousPtr.trans (previousEq.trans hb.previousPtr.symm)
+  · exact ha.referencePtr.trans (referenceEq.trans hb.referencePtr.symm)
+  · exact ha.currentPtr.trans (currentEq.trans hb.currentPtr.symm)
+  · exact (ha.keeps.regs .rsp (by decide)).trans (h.stacks.trans (hb.keeps.regs .rsp (by decide)).symm)
+  · exact (ha.keeps.regs .rbp (by decide)).trans (h.bases.trans (hb.keeps.regs .rbp (by decide)).symm)
+
+theorem prepare_public_rel (p : Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) Impl.Argon2.X86_64.FillKernel.prepare
+      FillCompress.CodeRelated := by
+  have trace := (mapping_public_rel p pass lane slice index).seq (pointers_trace p lane slice index)
+  have full := trace.wpDep (fun s t h =>
+    ⟨prepare_ok s p pass lane slice index h.left, prepare_ok t p pass lane slice index h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact prepared_public hp ha hb
+
+theorem code_rel (p : Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) Impl.Argon2.X86_64.FillKernel.code
+      (fun _ _ => True) := (prepare_public_rel p pass lane slice index).seq FillCompress.code_rel
+
+end VG.Proof.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelLayout.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelLayout.lean
new file mode 100644
index 000000000..f822a6935
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelLayout.lean
@@ -0,0 +1,101 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointersNat
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompress
+import VerifiedGarbage.Impl.Argon2.X86_64.FillKernel
+
+/-! One allocation invariant covers all matrix cells used by the filling step. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+def matrix (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 232) 64
+
+def work (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 248) 64
+
+structure Layout (p : Params) (s : State) : Prop where
+  frameRead : ∀ d ∈ [0, 16, 184, 232, 248], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8
+  frameWrite : InRegions s.wr (off (s.gpr .rbp) 16) 8
+  matrixWrite : Covers [⟨matrix s, p.blocks * 1024⟩] s.wr
+  workWrite : Covers [⟨work s, 5120⟩] s.wr
+  matrixWork : (⟨matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨work s, 5120⟩
+  matrixFrame : (⟨matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨s.gpr .rbp, 272⟩
+  matrixStack : (⟨matrix s, p.blocks * 1024⟩ : Region).Disjoint (below (s.gpr .rsp) 8)
+  frameWork : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨work s, 5120⟩
+  frameStack : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint (below (s.gpr .rsp) 8)
+  stackWork : (below (s.gpr .rsp) 8).Disjoint ⟨work s, 5120⟩
+
+theorem Layout.of_keeps {p : Params} {s t : State} (h : Layout p s)
+    (k : Divide.Keeps ReferenceMap.changed s t) : Layout p t := by
+  have bp := k.regs .rbp (by decide)
+  have sp := k.regs .rsp (by decide)
+  have matrix' : matrix t = matrix s := by unfold matrix; rw [bp, k.mem]
+  have work' : work t = work s := by unfold work; rw [bp, k.mem]
+  constructor
+  · rw [k.rd, k.wr, bp]; exact h.frameRead
+  · rw [k.wr, bp]; exact h.frameWrite
+  · rw [matrix', k.wr]; exact h.matrixWrite
+  · rw [work', k.wr]; exact h.workWrite
+  · rw [matrix', work']; exact h.matrixWork
+  · rw [matrix', bp]; exact h.matrixFrame
+  · rw [matrix', sp]; exact h.matrixStack
+  · rw [bp, work']; exact h.frameWork
+  · rw [bp, sp]; exact h.frameStack
+  · rw [sp, work']; exact h.stackWork
+
+theorem cell_sub (p : Params) (base : Addr) (positive : 0 < p.lanes) {lane column : Nat}
+    (hl : lane < p.lanes) (hc : column < p.laneLen) :
+    Region.Sub ⟨FillPointers.cell base p lane column, 1024⟩ ⟨base, p.blocks * 1024⟩ :=
+  Offset.sub_base base (Proof.Argon2.cell_bytes p positive hl hc)
+
+theorem Layout.cell_cover {p : Params} {s : State} (h : Layout p s) (positive : 0 < p.lanes)
+    {lane column : Nat} (hl : lane < p.lanes) (hc : column < p.laneLen) :
+    Covers [⟨FillPointers.cell (matrix s) p lane column, 1024⟩] s.wr := by
+  have sub : Covers [⟨FillPointers.cell (matrix s) p lane column, 1024⟩]
+      [⟨matrix s, p.blocks * 1024⟩] := Covers.of_sub (by
+        intro r hr
+        simp only [List.mem_singleton] at hr
+        subst r
+        exact ⟨⟨matrix s, p.blocks * 1024⟩, by simp, (lane * p.laneLen + column) * 1024,
+          rfl, Proof.Argon2.cell_bytes p positive hl hc⟩)
+  exact fun a n ha => h.matrixWrite a n (sub a n ha)
+
+theorem compress_ready (p : Params) (s : State) (layout : Layout p s)
+    (positive : 0 < p.lanes) (leftLane leftColumn rightLane rightColumn destLane destColumn : Nat)
+    (ll : leftLane < p.lanes) (lc : leftColumn < p.laneLen)
+    (rl : rightLane < p.lanes) (rc : rightColumn < p.laneLen)
+    (dl : destLane < p.lanes) (dc : destColumn < p.laneLen)
+    (left : s.gpr .rdi = FillPointers.cell (matrix s) p leftLane leftColumn)
+    (right : s.gpr .rsi = FillPointers.cell (matrix s) p rightLane rightColumn)
+    (dest : s.gpr .r10 = FillPointers.cell (matrix s) p destLane destColumn) : FillCompress.Ready s := by
+  have leftSub := cell_sub p (matrix s) positive ll lc
+  have rightSub := cell_sub p (matrix s) positive rl rc
+  have destSub := cell_sub p (matrix s) positive dl dc
+  have read (lane column : Nat) (hl : lane < p.lanes) (hc : column < p.laneLen) :
+      Covers [⟨FillPointers.cell (matrix s) p lane column, 1024⟩] (s.rd ++ s.wr) := by
+    intro a n ha
+    obtain ⟨r, hr, hc⟩ := layout.cell_cover positive hl hc a n ha
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  constructor
+  · intro d hd
+    exact layout.frameRead d (by
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hd
+      rcases hd with rfl | rfl | rfl <;> simp)
+  · exact layout.frameWrite
+  · rw [left]; exact read leftLane leftColumn ll lc
+  · rw [right]; exact read rightLane rightColumn rl rc
+  · rw [dest]; exact layout.cell_cover positive dl dc
+  · exact layout.workWrite
+  · rw [left]; exact layout.matrixWork.sub_left leftSub
+  · rw [right]; exact layout.matrixWork.sub_left rightSub
+  · rw [dest]; exact layout.matrixWork.sub_left destSub
+  · exact layout.frameWork
+  · rw [left]; exact layout.matrixFrame.sub_left leftSub
+  · rw [right]; exact layout.matrixFrame.sub_left rightSub
+  · rw [dest]; exact layout.matrixFrame.sub_left destSub
+  · rw [left]; exact (layout.matrixStack.sub_left leftSub).symm
+  · rw [right]; exact (layout.matrixStack.sub_left rightSub).symm
+  · exact layout.stackWork
+  · rw [dest]; exact layout.matrixStack.sub_left destSub
+  · exact layout.frameStack
+
+end VG.Proof.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelMappingCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelMappingCT.lean
new file mode 100644
index 000000000..2d48c8db4
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelMappingCT.lean
@@ -0,0 +1,114 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelPrepare
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapCT
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointersCT
+
+/-! Reference mapping exposes no more than the permitted reference coordinates. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+structure Related (p : Params) (pass lane slice index : Nat) (s t : State) : Prop where
+  left : Ready p pass lane slice index s
+  right : Ready p pass lane slice index t
+  bases : s.gpr .rbp = t.gpr .rbp
+  stacks : s.gpr .rsp = t.gpr .rsp
+  matrices : matrix s = matrix t
+  scratch : work s = work t
+  references : Spec.Argon2.reference p pass lane slice index (s.gpr .rdi) =
+    Spec.Argon2.reference p pass lane slice index (t.gpr .rdi)
+
+structure PointerRelated (p : Params) (lane slice index : Nat) (s t : State) : Prop where
+  left : Layout p s
+  right : Layout p t
+  leftPosition : ReferenceMap.Position p lane slice index s
+  rightPosition : ReferenceMap.Position p lane slice index t
+  bases : s.gpr .rbp = t.gpr .rbp
+  matrices : matrix s = matrix t
+
+theorem lanes_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block Impl.Argon2.X86_64.FillKernel.lanes) (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 lanes_ready (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : Ready p pass lane slice index s) :
+    WP isa (.block Impl.Argon2.X86_64.FillKernel.lanes) s fun t =>
+      ReferenceMap.Ready p pass lane slice index t ∧ Divide.Keeps ReferenceMap.changed s t := by
+  refine (load_ok s .rsi 184 (h.layout.frameRead 184 (by simp))).mono ?_
+  rintro t ⟨lanes, keeps⟩
+  have k : Divide.Keeps ReferenceMap.changed s t := keeps.mono (by decide)
+  refine ⟨⟨h.bounds, h.position.of_keeps k, lanes.trans h.lanesWord, ?_, ?_⟩, k⟩
+  · rw [k.rd, k.wr, k.regs .rbp (by decide)]
+    simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero]
+      using h.layout.frameRead 0 (by simp)
+  · rw [k.mem, k.regs .rbp (by decide)]
+    simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero] using h.passWord
+
+theorem lanes_public_rel (p : Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) (.block Impl.Argon2.X86_64.FillKernel.lanes)
+      (ReferenceMap.Related p pass lane slice index) := by
+  have trace := lanes_rel.mono (P' := Related p pass lane slice index)
+    (fun _ _ h => h.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨lanes_ready s p pass lane slice index h.left, lanes_ready t p pass lane slice index h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact ⟨ha.1, hb.1, (ha.2.regs .rbp (by decide)).trans
+    (hp.bases.trans (hb.2.regs .rbp (by decide)).symm)⟩
+
+theorem mapping_public_rel (p : Params) (pass lane slice index : Nat) :
+    RelCT isa (Related p pass lane slice index) Impl.Argon2.X86_64.FillKernel.mapping
+      (PointerRelated p lane slice index) := by
+  have trace := (lanes_public_rel p pass lane slice index).seq (ReferenceMap.code_rel p pass lane slice index)
+  have full := trace.wpDep (fun s t h =>
+    ⟨mapping_ok s p pass lane slice index h.left, mapping_ok t p pass lane slice index h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨hp.left.layout.of_keeps ha.keeps, hp.right.layout.of_keeps hb.keeps,
+    hp.left.position.of_keeps ha.keeps, hp.right.position.of_keeps hb.keeps, ?_, ?_⟩
+  · exact (ha.keeps.regs .rbp (by decide)).trans (hp.bases.trans (hb.keeps.regs .rbp (by decide)).symm)
+  · unfold matrix
+    rw [ha.keeps.mem, hb.keeps.mem, ha.keeps.regs .rbp (by decide), hb.keeps.regs .rbp (by decide)]
+    exact hp.matrices
+
+theorem matrix_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    (.block Impl.Argon2.X86_64.FillKernel.matrix) (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 pointers_trace (p : Params) (lane slice index : Nat) :
+    RelCT isa (PointerRelated p lane slice index) Impl.Argon2.X86_64.FillKernel.pointers
+      (fun _ _ => True) := by
+  have trace := matrix_rel.mono (P' := PointerRelated p lane slice index)
+    (fun _ _ h => h.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h =>
+    ⟨load_ok s .r8 232 (h.left.frameRead 232 (by simp)),
+      load_ok t .r8 232 (h.right.frameRead 232 (by simp))⟩)
+  have args : RelCT isa (PointerRelated p lane slice index) (.block Impl.Argon2.X86_64.FillKernel.matrix)
+      (fun s t => ∀ r ∈ [Reg.r8, .rbx, .r12, .r13, .r14, .r15], s.gpr r = t.gpr r) :=
+    full.mono (fun _ _ h => h) (by
+      intro a b h r hr
+      obtain ⟨_, s, t, hp, ⟨va, ka⟩, ⟨vb, kb⟩⟩ := h
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl | rfl | rfl | rfl | rfl
+      · exact va.trans (hp.matrices.trans vb.symm)
+      all_goals rw [ka.regs _ (by decide), kb.regs _ (by decide)]
+      · exact hp.leftPosition.current.trans hp.rightPosition.current.symm
+      · exact hp.leftPosition.laneLength.trans hp.rightPosition.laneLength.symm
+      · exact hp.leftPosition.segmentLength.trans hp.rightPosition.segmentLength.symm
+      · exact hp.leftPosition.slice.trans hp.rightPosition.slice.symm
+      · exact hp.leftPosition.index.trans hp.rightPosition.index.symm)
+  exact (args.seq FillPointers.code_rel).mono (fun _ _ h => h) (fun _ _ _ => trivial)
+
+end VG.Proof.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelPrepare.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelPrepare.lean
new file mode 100644
index 000000000..2285bbed3
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillKernelPrepare.lean
@@ -0,0 +1,67 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillKernelArgs
+
+/-! Complete active-cell update from a random word and the matrix allocation. -/
+
+namespace VG.Proof.Argon2.X86_64.FillKernel
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+def currentColumn (p : Params) (slice index : Nat) : Nat := slice * p.segmentLen + index
+
+def previousColumn (p : Params) (slice index : Nat) : Nat :=
+  (currentColumn p slice index + p.laneLen - 1) % p.laneLen
+
+def current (s : State) (p : Params) (lane slice index : Nat) : Addr :=
+  FillPointers.cell (matrix s) p lane (currentColumn p slice index)
+
+def previous (s : State) (p : Params) (lane slice index : Nat) : Addr :=
+  FillPointers.cell (matrix s) p lane (previousColumn p slice index)
+
+def referenced (s : State) (p : Params) (pass lane slice index : Nat) : Addr :=
+  let ref := Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)
+  FillPointers.cell (matrix s) p ref.1 ref.2
+
+structure Prepared (s t : State) (p : Params) (pass lane slice index : Nat) : Prop where
+  ready : FillCompress.Ready t
+  currentPtr : t.gpr .r10 = current s p lane slice index
+  previousPtr : t.gpr .rdi = previous s p lane slice index
+  referencePtr : t.gpr .rsi = referenced s p pass lane slice index
+  keeps : Divide.Keeps ReferenceMap.changed s t
+
+theorem prepare_ok (s : State) (p : Params) (pass lane slice index : Nat)
+    (h : Ready p pass lane slice index s) :
+    WP isa Impl.Argon2.X86_64.FillKernel.prepare s (Prepared s · p pass lane slice index) := by
+  unfold Impl.Argon2.X86_64.FillKernel.prepare
+  refine WP.seq ((mapping_ok s p pass lane slice index h).mono ?_)
+  intro a mapped
+  let ref := Spec.Argon2.reference p pass lane slice index (s.gpr .rdi)
+  refine ((pointers_ok a p pass lane slice index ref.1 ref.2
+    (h.layout.of_keeps mapped.keeps) h.bounds (h.position.of_keeps mapped.keeps)
+    mapped.selected mapped.column).mono ?_)
+  intro b pointers
+  have keeps := mapped.keeps.trans pointers.keeps
+  have matrixA : matrix a = matrix s := by
+    unfold matrix; rw [mapped.keeps.mem, mapped.keeps.regs .rbp (by decide)]
+  have matrixB : matrix b = matrix a := by
+    unfold matrix; rw [pointers.keeps.mem, pointers.keeps.regs .rbp (by decide)]
+  have cur : b.gpr .r10 = current s p lane slice index := by
+    rw [pointers.current, matrixA]; rfl
+  have prev : b.gpr .rdi = previous s p lane slice index := by
+    rw [pointers.previous, matrixA]; rfl
+  have other : b.gpr .rsi = referenced s p pass lane slice index := by
+    rw [pointers.reference, matrixA]; rfl
+  have columnBound := Proof.Argon2.column_lt p h.bounds.lanesPositive h.bounds.sliceBound h.bounds.indexBound
+  have previousBound := Proof.Argon2.previous_column_lt p h.bounds.lanesPositive h.bounds.memoryMinimum
+    (slice * p.segmentLen + index)
+  obtain ⟨refLane, refColumn⟩ := Proof.Argon2.reference_bounds p h.bounds.lanesPositive
+    h.bounds.memoryMinimum pass lane slice index (s.gpr .rdi) h.bounds.laneBound
+  have compressReady : FillCompress.Ready b := by
+    apply compress_ready p b (h.layout.of_keeps keeps) h.bounds.lanesPositive
+      lane (previousColumn p slice index) ref.1 ref.2 lane (currentColumn p slice index)
+      h.bounds.laneBound previousBound refLane refColumn h.bounds.laneBound columnBound
+    · rw [pointers.previous, matrixB]; rfl
+    · rw [pointers.reference, matrixB]
+    · rw [pointers.current, matrixB]; rfl
+  exact ⟨compressReady, cur, prev, other, keeps⟩
+
+end VG.Proof.Argon2.X86_64.FillKernel
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersNat.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersNat.lean
new file mode 100644
index 000000000..1e4643517
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersNat.lean
@@ -0,0 +1,51 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointers
+import VerifiedGarbage.Proof.Argon2.X86_64.Memory
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceMapState
+import VerifiedGarbage.Proof.Argon2.FillPositions
+
+/-! Matrix pointers are the natural-number block offsets in the specification. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+def cell (base : Addr) (p : Spec.Argon2.Params) (lane column : Nat) : Addr :=
+  off base ((lane * p.laneLen + column) * 1024)
+
+theorem address_nat (base : Addr) (lane column q : Nat) :
+    address base (BitVec.ofNat 64 lane) (BitVec.ofNat 64 column) (BitVec.ofNat 64 q) =
+      off base ((lane * q + column) * 1024) := by
+  unfold address off
+  change (BitVec.ofNat 64 lane * BitVec.ofNat 64 q + BitVec.ofNat 64 column) *
+    BitVec.ofNat 64 1024 + base = _
+  rw [← BitVec.ofNat_mul, ← BitVec.ofNat_add, ← BitVec.ofNat_mul, BitVec.add_comm]
+
+theorem code_nat_ok (s : State) (p : Spec.Argon2.Params) (pass lane slice index refLane refColumn : Nat)
+    (bounds : ReferenceMap.Bounds p pass lane slice index)
+    (position : ReferenceMap.Position p lane slice index s)
+    (rl : s.gpr .r9 = BitVec.ofNat 64 refLane)
+    (rc : s.gpr .rdi = BitVec.ofNat 64 refColumn) :
+    WP isa code s fun t =>
+      t.gpr .r10 = cell (s.gpr .r8) p lane (slice * p.segmentLen + index) ∧
+      t.gpr .rdi = cell (s.gpr .r8) p lane ((slice * p.segmentLen + index + p.laneLen - 1) % p.laneLen) ∧
+      t.gpr .rsi = cell (s.gpr .r8) p refLane refColumn ∧ Divide.Keeps changed s t := by
+  refine (code_ok s).mono ?_
+  rintro t ⟨current, previous, reference, keeps⟩
+  have col : column s = BitVec.ofNat 64 (slice * p.segmentLen + index) := by
+    unfold column
+    rw [position.slice, position.segmentLength, position.index, ← BitVec.ofNat_mul, ← BitVec.ofNat_add]
+  have prev : predecessor s = BitVec.ofNat 64
+      ((slice * p.segmentLen + index + p.laneLen - 1) % p.laneLen) := by
+    unfold predecessor
+    rw [col, position.laneLength]
+    have positive := Proof.Argon2.segmentLen_ge_two p bounds.lanesPositive bounds.memoryMinimum
+    have q := Proof.Argon2.laneLen_segments p bounds.lanesPositive
+    exact FillColumn.previous_word_nat _ _ (by omega)
+      (Nat.lt_trans bounds.laneLength_bound (by decide))
+      (Proof.Argon2.column_lt p bounds.lanesPositive bounds.sliceBound bounds.indexBound)
+  refine ⟨?_, ?_, ?_, keeps⟩
+  · rw [current, position.current, col, position.laneLength, address_nat]; rfl
+  · rw [previous, position.current, prev, position.laneLength, address_nat]; rfl
+  · rw [reference, rl, rc, position.laneLength, address_nat]; rfl
+
+end VG.Proof.Argon2.X86_64.FillPointers