Argon2 on x86-64: prove memory initialization and reference-index arithmetic

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/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/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/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

lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean

@@ -0,0 +1,116 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLoop
+import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitSetup
+import VerifiedGarbage.Proof.Argon2.Dimensions
+
+/-! # Functional correctness of complete memory initialization -/
+
+namespace VG.Proof.Argon2.X86_64.MemoryInit
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit
+open VG.Proof.Argon2.X86_64.Initial (wordAt)
+open VG.Spec.Blake2 (bytesAt)
+
+theorem Cleared.frame {s t : State} {memory : Addr} {blocks : Nat}
+    (h : Cleared s t memory blocks) (bound : 1024 * blocks < 2 ^ 64) :
+    Frame [⟨memory, 1024 * blocks⟩] s.mem t.mem := by
+  rw [h.mem]
+  simpa only [show 8 * (128 * blocks) = 1024 * blocks by omega] using
+    clearMem_frame s.mem memory (128 * blocks) (by omega)
+
+theorem Cleared.word {s t : State} {memory : Addr} {blocks d : Nat}
+    (h : Cleared s t memory blocks) (space : Space s memory (1024 * blocks))
+    (offset : d + 8 ≤ 272) : wordAt t d = wordAt s d := by
+  unfold wordAt
+  rw [h.other .rbp (by decide) (by decide) (by decide)]
+  apply (h.frame space.bound).readW (r := ⟨s.gpr .rbp, 272⟩)
+    (Offset.contains_base _ offset (by omega)) ?_ (by decide)
+  intro r hr; simp only [List.mem_singleton] at hr; subst r
+  exact space.frameMatrix
+
+theorem code_ok (v : Proof.Blake2.X86_64.Backend) (name : String)
+    (s : State) (memory : Addr) (lanes q : Nat) (lo : 1 ≤ lanes) (hq : 2 ≤ q)
+    (lanesBound : lanes < 2 ^ 64) (space : Space s memory (1024 * (lanes * q)))
+    (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8)
+    (lanesRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 184) 8)
+    (blocksRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 240) 8)
+    (memoryWord : wordAt s memoryOffset = memory)
+    (lanesWord : wordAt s VG.Impl.Argon2.X86_64.Initial.lanesOffset = BitVec.ofNat 64 lanes)
+    (blocksWord : wordAt s blocksOffset = BitVec.ofNat 64 (lanes * q))
+    (laneLength : s.gpr .r13 = BitVec.ofNat 64 q) :
+    WP isa (code name (HPrime.hash v)) s fun t =>
+      Initialized t.mem memory lanes q lanes (bytesAt s.mem (s.gpr .rbp) 64) ∧
+      t.gpr .rbp = s.gpr .rbp ∧ t.gpr .rbx = s.gpr .rbx ∧ t.gpr .rsp = s.gpr .rsp ∧
+      t.rd = s.rd ∧ t.wr = s.wr ∧
+      Frame [⟨memory, 1024 * (lanes * q)⟩, ⟨s.gpr .rbx, 16384⟩,
+        below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem t.mem := by
+  unfold code lanesSetupCode
+  have blocksPositive : 1 ≤ lanes * q := by
+    have mul := Nat.mul_le_mul_right q lo
+    rw [Nat.one_mul] at mul; omega
+  refine WP.seq ((clear_ok s memory (lanes * q) blocksPositive space.bound memoryRead
+    blocksRead memoryWord blocksWord space.matrix).mono ?_)
+  intro a ha
+  have bpA := ha.other .rbp (by decide) (by decide) (by decide)
+  have bxA := ha.other .rbx (by decide) (by decide) (by decide)
+  have spA := ha.other .rsp (by decide) (by decide) (by decide)
+  have spaceA := space.same ha.wr bpA bxA spA
+  have hashA : bytesAt a.mem (a.gpr .rbp) 64 = bytesAt s.mem (s.gpr .rbp) 64 := by
+    rw [bpA]
+    apply Proof.Blake2.bytesAt_congr
+    intro i hi
+    exact (ha.frame space.bound).bytes (R := ⟨s.gpr .rbp, 64⟩) (by
+      intro r hr; simp only [List.mem_singleton] at hr; subst r
+      exact space.frameMatrix.sub_left (Region.sub_prefix (by decide)))
+      (show (64 : Nat) ≤ 2 ^ 64 from by decide) hi
+  refine WP.seq ((lanesSetup_ok a memory lanes q
+    (by rw [ha.rd, ha.wr, bpA]; exact memoryRead)
+    (by rw [ha.rd, ha.wr, bpA]; exact lanesRead)
+    ((ha.word space (by decide)).trans memoryWord)
+    ((ha.word space (by decide)).trans lanesWord)
+    ((ha.other .r13 (by decide) (by decide) (by decide)).trans laneLength)).mono ?_)
+  intro b hb
+  have bpB := hb.other .rbp (by decide) (by decide) (by decide) (by decide)
+  have bxB := hb.other .rbx (by decide) (by decide) (by decide) (by decide)
+  have spB := hb.other .rsp (by decide) (by decide) (by decide) (by decide)
+  have spaceB := spaceA.same hb.wr bpB bxB spB
+  refine (lanesLoop_ok v name b memory lanes q (bytesAt s.mem (s.gpr .rbp) 64)
+    spaceB lo lanesBound hq hb.destination hb.lane hb.remaining hb.stride ?_ ?_).mono ?_
+  · rw [hb.mem, ha.mem]
+    exact initialized_zero s.mem memory lanes q space.bound _
+  · rw [hb.mem, bpB]; exact hashA
+  · intro t ht
+    refine ⟨ht.initialized, ht.keeps.rbp.trans (bpB.trans bpA),
+      ht.keeps.rbx.trans (bxB.trans bxA), ht.keeps.rsp.trans (spB.trans spA),
+      ht.keeps.rd.trans (hb.rd.trans ha.rd), ht.keeps.wr.trans (hb.wr.trans ha.wr), ?_⟩
+    have fb : Frame [⟨memory, 1024 * (lanes * q)⟩, ⟨s.gpr .rbx, 16384⟩,
+        below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem b.mem := by
+      rw [hb.mem]
+      exact (ha.frame space.bound).mono (by
+        intro r hr
+        simp only [List.mem_singleton] at hr
+        subst r
+        exact List.mem_cons_self ..)
+    apply fb.trans
+    have f := ht.keeps.frame
+    rw [bpB, bpA, bxB, bxA, spB, spA] at f
+    exact f
+
+/-- Every cell agrees with the reviewed initialization spec, in lane-major order. -/
+theorem Initialized.spec {m : Mem} {base : Addr} {p : Spec.Argon2.Params}
+    {h0 : List Byte} (hl : 0 < p.lanes) (hq : 0 < p.laneLen)
+    (h : Initialized m base p.lanes p.laneLen p.lanes h0)
+    (k : Nat) (hk : k < p.blocks) :
+    Spec.Argon2.blockAt m (base + BitVec.ofNat 64 (1024 * k)) =
+      (Spec.Argon2.initMemory p h0).memory[k]'(by
+        rw [Proof.Argon2.initMemory_size]; exact hk) := by
+  have blocks := Proof.Argon2.blocks_lanes p hl
+  have lane : k / p.laneLen < p.lanes := by
+    apply (Nat.div_lt_iff_lt_mul hq).mpr
+    simpa only [blocks] using hk
+  have cell := h (k / p.laneLen) lane (k % p.laneLen) (Nat.mod_lt _ hq)
+  rw [Nat.mul_comm (k / p.laneLen) p.laneLen, Nat.div_add_mod] at cell
+  simp only [lane, true_and] at cell
+  rw [Proof.Argon2.initMemory_cell p h0 k hk]
+  exact cell
+
+end VG.Proof.Argon2.X86_64.MemoryInit