Argon2 on x86-64: prove reference-window counts and starts

lean/VerifiedGarbage/Impl/Argon2/X86_64/CountCandidates.lean

@@ -0,0 +1,31 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! # The two eligible reference windows
+
+`r9` is the pass, `r12` the lane length, `r13` the segment length, `r14`
+the slice and `r15` the index within the segment. `rdx` receives the count
+for the current lane; `rcx` receives the count for another lane. Only the
+public pass controls a branch. The zero-index adjustment uses a borrow mask.
+-/
+
+namespace VG.Impl.Argon2.X86_64.CountCandidates
+
+open VG.X86_64
+
+def first : List Instr := [
+  .mov .rax (.reg .r13), .mul .r14, .mov .rcx (.reg .rax), .mov .rdx (.reg .rax),
+  .alu .add .rdx (.reg .r15), .alu .sub .rdx (.imm 1)]
+
+def later : List Instr := [
+  .mov .rax (.reg .r12), .alu .sub .rax (.reg .r13), .mov .rcx (.reg .rax),
+  .mov .rdx (.reg .rax), .alu .add .rdx (.reg .r15), .alu .sub .rdx (.imm 1)]
+
+def adjust : List Instr := [
+  .mov .r8 (.reg .r15), .alu .sub .r8 (.imm 1), .alu .sbb .r9 (.reg .r9),
+  .alu .add .rcx (.reg .r9)]
+
+def code : Prog isa :=
+  .seq (.block [.alu .cmp .r9 (.imm 0)])
+    (.seq (.ite .e (.block first) (.block later)) (.block adjust))
+
+end VG.Impl.Argon2.X86_64.CountCandidates

lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean

@@ -0,0 +1,67 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Initial
+
+/-!
+# Argon2 memory initialization on x86-64
+
+`rbp` addresses the derivation frame containing H₀ and the public arguments;
+`rbx` addresses hash scratch. `r13` holds the lane length in blocks, as
+computed by the parameter-setup layer. The complete matrix is cleared before
+H′ initializes columns zero and one of every lane. This establishes exactly
+`Spec.Argon2.initMemory` even when the allocation initially contains arbitrary
+bytes. Each H′ call uses the supplied BLAKE2b backend.
+-/
+
+namespace VG.Impl.Argon2.X86_64.MemoryInit
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64.HPrime (at_ Hash)
+
+/-- The memory pointer and allocated block count in the enclosing frame. -/
+def memoryOffset : Nat := 232
+def blocksOffset : Nat := 240
+
+/-- Clear one word, advancing the destination and public countdown. -/
+def clearWord : List Instr :=
+  [.store (at_ .r14) .rcx, .alu .add .r14 (.imm 8), .alu .sub .rax (.imm 1)]
+
+def clearHeader : List Instr :=
+  [.mov .r14 (.mem (at_ .rbp memoryOffset)), .mov .rax (.mem (at_ .rbp blocksOffset)),
+    .mov32 .rcx (.imm 0)]
+
+def clearSetup : List Instr := clearHeader ++ List.replicate 7 (.alu .add .rax (.reg .rax))
+
+def clearSetupCode : Prog isa := .block clearSetup
+
+def clear : Prog isa := .seq clearSetupCode (.loop (.block clearWord) .ne)
+
+/-- Reset the matrix pointer and lane number, retaining the lane stride in bytes. -/
+def lanesHeader : List Instr :=
+  [.mov .r14 (.mem (at_ .rbp memoryOffset)), .mov32 .r12 (.imm 0),
+    .mov .r15 (.mem (at_ .rbp Initial.lanesOffset))]
+
+def lanesSetup : List Instr := lanesHeader ++ List.replicate 10 (.alu .add .r13 (.reg .r13))
+
+def lanesSetupCode : Prog isa := .block lanesSetup
+
+/-- H′(1024, H₀ || LE32(column) || LE32(lane)). -/
+def blockArgs (column : Nat) : List Instr :=
+  [.mov32 .rax (.imm (BitVec.ofNat 32 column)), .store32 (at_ .rbp 64) .rax,
+    .store32 (at_ .rbp 68) .r12, .mov .rdi (.reg .rbp), .mov32 .rsi (.imm 72),
+    .mov .rdx (.reg .r14), .mov32 .rcx (.imm 1024), .mov .r8 (.reg .rbx)]
+
+def block (name : String) (h : Hash) (column : Nat) : Prog isa :=
+  .seq (.block (blockArgs column)) (.call name (HPrime.code h))
+
+/-- Initialize one lane, then advance to the next lane's first block. -/
+def lane (name : String) (h : Hash) : Prog isa :=
+  .seq (block name h 0)
+  (.seq (.block [.alu .add .r14 (.imm 1024)])
+  (.seq (block name h 1)
+    (.block [.alu .add .r14 (.reg .r13), .alu .sub .r14 (.imm 1024),
+      .alu .add .r12 (.imm 1), .alu .sub .r15 (.imm 1)])))
+
+/-- Zero the matrix and initialize both leading blocks in every lane. -/
+def code (name : String) (h : Hash) : Prog isa :=
+  .seq clear (.seq lanesSetupCode (.loop (lane name h) .ne))
+
+end VG.Impl.Argon2.X86_64.MemoryInit

lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceCount.lean

@@ -0,0 +1,16 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.CountCandidates
+import VerifiedGarbage.Impl.Argon2.X86_64.SelectWindow
+
+/-! Compute both reference windows and select one without a secret branch.
+
+`rdi` and `rsi` are the reference and current lanes. The pass and segment
+position use CountCandidates' registers. `r8` receives the selected count.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ReferenceCount
+
+open VG VG.X86_64
+
+def code : Prog isa := .seq CountCandidates.code SelectWindow.code
+
+end VG.Impl.Argon2.X86_64.ReferenceCount

lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceLane.lean

@@ -0,0 +1,19 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.Divide
+
+/-! # Selecting a lane from J₂ with fixed-time division
+
+`rdi` contains the full address word and `rsi` the positive lane count.
+`r8` receives J₂ modulo the lane count; `r11` retains the address word
+for the subsequent J₁ mapping. The first slice of pass zero instead uses
+the current lane; the enclosing public loop selects that case separately.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ReferenceLane
+
+open VG.X86_64
+
+def highArgs : List Instr := [.mov .r11 (.reg .rdi), .shift .shr .rdi 32]
+
+def code : Prog isa := .seq (.block highArgs) Divide.code
+
+end VG.Impl.Argon2.X86_64.ReferenceLane

lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceStart.lean

@@ -0,0 +1,25 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! Start of the chronological reference window.
+
+The public pass, slice and segment length are in `r9`, `r14` and `r13`.
+`r10` receives zero on pass zero or the last slice, otherwise the column
+at the beginning of the next slice. No division is needed.
+-/
+
+namespace VG.Impl.Argon2.X86_64.ReferenceStart
+
+open VG.X86_64
+
+def zero : List Instr := [.mov .r10 (.imm 0)]
+
+def advance : List Instr := [
+  .mov .rax (.reg .r14), .alu .add .rax (.imm 1), .mul .r13,
+  .mov .r10 (.reg .rax), .alu .cmp .r14 (.imm 3)]
+
+def code : Prog isa :=
+  .seq (.block [.alu .cmp .r9 (.imm 0)])
+    (.ite .e (.block zero)
+      (.seq (.block advance) (.ite .e (.block zero) (.block []))))
+
+end VG.Impl.Argon2.X86_64.ReferenceStart

lean/VerifiedGarbage/Impl/Argon2/X86_64/Relative.lean

@@ -0,0 +1,19 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! # Argon2's squared mapping into an eligible reference window
+
+`rdi` contains J₁ in its low half and `rsi` contains the positive window
+length. Both products fit in 64 bits for the RFC's 32-bit dimensions. The
+code has no branches or memory accesses, including for secret J₁ values.
+-/
+
+namespace VG.Impl.Argon2.X86_64.Relative
+
+open VG.X86_64
+
+def code : Prog isa := .block [
+  .mov32 .rax (.reg .rdi), .mul .rax, .shift .shr .rax 32,
+  .mul .rsi, .shift .shr .rax 32, .mov .rcx (.reg .rsi),
+  .alu .sub .rcx (.imm 1), .alu .sub .rcx (.reg .rax), .mov .rax (.reg .rcx)]
+
+end VG.Impl.Argon2.X86_64.Relative

lean/VerifiedGarbage/Impl/Argon2/X86_64/SelectWindow.lean

@@ -0,0 +1,20 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! # Select the eligible window without branching on the reference lane
+
+`rdi,rsi` are the reference and current lanes; `rdx,rcx` hold the same-lane
+and cross-lane window lengths. `r8` receives the selected length. Subtracting
+one from the lanes' XOR borrows exactly when the lanes match, supplying the
+mask for the selection. The counts may be secret too.
+-/
+
+namespace VG.Impl.Argon2.X86_64.SelectWindow
+
+open VG.X86_64
+
+def code : Prog isa := .block [
+  .mov .rax (.reg .rdi), .alu .xor .rax (.reg .rsi), .alu .sub .rax (.imm 1),
+  .alu .sbb .rax (.reg .rax), .mov .r8 (.reg .rcx), .alu .xor .rdx (.reg .rcx),
+  .alu .and .rdx (.reg .rax), .alu .xor .r8 (.reg .rdx)]
+
+end VG.Impl.Argon2.X86_64.SelectWindow

lean/VerifiedGarbage/Impl/Argon2/X86_64/Wrap.lean

@@ -0,0 +1,18 @@
+import VerifiedGarbage.TCB.X86_64.Isa
+
+/-! # Wrap a reference-column sum with one masked subtraction
+
+`rdi` is the sum and `rsi` the positive lane length. A sum below twice the
+lane length needs at most one subtraction; the borrow mask selects the
+original sum when it is already in range. No secret controls a branch.
+-/
+
+namespace VG.Impl.Argon2.X86_64.Wrap
+
+open VG.X86_64
+
+def code : Prog isa := .block [
+  .mov .r10 (.reg .rdi), .alu .sub .rdi (.reg .rsi), .alu .sbb .rax (.reg .rax),
+  .alu .xor .r10 (.reg .rdi), .alu .and .r10 (.reg .rax), .alu .xor .rdi (.reg .r10)]
+
+end VG.Impl.Argon2.X86_64.Wrap

lean/VerifiedGarbage/Proof/Argon2/MemoryInit.lean

@@ -0,0 +1,46 @@
+import VerifiedGarbage.Spec.Argon2.Contract
+import VerifiedGarbage.Proof.Blake2.Stream
+
+/-! # The RFC initialization blocks as byte strings in memory -/
+
+namespace VG.Proof.Argon2
+
+open VG VG.Spec.Argon2
+open VG.Spec.Blake2 (bytesAt)
+
+/-- A complete byte representation parses to the block at the same address. -/
+theorem parseBlock_bytesAt (m : Mem) (p : Addr) : parseBlock (bytesAt m p 1024) = blockAt m p := by
+  apply Vector.ext
+  intro j hj
+  simp only [parseBlock, blockAt, Vector.getElem_ofFn, Spec.Blake2.leWord,
+    Proof.Blake2.read_eq_leBytes, BitVec.setWidth_eq]
+  apply Proof.Blake2.leBytes_congr
+  intro k hk
+  have bound : 8 * j + k < 1024 := by omega
+  simp only [bytesAt, List.getD_eq_getElem?_getD, List.getElem?_map,
+    List.getElem?_range bound, Option.map_some, Option.getD_some,
+    BitVec.ofNat_add, BitVec.add_assoc]
+
+/-- Initialization contains one 1024-byte H′ result at each leading cell. -/
+def initialBytes (h0 : List Byte) (lane column : Nat) : List Byte :=
+  hPrime 1024 (h0 ++ le32 column ++ le32 lane)
+
+/-- The byte-level call result is sufficient for the word-level matrix spec. -/
+theorem blockAt_of_initialBytes (m : Mem) (p : Addr) (h0 : List Byte)
+    (lane column : Nat) (h : bytesAt m p 1024 = initialBytes h0 lane column) :
+    blockAt m p = parseBlock (initialBytes h0 lane column) := by
+  rw [← parseBlock_bytesAt, h]
+
+theorem initMemory_size (p : Params) (h0 : List Byte) :
+    (initMemory p h0).memory.size = p.blocks := by
+  simp only [initMemory, Array.size_map, List.size_toArray, List.length_range]
+
+theorem initMemory_cell (p : Params) (h0 : List Byte) (k : Nat) (hk : k < p.blocks) :
+    (initMemory p h0).memory[k]'(by rw [initMemory_size]; exact hk) =
+      if k % p.laneLen < 2 then
+        parseBlock (initialBytes h0 (k / p.laneLen) (k % p.laneLen))
+      else zeroBlock := by
+  simp only [initMemory, Array.getElem_map, List.getElem_toArray, List.getElem_range,
+    initialBytes]
+
+end VG.Proof.Argon2

lean/VerifiedGarbage/Proof/Argon2/Reference.lean

@@ -0,0 +1,95 @@
+import VerifiedGarbage.Proof.Argon2.Dimensions
+
+/-! # Bounds for the quadratic reference-window mapping in RFC 9106 §3.4.2 -/
+
+namespace VG.Proof.Argon2
+
+theorem reference_square_bound (j : Nat) (hj : j < 2 ^ 32) : j * j < 2 ^ 64 := by
+  exact Nat.lt_of_lt_of_eq (Nat.mul_self_lt_mul_self hj) (by decide)
+
+theorem reference_scaled_bound (j : Nat) (hj : j < 2 ^ 32) :
+    j * j / 2 ^ 32 < 2 ^ 32 := by
+  apply (Nat.div_lt_iff_lt_mul (by decide : 0 < 2 ^ 32)).mpr
+  exact Nat.lt_of_lt_of_eq (reference_square_bound j hj) (by decide)
+
+theorem reference_product_bound (count j : Nat) (hc : count < 2 ^ 32)
+    (hj : j < 2 ^ 32) : count * (j * j / 2 ^ 32) < 2 ^ 64 := by
+  exact Nat.lt_of_lt_of_eq (Nat.mul_lt_mul_of_lt_of_lt hc (reference_scaled_bound j hj))
+    (by decide)
+
+theorem reference_scale_lt_count (count j : Nat) (hc : 0 < count) (hj : j < 2 ^ 32) :
+    count * (j * j / 2 ^ 32) / 2 ^ 32 < count := by
+  apply (Nat.div_lt_iff_lt_mul (by decide : 0 < 2 ^ 32)).mpr
+  exact Nat.mul_lt_mul_of_pos_left (reference_scaled_bound j hj) hc
+
+theorem reference_relative_bound (count j : Nat) (hc : 0 < count) :
+    count - 1 - count * (j * j / 2 ^ 32) / 2 ^ 32 < count := by
+  omega
+
+open VG.Spec.Argon2
+
+theorem reference_count_lt_lane (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (pass slice index : Nat) (same : Bool)
+    (hs : slice < 4) (hi : index < p.segmentLen) :
+    referenceCount p pass slice index same < p.laneLen := by
+  have seg := segmentLen_ge_two p hl hm
+  have len := laneLen_segments p hl
+  have column := column_lt p hl hs hi
+  unfold referenceCount
+  by_cases first : pass = 0
+  · rw [ite_eq_left first]
+    cases same
+    · simp only [Bool.false_eq_true, ite_false]
+      split <;> omega
+    · simp only [ite_true]
+      omega
+  · rw [ite_eq_right first]
+    cases same
+    · simp only [Bool.false_eq_true, ite_false]
+      split <;> omega
+    · simp only [ite_true]
+      omega
+
+theorem reference_count_positive (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (pass slice index : Nat) (same : Bool)
+    (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index)
+    (firstLane : pass = 0 → slice = 0 → same = true) :
+    0 < referenceCount p pass slice index same := by
+  have seg := segmentLen_ge_two p hl hm
+  have len := laneLen_segments p hl
+  unfold referenceCount
+  by_cases first : pass = 0
+  · rw [ite_eq_left first]
+    by_cases zero : slice = 0
+    · simp only [firstLane first zero, zero, Nat.zero_mul, ite_true]
+      omega
+    · have mul := Nat.mul_le_mul_right p.segmentLen (show 1 ≤ slice by omega)
+      rw [Nat.one_mul] at mul
+      cases same
+      · simp only [Bool.false_eq_true, ite_false]
+        split <;> omega
+      · simp only [ite_true]
+        omega
+  · rw [ite_eq_right first]
+    cases same
+    · simp only [Bool.false_eq_true, ite_false]
+      split <;> omega
+    · simp only [ite_true]
+      omega
+
+theorem reference_count_32 (p : Params) (hl : 0 < p.lanes)
+    (hm : 8 * p.lanes ≤ p.memory) (memoryBound : p.memory < 2 ^ 32)
+    (pass slice index : Nat) (same : Bool) (hs : slice < 4) (hi : index < p.segmentLen) :
+    referenceCount p pass slice index same < 2 ^ 32 := by
+  have laneBlocks := Nat.le_mul_of_pos_left p.laneLen hl
+  rw [← blocks_lanes p hl] at laneBlocks
+  exact Nat.lt_of_lt_of_le (reference_count_lt_lane p hl hm pass slice index same hs hi)
+    (Nat.le_trans laneBlocks (Nat.le_trans (blocks_le_memory p) (Nat.le_of_lt memoryBound)))
+
+theorem reference_wrap (sum q : Nat) (bound : sum < 2 * q) :
+    sum % q = if sum < q then sum else sum - q := by
+  by_cases small : sum < q
+  · rw [ite_eq_left small, Nat.mod_eq_of_lt small]
+  · rw [ite_eq_right small, Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)]
+
+end VG.Proof.Argon2