Argon2 on x86-64: compose the complete block update proof

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

@@ -26,6 +26,8 @@ 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)
+def setup : Prog isa := .seq (.block saveCurrent) (.block compressArgs)
+
+def code : Prog isa := .seq setup operation
 
 end VG.Impl.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompress.lean

@@ -0,0 +1,52 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressSetup
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressLit
+
+/-! The complete compression/update sequence from allocation and frame invariants. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillCompress
+
+def writes (s : State) : List Region :=
+  [⟨s.gpr .r10, 1024⟩, ⟨work s + 4096, 1024⟩, ⟨work s, 4096⟩,
+    below (s.gpr .rsp) 8, ⟨off (s.gpr .rbp) 16, 8⟩]
+
+structure Done (s t : State) : Prop where
+  block : blockAt t.mem (s.gpr .r10) =
+    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 (s.gpr .r10))
+  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
+
+theorem code_ok (s : State) (h : Ready s) : WP isa code s (Done s) := by
+  unfold code
+  refine WP.seq ((setup_ok s h).mono ?_)
+  intro a prepared
+  refine (operation_ok a prepared.ready).mono ?_
+  intro t done
+  refine ⟨?_, fun r hr => (done.regs r hr).trans (prepared.regs r hr),
+    done.rd.trans prepared.rd, done.wr.trans prepared.wr, ?_⟩
+  · have block := done.block
+    rw [prepared.oldBlock, prepared.dest, prepared.counter, prepared.leftBlock,
+      prepared.rightBlock] at block
+    exact block
+  · have frame : Frame (writes s) a.mem t.mem := by
+      have original := done.frame
+      rw [prepared.dest] at original
+      simp only [callWrites, prepared.output, prepared.scratch,
+        prepared.regs .rsp (by simp [calleeSaved])] at original
+      exact original.mono (by intro r hr; exact List.mem_append_left _ hr)
+    have savedFrame : Frame (writes s) s.mem a.mem := prepared.frame.mono (by
+      intro r hr
+      simp only [prefixWrites, List.mem_singleton] at hr
+      subst r
+      simp [writes])
+    exact savedFrame.trans frame
+
+theorem code_mx_ok (s : State) (h : Ready s) :
+    WP isa code s fun t => Done s t ∧ t.mxcsr = s.mxcsr :=
+  WP.mono_mx (by lit_decide) (code_ok s h) (fun _ done mx => ⟨done, mx⟩)
+
+end VG.Proof.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCT.lean

@@ -0,0 +1,54 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompress
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressOperationCT
+
+/-! Compose the setup trace with compression and the full block write. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillCompress
+
+structure CodeRelated (s t : State) : Prop where
+  left : Ready s
+  right : Ready t
+  args : ∀ r ∈ [Reg.rdi, .rsi, .r10, .rsp, .rbp], s.gpr r = t.gpr r
+  scratch : work s = work t
+  counter : pass s = pass t
+
+theorem setup_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp)
+    setup (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [.rbp])
+    (fun _ _ h => Taint.agree_ofRegs (by
+      intro r hr
+      simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+      subst r
+      exact h)) (by taint_decide)
+
+theorem prepared_public {s t a b : State} (h : CodeRelated s t)
+    (ha : Prepared s a) (hb : Prepared t b) : Related a b := by
+  refine ⟨ha.ready, hb.ready, ?_, ha.dest.trans ((h.args .r10 (by simp)).trans hb.dest.symm),
+    ha.counter.trans (h.counter.trans hb.counter.symm)⟩
+  intro r hr
+  simp only [List.mem_cons, List.not_mem_nil, or_false] at hr
+  rcases hr with rfl | rfl | rfl | rfl | rfl | rfl
+  · exact ha.left.trans ((h.args .rdi (by simp)).trans hb.left.symm)
+  · exact ha.right.trans ((h.args .rsi (by simp)).trans hb.right.symm)
+  · exact ha.output.trans ((congrArg (· + (4096 : Addr)) h.scratch).trans hb.output.symm)
+  · exact ha.scratch.trans (h.scratch.trans hb.scratch.symm)
+  · exact (ha.regs .rsp (by simp [calleeSaved])).trans
+      ((h.args .rsp (by simp)).trans (hb.regs .rsp (by simp [calleeSaved])).symm)
+  · exact (ha.regs .rbp (by simp [calleeSaved])).trans
+      ((h.args .rbp (by simp)).trans (hb.regs .rbp (by simp [calleeSaved])).symm)
+
+theorem setup_public_rel : RelCT isa CodeRelated setup Related := by
+  have trace := setup_rel.mono (P' := CodeRelated)
+    (fun _ _ h => h.args .rbp (by simp)) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨setup_ok s h.left, setup_ok t h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  exact prepared_public hp ha hb
+
+theorem code_rel : RelCT isa CodeRelated code (fun _ _ => True) :=
+  setup_public_rel.seq operation_rel
+
+end VG.Proof.Argon2.X86_64.FillCompress

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressSetup.lean

@@ -0,0 +1,162 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressOperation
+
+/-! Establish compression-and-write invariants from the frame and allocations. -/
+
+namespace VG.Proof.Argon2.X86_64.FillCompress
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillCompress
+
+def work (s : State) : Addr := s.mem.readW (off (s.gpr .rbp) 248) 64
+
+def prefixWrites (s : State) : List Region := [⟨off (s.gpr .rbp) 16, 8⟩]
+
+structure Ready (s : State) : Prop where
+  frameRead : ∀ d ∈ [0, 16, 248], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8
+  frameWrite : InRegions s.wr (off (s.gpr .rbp) 16) 8
+  leftRead : Covers [⟨s.gpr .rdi, 1024⟩] (s.rd ++ s.wr)
+  rightRead : Covers [⟨s.gpr .rsi, 1024⟩] (s.rd ++ s.wr)
+  destinationWrite : Covers [⟨s.gpr .r10, 1024⟩] s.wr
+  workWrite : Covers [⟨work s, 5120⟩] s.wr
+  leftWork : (⟨s.gpr .rdi, 1024⟩ : Region).Disjoint ⟨work s, 5120⟩
+  rightWork : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨work s, 5120⟩
+  destinationWork : (⟨s.gpr .r10, 1024⟩ : Region).Disjoint ⟨work s, 5120⟩
+  frameWork : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨work s, 5120⟩
+  leftFrame : (⟨s.gpr .rdi, 1024⟩ : Region).Disjoint ⟨s.gpr .rbp, 272⟩
+  rightFrame : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨s.gpr .rbp, 272⟩
+  destinationFrame : (⟨s.gpr .r10, 1024⟩ : Region).Disjoint ⟨s.gpr .rbp, 272⟩
+  stackLeft : (below (s.gpr .rsp) 8).Disjoint ⟨s.gpr .rdi, 1024⟩
+  stackRight : (below (s.gpr .rsp) 8).Disjoint ⟨s.gpr .rsi, 1024⟩
+  stackWork : (below (s.gpr .rsp) 8).Disjoint ⟨work s, 5120⟩
+  destinationStack : (⟨s.gpr .r10, 1024⟩ : Region).Disjoint (below (s.gpr .rsp) 8)
+  frameStack : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint (below (s.gpr .rsp) 8)
+
+structure Prepared (s t : State) : Prop where
+  ready : OperationReady t
+  dest : destination t = s.gpr .r10
+  counter : pass t = pass s
+  scratch : t.gpr .rcx = work s
+  output : t.gpr .rdx = work s + 4096
+  left : t.gpr .rdi = s.gpr .rdi
+  right : t.gpr .rsi = s.gpr .rsi
+  regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r
+  rd : t.rd = s.rd
+  wr : t.wr = s.wr
+  frame : Frame (prefixWrites s) s.mem t.mem
+  leftBlock : blockAt t.mem (t.gpr .rdi) = blockAt s.mem (s.gpr .rdi)
+  rightBlock : blockAt t.mem (t.gpr .rsi) = blockAt s.mem (s.gpr .rsi)
+  oldBlock : blockAt t.mem (destination t) = blockAt s.mem (s.gpr .r10)
+
+theorem block_frame {m m' : Mem} {rs : List Region} (hf : Frame rs m m')
+    (p : Addr) (sep : ∀ r ∈ rs, (⟨p, 1024⟩ : Region).Disjoint r) :
+    blockAt m' p = blockAt m p := by
+  apply Vector.ext
+  intro i hi
+  have read : m'.readW (off p (8 * i)) 64 = m.readW (off p (8 * i)) 64 :=
+    hf.readW (r := ⟨p, 1024⟩) (Offset.contains_base p (by omega) (by omega)) sep (by decide)
+  rw [← blockAt_get m' p ⟨i, hi⟩, ← blockAt_get m p ⟨i, hi⟩] at read
+  exact read
+
+theorem work_cover (s : State) (h : Ready s) (d n : Nat) (hd : d + n ≤ 5120) :
+    Covers [⟨off (work s) d, n⟩] s.wr := by
+  have sub : Covers [⟨off (work s) d, n⟩] [⟨work s, 5120⟩] := by
+    apply Covers.of_sub
+    intro r hr
+    simp only [List.mem_singleton] at hr
+    subst r
+    exact ⟨⟨work s, 5120⟩, by simp, d, rfl, hd⟩
+  exact fun p n hp => h.workWrite p n (sub p n hp)
+
+theorem prepared_of_setup (s a b : State) (h : Ready s)
+    (mem : a.mem = s.mem.writeW (off (s.gpr .rbp) 16) (s.gpr .r10))
+    (regs : a.gpr = s.gpr) (rd : a.rd = s.rd) (wr : a.wr = s.wr)
+    (scratch : b.gpr .rcx = a.mem.readW (off (a.gpr .rbp) 248) 64)
+    (output : b.gpr .rdx = a.mem.readW (off (a.gpr .rbp) 248) 64 + 4096)
+    (keeps : Divide.Keeps [.rcx, .rdx] a b) : Prepared s b := by
+  have g (r : Reg) (hr : r ∉ [Reg.rcx, .rdx]) : b.gpr r = s.gpr r :=
+    (keeps.regs r hr).trans (congrFun regs r)
+  have brd : b.rd = s.rd := keeps.rd.trans rd
+  have bwr : b.wr = s.wr := keeps.wr.trans wr
+  have bm : b.mem = s.mem.writeW (off (s.gpr .rbp) 16) (s.gpr .r10) := keeps.mem.trans mem
+  have unchanged (d : Nat) (sep : d + 8 ≤ 16 ∨ 24 ≤ d) (bound : d + 8 ≤ 272) :
+      b.mem.readW (off (b.gpr .rbp) d) 64 = s.mem.readW (off (s.gpr .rbp) d) 64 := by
+    rw [bm, g .rbp (by decide)]
+    exact Mem.readW_writeW_sep (Offset.sep _ sep (by omega) (by decide)) (by decide)
+  have work' : b.gpr .rcx = work s := by
+    rw [scratch, regs, mem]
+    exact Mem.readW_writeW_sep (Offset.sep _ (by decide) (by decide) (by decide)) (by decide)
+  have out' : b.gpr .rdx = work s + 4096 := by
+    rw [output, regs, mem,
+      Mem.readW_writeW_sep (Offset.sep _ (by decide) (by decide) (by decide)) (by decide), work]
+  have dest : destination b = s.gpr .r10 := by
+    unfold destination
+    rw [bm, g .rbp (by decide), Mem.readW_writeW_self64]
+  have counter : pass b = pass s := unchanged 0 (by decide) (by decide)
+  have frame : Frame (prefixWrites s) s.mem b.mem := by
+    rw [bm]
+    exact (Frame.refl _ _).writeW (r := ⟨off (s.gpr .rbp) 16, 8⟩) (by simp [prefixWrites]) _
+      (Region.contains_self _ _)
+  have cellFrame (p : Addr) (sep : (⟨p, 1024⟩ : Region).Disjoint ⟨s.gpr .rbp, 272⟩) :
+      blockAt b.mem p = blockAt s.mem p :=
+    block_frame frame p (by
+      intro r hr
+      simp only [prefixWrites, List.mem_singleton] at hr
+      subst r
+      exact sep.sub_right (Offset.sub_base _ (by decide)))
+  have tempSub : Region.Sub ⟨work s + 4096, 1024⟩ ⟨work s, 5120⟩ :=
+    Offset.sub_base _ (by decide)
+  have scratchSub : Region.Sub ⟨work s, 4096⟩ ⟨work s, 5120⟩ := Region.sub_prefix (by decide)
+  refine ⟨?_, dest, counter, work', out', g .rdi (by decide), g .rsi (by decide), ?_, brd, bwr,
+    frame, ?_, ?_, ?_⟩
+  · refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+    · refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
+      · rw [g .rdi (by decide), brd, bwr]; exact h.leftRead
+      · rw [g .rsi (by decide), brd, bwr]; exact h.rightRead
+      · rw [out', bwr]; exact work_cover s h 4096 1024 (by decide)
+      · rw [work', bwr]
+        simpa only [off, show BitVec.ofNat 64 0 = 0#64 from rfl, BitVec.add_zero]
+          using work_cover s h 0 4096 (by decide)
+      · rw [g .rdi (by decide), work']; exact h.leftWork.sub_right scratchSub
+      · rw [g .rsi (by decide), work']; exact h.rightWork.sub_right scratchSub
+      · rw [out', work']; exact Offset.disjoint_base _ (by decide) (by decide)
+      · rw [g .rsp (by decide), g .rdi (by decide)]; exact h.stackLeft
+      · rw [g .rsp (by decide), g .rsi (by decide)]; exact h.stackRight
+      · rw [g .rsp (by decide), out']; exact h.stackWork.sub_right tempSub
+      · rw [g .rsp (by decide), work']; exact h.stackWork.sub_right scratchSub
+    · intro d hd
+      rw [brd, bwr, g .rbp (by decide)]; exact h.frameRead d hd
+    · rw [unchanged 248 (by decide) (by decide), work']; rfl
+    · rw [work', out']
+    · rw [dest, bwr]; exact h.destinationWrite
+    · intro r hr
+      simp only [callWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl | rfl
+      · rw [g .rbp (by decide), out']; exact h.frameWork.sub_right tempSub
+      · rw [g .rbp (by decide), work']; exact h.frameWork.sub_right scratchSub
+      · rw [g .rbp (by decide), g .rsp (by decide)]; exact h.frameStack
+    · intro r hr
+      rw [dest]
+      simp only [callWrites, List.mem_cons, List.not_mem_nil, or_false] at hr
+      rcases hr with rfl | rfl | rfl
+      · rw [out']; exact h.destinationWork.sub_right tempSub
+      · rw [work']; exact h.destinationWork.sub_right scratchSub
+      · rw [g .rsp (by decide)]; exact h.destinationStack
+  · intro r hr
+    apply g r
+    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 [g .rdi (by decide)]; exact cellFrame _ h.leftFrame
+  · rw [g .rsi (by decide)]; exact cellFrame _ h.rightFrame
+  · rw [dest]; exact cellFrame _ h.destinationFrame
+
+theorem setup_ok (s : State) (h : Ready s) :
+    WP isa setup s (Prepared s) := by
+  unfold setup
+  refine WP.seq ((saveCurrent_ok s h.frameWrite).mono ?_)
+  rintro a ⟨mem, regs, rd, wr, _⟩
+  have read : InRegions (a.rd ++ a.wr) (off (a.gpr .rbp) 248) 8 := by
+    rw [rd, wr, regs]; exact h.frameRead 248 (by simp)
+  refine (compressArgs_ok a read).mono ?_
+  rintro b ⟨scratch, output, keeps⟩
+  exact prepared_of_setup s a b h mem regs rd wr scratch output keeps
+
+end VG.Proof.Argon2.X86_64.FillCompress