Argon2 on x86-64: prove independent-address caching

lean/VerifiedGarbage/Impl/Argon2/X86_64/AddressCache.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCalls
+
+/-! Cache one address block per 128 segment positions. Frame offset eight holds
+its one-based counter; initializing it to zero forces generation even when the
+first filled index is two. Only public counters control regeneration.
+-/
+
+namespace VG.Impl.Argon2.X86_64.AddressCache
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def check : List Instr := [
+  .mov .rax (.reg .r15), .shift .shr .rax 7, .alu .add .rax (.imm 1),
+  .alu .cmp .rax (.mem (at_ .rbp 8))]
+
+def save : List Instr := [.store (at_ .rbp 8) .rax]
+
+def select : Prog isa := .seq (.block check)
+  (.ite .e (.block []) (.seq (.block save) AddressCalls.code))
+
+def wordArgs : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)), .mov .rax (.reg .r15), .alu .and .rax (.imm 127)]
+
+def wordRead : List Instr := [
+  .mov .rdi (.mem { base := .rcx, index := some .rax, scale := 8, disp := 6144 })]
+
+def word : Prog isa := .seq (.block wordArgs) (.block wordRead)
+
+def code : Prog isa := .seq select word
+
+end VG.Impl.Argon2.X86_64.AddressCache

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCache.lean

@@ -0,0 +1,49 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheSelect
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheWord
+
+/-! Complete cached random-word selection against RFC 9106's address block. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+structure Done (s t : State) (p : Params) (pass lane slice : Nat) : Prop where
+  selected : Selected s t p pass lane slice
+  random : t.gpr .rdi =
+    (addressBlock p pass lane slice (wanted s))[(s.gpr .r15).toNat % 128]'(Nat.mod_lt _ (by decide))
+
+theorem code_ok (p : Params) (pass lane slice old : Nat) (s : State)
+    (h : Ready p pass lane slice old s) :
+    WP isa code s (Done s · p pass lane slice) := by
+  unfold code
+  refine WP.seq ((selected_ok p pass lane slice old s h).mono ?_)
+  intro a selected
+  refine (word_ok a selected.layout).mono ?_
+  rintro t ⟨random, keeps⟩
+  have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r := by
+    intro r hr
+    have ne : r ∉ [Reg.rcx, .rax, .rdi] := by
+      simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+    exact (keeps.regs r ne).trans (selected.regs r hr)
+  have bp := keeps.regs .rbp (by decide)
+  have sp := keeps.regs .rsp (by decide)
+  have work' : AddressCalls.work t = AddressCalls.work a := by
+    unfold AddressCalls.work; rw [bp, keeps.mem]
+  have layout : AddressCalls.Ready t := by
+    constructor
+    · rw [keeps.rd, keeps.wr, bp]; exact selected.layout.frameRead
+    · rw [work', keeps.wr]; exact selected.layout.workWrite
+    · rw [bp, work']; exact selected.layout.frameWork
+    · rw [bp, sp]; exact selected.layout.frameStack
+    · rw [sp, work']; exact selected.layout.stackWork
+  refine ⟨⟨?_, layout, work'.trans selected.work_eq, regs,
+    keeps.rd.trans selected.rd, keeps.wr.trans selected.wr, ?_,
+    keeps.mxcsr.trans selected.mxcsr, ?_⟩, ?_⟩
+  · rw [keeps.mem]; exact selected.block
+  · rw [keeps.mem]; exact selected.frame
+  · rw [bp, keeps.mem]; exact selected.counterWord
+  · rw [selected.work_eq, selected.regs .r15 (by simp [calleeSaved]), selected.block] at random
+    exact random
+
+end VG.Proof.Argon2.X86_64.AddressCache

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheMeta.lean

@@ -0,0 +1,77 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceStart
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCache
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCallsPrepare
+
+/-! Public cache counters and indexed-word arguments. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.AddressCache
+
+def counter (index : Addr) : Addr := (index >>> 7) + 1
+
+theorem check_ok (s : State)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 8) 8) :
+    WP isa (.block check) s fun t => t.gpr .rax = counter (s.gpr .r15) ∧
+      t.zf = decide (counter (s.gpr .r15) = s.mem.readW (off (s.gpr .rbp) 8) 64) ∧
+      Divide.Keeps [.rax] s t := by
+  apply WP.of_runBlock
+  simp only [check, counter, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc,
+    execShift, execAlu, State.load64, ea_at, hr, RegUpd.gpr_setReg, RegUpd.gpr_setFlags,
+    RegUpd.gpr_arithFlags, RegUpd.mem_setReg, RegUpd.mem_setFlags, RegUpd.mem_arithFlags,
+    RegUpd.rd_setReg, RegUpd.rd_setFlags, RegUpd.rd_arithFlags,
+    RegUpd.wr_setReg, RegUpd.wr_setFlags, RegUpd.wr_arithFlags,
+    RegUpd.zf_arithFlags, reduceCtorEq, ite_true, ite_false, and_self,
+    show 1 ≤ (7 : Nat) ∧ (7 : Nat) ≤ 63 from by decide,
+    show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl,
+    Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨trivial, ?_, ?_⟩
+  · apply Bool.eq_iff_iff.mpr
+    simp only [beq_iff_eq, ReferenceStart.sub_zero_iff]
+    exact ⟨fun h => decide_eq_true h, of_decide_eq_true⟩
+  · constructor
+    · intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      simp only [RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags, hr, ite_false]
+    all_goals rfl
+
+theorem counter_nat (index : Addr) : counter index = BitVec.ofNat 64 (index.toNat / 128 + 1) := by
+  have shifted : index >>> 7 = BitVec.ofNat 64 (index.toNat / 128) := by
+    apply BitVec.eq_of_toNat_eq
+    rw [BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, BitVec.toNat_ofNat,
+      Nat.mod_eq_of_lt (by have := index.isLt; omega)]
+  unfold counter
+  rw [shifted]
+  exact (BitVec.ofNat_add _ _).symm
+
+theorem counter_ne_zero (index : Addr) : counter index ≠ 0 := by
+  have bound : index.toNat / 128 + 1 < 2 ^ 64 := by have := index.isLt; omega
+  intro h
+  have nat := congrArg BitVec.toNat h
+  rw [counter_nat, BitVec.toNat_ofNat, Nat.mod_eq_of_lt bound] at nat
+  change index.toNat / 128 + 1 = 0 at nat
+  omega
+
+theorem wordArgs_ok (s : State)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block wordArgs) s fun t => t.gpr .rcx = AddressCalls.work s ∧
+      t.gpr .rax = s.gpr .r15 &&& 127 ∧ Divide.Keeps [.rcx, .rax] s t := by
+  apply WP.of_runBlock
+  simp only [wordArgs, AddressCalls.work, runBlock_cons, runStep_some, runBlock_nil,
+    exec, readSrc, State.load64, ea_at, hr, execAlu,
+    RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, reduceCtorEq, ite_true, ite_false,
+    show BitVec.signExtend 64 (127 : BitVec 32) = (127 : Addr) from rfl,
+    Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left']
+  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, RegUpd.gpr_arithFlags, hr.1, hr.2, ite_false]
+  all_goals rfl
+
+theorem index_nat (index : Addr) : index &&& 127 = BitVec.ofNat 64 (index.toNat % 128) := by
+  apply BitVec.eq_of_toNat_eq
+  rw [BitVec.toNat_and, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)]
+  exact Nat.and_two_pow_sub_one_eq_mod index.toNat 7
+
+end VG.Proof.Argon2.X86_64.AddressCache

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSave.lean

@@ -0,0 +1,65 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheMeta
+
+/-! Save the public cache counter without disturbing scratch or header fields. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+theorem save_ok (s : State) (hw : InRegions s.wr (off (s.gpr .rbp) 8) 8) :
+    WP isa (.block save) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rbp) 8) (s.gpr .rax) ∧
+      t.gpr = s.gpr ∧ t.rd = s.rd ∧ t.wr = s.wr ∧ t.mxcsr = s.mxcsr := by
+  apply WP.of_runBlock
+  simp only [save, 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⟩
+
+structure Saved (s t : State) : Prop where
+  mem : t.mem = s.mem.writeW (off (s.gpr .rbp) 8) (s.gpr .rax)
+  regs : t.gpr = s.gpr
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  mxcsr : t.mxcsr = s.mxcsr
+  ready : AddressCalls.Ready t
+  work_eq : AddressCalls.work t = AddressCalls.work s
+  frame : Frame [⟨off (s.gpr .rbp) 8, 8⟩] s.mem t.mem
+
+theorem save_ready (s : State) (h : AddressCalls.Ready s)
+    (hw : InRegions s.wr (off (s.gpr .rbp) 8) 8) : WP isa (.block save) s (Saved s) := by
+  refine (save_ok s hw).mono ?_
+  rintro t ⟨mem, regs, rd, wr, mx⟩
+  have work' : AddressCalls.work t = AddressCalls.work s := by
+    unfold AddressCalls.work
+    rw [regs, mem, Mem.readW_writeW_sep (Offset.sep _ (by decide) (by decide) (by decide)) (by decide)]
+  have ready : AddressCalls.Ready t := by
+    constructor
+    · rw [rd, wr, regs]; exact h.frameRead
+    · rw [work', wr]; exact h.workWrite
+    · rw [regs, work']; exact h.frameWork
+    · rw [regs]; exact h.frameStack
+    · rw [regs, work']; exact h.stackWork
+  refine ⟨mem, regs, rd, wr, mx, ready, work', ?_⟩
+  rw [mem]
+  exact (Frame.refl _ _).writeW (r := ⟨off (s.gpr .rbp) 8, 8⟩) (by simp) _
+    (Region.contains_self _ _)
+
+theorem Saved.read {s t : State} (h : Saved s t) (d : Nat)
+    (hd : d + 8 ≤ 8 ∨ 16 ≤ d) (bound : d + 8 ≤ 272) :
+    t.mem.readW (off (t.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 := by
+  rw [h.regs, h.mem]
+  exact Mem.readW_writeW_sep (Offset.sep _ hd (by omega) (by decide)) (by decide)
+
+theorem Saved.words {s t : State} {p : Params} {pass lane slice old counter : Nat}
+    (h : Saved s t) (words : AddressHeader.Words p pass lane slice old s)
+    (value : s.gpr .rax = BitVec.ofNat 64 counter) :
+    AddressHeader.Words p pass lane slice counter t := by
+  refine ⟨(h.read 0 (by decide) (by decide)).trans words.passWord,
+    ?_, ?_, (h.read 240 (by decide) (by decide)).trans words.blocksWord,
+    (h.read 72 (by decide) (by decide)).trans words.passesWord,
+    (h.read 112 (by decide) (by decide)).trans words.variantWord, ?_⟩
+  · rw [h.regs]; exact words.laneWord
+  · rw [h.regs]; exact words.sliceWord
+  · rw [h.regs, h.mem, Mem.readW_writeW_self64, value]
+
+end VG.Proof.Argon2.X86_64.AddressCache

lean/VerifiedGarbage/Proof/Argon2/X86_64/AddressCacheSelect.lean

@@ -0,0 +1,114 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheSave
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressGeneration
+
+/-! Regenerate only when the public one-based block counter changes. -/
+
+namespace VG.Proof.Argon2.X86_64.AddressCache
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.AddressCache
+
+def wanted (s : State) : Nat := (s.gpr .r15).toNat / 128 + 1
+
+def writes (s : State) : List Region :=
+  [⟨AddressCalls.work s, 8192⟩, below (s.gpr .rsp) 8, ⟨off (s.gpr .rbp) 8, 8⟩]
+
+structure Ready (p : Params) (pass lane slice old : Nat) (s : State) : Prop where
+  layout : AddressCalls.Ready s
+  reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8
+  write : InRegions s.wr (off (s.gpr .rbp) 8) 8
+  words : AddressHeader.Words p pass lane slice old s
+  cached : counter (s.gpr .r15) = s.mem.readW (off (s.gpr .rbp) 8) 64 →
+    blockAt s.mem (off (AddressCalls.work s) 6144) = addressBlock p pass lane slice (wanted s)
+
+theorem ready_zero (p : Params) (pass lane slice : Nat) (s : State)
+    (layout : AddressCalls.Ready s)
+    (reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8)
+    (write : InRegions s.wr (off (s.gpr .rbp) 8) 8)
+    (words : AddressHeader.Words p pass lane slice 0 s) : Ready p pass lane slice 0 s :=
+  ⟨layout, reads, write, words, fun same => False.elim
+    (counter_ne_zero _ (same.trans words.counterWord))⟩
+
+structure Selected (s t : State) (p : Params) (pass lane slice : Nat) : Prop where
+  block : blockAt t.mem (off (AddressCalls.work s) 6144) = addressBlock p pass lane slice (wanted s)
+  layout : AddressCalls.Ready t
+  work_eq : AddressCalls.work t = AddressCalls.work s
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (writes s) s.mem t.mem
+  mxcsr : t.mxcsr = s.mxcsr
+  counterWord : t.mem.readW (off (t.gpr .rbp) 8) 64 = counter (s.gpr .r15)
+
+theorem check_stable {s a : State} (h : AddressCalls.Ready s) (k : Divide.Keeps [.rax] s a) :
+    AddressCalls.Stable s a := by
+  apply AddressCalls.stable_of_frame h _ k.rd k.wr _ k.mxcsr
+  · intro r hr
+    apply k.regs
+    simp only [calleeSaved, List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> decide
+  · rw [k.mem]; exact Frame.refl _ _
+
+theorem selected_ok (p : Params) (pass lane slice old : Nat) (s : State)
+    (h : Ready p pass lane slice old s) :
+    WP isa select s (Selected s · p pass lane slice) := by
+  unfold select
+  refine WP.seq ((check_ok s (h.reads 8 (by simp))).mono ?_)
+  rintro a ⟨value, flag, keeps⟩
+  have stableA := check_stable h.layout keeps
+  refine WP.ite (decide (counter (s.gpr .r15) = s.mem.readW (off (s.gpr .rbp) 8) 64))
+    (by simp only [eval, flag]) ?_ ?_
+  · intro same
+    have equal := of_decide_eq_true same
+    apply WP.of_runBlock
+    simp only [runBlock_nil, Option.some.injEq, exists_eq_left']
+    refine ⟨?_, stableA.ready, stableA.work_eq, stableA.regs, keeps.rd, keeps.wr,
+      ?_, keeps.mxcsr, ?_⟩
+    · rw [keeps.mem]; exact h.cached equal
+    · rw [keeps.mem]; exact Frame.refl _ _
+    · rw [stableA.regs .rbp (by simp [calleeSaved]), keeps.mem]; exact equal.symm
+  · intro _
+    have write : InRegions a.wr (off (a.gpr .rbp) 8) 8 := by
+      rw [keeps.wr, stableA.regs .rbp (by simp [calleeSaved])]; exact h.write
+    refine WP.seq ((save_ready a stableA.ready write).mono ?_)
+    intro b saved
+    have words : AddressHeader.Words p pass lane slice (wanted s) b := by
+      apply saved.words (stableA.words h.layout h.words)
+      rw [value, counter_nat]; rfl
+    have reads : ∀ d ∈ [0, 8, 72, 112, 240], InRegions (b.rd ++ b.wr) (off (b.gpr .rbp) d) 8 := by
+      rw [saved.rd, saved.wr, saved.regs]; exact stableA.reads h.reads
+    refine (AddressCalls.code_ok p pass lane slice (wanted s) b saved.ready reads words).mono ?_
+    rintro t ⟨generated, mx⟩
+    have workB : AddressCalls.work b = AddressCalls.work s := saved.work_eq.trans stableA.work_eq
+    have regsB (r : Reg) (hr : r ∈ calleeSaved) : b.gpr r = s.gpr r :=
+      (congrFun saved.regs r).trans (stableA.regs r hr)
+    have regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r :=
+      fun r hr => (generated.regs r hr).trans (regsB r hr)
+    have firstFrame : Frame (writes s) s.mem b.mem := by
+      have frame := saved.frame
+      rw [stableA.regs .rbp (by simp [calleeSaved]), keeps.mem] at frame
+      exact frame.mono (by intro r hr; simp only [List.mem_singleton] at hr; subst r; simp [writes])
+    have finalFrame : Frame (writes s) b.mem t.mem := by
+      have frame := generated.frame
+      rw [AddressCalls.writes, workB, regsB .rsp (by simp [calleeSaved])] at frame
+      exact frame.mono (by
+        intro r hr
+        simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+        rcases hr with rfl | rfl <;> simp [writes])
+    refine ⟨?_, generated.ready, generated.work.trans workB, regs,
+      generated.rd.trans (saved.rd.trans keeps.rd), generated.wr.trans (saved.wr.trans keeps.wr),
+      firstFrame.trans finalFrame, mx.trans (saved.mxcsr.trans keeps.mxcsr), ?_⟩
+    · have block := generated.block
+      rw [workB] at block
+      exact block
+    · have preserved : t.mem.readW (off (b.gpr .rbp) 8) 64 = b.mem.readW (off (b.gpr .rbp) 8) 64 :=
+        generated.frame.readW (r := ⟨b.gpr .rbp, 272⟩)
+          (Offset.contains_base _ (by decide) (by decide)) (by
+            intro r hr
+            simp only [AddressCalls.writes, List.mem_cons, List.not_mem_nil, or_false] at hr
+            rcases hr with rfl | rfl
+            · exact saved.ready.frameWork
+            · exact saved.ready.frameStack) (by decide)
+      rw [generated.regs .rbp (by simp [calleeSaved]), preserved, saved.regs, saved.mem,
+        Mem.readW_writeW_self64, value]
+
+end VG.Proof.Argon2.X86_64.AddressCache