Argon2 on x86-64: prove complete segment setup and filling

lean/VerifiedGarbage/Impl/Argon2/X86_64/SegmentSetup.lean

@@ -0,0 +1,25 @@
+import VerifiedGarbage.Impl.Argon2.X86_64.FillSegment
+import VerifiedGarbage.Impl.Argon2.X86_64.AddressCache
+
+/-! Reset the address cache per segment and skip the two initialized cells. -/
+
+namespace VG.Impl.Argon2.X86_64.SegmentSetup
+
+open VG.X86_64
+open VG.Impl.Argon2.X86_64 (at_)
+
+def reset : Prog isa := .seq (.block [.mov .rax (.imm 0)]) (.block AddressCache.save)
+
+def first : List Instr := [
+  .mov .rcx (.mem (at_ .rbp 0)), .alu .or .rcx (.reg .r14), .alu .cmp .rcx (.imm 0)]
+
+def index : Prog isa := .seq (.block first)
+  (.ite .e (.block [.mov .r15 (.imm 2)]) (.block [.mov .r15 (.imm 0)]))
+
+def check : List Instr := [.alu .cmp .r15 (.reg .r13)]
+
+def prepare : Prog isa := .seq reset index
+
+def code : Prog isa := .seq prepare (.seq (.block check) (.ite .b FillSegment.loop (.block [])))
+
+end VG.Impl.Argon2.X86_64.SegmentSetup

lean/VerifiedGarbage/Proof/Argon2/SegmentStart.lean

@@ -0,0 +1,26 @@
+import VerifiedGarbage.Proof.Argon2.Segment
+
+/-! The first two cells of pass zero's first segment are already initialized. -/
+
+namespace VG.Proof.Argon2
+
+open VG.Spec.Argon2
+
+def segmentStart (pass slice : Nat) : Nat := if pass = 0 ∧ slice = 0 then 2 else 0
+
+theorem segment_first_two (p : Params) (lane : Nat) (state : FillState) :
+    segment p 0 lane 0 0 2 state = state := by
+  rw [segment_succ, segment_succ, segment_zero]
+  simp only [fillBlock, Nat.reduceAdd, and_self, Nat.reduceLT, ite_true]
+
+theorem segment_start (p : Params) (pass lane slice : Nat) (state : FillState) (minimum : 2 ≤ p.segmentLen) :
+    segment p pass lane slice 0 p.segmentLen state =
+      segment p pass lane slice (segmentStart pass slice) (p.segmentLen - segmentStart pass slice) state := by
+  by_cases first : pass = 0 ∧ slice = 0
+  · obtain ⟨rfl, rfl⟩ := first
+    have append := segment_append p 0 lane 0 0 2 (p.segmentLen - 2) state
+    rw [show 2 + (p.segmentLen - 2) = p.segmentLen by omega, segment_first_two] at append
+    exact append
+  · simp only [segmentStart, first, ite_false, Nat.sub_zero]
+
+end VG.Proof.Argon2

lean/VerifiedGarbage/Proof/Argon2/X86_64/FillContext.lean

@@ -0,0 +1,61 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.FillSegment
+
+/-! A segment context allows its starting and final indices, including an empty suffix. -/
+
+namespace VG.Proof.Argon2.X86_64.FillContext
+
+open VG VG.X86_64 VG.Spec.Argon2
+
+structure Parameters (p : Params) (pass lane slice : Nat) : Prop where
+  lanesPositive : 0 < p.lanes
+  lanesBound : p.lanes < 2 ^ 32
+  memoryMinimum : 8 * p.lanes ≤ p.memory
+  memoryBound : p.memory < 2 ^ 32
+  passBound : pass < 2 ^ 32
+  laneBound : lane < p.lanes
+  sliceBound : slice < 4
+
+structure Ready (p : Params) (pass lane slice index old : Nat) (s : State) : Prop where
+  parameters : Parameters p pass lane slice
+  layout : FillKernel.Layout p s
+  cache : AddressCache.Invariant p pass lane slice old s
+  matrixWork : (⟨FillKernel.matrix s, p.blocks * 1024⟩ : Region).Disjoint ⟨AddressCalls.work s, 8192⟩
+  position : ReferenceMap.Position p lane slice index s
+  lanesWord : s.mem.readW (off (s.gpr .rbp) 184) 64 = BitVec.ofNat 64 p.lanes
+
+theorem Ready.activate {p : Params} {pass lane slice index old : Nat} {s : State}
+    (h : Ready p pass lane slice index old s) (bound : index < p.segmentLen)
+    (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index) : RandomSource.Ready p pass lane slice index old s :=
+  ⟨⟨h.layout, ⟨h.parameters.lanesPositive, h.parameters.lanesBound, h.parameters.memoryMinimum,
+    h.parameters.memoryBound, h.parameters.passBound, h.parameters.laneBound, h.parameters.sliceBound,
+    bound, active⟩, h.position, h.cache.words.passWord, h.lanesWord⟩, h.cache, h.matrixWork⟩
+
+theorem Parameters.segment_bound {p : Params} {pass lane slice : Nat} (h : Parameters p pass lane slice) :
+    2 ≤ p.segmentLen ∧ p.segmentLen < 2 ^ 64 := by
+  have minimum := Proof.Argon2.segmentLen_ge_two p h.lanesPositive h.memoryMinimum
+  have le : p.segmentLen ≤ p.blocks := by
+    have blocks := Proof.Argon2.blocks_lanes p h.lanesPositive
+    have segments := Proof.Argon2.laneLen_segments p h.lanesPositive
+    have laneLe : p.laneLen ≤ p.blocks := by rw [blocks]; exact Nat.le_mul_of_pos_left _ h.lanesPositive
+    omega
+  exact ⟨minimum, Nat.lt_of_le_of_lt le
+    (Nat.lt_trans (Nat.lt_of_le_of_lt (Proof.Argon2.blocks_le_memory p) h.memoryBound) (by decide))⟩
+
+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
+  have bp := k.regs .rbp (by decide)
+  have base : FillKernel.matrix t = FillKernel.matrix s := by unfold FillKernel.matrix; rw [k.mem, bp]
+  have work : AddressCalls.work t = AddressCalls.work s := by unfold AddressCalls.work; rw [k.mem, bp]
+  refine ⟨h.parameters, h.layout.of_preserved bp (k.regs .rsp (by decide)) base work k.rd k.wr,
+    h.cache.of_keeps k, ?_, h.position.of_keeps k, ?_⟩
+  · rw [base, work]; exact h.matrixWork
+  · rw [k.mem, bp]; exact h.lanesWord
+
+theorem finished_context {p : Params} {pass lane slice : Nat} {s t : State} {state : FillState}
+    (parameters : Parameters p pass lane slice) (h : FillSegment.Finished s t p pass lane slice state) :
+    ∃ old, Ready p pass lane slice p.segmentLen old t := by
+  obtain ⟨old, cache⟩ := h.cache
+  exact ⟨old, parameters, h.layout, cache, h.matrixWork, h.position, h.lanesWord⟩
+
+end VG.Proof.Argon2.X86_64.FillContext

lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetup.lean

@@ -0,0 +1,43 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupCheck
+import VerifiedGarbage.Proof.Argon2.SegmentStart
+
+/-! Fill one complete segment, including the initialized prefix and empty suffix. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+theorem code_ok (s : State) (p : Params) (pass lane slice : Nat)
+    (h : Ready p pass lane slice s) (state : FillState)
+    (represented : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks state.memory) :
+    WP isa code s (FillSegment.Finished s · p pass lane slice
+      (Proof.Argon2.segment p pass lane slice 0 p.segmentLen state)) := by
+  rw [Proof.Argon2.segment_start p pass lane slice state h.parameters.segment_bound.1]
+  change WP isa code s (FillSegment.Finished s · p pass lane slice
+    (Proof.Argon2.segment p pass lane slice (start pass slice) (p.segmentLen - start pass slice) state))
+  unfold code
+  refine WP.seq ((prepare_ok s p pass lane slice h).mono ?_)
+  intro a prepared
+  refine WP.seq ((check_prepared_ok prepared).mono ?_)
+  rintro b ⟨prepared, flag⟩
+  have matrix := prepared.represents h state.memory represented
+  refine WP.ite (decide (start pass slice < p.segmentLen)) (by simp only [eval, flag]) ?_ ?_
+  · intro taken
+    have bound := of_decide_eq_true taken
+    have active := prepared.context.activate bound (start_active pass slice)
+    refine (FillSegment.loop_ok (p.segmentLen - start pass slice) b p pass lane slice (start pass slice) 0
+      active state matrix (by omega) (by omega)).mono ?_
+    intro t finished
+    exact finished_prepared prepared finished
+  · intro skipped
+    have bound := of_decide_eq_false skipped
+    have minimum := h.parameters.segment_bound.1
+    have last : start pass slice = p.segmentLen := by have := start_le pass slice p.segmentLen minimum; omega
+    have finished : FillSegment.Finished b b p pass lane slice state :=
+      ⟨matrix, rfl, rfl, last ▸ prepared.context.position, prepared.context.layout,
+        ⟨0, prepared.context.cache⟩, prepared.context.matrixWork, prepared.context.cache.words.passWord,
+        prepared.context.lanesWord, fun _ _ _ => rfl, rfl, rfl, Frame.refl _ _, rfl⟩
+    rw [last, Nat.sub_self, Proof.Argon2.segment_zero]
+    exact WP.block_nil (finished_prepared prepared finished)
+
+end VG.Proof.Argon2.X86_64.SegmentSetup

lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCT.lean

@@ -0,0 +1,120 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetup
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupTrace
+import VerifiedGarbage.Proof.Argon2.X86_64.FillSegmentCT
+
+/-! Complete segment setup and filling expose only the specified reference log. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+structure Related (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) (s t : State) : Prop where
+  ready : RelatedReady p pass lane slice s t
+  leftMatrix : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks leftState.memory
+  rightMatrix : Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks rightState.memory
+  indices : (Proof.Argon2.segment p pass lane slice 0 p.segmentLen leftState).indices =
+    (Proof.Argon2.segment p pass lane slice 0 p.segmentLen rightState).indices
+
+structure PreparedRelated (p : Params) (pass lane slice : Nat) (leftState rightState : FillState)
+    (s t : State) : Prop where
+  left : FillContext.Ready p pass lane slice (start pass slice) 0 s
+  right : FillContext.Ready p pass lane slice (start pass slice) 0 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
+  leftMatrix : Proof.Argon2.Represents s.mem (FillKernel.matrix s) p.blocks leftState.memory
+  rightMatrix : Proof.Argon2.Represents t.mem (FillKernel.matrix t) p.blocks rightState.memory
+  indices : (Proof.Argon2.segment p pass lane slice (start pass slice) (p.segmentLen - start pass slice) leftState).indices =
+    (Proof.Argon2.segment p pass lane slice (start pass slice) (p.segmentLen - start pass slice) rightState).indices
+
+theorem prepare_public_rel (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) :
+    RelCT isa (Related p pass lane slice leftState rightState) prepare
+      (PreparedRelated p pass lane slice leftState rightState) := by
+  have trace := (prepare_trace p pass lane slice).mono
+    (P' := Related p pass lane slice leftState rightState) (fun _ _ h => h.ready) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨prepare_ok s p pass lane slice h.ready.left, prepare_ok t p pass lane slice h.ready.right⟩)
+  refine full.mono (fun _ _ h => h) ?_
+  intro a b h
+  obtain ⟨_, s, t, hp, ha, hb⟩ := h
+  refine ⟨ha.context, hb.context, ?_, ?_, ha.matrix.trans (hp.ready.matrices.trans hb.matrix.symm),
+    ha.work.trans (hp.ready.work.trans hb.work.symm), ha.represents hp.ready.left leftState.memory hp.leftMatrix,
+    hb.represents hp.ready.right rightState.memory hp.rightMatrix, ?_⟩
+  · rw [ha.regs .rbp (by simp [calleeSaved]) (by decide), hb.regs .rbp (by simp [calleeSaved]) (by decide)]
+    exact hp.ready.bases
+  · rw [ha.regs .rsp (by simp [calleeSaved]) (by decide), hb.regs .rsp (by simp [calleeSaved]) (by decide)]
+    exact hp.ready.stacks
+  · have indices := hp.indices
+    rw [Proof.Argon2.segment_start p pass lane slice leftState hp.ready.left.parameters.segment_bound.1,
+      Proof.Argon2.segment_start p pass lane slice rightState hp.ready.right.parameters.segment_bound.1] at indices
+    exact indices
+
+theorem PreparedRelated.of_keeps {p : Params} {pass lane slice : Nat} {leftState rightState : FillState}
+    {s t a b : State} (h : PreparedRelated p pass lane slice leftState rightState s t)
+    (ka : Divide.Keeps [] s a) (kb : Divide.Keeps [] t b) :
+    PreparedRelated p pass lane slice leftState rightState a b := by
+  refine ⟨h.left.of_keeps (ka.mono (by decide)), h.right.of_keeps (kb.mono (by decide)), ?_, ?_, ?_, ?_, ?_, ?_, h.indices⟩
+  · rw [ka.regs .rbp (by simp), kb.regs .rbp (by simp)]; exact h.bases
+  · rw [ka.regs .rsp (by simp), kb.regs .rsp (by simp)]; exact h.stacks
+  · unfold FillKernel.matrix
+    rw [ka.mem, kb.mem, ka.regs .rbp (by simp), kb.regs .rbp (by simp)]; exact h.matrices
+  · unfold AddressCalls.work
+    rw [ka.mem, kb.mem, ka.regs .rbp (by simp), kb.regs .rbp (by simp)]; exact h.work
+  · unfold FillKernel.matrix; rw [ka.mem, ka.regs .rbp (by simp)]; exact h.leftMatrix
+  · unfold FillKernel.matrix; rw [kb.mem, kb.regs .rbp (by simp)]; exact h.rightMatrix
+
+theorem check_context_ok (s : State) (p : Params) (pass lane slice : Nat)
+    (h : FillContext.Ready p pass lane slice (start pass slice) 0 s) : WP isa (.block check) s fun t =>
+      t.cf = decide (start pass slice < p.segmentLen) ∧ Divide.Keeps [] s t := by
+  refine (check_ok s).mono ?_
+  rintro t ⟨flag, keeps⟩
+  have minimum := h.parameters.segment_bound
+  refine ⟨?_, keeps⟩
+  rw [flag, h.position.index, h.position.segmentLength,
+    ReferenceMap.word_nat (start pass slice) (Nat.lt_of_le_of_lt (start_le _ _ _ minimum.1) minimum.2),
+    ReferenceMap.word_nat p.segmentLen minimum.2]
+
+theorem check_trace : RelCT isa (fun _ _ : State => True) (.block check) (fun _ _ => True) :=
+  RelCT.taint (A := taint) (Taint.ofRegs [])
+    (fun _ _ _ => Taint.agree_ofRegs (by intro r hr; simp at hr)) (by taint_decide)
+
+theorem check_public_rel (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) :
+    RelCT isa (PreparedRelated p pass lane slice leftState rightState) (.block check)
+      (fun s t => PreparedRelated p pass lane slice leftState rightState s t ∧
+        s.cf = decide (start pass slice < p.segmentLen) ∧ t.cf = decide (start pass slice < p.segmentLen)) := by
+  have trace := check_trace.mono (P' := PreparedRelated p pass lane slice leftState rightState)
+    (fun _ _ _ => trivial) (fun _ _ h => h)
+  have full := trace.wpDep (fun s t h => ⟨check_context_ok s p pass lane slice h.left, check_context_ok t p pass lane slice 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, fb⟩
+
+theorem code_rel (p : Params) (pass lane slice : Nat) (leftState rightState : FillState) :
+    RelCT isa (Related p pass lane slice leftState rightState) code (fun _ _ => True) := by
+  have branches : RelCT isa
+      (fun s t => PreparedRelated p pass lane slice leftState rightState s t ∧
+        s.cf = decide (start pass slice < p.segmentLen) ∧ t.cf = decide (start pass slice < p.segmentLen))
+      (.ite .b Impl.Argon2.X86_64.FillSegment.loop (.block [])) (fun _ _ => True) := by
+    refine RelCT.ite (by intro s t h; simp only [eval, h.2.1, h.2.2]) ?_ ?_
+    · intro s t ts tt a b hp ea eb
+      have active : start pass slice < p.segmentLen := by
+        have taken := hp.2
+        simp only [eval, hp.1.2.1, Option.some.injEq, decide_eq_true_eq] at taken
+        exact taken
+      have left := hp.1.1.left.activate active (start_active pass slice)
+      have right := hp.1.1.right.activate active (start_active pass slice)
+      have related : FillSegment.Related p pass lane slice (start pass slice)
+          (p.segmentLen - start pass slice) 0 leftState rightState s t :=
+        ⟨⟨left, right, hp.1.1.bases, hp.1.1.stacks, hp.1.1.matrices, hp.1.1.work⟩,
+          hp.1.1.leftMatrix, hp.1.1.rightMatrix, hp.1.1.indices⟩
+      exact FillSegment.loop_rel p pass lane slice (start pass slice) (p.segmentLen - start pass slice) 0
+        leftState rightState (by omega) (by omega) _ _ _ _ _ _ related ea eb
+    · have noop : RelCT isa (fun _ _ : State => True) (.block []) (fun _ _ => True) :=
+        RelCT.taint (A := taint) (Taint.ofRegs [])
+          (fun _ _ _ => Taint.agree_ofRegs (by intro r hr; simp at hr)) (by taint_decide)
+      exact noop.mono (fun _ _ _ => trivial) (fun _ _ h => h)
+  exact (prepare_public_rel p pass lane slice leftState rightState).seq
+    ((check_public_rel p pass lane slice leftState rightState).seq branches)
+
+end VG.Proof.Argon2.X86_64.SegmentSetup

lean/VerifiedGarbage/Proof/Argon2/X86_64/SegmentSetupCheck.lean

@@ -0,0 +1,49 @@
+import VerifiedGarbage.Proof.Argon2.X86_64.SegmentSetupPrepare
+
+/-! Check the prepared index before entering the nonempty segment loop. -/
+
+namespace VG.Proof.Argon2.X86_64.SegmentSetup
+
+open VG VG.X86_64 VG.Spec.Argon2 VG.Impl.Argon2.X86_64.SegmentSetup
+
+theorem Prepared.of_keeps {p : Params} {pass lane slice : Nat} {s a t : State}
+    (h : Prepared s a p pass lane slice) (k : Divide.Keeps [] a t) : Prepared s t p pass lane slice := by
+  have bp := k.regs .rbp (by decide)
+  have base : FillKernel.matrix t = FillKernel.matrix a := by unfold FillKernel.matrix; rw [k.mem, bp]
+  have work : AddressCalls.work t = AddressCalls.work a := by unfold AddressCalls.work; rw [k.mem, bp]
+  refine ⟨h.context.of_keeps (k.mono (by decide)), base.trans h.matrix, work.trans h.work,
+    ?_, k.rd.trans h.rd, k.wr.trans h.wr, ?_, k.mxcsr.trans h.mxcsr⟩
+  · intro r hr ne; exact (k.regs r (by simp)).trans (h.regs r hr ne)
+  · rw [k.mem]; exact h.frame
+
+theorem check_prepared_ok {p : Params} {pass lane slice : Nat} {s a : State}
+    (h : Prepared s a p pass lane slice) : WP isa (.block check) a fun t =>
+      Prepared s t p pass lane slice ∧ t.cf = decide (start pass slice < p.segmentLen) := by
+  refine (check_ok a).mono ?_
+  rintro t ⟨flag, keeps⟩
+  have minimum := h.context.parameters.segment_bound
+  refine ⟨h.of_keeps keeps, ?_⟩
+  rw [flag, h.context.position.index, h.context.position.segmentLength,
+    ReferenceMap.word_nat (start pass slice) (Nat.lt_of_le_of_lt (start_le _ _ _ minimum.1) minimum.2),
+    ReferenceMap.word_nat p.segmentLen minimum.2]
+
+theorem finished_prepared {p : Params} {pass lane slice : Nat} {s a t : State} {state : FillState}
+    (prepared : Prepared s a p pass lane slice) (finished : FillSegment.Finished a t p pass lane slice state) :
+    FillSegment.Finished s t p pass lane slice state := by
+  refine ⟨finished.represented, finished.matrix.trans prepared.matrix, finished.work.trans prepared.work,
+    finished.position, finished.layout, finished.cache, finished.matrixWork, finished.passWord, finished.lanesWord,
+    ?_, finished.rd.trans prepared.rd, finished.wr.trans prepared.wr, ?_, finished.mxcsr.trans prepared.mxcsr⟩
+  · intro r hr ne; exact (finished.regs r hr ne).trans (prepared.regs r hr ne)
+  · have firstFrame : Frame (FillBlock.writes s p) s.mem a.mem := by
+      apply prepared.frame.sub
+      intro r hr
+      simp only [List.mem_singleton] at hr
+      subst r
+      exact ⟨⟨off (s.gpr .rbp) 8, 16⟩, by simp [FillBlock.writes], Region.sub_prefix (by decide)⟩
+    have rest := finished.frame
+    rw [FillBlock.writes, prepared.matrix, prepared.work,
+      prepared.regs .rsp (by simp [calleeSaved]) (by decide),
+      prepared.regs .rbp (by simp [calleeSaved]) (by decide)] at rest
+    exact firstFrame.trans rest
+
+end VG.Proof.Argon2.X86_64.SegmentSetup