Argon2 on x86-64: prove compression calls and block updates

lean/VerifiedGarbage/Impl/Argon2/X86_64/FillCompress.lean

@@ -0,0 +1,31 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillWrite
+import VerifiedGarbage.Spec.Argon2.Contract
+
+/-! Compress the selected previous/reference blocks and update the current
+matrix cell. Pointer setup supplied `r10` (current), `rdi` (previous), and
+`rsi` (reference). The derivation frame holds the pass at offset zero and
+scratch pointer at offset 248; offset 16 retains the destination across G.
+The first 4096 scratch bytes belong to G, and its output is at offset 4096.
+-/
+
+namespace VG.Impl.Argon2.X86_64.FillCompress
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def saveCurrent : List Instr := [.store (at_ .rbp 16) .r10]
+
+def compressArgs : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 248)), .mov .rdx (.reg .rcx), .alu .add .rdx (.imm 4096)]
+
+def writeArgs : List Instr := [
+  .mov .rdi (.mem (at_ .rbp 16)), .mov .rsi (.mem (at_ .rbp 248)),
+  .alu .add .rsi (.imm 4096), .mov .r9 (.mem (at_ .rbp 0))]
+
+def operation : Prog isa :=
+  .seq (.call Spec.Argon2.compressApi.name VG.Impl.Argon2.X86_64.compress)
+    (.seq (.block writeArgs) FillWrite.code)
+
+def code : Prog isa := .seq (.block saveCurrent) (.seq (.block compressArgs) operation)
+
+end VG.Impl.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressArgs.lean

@@ -0,0 +1,64 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillCompress
+import VerifiedGarbage.Proof.Argon2.X86_64.Memory
+import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep
+
+/-! Save the current cell across G and reload the block-write arguments. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillCompress
+
+theorem saveCurrent_ok (s : State)
+    (hw : InRegions s.wr (off (s.gpr .rbp) 16) 8) :
+    WP isa (.block saveCurrent) s fun t =>
+      t.mem = s.mem.writeW (off (s.gpr .rbp) 16) (s.gpr .r10) ∧
+      t.gpr = s.gpr ∧ t.rd = s.rd ∧ t.wr = s.wr ∧ t.mxcsr = s.mxcsr := by
+  apply WP.of_runBlock
+  simp only [saveCurrent, 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 compressArgs_ok (s : State)
+    (hr : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8) :
+    WP isa (.block compressArgs) s fun t =>
+      t.gpr .rcx = s.mem.readW (off (s.gpr .rbp) 248) 64 ∧
+      t.gpr .rdx = s.mem.readW (off (s.gpr .rbp) 248) 64 + 4096 ∧
+      Divide.Keeps [.rcx, .rdx] s t := by
+  apply WP.of_runBlock
+  simp only [compressArgs, 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, Option.map_some, Option.bind_some,
+    Option.some.injEq, exists_eq_left',
+    show BitVec.signExtend 64 (4096 : BitVec 32) = (4096 : Addr) from rfl]
+  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 writeArgs_ok (s : State)
+    (destRead : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 16) 8)
+    (workRead : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 248) 8)
+    (passRead : InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) 0) 8) :
+    WP isa (.block writeArgs) s fun t =>
+      t.gpr .rdi = s.mem.readW (off (s.gpr .rbp) 16) 64 ∧
+      t.gpr .rsi = s.mem.readW (off (s.gpr .rbp) 248) 64 + 4096 ∧
+      t.gpr .r9 = s.mem.readW (off (s.gpr .rbp) 0) 64 ∧
+      Divide.Keeps [.rdi, .rsi, .r9] s t := by
+  apply WP.of_runBlock
+  simp only [writeArgs, runBlock_cons, runStep_some, runBlock_nil, exec,
+    readSrc, State.load64, ea_at, destRead, workRead, passRead, execAlu,
+    RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg,
+    RegUpd.gpr_arithFlags, RegUpd.mem_arithFlags, RegUpd.rd_arithFlags,
+    RegUpd.wr_arithFlags, reduceCtorEq, ite_true, ite_false,
+    Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left',
+    show BitVec.signExtend 64 (4096 : BitVec 32) = (4096 : Addr) from rfl]
+  refine ⟨trivial, 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.1, hr.2.2, ite_false]
+  all_goals rfl
+
+end VG.Proof.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCall.lean

@@ -0,0 +1,101 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.Compress
+import VerifiedGarbage.Proof.Framework.X86_64.RelCT
+
+/-! Invoke the verified compression primitive with narrowed permissions,
+retaining the surrounding matrix and derivation frame. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64
+
+structure CallReady (s : State) : Prop where
+  left : Covers [⟨s.gpr .rdi, 1024⟩] (s.rd ++ s.wr)
+  right : Covers [⟨s.gpr .rsi, 1024⟩] (s.rd ++ s.wr)
+  output : Covers [⟨s.gpr .rdx, 1024⟩] s.wr
+  scratch : Covers [⟨s.gpr .rcx, 4096⟩] s.wr
+  leftScratch : (⟨s.gpr .rdi, 1024⟩ : Region).Disjoint ⟨s.gpr .rcx, 4096⟩
+  rightScratch : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨s.gpr .rcx, 4096⟩
+  outputScratch : (⟨s.gpr .rdx, 1024⟩ : Region).Disjoint ⟨s.gpr .rcx, 4096⟩
+  stackLeft : (below (s.gpr .rsp) 8).Disjoint ⟨s.gpr .rdi, 1024⟩
+  stackRight : (below (s.gpr .rsp) 8).Disjoint ⟨s.gpr .rsi, 1024⟩
+  stackOutput : (below (s.gpr .rsp) 8).Disjoint ⟨s.gpr .rdx, 1024⟩
+  stackScratch : (below (s.gpr .rsp) 8).Disjoint ⟨s.gpr .rcx, 4096⟩
+
+structure Called (s t : State) : Prop where
+  result : Spec.Argon2.blockAt t.mem (s.gpr .rdx) = Spec.Argon2.compress
+    (Spec.Argon2.blockAt s.mem (s.gpr .rdi)) (Spec.Argon2.blockAt s.mem (s.gpr .rsi))
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame [⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .rcx, 4096⟩, below (s.gpr .rsp) 8] s.mem t.mem
+
+theorem noSp : NoSp Impl.Argon2.X86_64.compress := by
+  have h : Impl.Argon2.X86_64.compress.allInstrs (fun i => !Taint.clobbers i .rsp) = true :=
+    by lit_decide
+  rw [Code.allInstrs_eq, List.all_eq_true] at h
+  intro i hi
+  simpa only [Bool.not_eq_true'] using h i hi
+
+theorem depth : Impl.Argon2.X86_64.compress.depth = 0 := by lit_decide
+
+theorem call_hyps (s : State) (h : CallReady s) :
+    compressLocal.pre (s.callEntry.withRegions [⟨s.gpr .rdi, 1024⟩, ⟨s.gpr .rsi, 1024⟩]
+      [⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .rcx, 4096⟩]) ∧
+    Covers [⟨s.gpr .rdi, 1024⟩, ⟨s.gpr .rsi, 1024⟩,
+      ⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .rcx, 4096⟩] (s.rd ++ s.wr) ∧
+    Covers [⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .rcx, 4096⟩] s.wr := by
+  have g : ∀ r, r ≠ .rsp → s.callEntry.gpr r = s.gpr r := fun _ hr => State.callEntry_gpr s hr
+  refine ⟨?_, ?_, ?_⟩
+  · simp only [compressLocal, State.withRegions_gpr, State.withRegions_rd,
+      State.withRegions_wr, g _ (by decide : Reg.rdi ≠ .rsp),
+      g _ (by decide : Reg.rsi ≠ .rsp), g _ (by decide : Reg.rdx ≠ .rsp),
+      g _ (by decide : Reg.rcx ≠ .rsp), State.callEntry_rsp]
+    exact ⟨trivial, trivial, h.outputScratch, h.leftScratch, h.rightScratch,
+      h.stackOutput, h.stackScratch⟩
+  · intro p n ⟨r, hr, hc⟩
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl | rfl | rfl
+    · exact h.left p n ⟨_, List.mem_singleton_self _, hc⟩
+    · exact h.right p n ⟨_, List.mem_singleton_self _, hc⟩
+    · obtain ⟨r, hr, hc⟩ := h.output p n ⟨_, List.mem_singleton_self _, hc⟩
+      exact ⟨r, List.mem_append_right _ hr, hc⟩
+    · obtain ⟨r, hr, hc⟩ := h.scratch p n ⟨_, List.mem_singleton_self _, hc⟩
+      exact ⟨r, List.mem_append_right _ hr, hc⟩
+  · intro p n ⟨r, hr, hc⟩
+    simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+    rcases hr with rfl | rfl
+    · exact h.output p n ⟨_, List.mem_singleton_self _, hc⟩
+    · exact h.scratch p n ⟨_, List.mem_singleton_self _, hc⟩
+
+theorem callEntry_block (s : State) (p : Addr)
+    (h : (below (s.gpr .rsp) 8).Disjoint ⟨p, 1024⟩) :
+    Spec.Argon2.blockAt s.callEntry.mem p = Spec.Argon2.blockAt s.mem p := by
+  have frame : Frame [below (s.gpr .rsp) 8] s.mem s.callEntry.mem := by
+    rw [State.callEntry_mem]
+    exact (Frame.refl _ _).writeW (r := below (s.gpr .rsp) 8) (by simp) _
+      (below_call _ (by decide) (by decide))
+  apply Vector.ext
+  intro i hi
+  have read := frame.readW (r := ⟨p, 1024⟩) (a := off p (8 * i)) (w := 64)
+    (Offset.contains_base p (d := 8 * i) (n := 8) (k := 1024) (by omega) (by omega))
+    (by intro r hr; simp only [List.mem_singleton] at hr; subst r; exact h.symm) (by decide)
+  rw [← blockAt_get s.callEntry.mem p ⟨i, hi⟩, ← blockAt_get s.mem p ⟨i, hi⟩] at read
+  exact read
+
+theorem call_ok (name : String) (s : State) (h : CallReady s) :
+    WP isa (.call name Impl.Argon2.X86_64.compress) s (Called s) := by
+  obtain ⟨pre, cover, writes⟩ := call_hyps s h
+  refine WP.call (k := compressLocal) compress_correct noSp (by rw [depth]; decide)
+    pre cover writes ?_
+  intro t rd wr regs frame _ ⟨u, memU, regsU, result⟩
+  change Spec.Argon2.blockAt u.mem (s.callEntry.gpr .rdx) = Spec.Argon2.compress
+    (Spec.Argon2.blockAt s.callEntry.mem (s.callEntry.gpr .rdi))
+    (Spec.Argon2.blockAt s.callEntry.mem (s.callEntry.gpr .rsi)) at result
+  rw [State.callEntry_gpr _ (by decide : Reg.rdx ≠ .rsp),
+    State.callEntry_gpr _ (by decide : Reg.rdi ≠ .rsp),
+    State.callEntry_gpr _ (by decide : Reg.rsi ≠ .rsp), memU,
+    callEntry_block s _ h.stackLeft, callEntry_block s _ h.stackRight] at result
+  rw [depth] at frame
+  exact ⟨result, regs, rd, wr, frame⟩
+
+end VG.Proof.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCallCT.lean

@@ -0,0 +1,30 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCall
+
+/-! Compression calls reveal only their argument addresses and stack pointer. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64
+
+theorem call_rel (name : String) {P : State → State → Prop}
+    (pre : ∀ s t, P s t → CallReady s ∧ CallReady t ∧
+      s.gpr .rdi = t.gpr .rdi ∧ s.gpr .rsi = t.gpr .rsi ∧
+      s.gpr .rdx = t.gpr .rdx ∧ s.gpr .rcx = t.gpr .rcx ∧ s.gpr .rsp = t.gpr .rsp) :
+    RelCT isa P (.call name Impl.Argon2.X86_64.compress) (fun _ _ => True) := by
+  apply RelCT.callEx (k := compressLocal) compress_correct compress_ct
+  intro s t hp
+  obtain ⟨hs, ht, di, si, dx, cx, sp⟩ := pre s t hp
+  obtain ⟨ps, cs, ws⟩ := call_hyps s hs
+  obtain ⟨pt, ct, wt⟩ := call_hyps t ht
+  refine ⟨_, _, _, _, ps, pt, ?_, cs, ws, ct, wt, sp⟩
+  change s.callEntry.gpr .rdi = t.callEntry.gpr .rdi ∧
+    s.callEntry.gpr .rsi = t.callEntry.gpr .rsi ∧
+    s.callEntry.gpr .rdx = t.callEntry.gpr .rdx ∧
+    s.callEntry.gpr .rcx = t.callEntry.gpr .rcx
+  simp only [State.callEntry_gpr _ (by decide : Reg.rdi ≠ .rsp),
+    State.callEntry_gpr _ (by decide : Reg.rsi ≠ .rsp),
+    State.callEntry_gpr _ (by decide : Reg.rdx ≠ .rsp),
+    State.callEntry_gpr _ (by decide : Reg.rcx ≠ .rsp)]
+  exact ⟨di, si, dx, cx⟩
+
+end VG.Proof.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressLit.lean

@@ -0,0 +1,11 @@
+import VerifiedGarbage.Proof.Framework.X86_64.Lit
+import VerifiedGarbage.Impl.Argon2.X86_64.FillCompress
+
+/-! Checked literals for compression and the enclosing argument setup. -/
+
+namespace VG
+
+materialize_code Impl.Argon2.X86_64.FillCompress.operation
+materialize_code Impl.Argon2.X86_64.FillCompress.code
+
+end VG

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperation.lean

@@ -0,0 +1,101 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressArgs
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCall
+import VerifiedGarbage.Proof.Argon2.X86_64.FillWriteCover
+
+/-! Compression followed by first/later-pass writing, preserving the frame
+slots and the old destination cell across the compression call. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillCompress
+
+def callWrites (s : State) : List Region :=
+  [⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .rcx, 4096⟩, below (s.gpr .rsp) 8]
+
+def destination (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 16) 64
+
+def pass (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 0) 64
+
+structure OperationReady (s : State) : Prop where
+  call : CallReady s
+  frameRead : ∀ d ∈ [0, 16, 248], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8
+  workWord : s.mem.readW (off (s.gpr .rbp) 248) 64 = s.gpr .rcx
+  outputPointer : s.gpr .rcx + 4096 = s.gpr .rdx
+  destinationWrite : Covers [⟨destination s, 1024⟩] s.wr
+  frameSafe : ∀ r ∈ callWrites s, (⟨s.gpr .rbp, 272⟩ : Region).Disjoint r
+  destinationSafe : ∀ r ∈ callWrites s, (⟨destination s, 1024⟩ : Region).Disjoint r
+
+structure OperationDone (s t : State) : Prop where
+  block : blockAt t.mem (destination s) =
+    let next := Spec.Argon2.compress (blockAt s.mem (s.gpr .rdi)) (blockAt s.mem (s.gpr .rsi))
+    if pass s = 0 then next else xorBlock next (blockAt s.mem (destination s))
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (⟨destination s, 1024⟩ :: callWrites s) s.mem t.mem
+
+theorem frame_word {s t : State} (h : OperationReady s) (called : Called s t)
+    (d : Nat) (hd : d + 8 ≤ 272) :
+    t.mem.readW (off (s.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 :=
+  called.frame.readW (r := ⟨s.gpr .rbp, 272⟩)
+    (Offset.contains_base _ hd (by omega)) h.frameSafe (by decide)
+
+theorem destination_unchanged {s t : State} (h : OperationReady s) (called : Called s t) :
+    blockAt t.mem (destination s) = blockAt s.mem (destination s) := by
+  apply Vector.ext
+  intro i hi
+  have read : t.mem.readW (off (destination s) (8 * i)) 64 =
+      s.mem.readW (off (destination s) (8 * i)) 64 :=
+    called.frame.readW (r := ⟨destination s, 1024⟩)
+      (Offset.contains_base _ (by omega) (by omega)) h.destinationSafe (by decide)
+  rw [← blockAt_get t.mem (destination s) ⟨i, hi⟩,
+    ← blockAt_get s.mem (destination s) ⟨i, hi⟩] at read
+  exact read
+
+theorem operation_ok (s : State) (h : OperationReady s) :
+    WP isa operation s (OperationDone s) := by
+  unfold operation
+  refine WP.seq ((call_ok _ s h.call).mono ?_)
+  intro a called
+  have bp : a.gpr .rbp = s.gpr .rbp := called.regs .rbp (by simp [calleeSaved])
+  have reads (d : Nat) (hd : d ∈ [0, 16, 248]) :
+      InRegions (a.rd ++ a.wr) (off (a.gpr .rbp) d) 8 := by
+    rw [called.rd, called.wr, bp]; exact h.frameRead d hd
+  refine WP.seq ((writeArgs_ok a (reads 16 (by simp)) (reads 248 (by simp))
+    (reads 0 (by simp))).mono ?_)
+  rintro b ⟨dest, src, counter, keeps⟩
+  have dest' : b.gpr .rdi = destination s := by
+    rw [dest, bp, frame_word h called 16 (by decide), destination]
+  have src' : b.gpr .rsi = s.gpr .rdx := by
+    rw [src, bp, frame_word h called 248 (by decide), h.workWord, h.outputPointer]
+  have counter' : b.gpr .r9 = pass s := by
+    rw [counter, bp, frame_word h called 0 (by decide), pass]
+  have readable : Covers [⟨b.gpr .rsi, 1024⟩] (b.rd ++ b.wr) := by
+    rw [src', keeps.rd, keeps.wr, called.rd, called.wr]
+    intro p n hp
+    obtain ⟨r, hr, hc⟩ := h.call.output p n hp
+    exact ⟨r, List.mem_append_right _ hr, hc⟩
+  have writable : Covers [⟨b.gpr .rdi, 1024⟩] b.wr := by
+    rw [dest', keeps.wr, called.wr]; exact h.destinationWrite
+  have sep : (⟨b.gpr .rsi, 1024⟩ : Region).Disjoint ⟨b.gpr .rdi, 1024⟩ := by
+    rw [src', dest']; exact (h.destinationSafe _ (by simp [callWrites])).symm
+  refine (FillWrite.code_cover_ok b readable writable sep).mono ?_
+  rintro t ⟨value, frame, tk, _⟩
+  refine ⟨?_, ?_, tk.2.1.trans (keeps.rd.trans called.rd),
+    tk.2.2.trans (keeps.wr.trans called.wr), ?_⟩
+  · rw [dest', src', counter', keeps.mem, called.result, destination_unchanged h called] at value
+    exact value
+  · intro r hr
+    have ne : r ≠ .rax := 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
+    have nk : r ∉ [Reg.rdi, .rsi, .r9] := 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 (tk.1 r ne).trans ((keeps.regs r nk).trans (called.regs r hr))
+  · rw [dest'] at frame
+    rw [keeps.mem] at frame
+    exact (called.frame.mono (by intro r hr; exact List.mem_cons_of_mem _ hr)).trans
+      (frame.mono (by simp))
+
+end VG.Proof.Argon2.X86_64.FillCompress