Argon2 on x86-64: prove independent-address input preparation

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressHeader.lean

@@ -0,0 +1,31 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Fill the first seven words of an independently generated address input.
+The input pointer is `rdi`; its remaining words were cleared once. The frame
+holds pass (0), address counter (8), passes (72), variant (112), blocks (240).
+Lane and slice remain in `rbx` and `r14`. The counter is supplied after the
+public address-generation loop advances it to its one-based value.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressHeader
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def registerWord (i : Nat) (r : Reg) : List Instr := [.store (at_ .rdi (8 * i)) r]
+
+def frameWord (i offset : Nat) : List Instr :=
+  [.mov .rax (.mem (at_ .rbp offset)), .store (at_ .rdi (8 * i)) .rax]
+
+def frameOffset (i : Nat) : Nat :=
+  if i = 0 then 0 else if i = 3 then 240 else if i = 4 then 72 else if i = 5 then 112 else 8
+
+def field (i : Nat) : List Instr :=
+  if i = 1 then registerWord i .rbx else if i = 2 then registerWord i .r14
+  else frameWord i (frameOffset i)
+
+def fields (n : Nat) : List Instr := (List.range n).flatMap field
+
+def code : Prog isa := .block (fields 7)
+
+end VG.Impl.Argon2.X86_64.AddressHeader

lean/VerifiedGarbage/Impl/Argon2/X86_64/ClearBlock.lean

@@ -0,0 +1,18 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Compress
+
+/-! Clear one 1024-byte address-generation block. The destination in `rdi`
+is public; neither the old contents nor any input value affects the trace.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ClearBlock
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def word (i : Nat) : List Instr := [.store (at_ .rdi (8 * i)) .rax]
+
+def words (n : Nat) : List Instr := (List.range n).flatMap word
+
+def code : Prog isa := .seq (.block [.mov .rax (.imm 0)]) (.block (words 128))
+
+end VG.Impl.Argon2.X86_64.ClearBlock

lean/VerifiedGarbage/Proof/Argon2/AddressInput.lean

@@ -0,0 +1,19 @@
+import VerifiedGarbage.Spec.Argon2
+
+/-! The input block of the reviewed independent-address specification. -/
+
+namespace VG.Proof.Argon2
+
+open VG.Spec.Argon2
+
+def addressInput (p : Params) (pass lane slice counter : Nat) : Block :=
+  zeroBlock |>.set 0 (BitVec.ofNat 64 pass) |>.set 1 (BitVec.ofNat 64 lane)
+    |>.set 2 (BitVec.ofNat 64 slice) |>.set 3 (BitVec.ofNat 64 p.blocks)
+    |>.set 4 (BitVec.ofNat 64 p.passes) |>.set 5 (BitVec.ofNat 64 p.variant.code)
+    |>.set 6 (BitVec.ofNat 64 counter)
+
+theorem addressBlock_eq (p : Params) (pass lane slice counter : Nat) :
+    addressBlock p pass lane slice counter =
+      compress zeroBlock (compress zeroBlock (addressInput p pass lane slice counter)) := rfl
+
+end VG.Proof.Argon2

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressHeader.lean

@@ -0,0 +1,100 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressHeaderWords
+import VerifiedGarbage.Proof.Framework.X86_64.Inline
+
+/-! Compose the seven input fields, preserving frame reads across every write. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressHeader
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressHeader
+
+def value (s : State) (i : Nat) : Addr :=
+  if i = 1 then s.gpr .rbx else if i = 2 then s.gpr .r14
+  else s.mem.readW (off (s.gpr .rbp) (frameOffset i)) 64
+
+def headerMem (s : State) (p : Addr) : Nat → Mem
+  | 0 => s.mem
+  | n + 1 => (headerMem s p n).writeW (off p (8 * n)) (value s n)
+
+theorem field_ok (s : State) (i : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) (frameOffset i)) 8)
+    (hw : InRegions s.wr (off (s.gpr .rdi) (8 * i)) 8) :
+    WP isa (.block (field i)) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rdi) (8 * i)) (value s i) ∧
+      CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by
+  unfold field value
+  by_cases one : i = 1
+  · simp only [one, ite_true]
+    refine (registerWord_ok s 1 .rbx (one ▸ hw)).mono ?_
+    rintro t ⟨mem, regs, rd, wr, mx⟩
+    exact ⟨mem, ⟨fun r _ => congrFun regs r, rd, wr⟩, mx⟩
+  · simp only [one, ite_false]
+    by_cases two : i = 2
+    · simp only [two, ite_true]
+      refine (registerWord_ok s 2 .r14 (two ▸ hw)).mono ?_
+      rintro t ⟨mem, regs, rd, wr, mx⟩
+      exact ⟨mem, ⟨fun r _ => congrFun regs r, rd, wr⟩, mx⟩
+    · simp only [two, ite_false]
+      refine (frameWord_ok s i (frameOffset i) hr hw).mono ?_
+      rintro t ⟨mem, regs, rd, wr, mx⟩
+      exact ⟨mem, ⟨regs, rd, wr⟩, mx⟩
+
+theorem offset_bound : ∀ i < 7, frameOffset i + 8 ≤ 272 := by decide +kernel
+
+theorem offset_read (s : State) (i : Nat)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8) :
+    InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) (frameOffset i)) 8 := by
+  apply reads
+  unfold frameOffset
+  split <;> [simp; skip]
+  split <;> [simp; skip]
+  split <;> [simp; skip]
+  split <;> simp
+
+theorem value_kept {s t : State} (keeps : CopyKeeps s t)
+    (hf : Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem)
+    (sep : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩)
+    (i : Nat) (hi : i < 7) : value t i = value s i := by
+  unfold value
+  rw [keeps.1 .rbx (by decide), keeps.1 .r14 (by decide), keeps.1 .rbp (by decide)]
+  have read : t.mem.readW (off (s.gpr .rbp) (frameOffset i)) 64 =
+      s.mem.readW (off (s.gpr .rbp) (frameOffset i)) 64 :=
+    hf.readW (r := ⟨s.gpr .rbp, 272⟩)
+      (Offset.contains_base _ (offset_bound i hi)
+        (Nat.lt_of_le_of_lt (Nat.le_trans (Nat.le_add_right _ _) (offset_bound i hi)) (by decide)))
+      (by intro r hr; simp only [List.mem_singleton] at hr; subst r; exact sep) (by decide)
+  rw [read]
+
+theorem prefix_ok (n : Nat) (hn : n ≤ 7) (s : State)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (write : Covers [⟨s.gpr .rdi, 1024⟩] s.wr)
+    (sep : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩) :
+    WP isa (.block (fields n)) s fun t =>
+      t.mem = headerMem s (s.gpr .rdi) n ∧
+      Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by
+  induction n with
+  | zero => exact WP.block_nil ⟨rfl, Frame.refl _ _, CopyKeeps.refl s, rfl⟩
+  | succ n ih =>
+    simp only [fields, List.range_succ, List.flatMap_append, List.flatMap_cons,
+      List.flatMap_nil, List.append_nil]
+    apply WP.block_append
+    refine (ih (by omega)).mono ?_
+    rintro a ⟨mem, frame, keeps, mx⟩
+    have dest : a.gpr .rdi = s.gpr .rdi := keeps.1 .rdi (by decide)
+    have read : InRegions (a.rd ++ a.wr) (off (a.gpr .rbp) (frameOffset n)) 8 := by
+      rw [keeps.2.1, keeps.2.2, keeps.1 .rbp (by decide)]
+      exact offset_read s n reads
+    have writable : InRegions a.wr (off (a.gpr .rdi) (8 * n)) 8 := by
+      rw [dest, keeps.2.2]
+      exact write _ _ ⟨⟨s.gpr .rdi, 1024⟩, by simp,
+        Offset.contains_base _ (d := 8 * n) (n := 8) (k := 1024) (by omega) (by omega)⟩
+    refine (field_ok a n read writable).mono ?_
+    rintro t ⟨mem', keeps', mx'⟩
+    have value' := value_kept keeps frame sep n (by omega)
+    refine ⟨?_, ?_, keeps.trans keeps', mx'.trans mx⟩
+    · rw [mem', dest, value', mem]
+      rfl
+    · rw [mem', dest]
+      exact frame.writeW (r := ⟨s.gpr .rdi, 1024⟩) (by simp) _
+        (Offset.contains_base _ (by omega) (by omega))
+
+end VG.Proof.Argon2.X86_64.AddressHeader

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressHeaderCorrect.lean

@@ -0,0 +1,64 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressHeader
+import VerifiedGarbage.Proof.Argon2.AddressInput
+
+/-! The prepared input agrees with RFC 9106's seven public address words. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressHeader
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressHeader
+
+def input (s : State) : Block :=
+  zeroBlock |>.set 0 (value s 0) |>.set 1 (value s 1) |>.set 2 (value s 2)
+    |>.set 3 (value s 3) |>.set 4 (value s 4) |>.set 5 (value s 5) |>.set 6 (value s 6)
+
+theorem headerMem_block (s : State) (p : Addr) (zero : blockAt s.mem p = zeroBlock) :
+    blockAt (headerMem s p 7) p = input s := by
+  rw [headerMem, blockAt_write_nat _ p 6 (by decide),
+    headerMem, blockAt_write_nat _ p 5 (by decide),
+    headerMem, blockAt_write_nat _ p 4 (by decide),
+    headerMem, blockAt_write_nat _ p 3 (by decide),
+    headerMem, blockAt_write_nat _ p 2 (by decide),
+    headerMem, blockAt_write_nat _ p 1 (by decide),
+    headerMem, blockAt_write_nat _ p 0 (by decide), headerMem, zero]
+  rfl
+
+theorem code_ok (s : State)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (write : Covers [⟨s.gpr .rdi, 1024⟩] s.wr)
+    (sep : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩)
+    (zero : blockAt s.mem (s.gpr .rdi) = zeroBlock) :
+    WP isa code s fun t => blockAt t.mem (s.gpr .rdi) = input s ∧
+      Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by
+  refine (prefix_ok 7 (by decide) s reads write sep).mono ?_
+  rintro t ⟨mem, frame, keeps, mx⟩
+  exact ⟨by rw [mem]; exact headerMem_block s _ zero, frame, keeps, mx⟩
+
+structure Words (p : Params) (pass lane slice counter : Nat) (s : State) : Prop where
+  passWord : s.mem.readW (off (s.gpr .rbp) 0) 64 = BitVec.ofNat 64 pass
+  laneWord : s.gpr .rbx = BitVec.ofNat 64 lane
+  sliceWord : s.gpr .r14 = BitVec.ofNat 64 slice
+  blocksWord : s.mem.readW (off (s.gpr .rbp) 240) 64 = BitVec.ofNat 64 p.blocks
+  passesWord : s.mem.readW (off (s.gpr .rbp) 72) 64 = BitVec.ofNat 64 p.passes
+  variantWord : s.mem.readW (off (s.gpr .rbp) 112) 64 = BitVec.ofNat 64 p.variant.code
+  counterWord : s.mem.readW (off (s.gpr .rbp) 8) 64 = BitVec.ofNat 64 counter
+
+theorem input_spec (p : Params) (pass lane slice counter : Nat) (s : State)
+    (h : Words p pass lane slice counter s) :
+    input s = Proof.Argon2.addressInput p pass lane slice counter := by
+  simp (config := {decide := true}) only [input, value, frameOffset,
+    ite_true, ite_false, h.passWord, h.laneWord, h.sliceWord, h.blocksWord,
+    h.passesWord, h.variantWord, h.counterWord, Proof.Argon2.addressInput]
+
+theorem code_spec_ok (p : Params) (pass lane slice counter : Nat) (s : State)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (write : Covers [⟨s.gpr .rdi, 1024⟩] s.wr)
+    (sep : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩)
+    (zero : blockAt s.mem (s.gpr .rdi) = zeroBlock)
+    (words : Words p pass lane slice counter s) :
+    WP isa code s fun t =>
+      blockAt t.mem (s.gpr .rdi) = Proof.Argon2.addressInput p pass lane slice counter ∧
+      Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr :=
+  (code_ok s reads write sep zero).mono (fun _ h =>
+    ⟨h.1.trans (input_spec p pass lane slice counter s words), h.2⟩)
+
+end VG.Proof.Argon2.X86_64.AddressHeader

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressHeaderLit.lean

@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressHeader
+
+/-! Checked literal of the independent-address input header. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.AddressHeader.code
+
+end VG

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressHeaderWords.lean

@@ -0,0 +1,38 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressHeader
+import VerifiedGarbage.Proof.Argon2.X86_64.BlockStore
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! Short independent-address input header writes. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressHeader
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressHeader
+
+theorem registerWord_ok (s : State) (i : Nat) (r : Reg)
+    (hw : InRegions s.wr (off (s.gpr .rdi) (8 * i)) 8) :
+    WP isa (.block (registerWord i r)) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rdi) (8 * i)) (s.gpr r) ∧
+      t.gpr = s.gpr ∧ t.rd = s.rd ∧ t.wr = s.wr ∧ t.mxcsr = s.mxcsr := by
+  apply WP.of_runBlock
+  simp only [registerWord, runBlock_cons, runStep_some, runBlock_nil, exec,
+    State.store64, ea_at, hw, ite_true, Option.some.injEq, exists_eq_left']
+  exact ⟨trivial, trivial, trivial, trivial, trivial⟩
+
+theorem frameWord_ok (s : State) (i offset : Nat)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) offset) 8)
+    (hw : InRegions s.wr (off (s.gpr .rdi) (8 * i)) 8) :
+    WP isa (.block (frameWord i offset)) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rdi) (8 * i))
+        (s.mem.readW (off (s.gpr .rbp) offset) 64) ∧
+      (∀ r, r ≠ .rax → t.gpr r = s.gpr r) ∧
+      t.rd = s.rd ∧ t.wr = s.wr ∧ t.mxcsr = s.mxcsr := by
+  apply WP.of_runBlock
+  simp only [frameWord, runBlock_cons, runStep_some, runBlock_nil, exec,
+    readSrc, State.load64, State.store64, ea_at, hr, hw,
+    RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg,
+    reduceCtorEq, ite_true, ite_false, Option.map_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, ?_, trivial, trivial, rfl⟩
+  intro r hr
+  simp only [hr, ite_false]
+
+end VG.Proof.Argon2.X86_64.AddressHeader

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressInputCT.lean

@@ -0,0 +1,26 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ClearBlockLit
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressHeaderLit
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Clearing and header preparation visit fixed offsets of public pointers. -/
+
+namespace VG.Proof.Argon2.X86_64
+
+open VG VG.X86_64
+
+theorem ClearBlock.code_rel : RelCT isa (fun s t => s.gpr .rdi = t.gpr .rdi)
+    Impl.Argon2.X86_64.ClearBlock.code (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rdi])
+    (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 AddressHeader.code_rel : RelCT isa
+    (fun s t => ∀ r ∈ [Reg.rdi, .rbp], s.gpr r = t.gpr r)
+    Impl.Argon2.X86_64.AddressHeader.code (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rdi, .rbp])
+    (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide)
+
+end VG.Proof.Argon2.X86_64

lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockStore.lean

@@ -0,0 +1,28 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.Initialize
+
+/-! A single matrix or scratch block word write as a vector update. -/
+
+namespace VG.Proof.Argon2.X86_64
+
+open VG VG.Spec.Argon2
+
+theorem blockAt_write (m : Mem) (p : Addr) (i : Fin 128) (v : Word) :
+    blockAt (m.writeW (off p (8 * i.val)) v) p = (blockAt m p).set i v := by
+  apply Vector.ext
+  intro j hj
+  simp only [blockAt, Vector.getElem_ofFn, Vector.getElem_set]
+  by_cases eq : i.val = j
+  · subst j
+    simp only [ite_true]
+    change (m.writeW (off p (8 * i.val)) v).readW (off p (8 * i.val)) 64 = v
+    exact Mem.readW_writeW_self64 _ _ _
+  · simp only [eq, ite_false]
+    change (m.writeW (off p (8 * i.val)) v).readW (off p (8 * j)) 64 =
+      m.readW (off p (8 * j)) 64
+    exact Mem.readW_writeW_sep (Offset.sep p (by omega) (by omega) (by omega)) (by decide)
+
+theorem blockAt_write_nat (m : Mem) (p : Addr) (i : Nat) (hi : i < 128) (v : Word) :
+    blockAt (m.writeW (off p (8 * i)) v) p = (blockAt m p).set i v hi :=
+  blockAt_write m p ⟨i, hi⟩ v
+
+end VG.Proof.Argon2.X86_64