From 066283a4fd6f5a485717850d84d6bbe832568ebd Mon Sep 17 00:00:00 2001
From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com>
Date: Thu, 1 Oct 2026 20:04:35 +0000
Subject: [PATCH] Prove complete Argon2 segment setup and filling

---
 .../Impl/Argon2/X86_64/SegmentSetup.lean      |  25 ++++
 .../Proof/Argon2/SegmentStart.lean            |  26 ++++
 .../Proof/Argon2/X86_64/FillContext.lean      |  61 +++++++++
 .../Proof/Argon2/X86_64/SegmentSetup.lean     |  43 +++++++
 .../Proof/Argon2/X86_64/SegmentSetupCT.lean   | 120 ++++++++++++++++++
 .../Argon2/X86_64/SegmentSetupCheck.lean      |  49 +++++++
 .../Argon2/X86_64/SegmentSetupPrepare.lean    |  68 ++++++++++
 .../Argon2/X86_64/SegmentSetupReady.lean      |  67 ++++++++++
 .../Argon2/X86_64/SegmentSetupReset.lean      |  48 +++++++
 .../Argon2/X86_64/SegmentSetupSteps.lean      |  88 +++++++++++++
 .../Argon2/X86_64/SegmentSetupTrace.lean      | 100 +++++++++++++++
 11 files changed, 695 insertions(+)
 create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/SegmentSetup.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/SegmentStart.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillContext.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetup.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCT.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCheck.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupPrepare.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReady.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReset.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupSteps.lean
 create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupTrace.lean

diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/SegmentSetup.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/SegmentSetup.lean
new file mode 100644
index 0000000000..365bc73600
--- /dev/null
+++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/SegmentSetup.lean
@@ -0,0 +1,25 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillSegment
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCache
+
+/-! Reset the address cache per segment and skip the two initialized cells. -/
+
+namespace VG.Impl.Argon2.X86_64.SegmentSetup
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def reset : Prog isa := .seq (.block [.mov .rax (.imm 0)]) (.block AddressCache.save)
+
+def first : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 0)), .alu .or .rcx (.reg .r14), .alu .cmp .rcx (.imm 0)]
+
+def index : Prog isa := .seq (.block first)
+  (.ite .e (.block [.mov .r15 (.imm 2)]) (.block [.mov .r15 (.imm 0)]))
+
+def check : List Instr := [.alu .cmp .r15 (.reg .r13)]
+
+def prepare : Prog isa := .seq reset index
+
+def code : Prog isa := .seq prepare (.seq (.block check) (.ite .b FillSegment.loop (.block [])))
+
+end VG.Impl.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/SegmentStart.lean b/lean/VerifiedGarbage/Proof/Argon2/SegmentStart.lean
new file mode 100644
index 0000000000..bb7d434c84
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/SegmentStart.lean
@@ -0,0 +1,26 @@
+import VerifiedGarbage.Proof.Argon2.Segment
+
+/-! The first two cells of pass zero's first segment are already initialized. -/
+
+namespace VG.Proof.Argon2
+
+open VG.Spec.Argon2
+
+def segmentStart (pass slice : Nat) : Nat := if pass = 0 ∧ slice = 0 then 2 else 0
+
+theorem segment_first_two (p : Params) (lane : Nat) (state : FillState) :
+    segment p 0 lane 0 0 2 state = state := by
+  rw [segment_succ, segment_succ, segment_zero]
+  simp only [fillBlock, Nat.reduceAdd, and_self, Nat.reduceLT, ite_true]
+
+theorem segment_start (p : Params) (pass lane slice : Nat) (state : FillState) (minimum : 2 ≤ p.segmentLen) :
+    segment p pass lane slice 0 p.segmentLen state =
+      segment p pass lane slice (segmentStart pass slice) (p.segmentLen - segmentStart pass slice) state := by
+  by_cases first : pass = 0 ∧ slice = 0
+  · obtain ⟨rfl, rfl⟩ := first
+    have append := segment_append p 0 lane 0 0 2 (p.segmentLen - 2) state
+    rw [show 2 + (p.segmentLen - 2) = p.segmentLen by omega, segment_first_two] at append
+    exact append
+  · simp only [segmentStart, first, ite_false, Nat.sub_zero]
+
+end VG.Proof.Argon2
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillContext.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillContext.lean
new file mode 100644
index 0000000000..2bbb6335d1
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillContext.lean
@@ -0,0 +1,61 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillSegment
+
+/-! A segment context allows its starting and final indices, including an empty suffix. -/
+
+namespace VG.Proof.Argon2.X86_64.FillContext
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+structure Parameters (p : Params) (pass lane slice : Nat) : Prop where
+  lanesPositive : 0 < p.lanes
+  lanesBound : p.lanes < 2 ^ 32
+  memoryMinimum : 8 * p.lanes ≤ p.memory
+  memoryBound : p.memory < 2 ^ 32
+  passBound : pass < 2 ^ 32
+  laneBound : lane < p.lanes
+  sliceBound : slice < 4
+
+structure Ready (p : Params) (pass lane slice index old : Nat) (s : State) : Prop where
+  parameters : Parameters p pass lane slice
+  layout : FillKernel.Layout p s
+  cache : AddressCache.Invariant p pass lane slice old s
+  matrixWork : (⟨FillKernel.matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨AddressCalls.work s, 8192⟩
+  position : ReferenceMap.Position p lane slice index s
+  lanesWord : s.mem.readW (off (s.gpr .rbp) 184) 64 = BitVec.ofNat 64 p.lanes
+
+theorem Ready.activate {p : Params} {pass lane slice index old : Nat} {s : State}
+    (h : Ready p pass lane slice index old s) (bound : index < p.segmentLen)
+    (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index) : RandomSource.Ready p pass lane slice index old s :=
+  ⟨⟨h.layout, ⟨h.parameters.lanesPositive, h.parameters.lanesBound, h.parameters.memoryMinimum,
+    h.parameters.memoryBound, h.parameters.passBound, h.parameters.laneBound, h.parameters.sliceBound,
+    bound, active⟩, h.position, h.cache.words.passWord, h.lanesWord⟩, h.cache, h.matrixWork⟩
+
+theorem Parameters.segment_bound {p : Params} {pass lane slice : Nat} (h : Parameters p pass lane slice) :
+    2 ≤ p.segmentLen ∧ p.segmentLen < 2 ^ 64 := by
+  have minimum := Proof.Argon2.segmentLen_ge_two p h.lanesPositive h.memoryMinimum
+  have le : p.segmentLen ≤ p.blocks := by
+    have blocks := Proof.Argon2.blocks_lanes p h.lanesPositive
+    have segments := Proof.Argon2.laneLen_segments p h.lanesPositive
+    have laneLe : p.laneLen ≤ p.blocks := by rw [blocks]; exact Nat.le_mul_of_pos_left _ h.lanesPositive
+    omega
+  exact ⟨minimum, Nat.lt_of_le_of_lt le
+    (Nat.lt_trans (Nat.lt_of_le_of_lt (Proof.Argon2.blocks_le_memory p) h.memoryBound) (by decide))⟩
+
+theorem Ready.of_keeps {p : Params} {pass lane slice index old : Nat} {s t : State}
+    (h : Ready p pass lane slice index old s) (k : Divide.Keeps ReferenceMap.changed s t) :
+    Ready p pass lane slice index old t := by
+  have bp := k.regs .rbp (by decide)
+  have base : FillKernel.matrix t = FillKernel.matrix s := by unfold FillKernel.matrix; rw [k.mem, bp]
+  have work : AddressCalls.work t = AddressCalls.work s := by unfold AddressCalls.work; rw [k.mem, bp]
+  refine ⟨h.parameters, h.layout.of_preserved bp (k.regs .rsp (by decide)) base work k.rd k.wr,
+    h.cache.of_keeps k, ?_, h.position.of_keeps k, ?_⟩
+  · rw [base, work]; exact h.matrixWork
+  · rw [k.mem, bp]; exact h.lanesWord
+
+theorem finished_context {p : Params} {pass lane slice : Nat} {s t : State} {state : FillState}
+    (parameters : Parameters p pass lane slice) (h : FillSegment.Finished s t p pass lane slice state) :
+    ∃ old, Ready p pass lane slice p.segmentLen old t := by
+  obtain ⟨old, cache⟩ := h.cache
+  exact ⟨old, parameters, h.layout, cache, h.matrixWork, h.position, h.lanesWord⟩
+
+end VG.Proof.Argon2.X86_64.FillContext
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetup.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetup.lean
new file mode 100644
index 0000000000..0362c2dd57
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetup.lean
@@ -0,0 +1,43 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupCheck
+import VerifiedGarbage.Proof.Argon2.SegmentStart
+
+/-! Fill one complete segment, including the initialized prefix and empty suffix. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+theorem code_ok (s : State) (p : Params) (pass lane slice : Nat)
+    (h : Ready p pass lane slice s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory) :
+    WP isa code s (FillSegment.Finished s · p pass lane slice
+      (Proof.Argon2.segment p pass lane slice 0 p.segmentLen state)) := by
+  rw [Proof.Argon2.segment_start p pass lane slice state h.parameters.segment_bound.1]
+  change WP isa code s (FillSegment.Finished s · p pass lane slice
+    (Proof.Argon2.segment p pass lane slice (start pass slice) (p.segmentLen - start pass slice) state))
+  unfold code
+  refine WP.seq ((prepare_ok s p pass lane slice h).mono ?_)
+  intro a prepared
+  refine WP.seq ((check_prepared_ok prepared).mono ?_)
+  rintro b ⟨prepared, flag⟩
+  have matrix := prepared.represents h state.memory represented
+  refine WP.ite (decide (start pass slice < p.segmentLen)) (by simp only [eval, flag]) ?_ ?_
+  · intro taken
+    have bound := of_decide_eq_true taken
+    have active := prepared.context.activate bound (start_active pass slice)
+    refine (FillSegment.loop_ok (p.segmentLen - start pass slice) b p pass lane slice (start pass slice) 0
+      active state matrix (by omega) (by omega)).mono ?_
+    intro t finished
+    exact finished_prepared prepared finished
+  · intro skipped
+    have bound := of_decide_eq_false skipped
+    have minimum := h.parameters.segment_bound.1
+    have last : start pass slice = p.segmentLen := by have := start_le pass slice p.segmentLen minimum; omega
+    have finished : FillSegment.Finished b b p pass lane slice state :=
+      ⟨matrix, rfl, rfl, last ▸ prepared.context.position, prepared.context.layout,
+        ⟨0, prepared.context.cache⟩, prepared.context.matrixWork, prepared.context.cache.words.passWord,
+        prepared.context.lanesWord, fun _ _ _ => rfl, rfl, rfl, Frame.refl _ _, rfl⟩
+    rw [last, Nat.sub_self, Proof.Argon2.segment_zero]
+    exact WP.block_nil (finished_prepared prepared finished)
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCT.lean
new file mode 100644
index 0000000000..7fa183e8d2
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCT.lean
@@ -0,0 +1,120 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetup
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupTrace
+import VerifiedGarbage.Proof.Argon2.X86_64.FillSegmentCT
+
+/-! Complete segment setup and filling expose only the specified reference log. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+structure Related (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) (s t : State) : Prop where
+  ready : RelatedReady p pass lane slice s t
+  leftMatrix : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks leftState.memory
+  rightMatrix : Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks rightState.memory
+  indices : (Proof.Argon2.segment p pass lane slice 0 p.segmentLen leftState).indices =
+    (Proof.Argon2.segment p pass lane slice 0 p.segmentLen rightState).indices
+
+structure PreparedRelated (p : Params) (pass lane slice : Nat) (leftState rightState : FillState)
+    (s t : State) : Prop where
+  left : FillContext.Ready p pass lane slice (start pass slice) 0 s
+  right : FillContext.Ready p pass lane slice (start pass slice) 0 t
+  bases : s.gpr .rbp = t.gpr .rbp
+  stacks : s.gpr .rsp = t.gpr .rsp
+  matrices : FillKernel.matrix s = FillKernel.matrix t
+  work : AddressCalls.work s = AddressCalls.work t
+  leftMatrix : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks leftState.memory
+  rightMatrix : Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks rightState.memory
+  indices : (Proof.Argon2.segment p pass lane slice (start pass slice) (p.segmentLen - start pass slice) leftState).indices =
+    (Proof.Argon2.segment p pass lane slice (start pass slice) (p.segmentLen - start pass slice) rightState).indices
+
+theorem prepare_public_rel (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) :
+    RelCT isa (Related p pass lane slice leftState rightState) prepare
+      (PreparedRelated p pass lane slice leftState rightState) := by
+  have trace := (prepare_trace p pass lane slice).mono
+    (P' := Related p pass lane slice leftState rightState) (fun _ _ h => h.ready) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨prepare_ok s p pass lane slice h.ready.left, prepare_ok t p pass lane slice h.ready.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨ha.context, hb.context, ?_, ?_, ha.matrix.trans (hp.ready.matrices.trans hb.matrix.symm),
+    ha.work.trans (hp.ready.work.trans hb.work.symm), ha.represents hp.ready.left leftState.memory hp.leftMatrix,
+    hb.represents hp.ready.right rightState.memory hp.rightMatrix, ?_⟩
+  · rw [ha.regs .rbp (by simp [calleeSaved]) (by decide), hb.regs .rbp (by simp [calleeSaved]) (by decide)]
+    exact hp.ready.bases
+  · rw [ha.regs .rsp (by simp [calleeSaved]) (by decide), hb.regs .rsp (by simp [calleeSaved]) (by decide)]
+    exact hp.ready.stacks
+  · have indices := hp.indices
+    rw [Proof.Argon2.segment_start p pass lane slice leftState hp.ready.left.parameters.segment_bound.1,
+      Proof.Argon2.segment_start p pass lane slice rightState hp.ready.right.parameters.segment_bound.1] at indices
+    exact indices
+
+theorem PreparedRelated.of_keeps {p : Params} {pass lane slice : Nat} {leftState rightState : FillState}
+    {s t a b : State} (h : PreparedRelated p pass lane slice leftState rightState s t)
+    (ka : Divide.Keeps [] s a) (kb : Divide.Keeps [] t b) :
+    PreparedRelated p pass lane slice leftState rightState a b := by
+  refine ⟨h.left.of_keeps (ka.mono (by decide)), h.right.of_keeps (kb.mono (by decide)), ?_, ?_, ?_, ?_, ?_, ?_, h.indices⟩
+  · rw [ka.regs .rbp (by simp), kb.regs .rbp (by simp)]; exact h.bases
+  · rw [ka.regs .rsp (by simp), kb.regs .rsp (by simp)]; exact h.stacks
+  · unfold FillKernel.matrix
+    rw [ka.mem, kb.mem, ka.regs .rbp (by simp), kb.regs .rbp (by simp)]; exact h.matrices
+  · unfold AddressCalls.work
+    rw [ka.mem, kb.mem, ka.regs .rbp (by simp), kb.regs .rbp (by simp)]; exact h.work
+  · unfold FillKernel.matrix; rw [ka.mem, ka.regs .rbp (by simp)]; exact h.leftMatrix
+  · unfold FillKernel.matrix; rw [kb.mem, kb.regs .rbp (by simp)]; exact h.rightMatrix
+
+theorem check_context_ok (s : State) (p : Params) (pass lane slice : Nat)
+    (h : FillContext.Ready p pass lane slice (start pass slice) 0 s) : WP isa (.block check) s fun t =>
+      t.cf = decide (start pass slice < p.segmentLen) ∧ Divide.Keeps [] s t := by
+  refine (check_ok s).mono ?_
+  rintro t ⟨flag, keeps⟩
+  have minimum := h.parameters.segment_bound
+  refine ⟨?_, keeps⟩
+  rw [flag, h.position.index, h.position.segmentLength,
+    ReferenceMap.word_nat (start pass slice) (Nat.lt_of_le_of_lt (start_le _ _ _ minimum.1) minimum.2),
+    ReferenceMap.word_nat p.segmentLen minimum.2]
+
+theorem check_trace : RelCT isa (fun _ _ : State => True) (.block check) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by intro r hr; simp at hr)) (by taint_decide)
+
+theorem check_public_rel (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) :
+    RelCT isa (PreparedRelated p pass lane slice leftState rightState) (.block check)
+      (fun s t => PreparedRelated p pass lane slice leftState rightState s t ∧
+        s.cf = decide (start pass slice < p.segmentLen) ∧ t.cf = decide (start pass slice < p.segmentLen)) := by
+  have trace := check_trace.mono (P' := PreparedRelated p pass lane slice leftState rightState)
+    (fun _ _ _ => trivial) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨check_context_ok s p pass lane slice h.left, check_context_ok t p pass lane slice h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ⟨fa, ka⟩, ⟨fb, kb⟩⟩ := h
+  exact ⟨hp.of_keeps ka kb, fa, fb⟩
+
+theorem code_rel (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) :
+    RelCT isa (Related p pass lane slice leftState rightState) code (fun _ _ => True) := by
+  have branches : RelCT isa
+      (fun s t => PreparedRelated p pass lane slice leftState rightState s t ∧
+        s.cf = decide (start pass slice < p.segmentLen) ∧ t.cf = decide (start pass slice < p.segmentLen))
+      (.ite .b Impl.Argon2.X86_64.FillSegment.loop (.block [])) (fun _ _ => True) := by
+    refine RelCT.ite (by intro s t h; simp only [eval, h.2.1, h.2.2]) ?_ ?_
+    · intro s t ts tt a b hp ea eb
+      have active : start pass slice < p.segmentLen := by
+        have taken := hp.2
+        simp only [eval, hp.1.2.1, Option.some.injEq, decide_eq_true_eq] at taken
+        exact taken
+      have left := hp.1.1.left.activate active (start_active pass slice)
+      have right := hp.1.1.right.activate active (start_active pass slice)
+      have related : FillSegment.Related p pass lane slice (start pass slice)
+          (p.segmentLen - start pass slice) 0 leftState rightState s t :=
+        ⟨⟨left, right, hp.1.1.bases, hp.1.1.stacks, hp.1.1.matrices, hp.1.1.work⟩,
+          hp.1.1.leftMatrix, hp.1.1.rightMatrix, hp.1.1.indices⟩
+      exact FillSegment.loop_rel p pass lane slice (start pass slice) (p.segmentLen - start pass slice) 0
+        leftState rightState (by omega) (by omega) _ _ _ _ _ _ related ea eb
+    · 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)
+      exact noop.mono (fun _ _ _ => trivial) (fun _ _ h => h)
+  exact (prepare_public_rel p pass lane slice leftState rightState).seq
+    ((check_public_rel p pass lane slice leftState rightState).seq branches)
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCheck.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCheck.lean
new file mode 100644
index 0000000000..48fcc0e760
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCheck.lean
@@ -0,0 +1,49 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupPrepare
+
+/-! Check the prepared index before entering the nonempty segment loop. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+theorem Prepared.of_keeps {p : Params} {pass lane slice : Nat} {s a t : State}
+    (h : Prepared s a p pass lane slice) (k : Divide.Keeps [] a t) : Prepared s t p pass lane slice := by
+  have bp := k.regs .rbp (by decide)
+  have base : FillKernel.matrix t = FillKernel.matrix a := by unfold FillKernel.matrix; rw [k.mem, bp]
+  have work : AddressCalls.work t = AddressCalls.work a := by unfold AddressCalls.work; rw [k.mem, bp]
+  refine ⟨h.context.of_keeps (k.mono (by decide)), base.trans h.matrix, work.trans h.work,
+    ?_, k.rd.trans h.rd, k.wr.trans h.wr, ?_, k.mxcsr.trans h.mxcsr⟩
+  · intro r hr ne; exact (k.regs r (by simp)).trans (h.regs r hr ne)
+  · rw [k.mem]; exact h.frame
+
+theorem check_prepared_ok {p : Params} {pass lane slice : Nat} {s a : State}
+    (h : Prepared s a p pass lane slice) : WP isa (.block check) a fun t =>
+      Prepared s t p pass lane slice ∧ t.cf = decide (start pass slice < p.segmentLen) := by
+  refine (check_ok a).mono ?_
+  rintro t ⟨flag, keeps⟩
+  have minimum := h.context.parameters.segment_bound
+  refine ⟨h.of_keeps keeps, ?_⟩
+  rw [flag, h.context.position.index, h.context.position.segmentLength,
+    ReferenceMap.word_nat (start pass slice) (Nat.lt_of_le_of_lt (start_le _ _ _ minimum.1) minimum.2),
+    ReferenceMap.word_nat p.segmentLen minimum.2]
+
+theorem finished_prepared {p : Params} {pass lane slice : Nat} {s a t : State} {state : FillState}
+    (prepared : Prepared s a p pass lane slice) (finished : FillSegment.Finished a t p pass lane slice state) :
+    FillSegment.Finished s t p pass lane slice state := by
+  refine ⟨finished.represented, finished.matrix.trans prepared.matrix, finished.work.trans prepared.work,
+    finished.position, finished.layout, finished.cache, finished.matrixWork, finished.passWord, finished.lanesWord,
+    ?_, finished.rd.trans prepared.rd, finished.wr.trans prepared.wr, ?_, finished.mxcsr.trans prepared.mxcsr⟩
+  · intro r hr ne; exact (finished.regs r hr ne).trans (prepared.regs r hr ne)
+  · have firstFrame : Frame (FillBlock.writes s p) s.mem a.mem := by
+      apply prepared.frame.sub
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      exact ⟨⟨off (s.gpr .rbp) 8, 16⟩, by simp [FillBlock.writes], Region.sub_prefix (by decide)⟩
+    have rest := finished.frame
+    rw [FillBlock.writes, prepared.matrix, prepared.work,
+      prepared.regs .rsp (by simp [calleeSaved]) (by decide),
+      prepared.regs .rbp (by simp [calleeSaved]) (by decide)] at rest
+    exact firstFrame.trans rest
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupPrepare.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupPrepare.lean
new file mode 100644
index 0000000000..650c27c48f
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupPrepare.lean
@@ -0,0 +1,68 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupReset
+
+/-! The prepared context covers ordinary and empty first-segment suffixes. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+structure Prepared (s t : State) (p : Params) (pass lane slice : Nat) : Prop where
+  context : FillContext.Ready p pass lane slice (start pass slice) 0 t
+  matrix : FillKernel.matrix t = FillKernel.matrix s
+  work : AddressCalls.work t = AddressCalls.work s
+  regs : ∀ r ∈ calleeSaved, r ≠ .r15 → t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame [⟨off (s.gpr .rbp) 8, 8⟩] s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+
+theorem prepare_ok (s : State) (p : Params) (pass lane slice : Nat) (h : Ready p pass lane slice s) :
+    WP isa prepare s (Prepared s · p pass lane slice) := by
+  unfold prepare
+  refine WP.seq ((reset_ok s p pass lane slice h).mono ?_)
+  intro a reset
+  refine (index_ok a pass slice (reset.ready.reads 0 (by simp)) reset.words.passWord reset.words.sliceWord
+    (Nat.lt_trans h.parameters.passBound (by decide))
+    (Nat.lt_trans h.parameters.sliceBound (by decide))).mono ?_
+  rintro t ⟨value, keeps⟩
+  have core := reset.ready.of_state (by
+    intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl | rfl | rfl <;> exact keeps.regs _ (by decide)) keeps.mem keeps.rd keeps.wr
+  have cacheA : AddressCache.Invariant p pass lane slice 0 a :=
+    ⟨reset.ready.addressLayout, reset.ready.reads, reset.ready.write, reset.words, by decide, Or.inl rfl⟩
+  have cache := cacheA.of_state (by
+    intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl <;> exact keeps.regs _ (by decide)) keeps.mem keeps.rd keeps.wr
+  have base : FillKernel.matrix t = FillKernel.matrix a := by
+    unfold FillKernel.matrix; rw [keeps.mem, keeps.regs .rbp (by decide)]
+  have work : AddressCalls.work t = AddressCalls.work a := by
+    unfold AddressCalls.work; rw [keeps.mem, keeps.regs .rbp (by decide)]
+  refine ⟨⟨core.parameters, core.layout, cache, core.matrixWork,
+    ⟨cache.words.laneWord, core.laneLength, core.segmentLength, cache.words.sliceWord, value⟩, core.lanesWord⟩,
+    base.trans reset.matrix, work.trans reset.work, ?_, keeps.rd.trans reset.rd,
+    keeps.wr.trans reset.wr, ?_, keeps.mxcsr.trans reset.mxcsr⟩
+  · intro r hr ne
+    have outside : r ∉ [Reg.rcx, .r15] := 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 <;> simp_all
+    exact (keeps.regs r outside).trans (reset.regs r hr)
+  · rw [keeps.mem]; exact reset.frame
+
+theorem Prepared.represents {p : Params} {pass lane slice : Nat} {s t : State}
+    (ready : Ready p pass lane slice s) (h : Prepared 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
+  rw [h.matrix]
+  refine ⟨represented.size, ?_⟩
+  intro k hk
+  apply Eq.trans _ (represented.block k hk)
+  apply FillCompress.block_frame h.frame
+  intro r hr
+  simp only [List.mem_singleton] at hr
+  subst r
+  exact (ready.layout.matrixFrame.sub_left (Proof.Argon2.matrixCell_sub _ _ _ hk)).sub_right
+    (Offset.sub_base _ (by decide))
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReady.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReady.lean
new file mode 100644
index 0000000000..b2519da98c
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReady.lean
@@ -0,0 +1,67 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupSteps
+
+/-! Segment setup needs no previously valid cached block. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+structure Ready (p : Params) (pass lane slice : Nat) (s : State) : Prop where
+  parameters : FillContext.Parameters p pass lane slice
+  layout : FillKernel.Layout p s
+  addressLayout : 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 : ∃ old, AddressHeader.Words p pass lane slice old s
+  matrixWork : (⟨FillKernel.matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨AddressCalls.work s, 8192⟩
+  laneLength : s.gpr .r12 = BitVec.ofNat 64 p.laneLen
+  segmentLength : s.gpr .r13 = BitVec.ofNat 64 p.segmentLen
+  lanesWord : s.mem.readW (off (s.gpr .rbp) 184) 64 = BitVec.ofNat 64 p.lanes
+
+theorem Ready.of_state {p : Params} {pass lane slice : Nat} {s t : State}
+    (h : Ready p pass lane slice s)
+    (regs : ∀ r ∈ [Reg.rbp, .rsp, .rbx, .r12, .r13, .r14], t.gpr r = s.gpr r)
+    (mem : t.mem = s.mem) (rd : t.rd = s.rd) (wr : t.wr = s.wr) : Ready p pass lane slice t := by
+  have bp := regs .rbp (by simp)
+  have sp := regs .rsp (by simp)
+  have base : FillKernel.matrix t = FillKernel.matrix s := by unfold FillKernel.matrix; rw [mem, bp]
+  have work : AddressCalls.work t = AddressCalls.work s := by unfold AddressCalls.work; rw [mem, bp]
+  refine ⟨h.parameters, h.layout.of_preserved bp sp base work rd wr, ?_, ?_, ?_, ?_, ?_,
+    (regs .r12 (by simp)).trans h.laneLength, (regs .r13 (by simp)).trans h.segmentLength, ?_⟩
+  · constructor
+    · rw [rd, wr, bp]; exact h.addressLayout.frameRead
+    · rw [wr, work]; exact h.addressLayout.workWrite
+    · rw [bp, work]; exact h.addressLayout.frameWork
+    · rw [bp, sp]; exact h.addressLayout.frameStack
+    · rw [sp, work]; exact h.addressLayout.stackWork
+  · rw [rd, wr, bp]; exact h.reads
+  · rw [wr, bp]; exact h.write
+  · obtain ⟨old, words⟩ := h.words
+    refine ⟨old, ?_, (regs .rbx (by simp)).trans words.laneWord,
+      (regs .r14 (by simp)).trans words.sliceWord, ?_, ?_, ?_, ?_⟩
+    all_goals rw [mem, bp]
+    · exact words.passWord
+    · exact words.blocksWord
+    · exact words.passesWord
+    · exact words.variantWord
+    · exact words.counterWord
+  · rw [base, work]; exact h.matrixWork
+  · rw [mem, bp]; exact h.lanesWord
+
+theorem Ready.saved {p : Params} {pass lane slice : Nat} {s t : State}
+    (h : Ready p pass lane slice s) (saved : AddressCache.Saved s t) : Ready p pass lane slice t := by
+  have bp := congrFun saved.regs Reg.rbp
+  have sp := congrFun saved.regs Reg.rsp
+  have base : FillKernel.matrix t = FillKernel.matrix s := saved.read 232 (by decide) (by decide)
+  refine ⟨h.parameters, h.layout.of_preserved bp sp base saved.work_eq saved.rd saved.wr,
+    saved.ready, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+  · rw [saved.rd, saved.wr, bp]; exact h.reads
+  · rw [saved.wr, bp]; exact h.write
+  · obtain ⟨old, words⟩ := h.words
+    exact ⟨(s.gpr .rax).toNat, saved.words words (by simp)⟩
+  · rw [base, saved.work_eq]; exact h.matrixWork
+  · rw [saved.regs]; exact h.laneLength
+  · rw [saved.regs]; exact h.segmentLength
+  · exact (saved.read 184 (by decide) (by decide)).trans h.lanesWord
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReset.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReset.lean
new file mode 100644
index 0000000000..0f25ef5375
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupReset.lean
@@ -0,0 +1,48 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupReady
+
+/-! Reset the counter while preserving the segment header and matrix allocation. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+structure Reset (s t : State) (p : Params) (pass lane slice : Nat) : Prop where
+  ready : Ready p pass lane slice t
+  words : AddressHeader.Words p pass lane slice 0 t
+  matrix : FillKernel.matrix t = FillKernel.matrix s
+  work : 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 [⟨off (s.gpr .rbp) 8, 8⟩] s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+
+theorem reset_ok (s : State) (p : Params) (pass lane slice : Nat) (h : Ready p pass lane slice s) :
+    WP isa reset s (Reset s · p pass lane slice) := by
+  unfold reset
+  refine WP.seq ((register_ok s .rax 0).mono ?_)
+  rintro a ⟨value, keeps⟩
+  have next := h.of_state (by
+    intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl | rfl | rfl <;> exact keeps.regs _ (by decide)) keeps.mem keeps.rd keeps.wr
+  refine (AddressCache.save_ready a next.addressLayout next.write).mono ?_
+  intro t saved
+  obtain ⟨old, words⟩ := next.words
+  have matrixA : FillKernel.matrix a = FillKernel.matrix s := by
+    unfold FillKernel.matrix; rw [keeps.mem, keeps.regs .rbp (by decide)]
+  have workA : AddressCalls.work a = AddressCalls.work s := by
+    unfold AddressCalls.work; rw [keeps.mem, keeps.regs .rbp (by decide)]
+  refine ⟨next.saved saved, saved.words words value,
+    (saved.read 232 (by decide) (by decide)).trans matrixA, saved.work_eq.trans workA,
+    ?_, saved.rd.trans keeps.rd, saved.wr.trans keeps.wr, ?_, saved.mxcsr.trans keeps.mxcsr⟩
+  · intro r hr
+    have ne : r ∉ [Reg.rax] := 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 (congrFun saved.regs r).trans (keeps.regs r ne)
+  · have frame := saved.frame
+    rw [keeps.mem, keeps.regs .rbp (by decide)] at frame
+    exact frame
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupSteps.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupSteps.lean
new file mode 100644
index 0000000000..ae237bed15
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupSteps.lean
@@ -0,0 +1,88 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.SegmentSetup
+import VerifiedGarbage.Proof.Argon2.X86_64.FillContext
+
+/-! Select index two only in slice zero of pass zero. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+def start (pass slice : Nat) : Nat := if pass = 0 ∧ slice = 0 then 2 else 0
+
+theorem start_active (pass slice : Nat) : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ start pass slice := by
+  unfold start; split <;> omega
+
+theorem start_le (pass slice : Nat) (g : Nat) (minimum : 2 ≤ g) : start pass slice ≤ g := by
+  unfold start; split <;> omega
+
+theorem first_ok (s : State) (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 0) 8) :
+    WP isa (.block first) s fun t =>
+      t.zf = decide (s.mem.readW (off (s.gpr .rbp) 0) 64 = 0#64 ∧ s.gpr .r14 = 0#64) ∧
+      Divide.Keeps [.rcx] s t := by
+  apply WP.of_runBlock
+  simp only [first, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, State.load64,
+    ea_at, hr, execAlu, RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, RegUpd.zf_arithFlags,
+    reduceCtorEq, ite_true, ite_false,
+    show BitVec.signExtend 64 (0 : BitVec 32) = (0 : Addr) from rfl,
+    Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨?_, ?_⟩
+  · change ((s.mem.readW (off (s.gpr .rbp) 0) 64 ||| s.gpr .r14) - 0#64 == 0#64) = _
+    rw [BitVec.sub_zero]
+    apply Bool.eq_iff_iff.mpr
+    simp only [beq_iff_eq, BitVec.or_eq_zero_iff, decide_eq_true_eq]
+  · constructor
+    · intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      simp only [RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, hr, ite_false]
+    all_goals rfl
+
+theorem register_ok (s : State) (register : Reg) (value : BitVec 32) :
+    WP isa (.block [.mov register (.imm value)]) s fun t =>
+      t.gpr register = value.signExtend 64 ∧ Divide.Keeps [register] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, RegUpd.gpr_setReg,
+    ite_true, Option.map_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    simp only [RegUpd.gpr_setReg, hr, ite_false]
+  all_goals rfl
+
+theorem index_ok (s : State) (pass slice : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 0) 8)
+    (passWord : s.mem.readW (off (s.gpr .rbp) 0) 64 = BitVec.ofNat 64 pass)
+    (sliceWord : s.gpr .r14 = BitVec.ofNat 64 slice)
+    (passBound : pass < 2 ^ 64) (sliceBound : slice < 2 ^ 64) : WP isa index s fun t =>
+      t.gpr .r15 = BitVec.ofNat 64 (start pass slice) ∧ Divide.Keeps [.rcx, .r15] s t := by
+  unfold index
+  refine WP.seq ((first_ok s hr).mono ?_)
+  rintro a ⟨flag, keeps⟩
+  have firstFlag : a.zf = decide (pass = 0 ∧ slice = 0) := by
+    rw [flag, passWord, sliceWord]
+    have passZero : BitVec.ofNat 64 pass = 0#64 ↔ pass = 0 := ReferenceMap.word_zero pass passBound
+    have sliceZero : BitVec.ofNat 64 slice = 0#64 ↔ slice = 0 := ReferenceMap.word_zero slice sliceBound
+    simp only [passZero, sliceZero]
+  refine WP.ite (decide (pass = 0 ∧ slice = 0)) (by simp only [eval, firstFlag]) ?_ ?_
+  · intro mode
+    refine (register_ok a .r15 2).mono ?_
+    rintro t ⟨value, changed⟩
+    refine ⟨?_, (keeps.mono (by decide)).trans (changed.mono (by decide))⟩
+    unfold start; simp only [of_decide_eq_true mode]; exact value
+  · intro mode
+    refine (register_ok a .r15 0).mono ?_
+    rintro t ⟨value, changed⟩
+    refine ⟨?_, (keeps.mono (by decide)).trans (changed.mono (by decide))⟩
+    unfold start; simp only [of_decide_eq_false mode, ite_false]; exact value
+
+theorem check_ok (s : State) : WP isa (.block check) s fun t =>
+    t.cf = decide ((s.gpr .r15).toNat < (s.gpr .r13).toNat) ∧ Divide.Keeps [] s t := by
+  apply WP.of_runBlock
+  simp only [check, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.cf_arithFlags, Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r _; exact congrFun (RegUpd.gpr_arithFlags _ _ _ _) r
+  all_goals rfl
+
+end VG.Proof.Argon2.X86_64.SegmentSetup
diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupTrace.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupTrace.lean
new file mode 100644
index 0000000000..5dc69d065f
--- /dev/null
+++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupTrace.lean
@@ -0,0 +1,100 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupPrepare
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Cache reset and initial-index selection branch only on public parameters. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+structure RelatedReady (p : Params) (pass lane slice : Nat) (s t : State) : Prop where
+  left : Ready p pass lane slice s
+  right : Ready p pass lane slice t
+  bases : s.gpr .rbp = t.gpr .rbp
+  stacks : s.gpr .rsp = t.gpr .rsp
+  matrices : FillKernel.matrix s = FillKernel.matrix t
+  work : AddressCalls.work s = AddressCalls.work t
+
+theorem RelatedReady.of_keeps {p : Params} {pass lane slice : Nat} {s t a b : State}
+    (h : RelatedReady p pass lane slice s t)
+    (ka : Divide.Keeps [.rax, .rcx, .r15] s a) (kb : Divide.Keeps [.rax, .rcx, .r15] t b) :
+    RelatedReady p pass lane slice a b := by
+  have protectedRegs : ∀ r ∈ [Reg.rbp, .rsp, .rbx, .r12, .r13, .r14], r ∉ [Reg.rax, .rcx, .r15] := by decide
+  refine ⟨h.left.of_state (fun r hr => ka.regs r (protectedRegs r hr)) ka.mem ka.rd ka.wr,
+    h.right.of_state (fun r hr => kb.regs r (protectedRegs r hr)) kb.mem kb.rd kb.wr, ?_, ?_, ?_, ?_⟩
+  · rw [ka.regs .rbp (by decide), kb.regs .rbp (by decide)]; exact h.bases
+  · rw [ka.regs .rsp (by decide), kb.regs .rsp (by decide)]; exact h.stacks
+  · unfold FillKernel.matrix
+    rw [ka.mem, kb.mem, ka.regs .rbp (by decide), kb.regs .rbp (by decide)]
+    exact h.matrices
+  · unfold AddressCalls.work
+    rw [ka.mem, kb.mem, ka.regs .rbp (by decide), kb.regs .rbp (by decide)]
+    exact h.work
+
+theorem reset_trace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp) reset (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 reset_public_rel (p : Params) (pass lane slice : Nat) :
+    RelCT isa (RelatedReady p pass lane slice) reset (RelatedReady p pass lane slice) := by
+  have trace := reset_trace.mono (P' := RelatedReady p pass lane slice)
+    (fun _ _ h => h.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨reset_ok s p pass lane slice h.left, reset_ok t p pass lane slice h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨ha.ready, hb.ready, ?_, ?_, ha.matrix.trans (hp.matrices.trans hb.matrix.symm),
+    ha.work.trans (hp.work.trans hb.work.symm)⟩
+  · rw [ha.regs .rbp (by simp [calleeSaved]), hb.regs .rbp (by simp [calleeSaved])]; exact hp.bases
+  · rw [ha.regs .rsp (by simp [calleeSaved]), hb.regs .rsp (by simp [calleeSaved])]; exact hp.stacks
+
+theorem first_spec_ok (s : State) (p : Params) (pass lane slice : Nat) (h : Ready p pass lane slice s) :
+    WP isa (.block first) s fun t => t.zf = decide (pass = 0 ∧ slice = 0) ∧ Divide.Keeps [.rcx] s t := by
+  obtain ⟨old, words⟩ := h.words
+  refine (first_ok s (h.reads 0 (by simp))).mono ?_
+  rintro t ⟨flag, keeps⟩
+  refine ⟨?_, keeps⟩
+  rw [flag, words.passWord, words.sliceWord]
+  have passZero : BitVec.ofNat 64 pass = 0#64 ↔ pass = 0 :=
+    ReferenceMap.word_zero pass (Nat.lt_trans h.parameters.passBound (by decide))
+  have sliceZero : BitVec.ofNat 64 slice = 0#64 ↔ slice = 0 :=
+    ReferenceMap.word_zero slice (Nat.lt_trans h.parameters.sliceBound (by decide))
+  simp only [passZero, sliceZero]
+
+theorem first_trace : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp) (.block first) (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 first_public_rel (p : Params) (pass lane slice : Nat) :
+    RelCT isa (RelatedReady p pass lane slice) (.block first)
+      (fun s t => RelatedReady p pass lane slice s t ∧ s.zf = t.zf) := by
+  have trace := first_trace.mono (P' := RelatedReady p pass lane slice)
+    (fun _ _ h => h.bases) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨first_spec_ok s p pass lane slice h.left, first_spec_ok t p pass lane slice h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ⟨fa, ka⟩, ⟨fb, kb⟩⟩ := h
+  exact ⟨hp.of_keeps (ka.mono (by decide)) (kb.mono (by decide)), fa.trans fb.symm⟩
+
+theorem index_trace (p : Params) (pass lane slice : Nat) :
+    RelCT isa (RelatedReady p pass lane slice) index (fun _ _ => True) := by
+  have two : RelCT isa (fun _ _ : State => True) (.block [.mov .r15 (.imm 2)]) (fun _ _ => True) :=
+    RelCT.taint (A := taint) (Taint.ofRegs [])
+      (fun _ _ _ => Taint.agree_ofRegs (by intro r hr; simp at hr)) (by taint_decide)
+  have zero : RelCT isa (fun _ _ : State => True) (.block [.mov .r15 (.imm 0)]) (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 (fun s t => RelatedReady p pass lane slice s t ∧ s.zf = t.zf)
+      (.ite .e (.block [.mov .r15 (.imm 2)]) (.block [.mov .r15 (.imm 0)])) (fun _ _ => True) :=
+    RelCT.ite (by intro s t h; simp only [eval, h.2])
+      (two.mono (fun _ _ _ => trivial) (fun _ _ h => h))
+      (zero.mono (fun _ _ _ => trivial) (fun _ _ h => h))
+  exact (first_public_rel p pass lane slice).seq branches
+
+theorem prepare_trace (p : Params) (pass lane slice : Nat) :
+    RelCT isa (RelatedReady p pass lane slice) prepare (fun _ _ => True) :=
+  (reset_public_rel p pass lane slice).seq (index_trace p pass lane slice)
+
+end VG.Proof.Argon2.X86_64.SegmentSetup