Argon2 on x86-64: prove filling columns and block addresses

lean/VerifiedGarbage/Impl/Argon2/X86_64/BlockAddress.lean

@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Lane-major matrix addressing. The matrix base is in `r8`, the lane
+in `rax`, the column in `rcx`, and the lane length in `r12`. The resulting
+block pointer is returned in `rax`. Scalar multiplication and ten doublings
+work on the baseline ISA, including when the reference coordinates are secret.
+-/
+
+namespace VG.Impl.Argon2.X86_64.BlockAddress
+
+open VG.X86_64
+
+def flatten : List Instr := [.mul .r12, .alu .add .rax (.reg .rcx)]
+
+def scale : List Instr := List.replicate 10 (.alu .add .rax (.reg .rax))
+
+def code : Prog isa :=
+  .seq (.block flatten) (.seq (.block scale) (.block [.alu .add .rax (.reg .r8)]))
+
+end VG.Impl.Argon2.X86_64.BlockAddress

lean/VerifiedGarbage/Impl/Argon2/X86_64/FillColumn.lean

@@ -0,0 +1,26 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Current and preceding columns in the filling loop. The public slice,
+segment length and offset are in `r14`, `r13` and `r15`, and the lane length
+is in `r12`. `rcx` receives the current column; `rdi` receives its cyclic
+predecessor. Only the public column-zero test controls a branch.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillColumn
+
+open VG.X86_64
+
+def current : List Instr := [
+  .mov .rax (.reg .r14), .mul .r13, .mov .rcx (.reg .rax),
+  .alu .add .rcx (.reg .r15)]
+
+def select : Prog isa := .ite .e
+  (.block [.mov .rdi (.reg .r12)]) (.block [.mov .rdi (.reg .rcx)])
+
+def previous : Prog isa :=
+  .seq (.block [.alu .cmp .rcx (.imm 0)])
+    (.seq select (.block [.alu .sub .rdi (.imm 1)]))
+
+def code : Prog isa := .seq (.block current) previous
+
+end VG.Impl.Argon2.X86_64.FillColumn

lean/VerifiedGarbage/Impl/Argon2/X86_64/FirstLane.lean

@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Force the current lane on the first slice of the first pass.
+
+The pass and slice are public in `r9` and `r14`. The current lane is in
+`rbx`; `r8` initially contains J₂ modulo the lane count. Only the public
+position controls a branch.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FirstLane
+
+open VG.X86_64
+
+def test : List Instr := [.mov .rax (.reg .r9), .alu .or .rax (.reg .r14)]
+
+def current : List Instr := [.mov .r8 (.reg .rbx)]
+
+def code : Prog isa := .seq (.block test) (.ite .e (.block current) (.block []))
+
+end VG.Impl.Argon2.X86_64.FirstLane

lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceMap.lean

@@ -0,0 +1,44 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceLane
+import VerifiedGarbage.Impl.Argon2.X86_64.FirstLane
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceStart
+import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceCount
+import VerifiedGarbage.Impl.Argon2.X86_64.Relative
+import VerifiedGarbage.Impl.Argon2.X86_64.Wrap
+
+/-! Complete mapping of J₁ and J₂ to a reference lane and column.
+
+`rdi` contains the random word and `rsi` the lane count. The current
+lane is in `rbx`, lane and segment lengths in `r12` and `r13`, slice and
+index in `r14` and `r15`. The pass counter is at the frame base `rbp`:
+H₀'s first word is reused after memory initialization. `r9` and `rdi`
+receive the reference lane and column. The input word is retained in `r11`.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ReferenceMap
+
+open VG.X86_64
+
+def loadPass : List Instr := [.mov .r9 (.mem { base := .rbp })]
+
+def laneArgs : List Instr := [.mov .rdi (.reg .r8), .mov .rsi (.reg .rbx)]
+
+def relativeArgs : List Instr := [
+  .mov .r9 (.reg .rdi), .mov .rdi (.reg .r11), .mov .rsi (.reg .r8)]
+
+def wrapArgs : List Instr := [
+  .mov .rdi (.reg .rax), .alu .add .rdi (.reg .r10), .mov .rsi (.reg .r12)]
+
+def chooseLane : Prog isa :=
+  .seq ReferenceLane.code (.seq (.block loadPass) FirstLane.code)
+
+def prepareLanes : Prog isa := .seq chooseLane (.block laneArgs)
+
+def window : Prog isa := .seq ReferenceStart.code ReferenceCount.code
+
+def relative : Prog isa := .seq (.block relativeArgs) Relative.code
+
+def finish : Prog isa := .seq (.block wrapArgs) Wrap.code
+
+def code : Prog isa := .seq prepareLanes (.seq window (.seq relative finish))
+
+end VG.Impl.Argon2.X86_64.ReferenceMap

lean/VerifiedGarbage/Proof/Argon2/FillPositions.lean

@@ -0,0 +1,55 @@
+import VerifiedGarbage.Proof.Argon2.Dimensions
+import VerifiedGarbage.Proof.Framework.Offset
+
+/-! Bounds for every block address used by the filling loop. -/
+
+namespace VG.Proof.Argon2
+
+open VG.Spec.Argon2
+
+theorem previous_column_lt (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (column : Nat) :
+    (column + p.laneLen - 1) % p.laneLen < p.laneLen := by
+  have seg := segmentLen_ge_two p hl hm
+  have lanes := laneLen_segments p hl
+  exact Nat.mod_lt _ (by omega)
+
+theorem cell_bytes (p : Params) (hl : 0 < p.lanes) {lane column : Nat}
+    (hlane : lane < p.lanes) (hcolumn : column < p.laneLen) :
+    (lane * p.laneLen + column) * 1024 + 1024 ≤ p.blocks * 1024 := by
+  have cell := cell_lt p hl hlane hcolumn
+  have scaled := Nat.mul_le_mul_right 1024 (show lane * p.laneLen + column + 1 ≤ p.blocks by omega)
+  simpa only [Nat.add_mul, Nat.one_mul] using scaled
+
+theorem current_cell_lt (p : Params) (hl : 0 < p.lanes) {lane slice index : Nat}
+    (hlane : lane < p.lanes) (hslice : slice < 4) (hindex : index < p.segmentLen) :
+    lane * p.laneLen + (slice * p.segmentLen + index) < p.blocks :=
+  cell_lt p hl hlane (column_lt p hl hslice hindex)
+
+theorem previous_cell_lt (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) {lane column : Nat} (hlane : lane < p.lanes) :
+    lane * p.laneLen + ((column + p.laneLen - 1) % p.laneLen) < p.blocks :=
+  cell_lt p hl hlane (previous_column_lt p hl hm column)
+
+theorem reference_cell_lt (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (pass lane slice index : Nat) (random : Word)
+    (hlane : lane < p.lanes) :
+    let ref := reference p pass lane slice index random
+    ref.1 * p.laneLen + ref.2 < p.blocks := by
+  obtain ⟨laneBound, columnBound⟩ := reference_bounds p hl hm pass lane slice index random hlane
+  exact cell_lt p hl laneBound columnBound
+
+theorem cell_contains (base : VG.Addr) (p : Params) (hl : 0 < p.lanes)
+    (hm : p.memory < 2 ^ 32) {lane column : Nat}
+    (hlane : lane < p.lanes) (hcolumn : column < p.laneLen) :
+    (⟨base, p.blocks * 1024⟩ : VG.Region).Contains
+      (base + BitVec.ofNat 64 ((lane * p.laneLen + column) * 1024)) 1024 := by
+  have bytes := cell_bytes p hl hlane hcolumn
+  have blocks : p.blocks < 2 ^ 32 := Nat.lt_of_le_of_lt (blocks_le_memory p) hm
+  have total : p.blocks * 1024 < 2 ^ 64 :=
+    Nat.lt_trans (Nat.mul_lt_mul_of_pos_right blocks (by decide : 0 < 1024)) (by decide +kernel)
+  exact VG.Offset.contains_base base
+    (d := (lane * p.laneLen + column) * 1024) (n := 1024) (k := p.blocks * 1024)
+    bytes (Nat.lt_of_le_of_lt (Nat.le_trans (Nat.le_add_right _ _) bytes) total)
+
+end VG.Proof.Argon2

lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddress.lean

@@ -0,0 +1,81 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.BlockAddress
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitScale
+import VerifiedGarbage.Proof.Framework.X86_64.Abi
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Fault-free matrix pointer calculation, with no memory accesses. -/
+
+namespace VG.Proof.Argon2.X86_64.BlockAddress
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.BlockAddress
+
+theorem flatten_ok (s : State) : WP isa (.block flatten) s fun t =>
+    t.gpr .rax = s.gpr .rax * s.gpr .r12 + s.gpr .rcx ∧
+    Divide.Keeps [.rax, .rdx] s t := by
+  apply WP.of_runBlock
+  simp only [flatten, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    execMul, execAlu, RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags,
+    reduceCtorEq, ite_true, ite_false, Option.bind_some, Option.some.injEq,
+    exists_eq_left', BitVec.ofNat_mul, BitVec.ofNat_toNat, BitVec.setWidth_eq]
+  refine ⟨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, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags,
+      hr.1, hr.2, ite_false]
+  all_goals rfl
+
+theorem scale_ok (s : State) : WP isa (.block scale) s fun t =>
+    t.gpr .rax = s.gpr .rax * 1024 ∧ Divide.Keeps [.rax] s t := by
+  refine WP.mono_mx (by decide +kernel) (MemoryInit.scale_ok s .rax 10) ?_
+  intro t h mx
+  refine ⟨h.value, ?_, h.mem, h.rd, h.wr, mx⟩
+  intro r hr
+  exact h.other r (by simpa only [List.mem_cons, List.not_mem_nil, or_false] using hr)
+
+theorem base_ok (s : State) : WP isa (.block [.alu .add .rax (.reg .r8)]) s fun t =>
+    t.gpr .rax = s.gpr .rax + s.gpr .r8 ∧ Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, Option.bind_some,
+    Option.some.injEq, exists_eq_left']
+  refine ⟨by simp only [ite_true], ?_⟩
+  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 code_ok (s : State) : WP isa code s fun t =>
+    t.gpr .rax = (s.gpr .rax * s.gpr .r12 + s.gpr .rcx) * 1024 + s.gpr .r8 ∧
+    Divide.Keeps [.rax, .rdx] s t := by
+  unfold code
+  refine WP.seq ((flatten_ok s).mono ?_)
+  rintro a ⟨flat, ka⟩
+  refine WP.seq ((scale_ok a).mono ?_)
+  rintro b ⟨scaled, kb⟩
+  refine (base_ok b).mono ?_
+  rintro t ⟨result, kt⟩
+  refine ⟨?_, ka.trans ((kb.mono (by simp)).trans (kt.mono (by simp)))⟩
+  rw [result, scaled, flat, kb.regs .r8 (by decide), ka.regs .r8 (by decide)]
+
+theorem code_nat_ok (s : State) (lane column q : Nat)
+    (hl : s.gpr .rax = BitVec.ofNat 64 lane)
+    (hc : s.gpr .rcx = BitVec.ofNat 64 column)
+    (hq : s.gpr .r12 = BitVec.ofNat 64 q) :
+    WP isa code s fun t =>
+      t.gpr .rax = s.gpr .r8 + BitVec.ofNat 64 ((lane * q + column) * 1024) ∧
+      Divide.Keeps [.rax, .rdx] s t := by
+  refine (code_ok s).mono ?_
+  rintro t ⟨h, k⟩
+  refine ⟨?_, k⟩
+  rw [h, hl, hc, hq, ← BitVec.ofNat_mul, ← BitVec.ofNat_add]
+  change BitVec.ofNat 64 (lane * q + column) * BitVec.ofNat 64 1024 + s.gpr .r8 = _
+  rw [← BitVec.ofNat_mul, BitVec.add_comm]
+
+theorem code_secret_rel : RelCT isa (fun _ _ => True) code (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide)
+
+end VG.Proof.Argon2.X86_64.BlockAddress

lean/VerifiedGarbage/Proof/Argon2/X86_64/BlockAddressLit.lean

@@ -0,0 +1,10 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.BlockAddress
+
+/-! A checked literal for lane-major matrix block addressing. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.BlockAddress.code
+
+end VG