Argon2 on x86-64: prove filling pointers and block writes

lean/VerifiedGarbage/Impl/Argon2/X86_64/FillPointers.lean

@@ -0,0 +1,35 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.BlockAddress
+import VerifiedGarbage.Impl.Argon2.X86_64.FillColumn
+
+/-! Prepare the block pointers for one filling operation. `r8` is the matrix
+base; `rbx`, `r12`–`r15` retain the loop position. Reference mapping supplied
+the reference lane and column in `r9` and `rdi`. The current pointer is saved
+in `r10`, with the previous and reference pointers in `rdi` and `rsi`.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillPointers
+
+open VG.X86_64
+
+def saveReference : List Instr := [.mov .rsi (.reg .rdi)]
+
+def currentArgs : List Instr := [.mov .rax (.reg .rbx)]
+
+def previousArgs : List Instr := [
+  .mov .r10 (.reg .rax), .mov .rcx (.reg .rdi), .mov .rax (.reg .rbx)]
+
+def referenceArgs : List Instr := [
+  .mov .r11 (.reg .rax), .mov .rcx (.reg .rsi), .mov .rax (.reg .r9)]
+
+def finishArgs : List Instr := [.mov .rsi (.reg .rax), .mov .rdi (.reg .r11)]
+
+def current : Prog isa := .seq (.block currentArgs) BlockAddress.code
+
+def previous : Prog isa := .seq (.block previousArgs) BlockAddress.code
+
+def reference : Prog isa := .seq (.block referenceArgs) BlockAddress.code
+
+def code : Prog isa := .seq (.block saveReference) (.seq FillColumn.code
+  (.seq current (.seq previous (.seq reference (.block finishArgs)))))
+
+end VG.Impl.Argon2.X86_64.FillPointers

lean/VerifiedGarbage/Impl/Argon2/X86_64/FillWrite.lean

@@ -0,0 +1,24 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Write the compression result into the current matrix block. `rsi` points
+to the temporary result and `rdi` to the matrix destination; `r9` is the public
+pass number. Pass zero copies the result, and later passes XOR the old cell.
+Both paths visit every word in ascending order.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillWrite
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def word (xorOld : Bool) (i : Nat) : List Instr :=
+  [.mov .rax (.mem (at_ .rsi (8 * i)))] ++
+    (if xorOld then [.alu .xor .rax (.mem (at_ .rdi (8 * i)))] else []) ++
+    [.store (at_ .rdi (8 * i)) .rax]
+
+def words (xorOld : Bool) (n : Nat) : List Instr := (List.range n).flatMap (word xorOld)
+
+def code : Prog isa := .seq (.block [.alu .cmp .r9 (.imm 0)])
+  (.ite .e (.block (words false 128)) (.block (words true 128)))
+
+end VG.Impl.Argon2.X86_64.FillWrite

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointers.lean

@@ -0,0 +1,99 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointersArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.FillColumn
+import VerifiedGarbage.Proof.Argon2.X86_64.BlockAddress
+
+/-! Compose the matrix addresses while retaining the enclosing loop position. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+def address (base lane column q : Addr) : Addr := (lane * q + column) * 1024 + base
+
+def column (s : State) : Addr := s.gpr .r14 * s.gpr .r13 + s.gpr .r15
+
+def predecessor (s : State) : Addr :=
+  (if column s = 0 then s.gpr .r12 else column s) - 1
+
+def changed : List Reg := [.rax, .rdx, .rcx, .rdi, .rsi, .r10, .r11]
+
+theorem current_ok (s : State) : WP isa current s fun t =>
+    t.gpr .rax = address (s.gpr .r8) (s.gpr .rbx) (s.gpr .rcx) (s.gpr .r12) ∧
+    Divide.Keeps [.rax, .rdx] s t := by
+  unfold current
+  refine WP.seq ((currentArgs_ok s).mono ?_)
+  rintro a ⟨lane, ka⟩
+  refine (BlockAddress.code_ok a).mono ?_
+  rintro t ⟨pointer, kt⟩
+  refine ⟨?_, (ka.mono (by simp)).trans kt⟩
+  rw [pointer, lane, ka.regs .r12 (by decide), ka.regs .rcx (by decide), ka.regs .r8 (by decide), address]
+
+theorem previous_ok (s : State) : WP isa previous s fun t =>
+    t.gpr .r10 = s.gpr .rax ∧
+    t.gpr .rax = address (s.gpr .r8) (s.gpr .rbx) (s.gpr .rdi) (s.gpr .r12) ∧
+    Divide.Keeps [.rax, .rdx, .rcx, .r10] s t := by
+  unfold previous
+  refine WP.seq ((previousArgs_ok s).mono ?_)
+  rintro a ⟨saved, col, lane, ka⟩
+  refine (BlockAddress.code_ok a).mono ?_
+  rintro t ⟨pointer, kt⟩
+  refine ⟨(kt.regs .r10 (by decide)).trans saved, ?_,
+    (ka.mono (by simp)).trans (kt.mono (by simp))⟩
+  rw [pointer, lane, col, ka.regs .r12 (by decide), ka.regs .r8 (by decide), address]
+
+theorem reference_ok (s : State) : WP isa reference s fun t =>
+    t.gpr .r11 = s.gpr .rax ∧
+    t.gpr .rax = address (s.gpr .r8) (s.gpr .r9) (s.gpr .rsi) (s.gpr .r12) ∧
+    Divide.Keeps [.rax, .rdx, .rcx, .r11] s t := by
+  unfold reference
+  refine WP.seq ((referenceArgs_ok s).mono ?_)
+  rintro a ⟨saved, col, lane, ka⟩
+  refine (BlockAddress.code_ok a).mono ?_
+  rintro t ⟨pointer, kt⟩
+  refine ⟨(kt.regs .r11 (by decide)).trans saved, ?_,
+    (ka.mono (by simp)).trans (kt.mono (by simp))⟩
+  rw [pointer, lane, col, ka.regs .r12 (by decide), ka.regs .r8 (by decide), address]
+
+theorem code_ok (s : State) : WP isa code s fun t =>
+    t.gpr .r10 = address (s.gpr .r8) (s.gpr .rbx) (column s) (s.gpr .r12) ∧
+    t.gpr .rdi = address (s.gpr .r8) (s.gpr .rbx) (predecessor s) (s.gpr .r12) ∧
+    t.gpr .rsi = address (s.gpr .r8) (s.gpr .r9) (s.gpr .rdi) (s.gpr .r12) ∧
+    Divide.Keeps changed s t := by
+  unfold code
+  refine WP.seq ((saveReference_ok s).mono ?_)
+  rintro a ⟨refColumn, ka⟩
+  refine WP.seq ((FillColumn.code_ok a).mono ?_)
+  rintro b ⟨curColumn, prevColumn, kb⟩
+  refine WP.seq ((current_ok b).mono ?_)
+  rintro c ⟨curPointer, kc⟩
+  refine WP.seq ((previous_ok c).mono ?_)
+  rintro d ⟨savedCurrent, prevPointer, kd⟩
+  refine WP.seq ((reference_ok d).mono ?_)
+  rintro e ⟨savedPrevious, refPointer, ke⟩
+  refine (finishArgs_ok e).mono ?_
+  rintro t ⟨referenceResult, previousResult, kt⟩
+  have coords : column a = column s := by
+    unfold column
+    rw [ka.regs .r14 (by decide), ka.regs .r13 (by decide), ka.regs .r15 (by decide)]
+  refine ⟨?_, ?_, ?_, ?_⟩
+  · rw [kt.regs .r10 (by decide), ke.regs .r10 (by decide), savedCurrent, curPointer,
+      kb.regs .r8 (by decide), ka.regs .r8 (by decide), kb.regs .rbx (by decide),
+      ka.regs .rbx (by decide), kb.regs .r12 (by decide), ka.regs .r12 (by decide), curColumn]
+    exact congrArg (fun col => address (s.gpr .r8) (s.gpr .rbx) col (s.gpr .r12)) coords
+  · rw [previousResult, savedPrevious, prevPointer, kc.regs .r8 (by decide),
+      kc.regs .rbx (by decide), kc.regs .rdi (by decide), kc.regs .r12 (by decide),
+      kb.regs .r8 (by decide), ka.regs .r8 (by decide), kb.regs .rbx (by decide),
+      ka.regs .rbx (by decide), kb.regs .r12 (by decide), ka.regs .r12 (by decide), prevColumn]
+    change address _ _ ((if column a = 0 then a.gpr .r12 else column a) - 1) _ = _
+    rw [coords, ka.regs .r12 (by decide), predecessor]
+  · rw [referenceResult, refPointer, kd.regs .r8 (by decide), kd.regs .r9 (by decide),
+      kd.regs .rsi (by decide), kd.regs .r12 (by decide), kc.regs .r8 (by decide),
+      kc.regs .r9 (by decide), kc.regs .rsi (by decide), kc.regs .r12 (by decide),
+      kb.regs .r8 (by decide), kb.regs .r9 (by decide), kb.regs .rsi (by decide),
+      kb.regs .r12 (by decide), ka.regs .r8 (by decide), ka.regs .r9 (by decide),
+      ka.regs .r12 (by decide), refColumn]
+  · exact (((((ka.mono (by simp [changed])).trans (kb.mono (by simp [changed]))).trans
+      (kc.mono (by simp [changed]))).trans (kd.mono (by simp [changed]))).trans
+      (ke.mono (by simp [changed]))).trans (kt.mono (by simp [changed]))
+
+end VG.Proof.Argon2.X86_64.FillPointers

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersArgs.lean

@@ -0,0 +1,76 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillPointers
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! Short register-setup steps for the filling pointers. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+theorem saveReference_ok (s : State) : WP isa (.block saveReference) s fun t =>
+    t.gpr .rsi = s.gpr .rdi ∧ Divide.Keeps [.rsi] s t := by
+  apply WP.of_runBlock
+  simp only [saveReference, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg, ite_true]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    exact ite_eq_right hr
+  all_goals rfl
+
+theorem currentArgs_ok (s : State) : WP isa (.block currentArgs) s fun t =>
+    t.gpr .rax = s.gpr .rbx ∧ Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [currentArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg, ite_true]
+  refine ⟨trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    exact ite_eq_right hr
+  all_goals rfl
+
+theorem previousArgs_ok (s : State) : WP isa (.block previousArgs) s fun t =>
+    t.gpr .r10 = s.gpr .rax ∧ t.gpr .rcx = s.gpr .rdi ∧ t.gpr .rax = s.gpr .rbx ∧
+    Divide.Keeps [.r10, .rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [previousArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg,
+    reduceCtorEq, ite_true, ite_false]
+  refine ⟨trivial, trivial, trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+    simp only [RegUpd.gpr_setReg, hr.1, hr.2.1, hr.2.2, ite_false]
+  all_goals rfl
+
+theorem referenceArgs_ok (s : State) : WP isa (.block referenceArgs) s fun t =>
+    t.gpr .r11 = s.gpr .rax ∧ t.gpr .rcx = s.gpr .rsi ∧ t.gpr .rax = s.gpr .r9 ∧
+    Divide.Keeps [.r11, .rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [referenceArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg,
+    reduceCtorEq, ite_true, ite_false]
+  refine ⟨trivial, trivial, trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+    simp only [RegUpd.gpr_setReg, hr.1, hr.2.1, hr.2.2, ite_false]
+  all_goals rfl
+
+theorem finishArgs_ok (s : State) : WP isa (.block finishArgs) s fun t =>
+    t.gpr .rsi = s.gpr .rax ∧ t.gpr .rdi = s.gpr .r11 ∧
+    Divide.Keeps [.rsi, .rdi] s t := by
+  apply WP.of_runBlock
+  simp only [finishArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    Option.map_some, Option.some.injEq, exists_eq_left', RegUpd.gpr_setReg,
+    reduceCtorEq, ite_true, ite_false]
+  refine ⟨trivial, trivial, ?_⟩
+  constructor
+  · intro r hr
+    simp only [List.mem_cons, List.not_mem_nil, or_false, not_or] at hr
+    simp only [RegUpd.gpr_setReg, hr.1, hr.2, ite_false]
+  all_goals rfl
+
+end VG.Proof.Argon2.X86_64.FillPointers

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersCT.lean

@@ -0,0 +1,17 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillPointersLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! The pointer setup only branches on the public current column.
+Reference coordinates may differ without changing its execution trace. -/
+
+namespace VG.Proof.Argon2.X86_64.FillPointers
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillPointers
+
+theorem code_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.r8, .rbx, .r12, .r13, .r14, .r15], s.gpr r = t.gpr r) code
+    (fun s t => ∀ r ∈ [Reg.r10], s.gpr r = t.gpr r) :=
+  RelCT.taintRegs (τ := Taint.ofRegs [.r8, .rbx, .r12, .r13, .r14, .r15])
+    (fun _ _ h => Taint.agree_ofRegs h) [Reg.r10] (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.FillPointers

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillPointersLit.lean

@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FillPointers
+
+/-! Checked literal of the complete filling pointer setup. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FillPointers.code
+
+end VG

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWrite.lean

@@ -0,0 +1,52 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillWritePrefix
+import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidates
+
+/-! Whole-block first-pass copying and later-pass XOR, with a frame proof. -/
+
+namespace VG.Proof.Argon2.X86_64.FillWrite
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillWrite
+
+theorem code_ok (s : State)
+    (hs : (⟨s.gpr .rsi, 1024⟩ : Region) ∈ s.rd ++ s.wr)
+    (hw : (⟨s.gpr .rdi, 1024⟩ : Region) ∈ s.wr)
+    (hd : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩) :
+    WP isa code s fun t =>
+      blockAt t.mem (s.gpr .rdi) =
+        (if s.gpr .r9 = 0 then blockAt s.mem (s.gpr .rsi)
+          else xorBlock (blockAt s.mem (s.gpr .rsi)) (blockAt s.mem (s.gpr .rdi))) ∧
+      Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by
+  unfold code
+  refine WP.seq ((CountCandidates.compare_ok s).mono ?_)
+  rintro a ⟨flag, ka⟩
+  have src : a.gpr .rsi = s.gpr .rsi := ka.regs .rsi (by simp)
+  have dest : a.gpr .rdi = s.gpr .rdi := ka.regs .rdi (by simp)
+  have hs' : (⟨a.gpr .rsi, 1024⟩ : Region) ∈ a.rd ++ a.wr := by
+    rw [src, ka.rd, ka.wr]; exact hs
+  have hw' : (⟨a.gpr .rdi, 1024⟩ : Region) ∈ a.wr := by
+    rw [dest, ka.wr]; exact hw
+  have hd' : (⟨a.gpr .rsi, 1024⟩ : Region).Disjoint ⟨a.gpr .rdi, 1024⟩ := by
+    rw [src, dest]; exact hd
+  refine WP.ite (decide (s.gpr .r9 = 0)) (by simp only [eval, flag]) ?_ ?_
+  · intro h
+    have zero := of_decide_eq_true h
+    refine (prefix_ok false 128 (by decide) a hs' hw' hd').mono ?_
+    rintro t ⟨written, frame, keeps, mx⟩
+    refine ⟨?_, ?_, ?_, mx.trans ka.mxcsr⟩
+    · rw [dest] at written
+      rw [ite_eq_left zero, written_block written]
+      simp only [result, Bool.false_eq_true, ite_false, ka.mem, src]
+    · rw [dest, ka.mem] at frame; exact frame
+    · exact (show CopyKeeps s a from ⟨fun r _ => ka.regs r (by simp), ka.rd, ka.wr⟩).trans keeps
+  · intro h
+    have nonzero := of_decide_eq_false h
+    refine (prefix_ok true 128 (by decide) a hs' hw' hd').mono ?_
+    rintro t ⟨written, frame, keeps, mx⟩
+    refine ⟨?_, ?_, ?_, mx.trans ka.mxcsr⟩
+    · rw [dest] at written
+      rw [ite_eq_right nonzero, written_block written]
+      simp only [result, ite_true, ka.mem, src]
+    · rw [dest, ka.mem] at frame; exact frame
+    · exact (show CopyKeeps s a from ⟨fun r _ => ka.regs r (by simp), ka.rd, ka.wr⟩).trans keeps
+
+end VG.Proof.Argon2.X86_64.FillWrite

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCT.lean

@@ -0,0 +1,16 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillWriteLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Both write paths have a public, fixed sequence of memory accesses. -/
+
+namespace VG.Proof.Argon2.X86_64.FillWrite
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillWrite
+
+theorem code_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.r9, .rdi, .rsi], s.gpr r = t.gpr r) code
+    (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.r9, .rdi, .rsi])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.FillWrite

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteLit.lean

@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FillWrite
+
+/-! Checked literal of the complete copy/XOR block write. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FillWrite.code
+
+end VG