Argon2 on x86-64: prove complete filling random-word dispatch

lean/VerifiedGarbage/Impl/Argon2/X86_64/RandomSource.lean

@@ -0,0 +1,17 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressMode
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCache
+import VerifiedGarbage.Impl.Argon2.X86_64.DependentWord
+
+/-! Dispatch the filling random word using the public segment addressing mode. -/
+
+namespace VG.Impl.Argon2.X86_64.RandomSource
+
+open VG.X86_64
+
+def test : List Instr := [.alu .cmp .r10 (.imm 0)]
+
+def prepare : Prog isa := .seq AddressMode.code (.block test)
+
+def code : Prog isa := .seq prepare (.ite .e DependentWord.code AddressCache.code)
+
+end VG.Impl.Argon2.X86_64.RandomSource

lean/VerifiedGarbage/Proof/Argon2/X86_64/RandomSource.lean

@@ -0,0 +1,100 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.RandomSourcePrepare
+import VerifiedGarbage.Proof.Argon2.X86_64.DependentWordState
+
+/-! Both random sources satisfy the same filling-step postcondition. -/
+
+namespace VG.Proof.Argon2.X86_64.RandomSource
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+def writes (s : State) : List Region := AddressCache.writes s
+
+structure Done (s t : State) (p : Params) (pass lane slice index : Nat) (state : FillState) : Prop where
+  random : t.gpr .rdi = Proof.Argon2.FillStep.random p pass lane slice index state.memory
+  ready : ∃ old, Ready p pass lane slice index old t
+  represented : Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks state.memory
+  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
+
+theorem Ready.index_nat {p : Params} {pass lane slice index old : Nat} {s : State}
+    (h : Ready p pass lane slice index old s) : (s.gpr .r15).toNat = index := by
+  rw [h.filling.position.index, ReferenceMap.word_nat index h.filling.bounds.index_bound64]
+
+theorem independent_ok (s : State) (p : Params) (pass lane slice index old : Nat)
+    (h : Ready p pass lane slice index old s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory)
+    (mode : independent p pass slice = true) :
+    WP isa Impl.Argon2.X86_64.AddressCache.code s (Done s · p pass lane slice index state) := by
+  refine (AddressCache.code_ok p pass lane slice old s h.cache.ready).mono ?_
+  intro t done
+  have base : FillKernel.matrix t = FillKernel.matrix s :=
+    done.selected.frame_word h.cache.layout 232 (by decide) (by decide)
+  have nextReady : Ready p pass lane slice index (AddressCache.wanted s) t := by
+    refine ⟨done.selected.filling_ready h.cache.layout h.filling,
+      done.selected.invariant h.cache.ready, ?_⟩
+    rw [base, done.selected.work_eq]; exact h.matrixWork
+  refine ⟨?_, ⟨_, nextReady⟩,
+    done.selected.represents h.cache.layout h.filling h.matrixWork state.memory represented,
+    done.selected.regs, done.selected.rd, done.selected.wr, done.selected.frame, done.selected.mxcsr⟩
+  have random := done.random
+  unfold AddressCache.wanted at random
+  rw [h.index_nat] at random
+  unfold Proof.Argon2.FillStep.random
+  simp only [mode, ite_true]
+  exact random
+
+theorem dependent_ok (s : State) (p : Params) (pass lane slice index old : Nat)
+    (h : Ready p pass lane slice index old s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory)
+    (mode : independent p pass slice = false) :
+    WP isa Impl.Argon2.X86_64.DependentWord.code s (Done s · p pass lane slice index state) := by
+  refine (DependentWord.state_ok s p pass lane slice index h.filling state represented mode).mono ?_
+  rintro t ⟨random, _, matrix, keeps⟩
+  refine ⟨random, ⟨old, h.of_keeps keeps⟩, matrix, ?_, keeps.rd, keeps.wr, ?_, keeps.mxcsr⟩
+  · intro r hr
+    apply keeps.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 [keeps.mem]; exact Frame.refl _ _
+
+theorem code_ok (s : State) (p : Params) (pass lane slice index old : Nat)
+    (h : Ready p pass lane slice index old s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory) :
+    WP isa Impl.Argon2.X86_64.RandomSource.code s (Done s · p pass lane slice index state) := by
+  unfold Impl.Argon2.X86_64.RandomSource.code
+  refine WP.seq ((prepare_ok s p pass lane slice index old h).mono ?_)
+  rintro a ⟨flag, keeps⟩
+  have next := h.of_keeps keeps
+  have representedA : Proof.Argon2.Represents a.mem (FillKernel.matrix a) p.blocks state.memory := by
+    have base : FillKernel.matrix a = FillKernel.matrix s := by
+      unfold FillKernel.matrix; rw [keeps.mem, keeps.regs .rbp (by decide)]
+    rw [base, keeps.mem]; exact represented
+  have finish {t : State} (done : Done a t p pass lane slice index state) :
+      Done s t p pass lane slice index state := by
+    refine ⟨done.random, done.ready, done.represented, ?_, done.rd.trans keeps.rd,
+      done.wr.trans keeps.wr, ?_, done.mxcsr.trans keeps.mxcsr⟩
+    · intro r hr
+      have ne : r ∉ ReferenceMap.changed := 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 (done.regs r hr).trans (keeps.regs r ne)
+    · have frame := done.frame
+      unfold writes AddressCache.writes AddressCalls.work at frame ⊢
+      rw [keeps.mem, keeps.regs .rbp (by decide), keeps.regs .rsp (by decide)] at frame
+      exact frame
+  refine WP.ite (!independent p pass slice) (by simp only [eval, flag]) ?_ ?_
+  · intro mode
+    have dependent : independent p pass slice = false := by
+      cases eq : independent p pass slice <;> simp_all
+    exact (dependent_ok a p pass lane slice index old next state representedA dependent).mono
+      (fun _ done => finish done)
+  · intro mode
+    have independent : independent p pass slice = true := by
+      cases eq : independent p pass slice <;> simp_all
+    exact (independent_ok a p pass lane slice index old next state representedA independent).mono
+      (fun _ done => finish done)
+
+end VG.Proof.Argon2.X86_64.RandomSource

lean/VerifiedGarbage/Proof/Argon2/X86_64/RandomSourceCT.lean

@@ -0,0 +1,74 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.RandomSourcePrepare
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressModeCT
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheSelectCT
+import VerifiedGarbage.Proof.Argon2.X86_64.DependentWordCT
+
+/-! Source dispatch and cached-word selection use only public addresses and guards. -/
+
+namespace VG.Proof.Argon2.X86_64.RandomSource
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.RandomSource
+
+structure Related (p : Params) (pass lane slice index old : Nat) (s t : State) : Prop where
+  left : Ready p pass lane slice index old s
+  right : Ready p pass lane slice index old t
+  bases : s.gpr .rbp = t.gpr .rbp
+  stacks : s.gpr .rsp = t.gpr .rsp
+  matrices : FillKernel.matrix s = FillKernel.matrix t
+  work : AddressCalls.work s = AddressCalls.work t
+
+theorem Related.of_keeps {p : Params} {pass lane slice index old : Nat} {s t a b : State}
+    (h : Related p pass lane slice index old s t)
+    (ka : Divide.Keeps ReferenceMap.changed s a) (kb : Divide.Keeps ReferenceMap.changed t b) :
+    Related p pass lane slice index old a b := by
+  refine ⟨h.left.of_keeps ka, h.right.of_keeps kb, ?_, ?_, ?_, ?_⟩
+  · rw [ka.regs .rbp (by decide), kb.regs .rbp (by decide)]; exact h.bases
+  · rw [ka.regs .rsp (by decide), kb.regs .rsp (by decide)]; exact h.stacks
+  · unfold FillKernel.matrix
+    rw [ka.mem, kb.mem, ka.regs .rbp (by decide), kb.regs .rbp (by decide)]
+    exact h.matrices
+  · unfold AddressCalls.work
+    rw [ka.mem, kb.mem, ka.regs .rbp (by decide), kb.regs .rbp (by decide)]
+    exact h.work
+
+theorem test_rel : RelCT isa (fun _ _ : State => True) (.block test) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by intro r hr; simp at hr)) (by taint_decide)
+
+theorem prepare_rel (p : Params) (pass lane slice index old : Nat) :
+    RelCT isa (Related p pass lane slice index old) prepare
+      (fun s t => Related p pass lane slice index old s t ∧ s.zf = t.zf) := by
+  have trace := AddressMode.code_rel.seq test_rel
+  have narrowed := trace.mono (P' := Related p pass lane slice index old)
+    (fun _ _ h => h.bases) (fun _ _ h => h)
+  have full := narrowed.wpDep (fun s t h =>
+    ⟨prepare_ok s p pass lane slice index old h.left,
+      prepare_ok t p pass lane slice index old h.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ⟨fa, ka⟩, ⟨fb, kb⟩⟩ := h
+  exact ⟨hp.of_keeps ka kb, fa.trans fb.symm⟩
+
+theorem Related.cache {p : Params} {pass lane slice index old : Nat} {s t : State}
+    (h : Related p pass lane slice index old s t) : AddressCache.ReadyRelated p pass lane slice old s t := by
+  refine ⟨h.left.cache.ready, h.right.cache.ready,
+    ⟨⟨⟨h.left.cache.layout, h.right.cache.layout, h.bases, h.stacks, h.work⟩,
+      h.left.cache.reads, h.right.cache.reads⟩, ?_, ?_, h.left.cache.write, h.right.cache.write⟩⟩
+  · exact h.left.filling.position.index.trans h.right.filling.position.index.symm
+  · exact h.left.cache.words.counterWord.trans h.right.cache.words.counterWord.symm
+
+theorem code_rel (p : Params) (pass lane slice index old : Nat) :
+    RelCT isa (Related p pass lane slice index old) code (fun _ _ => True) := by
+  have branches : RelCT isa
+      (fun s t => Related p pass lane slice index old s t ∧ s.zf = t.zf)
+      (.ite .e Impl.Argon2.X86_64.DependentWord.code Impl.Argon2.X86_64.AddressCache.code)
+      (fun _ _ => True) := by
+    apply RelCT.ite (by intro s t h; simp only [eval, h.2])
+    · exact (DependentWord.code_rel p pass lane slice index).mono
+        (fun _ _ h => ⟨h.1.1.left.filling, h.1.1.right.filling, h.1.1.bases, h.1.1.matrices⟩)
+        (fun _ _ h => h)
+    · exact (AddressCache.code_rel p pass lane slice old).mono
+        (fun _ _ h => h.1.1.cache) (fun _ _ h => h)
+  exact (prepare_rel p pass lane slice index old).seq branches
+
+end VG.Proof.Argon2.X86_64.RandomSource

lean/VerifiedGarbage/Proof/Argon2/X86_64/RandomSourcePrepare.lean

@@ -0,0 +1,60 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.RandomSource
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressMode
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheInvariant
+import VerifiedGarbage.Proof.Argon2.X86_64.AddressCacheMatrix
+
+/-! Retain the source invariants while selecting the public addressing mode. -/
+
+namespace VG.Proof.Argon2.X86_64.RandomSource
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.RandomSource
+
+structure Ready (p : Params) (pass lane slice index old : Nat) (s : State) : Prop where
+  filling : FillKernel.Ready p pass lane slice index s
+  cache : AddressCache.Invariant p pass lane slice old s
+  matrixWork : (⟨FillKernel.matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨AddressCalls.work s, 8192⟩
+
+theorem Ready.of_keeps {p : Params} {pass lane slice index old : Nat} {s t : State}
+    (h : Ready p pass lane slice index old s) (k : Divide.Keeps ReferenceMap.changed s t) :
+    Ready p pass lane slice index old t := by
+  refine ⟨h.filling.of_keeps k, h.cache.of_keeps k, ?_⟩
+  have matrix : FillKernel.matrix t = FillKernel.matrix s := by
+    unfold FillKernel.matrix; rw [k.mem, k.regs .rbp (by decide)]
+  have work : AddressCalls.work t = AddressCalls.work s := by
+    unfold AddressCalls.work; rw [k.mem, k.regs .rbp (by decide)]
+  rw [matrix, work]; exact h.matrixWork
+
+theorem test_ok (s : State) : WP isa (.block test) s fun t =>
+    t.zf = decide (s.gpr .r10 = 0#64) ∧ Divide.Keeps [] s t := by
+  apply WP.of_runBlock
+  simp only [test, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu,
+    RegUpd.zf_arithFlags, show BitVec.signExtend 64 (0 : BitVec 32) = (0 : Addr) from rfl,
+    Option.bind_some, Option.some.injEq, exists_eq_left']
+  refine ⟨?_, ?_⟩
+  · change (s.gpr .r10 - 0#64 == 0#64) = decide (s.gpr .r10 = 0#64)
+    rw [BitVec.sub_zero]
+    apply Bool.eq_iff_iff.mpr
+    simp only [beq_iff_eq, decide_eq_true_eq]
+  constructor
+  · intro r _; exact congrFun (RegUpd.gpr_arithFlags _ _ _ _) r
+  all_goals rfl
+
+theorem bool_zero : ∀ b : Bool, decide ((BitVec.ofBool b).setWidth 64 = 0#64) = !b := by
+  decide +kernel
+
+theorem prepare_ok (s : State) (p : Params) (pass lane slice index old : Nat)
+    (h : Ready p pass lane slice index old s) : WP isa prepare s fun t =>
+      t.zf = !independent p pass slice ∧ Divide.Keeps ReferenceMap.changed s t := by
+  unfold prepare
+  refine WP.seq ((AddressMode.code_spec_ok s p pass slice
+    (h.cache.reads 112 (by simp)) (h.cache.reads 0 (by simp))
+    h.cache.words.variantWord h.filling.passWord h.filling.position.slice
+    (Nat.lt_trans h.filling.bounds.passBound (by decide))
+    (Nat.lt_trans h.filling.bounds.sliceBound (by decide))).mono ?_)
+  rintro a ⟨mode, keeps⟩
+  refine (test_ok a).mono ?_
+  rintro t ⟨flag, tested⟩
+  refine ⟨?_, (keeps.mono (by decide)).trans (tested.mono (by decide))⟩
+  rw [flag, mode, bool_zero]
+
+end VG.Proof.Argon2.X86_64.RandomSource