Argon2 on x86-64: prove complete active-cell filling step

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

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

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

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

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

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