From 23f712302196412b7197e34ab3591d88cfebce48 Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 17:01:14 +0000 Subject: [PATCH] Prove Argon2 compression calls and the combined compression/write operation --- .../Impl/Argon2/X86_64/FillCompress.lean | 31 ++++++ .../Proof/Argon2/X86_64/FillCompressArgs.lean | 64 +++++++++++ .../Proof/Argon2/X86_64/FillCompressCall.lean | 101 ++++++++++++++++++ .../Argon2/X86_64/FillCompressCallCT.lean | 30 ++++++ .../Proof/Argon2/X86_64/FillCompressLit.lean | 11 ++ .../Argon2/X86_64/FillCompressOperation.lean | 101 ++++++++++++++++++ .../X86_64/FillCompressOperationCT.lean | 87 +++++++++++++++ .../X86_64/FillCompressOperationMx.lean | 14 +++ .../Proof/Argon2/X86_64/FillWriteCover.lean | 34 ++++++ 9 files changed, 473 insertions(+) create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/FillCompress.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressArgs.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCall.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCallCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressLit.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperation.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationMx.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCover.lean diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillCompress.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/FillCompress.lean new file mode 100644 index 000000000..fc4521ba8 --- /dev/null +++ b/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 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressArgs.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressArgs.lean new file mode 100644 index 000000000..09255a953 --- /dev/null +++ b/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 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCall.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCall.lean new file mode 100644 index 000000000..72355e261 --- /dev/null +++ b/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 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCallCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressCallCT.lean new file mode 100644 index 000000000..62d0b93ec --- /dev/null +++ b/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 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressLit.lean new file mode 100644 index 000000000..64e99d851 --- /dev/null +++ b/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 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperation.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperation.lean new file mode 100644 index 000000000..5bc25e566 --- /dev/null +++ b/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 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationCT.lean new file mode 100644 index 000000000..28cbeeb1d --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationCT.lean @@ -0,0 +1,87 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressOperation +import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressCallCT +import VerifiedGarbage.Proof.Argon2.X86_64.FillWriteCT + +/-! Only the compression argument addresses, public frame words and stack +pointer determine the compression-and-write trace. -/ + +namespace VG.Proof.Argon2.X86_64.FillCompress + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillCompress + +structure Related (s t : State) : Prop where + left : OperationReady s + right : OperationReady t + args : ∀ r ∈ [Reg.rdi, .rsi, .rdx, .rcx, .rsp, .rbp], s.gpr r = t.gpr r + dest : destination s = destination t + counter : pass s = pass t + +structure BeforeWrite (s t : State) : Prop where + leftRead : ∀ d ∈ [0, 16, 248], InRegions (s.rd ++ s.wr) (off (s.gpr .rbp) d) 8 + rightRead : ∀ d ∈ [0, 16, 248], InRegions (t.rd ++ t.wr) (off (t.gpr .rbp) d) 8 + bases : s.gpr .rbp = t.gpr .rbp + words : ∀ d ∈ [0, 16, 248], + s.mem.readW (off (s.gpr .rbp) d) 64 = t.mem.readW (off (t.gpr .rbp) d) 64 + +theorem called_public {s t a b : State} (hp : Related s t) + (ha : Called s a) (hb : Called t b) : BeforeWrite a b := by + have abp : a.gpr .rbp = s.gpr .rbp := ha.regs .rbp (by simp [calleeSaved]) + have bbp : b.gpr .rbp = t.gpr .rbp := hb.regs .rbp (by simp [calleeSaved]) + refine ⟨?_, ?_, abp.trans ((hp.args .rbp (by simp)).trans bbp.symm), ?_⟩ + · intro d hd + rw [ha.rd, ha.wr, abp]; exact hp.left.frameRead d hd + · intro d hd + rw [hb.rd, hb.wr, bbp]; exact hp.right.frameRead d hd + · intro d hd + rw [abp, bbp] + simp only [List.mem_cons, List.not_mem_nil, or_false] at hd + rcases hd with rfl | rfl | rfl + · rw [frame_word hp.left ha 0 (by decide), frame_word hp.right hb 0 (by decide)] + exact hp.counter + · rw [frame_word hp.left ha 16 (by decide), frame_word hp.right hb 16 (by decide)] + exact hp.dest + · rw [frame_word hp.left ha 248 (by decide), frame_word hp.right hb 248 (by decide), + hp.left.workWord, hp.right.workWord] + exact hp.args .rcx (by simp) + +theorem call_public_rel : RelCT isa Related + (.call Spec.Argon2.compressApi.name VG.Impl.Argon2.X86_64.compress) BeforeWrite := by + have trace := call_rel Spec.Argon2.compressApi.name (P := Related) (fun _ _ hp => + ⟨hp.left.call, hp.right.call, hp.args .rdi (by simp), hp.args .rsi (by simp), + hp.args .rdx (by simp), hp.args .rcx (by simp), hp.args .rsp (by simp)⟩) + have full := trace.wpDep (fun s t hp => + ⟨call_ok _ s hp.left.call, call_ok _ t hp.right.call⟩) + refine full.mono (fun _ _ h => h) ?_ + intro a b h + obtain ⟨_, s, t, hp, ha, hb⟩ := h + exact called_public hp ha hb + +theorem writeArgs_rel : RelCT isa (fun s t => s.gpr .rbp = t.gpr .rbp) + (.block writeArgs) (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 writeArgs_public_rel : RelCT isa BeforeWrite (.block writeArgs) + (fun s t => ∀ r ∈ [Reg.r9, .rdi, .rsi], s.gpr r = t.gpr r) := by + have trace := writeArgs_rel.mono (P' := BeforeWrite) (fun _ _ h => h.bases) (fun _ _ h => h) + have full := trace.wpDep (fun s t hp => + ⟨writeArgs_ok s (hp.leftRead 16 (by simp)) (hp.leftRead 248 (by simp)) (hp.leftRead 0 (by simp)), + writeArgs_ok t (hp.rightRead 16 (by simp)) (hp.rightRead 248 (by simp)) (hp.rightRead 0 (by simp))⟩) + refine full.mono (fun _ _ h => h) ?_ + intro a b h + obtain ⟨_, s, t, hp, ha, hb⟩ := h + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact ha.2.2.1.trans ((hp.words 0 (by simp)).trans hb.2.2.1.symm) + · exact ha.1.trans ((hp.words 16 (by simp)).trans hb.1.symm) + · exact ha.2.1.trans ((congrArg (· + (4096 : Addr)) (hp.words 248 (by simp))).trans hb.2.1.symm) + +theorem operation_rel : RelCT isa Related operation (fun _ _ => True) := + call_public_rel.seq (writeArgs_public_rel.seq FillWrite.code_rel) + +end VG.Proof.Argon2.X86_64.FillCompress diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationMx.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationMx.lean new file mode 100644 index 000000000..cc6069fef --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillCompressOperationMx.lean @@ -0,0 +1,14 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressOperation +import VerifiedGarbage.Proof.Argon2.X86_64.FillCompressLit + +/-! Baseline compression and the block write preserve all of MXCSR. -/ + +namespace VG.Proof.Argon2.X86_64.FillCompress + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.FillCompress + +theorem operation_mx_ok (s : State) (h : OperationReady s) : + WP isa operation s fun t => OperationDone s t ∧ t.mxcsr = s.mxcsr := + WP.mono_mx (by lit_decide) (operation_ok s h) (fun _ done mx => ⟨done, mx⟩) + +end VG.Proof.Argon2.X86_64.FillCompress diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCover.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCover.lean new file mode 100644 index 000000000..2da771373 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/FillWriteCover.lean @@ -0,0 +1,34 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.FillWrite +import VerifiedGarbage.Proof.Framework.X86_64.Inline + +/-! Use block writes in a matrix allocation with larger permission regions. -/ + +namespace VG.Proof.Argon2.X86_64.FillWrite + +open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.FillWrite + +theorem code_cover_ok (s : State) + (hs : Covers [⟨s.gpr .rsi, 1024⟩] (s.rd ++ s.wr)) + (hw : Covers [⟨s.gpr .rdi, 1024⟩] s.wr) + (hd : (⟨s.gpr .rsi, 1024⟩ : Region).Disjoint ⟨s.gpr .rdi, 1024⟩) : + WP isa code s fun t => + blockAt t.mem (s.gpr .rdi) = + (if s.gpr .r9 = 0 then blockAt s.mem (s.gpr .rsi) + else xorBlock (blockAt s.mem (s.gpr .rsi)) (blockAt s.mem (s.gpr .rdi))) ∧ + Frame [⟨s.gpr .rdi, 1024⟩] s.mem t.mem ∧ CopyKeeps s t ∧ t.mxcsr = s.mxcsr := by + let a := s.withRegions [⟨s.gpr .rsi, 1024⟩] [⟨s.gpr .rdi, 1024⟩] + obtain ⟨tr, t, he, value, frame, keeps, mx⟩ := code_ok a (by simp [a]) (by simp [a]) hd + have cover : Covers (a.rd ++ a.wr) (s.rd ++ s.wr) := by + intro p n ⟨r, hr, hc⟩ + change r ∈ [⟨s.gpr .rsi, 1024⟩, ⟨s.gpr .rdi, 1024⟩] at hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl + · exact hs p n ⟨_, by simp, hc⟩ + · obtain ⟨r, hr, hc⟩ := hw p n ⟨_, by simp, hc⟩ + exact ⟨r, List.mem_append_right _ hr, hc⟩ + have he' := Exec.widen (rd := s.rd) (wr := s.wr) he cover hw + simp only [a, State.withRegions_withRegions, State.withRegions_self] at he' + refine ⟨tr, t.withRegions s.rd s.wr, he', value, frame, ?_, mx⟩ + exact ⟨keeps.1, rfl, rfl⟩ + +end VG.Proof.Argon2.X86_64.FillWrite