From 8f1fe1782bdc2b5161ee5cf67919c8a9aab5029e Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 12:03:10 +0000 Subject: [PATCH 1/7] Argon2 on x86-64: prove memory initialization --- .../Impl/Argon2/X86_64/MemoryInit.lean | 63 +++++++++ .../Proof/Argon2/MemoryInit.lean | 46 +++++++ .../Proof/Argon2/X86_64/MemoryInit.lean | 116 +++++++++++++++++ .../Proof/Argon2/X86_64/MemoryInitArgs.lean | 81 ++++++++++++ .../Proof/Argon2/X86_64/MemoryInitBlock.lean | 93 +++++++++++++ .../Argon2/X86_64/MemoryInitBlockCT.lean | 57 ++++++++ .../Proof/Argon2/X86_64/MemoryInitCall.lean | 115 ++++++++++++++++ .../Proof/Argon2/X86_64/MemoryInitCallCT.lean | 36 +++++ .../Proof/Argon2/X86_64/MemoryInitClear.lean | 110 ++++++++++++++++ .../Argon2/X86_64/MemoryInitClearSetup.lean | 77 +++++++++++ .../Proof/Argon2/X86_64/MemoryInitFrame.lean | 72 ++++++++++ .../Proof/Argon2/X86_64/MemoryInitLane.lean | 108 +++++++++++++++ .../Proof/Argon2/X86_64/MemoryInitLaneCT.lean | 78 +++++++++++ .../Proof/Argon2/X86_64/MemoryInitLoop.lean | 74 +++++++++++ .../Proof/Argon2/X86_64/MemoryInitMatrix.lean | 50 +++++++ .../Proof/Argon2/X86_64/MemoryInitScale.lean | 47 +++++++ .../Proof/Argon2/X86_64/MemoryInitSetup.lean | 65 +++++++++ .../Proof/Argon2/X86_64/MemoryInitSpace.lean | 53 ++++++++ .../Proof/Argon2/X86_64/MemoryInitStage.lean | 123 ++++++++++++++++++ .../Proof/Argon2/X86_64/MemoryInitSteps.lean | 49 +++++++ 20 files changed, 1513 insertions(+) create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/MemoryInit.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitArgs.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlock.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlockCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCall.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCallCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClear.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitFrame.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLane.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLaneCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitMatrix.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitScale.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSetup.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSpace.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitStage.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSteps.lean diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean new file mode 100644 index 000000000..5804c8626 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean @@ -0,0 +1,63 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.Initial + +/-! +# Argon2 memory initialization on x86-64 + +`rbp` addresses the derivation frame containing H₀ and the public arguments; +`rbx` addresses hash scratch. `r13` holds the lane length in blocks, as +computed by the parameter-setup layer. The complete matrix is cleared before +H′ initializes columns zero and one of every lane. This establishes exactly +`Spec.Argon2.initMemory` even when the allocation initially contains arbitrary +bytes. Each H′ call uses the supplied BLAKE2b backend. +-/ + +namespace VG.Impl.Argon2.X86_64.MemoryInit + +open VG.X86_64 +open VG.Impl.Argon2.X86_64.HPrime (at_ Hash) + +/-- The memory pointer and allocated block count in the enclosing frame. -/ +def memoryOffset : Nat := 232 +def blocksOffset : Nat := 240 + +/-- Clear one word, advancing the destination and public countdown. -/ +def clearWord : List Instr := + [.store (at_ .r14) .rcx, .alu .add .r14 (.imm 8), .alu .sub .rax (.imm 1)] + +def clearHeader : List Instr := + [.mov .r14 (.mem (at_ .rbp memoryOffset)), .mov .rax (.mem (at_ .rbp blocksOffset)), + .mov32 .rcx (.imm 0)] + +def clearSetup : List Instr := clearHeader ++ List.replicate 7 (.alu .add .rax (.reg .rax)) + +def clear : Prog isa := .seq (.block clearSetup) (.loop (.block clearWord) .ne) + +/-- Reset the matrix pointer and lane number, retaining the lane stride in bytes. -/ +def lanesHeader : List Instr := + [.mov .r14 (.mem (at_ .rbp memoryOffset)), .mov32 .r12 (.imm 0), + .mov .r15 (.mem (at_ .rbp Initial.lanesOffset))] + +def lanesSetup : List Instr := lanesHeader ++ List.replicate 10 (.alu .add .r13 (.reg .r13)) + +/-- H′(1024, H₀ || LE32(column) || LE32(lane)). -/ +def blockArgs (column : Nat) : List Instr := + [.mov32 .rax (.imm (BitVec.ofNat 32 column)), .store32 (at_ .rbp 64) .rax, + .store32 (at_ .rbp 68) .r12, .mov .rdi (.reg .rbp), .mov32 .rsi (.imm 72), + .mov .rdx (.reg .r14), .mov32 .rcx (.imm 1024), .mov .r8 (.reg .rbx)] + +def block (name : String) (h : Hash) (column : Nat) : Prog isa := + .seq (.block (blockArgs column)) (.call name (HPrime.code h)) + +/-- Initialize one lane, then advance to the next lane's first block. -/ +def lane (name : String) (h : Hash) : Prog isa := + .seq (block name h 0) + (.seq (.block [.alu .add .r14 (.imm 1024)]) + (.seq (block name h 1) + (.block [.alu .add .r14 (.reg .r13), .alu .sub .r14 (.imm 1024), + .alu .add .r12 (.imm 1), .alu .sub .r15 (.imm 1)]))) + +/-- Zero the matrix and initialize both leading blocks in every lane. -/ +def code (name : String) (h : Hash) : Prog isa := + .seq clear (.seq (.block lanesSetup) (.loop (lane name h) .ne)) + +end VG.Impl.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/MemoryInit.lean b/lean/VerifiedGarbage/Proof/Argon2/MemoryInit.lean new file mode 100644 index 000000000..d9869a032 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/MemoryInit.lean @@ -0,0 +1,46 @@ +import VerifiedGarbage.Spec.Argon2.Contract +import VerifiedGarbage.Proof.Blake2.Stream + +/-! # The RFC initialization blocks as byte strings in memory -/ + +namespace VG.Proof.Argon2 + +open VG VG.Spec.Argon2 +open VG.Spec.Blake2 (bytesAt) + +/-- A complete byte representation parses to the block at the same address. -/ +theorem parseBlock_bytesAt (m : Mem) (p : Addr) : parseBlock (bytesAt m p 1024) = blockAt m p := by + apply Vector.ext + intro j hj + simp only [parseBlock, blockAt, Vector.getElem_ofFn, Spec.Blake2.leWord, + Proof.Blake2.read_eq_leBytes, BitVec.setWidth_eq] + apply Proof.Blake2.leBytes_congr + intro k hk + have bound : 8 * j + k < 1024 := by omega + simp only [bytesAt, List.getD_eq_getElem?_getD, List.getElem?_map, + List.getElem?_range bound, Option.map_some, Option.getD_some, + BitVec.ofNat_add, BitVec.add_assoc] + +/-- Initialization contains one 1024-byte H′ result at each leading cell. -/ +def initialBytes (h0 : List Byte) (lane column : Nat) : List Byte := + hPrime 1024 (h0 ++ le32 column ++ le32 lane) + +/-- The byte-level call result is sufficient for the word-level matrix spec. -/ +theorem blockAt_of_initialBytes (m : Mem) (p : Addr) (h0 : List Byte) + (lane column : Nat) (h : bytesAt m p 1024 = initialBytes h0 lane column) : + blockAt m p = parseBlock (initialBytes h0 lane column) := by + rw [← parseBlock_bytesAt, h] + +theorem initMemory_size (p : Params) (h0 : List Byte) : + (initMemory p h0).memory.size = p.blocks := by + simp only [initMemory, Array.size_map, List.size_toArray, List.length_range] + +theorem initMemory_cell (p : Params) (h0 : List Byte) (k : Nat) (hk : k < p.blocks) : + (initMemory p h0).memory[k]'(by rw [initMemory_size]; exact hk) = + if k % p.laneLen < 2 then + parseBlock (initialBytes h0 (k / p.laneLen) (k % p.laneLen)) + else zeroBlock := by + simp only [initMemory, Array.getElem_map, List.getElem_toArray, List.getElem_range, + initialBytes] + +end VG.Proof.Argon2 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean new file mode 100644 index 000000000..90de79f62 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean @@ -0,0 +1,116 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLoop +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitSetup +import VerifiedGarbage.Proof.Argon2.Dimensions + +/-! # Functional correctness of complete memory initialization -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Proof.Argon2.X86_64.Initial (wordAt) +open VG.Spec.Blake2 (bytesAt) + +theorem Cleared.frame {s t : State} {memory : Addr} {blocks : Nat} + (h : Cleared s t memory blocks) (bound : 1024 * blocks < 2 ^ 64) : + Frame [⟨memory, 1024 * blocks⟩] s.mem t.mem := by + rw [h.mem] + simpa only [show 8 * (128 * blocks) = 1024 * blocks by omega] using + clearMem_frame s.mem memory (128 * blocks) (by omega) + +theorem Cleared.word {s t : State} {memory : Addr} {blocks d : Nat} + (h : Cleared s t memory blocks) (space : Space s memory (1024 * blocks)) + (offset : d + 8 ≤ 272) : wordAt t d = wordAt s d := by + unfold wordAt + rw [h.other .rbp (by decide) (by decide) (by decide)] + apply (h.frame space.bound).readW (r := ⟨s.gpr .rbp, 272⟩) + (Offset.contains_base _ offset (by omega)) ?_ (by decide) + intro r hr; simp only [List.mem_singleton] at hr; subst r + exact space.frameMatrix + +theorem code_ok (v : Proof.Blake2.X86_64.Backend) (name : String) + (s : State) (memory : Addr) (lanes q : Nat) (lo : 1 ≤ lanes) (hq : 2 ≤ q) + (lanesBound : lanes < 2 ^ 64) (space : Space s memory (1024 * (lanes * q))) + (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8) + (lanesRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 184) 8) + (blocksRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 240) 8) + (memoryWord : wordAt s memoryOffset = memory) + (lanesWord : wordAt s VG.Impl.Argon2.X86_64.Initial.lanesOffset = BitVec.ofNat 64 lanes) + (blocksWord : wordAt s blocksOffset = BitVec.ofNat 64 (lanes * q)) + (laneLength : s.gpr .r13 = BitVec.ofNat 64 q) : + WP isa (code name (HPrime.hash v)) s fun t => + Initialized t.mem memory lanes q lanes (bytesAt s.mem (s.gpr .rbp) 64) ∧ + t.gpr .rbp = s.gpr .rbp ∧ t.gpr .rbx = s.gpr .rbx ∧ t.gpr .rsp = s.gpr .rsp ∧ + t.rd = s.rd ∧ t.wr = s.wr ∧ + Frame [⟨memory, 1024 * (lanes * q)⟩, ⟨s.gpr .rbx, 16384⟩, + below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem t.mem := by + unfold code + have blocksPositive : 1 ≤ lanes * q := by + have mul := Nat.mul_le_mul_right q lo + rw [Nat.one_mul] at mul; omega + refine WP.seq ((clear_ok s memory (lanes * q) blocksPositive space.bound memoryRead + blocksRead memoryWord blocksWord space.matrix).mono ?_) + intro a ha + have bpA := ha.other .rbp (by decide) (by decide) (by decide) + have bxA := ha.other .rbx (by decide) (by decide) (by decide) + have spA := ha.other .rsp (by decide) (by decide) (by decide) + have spaceA := space.same ha.wr bpA bxA spA + have hashA : bytesAt a.mem (a.gpr .rbp) 64 = bytesAt s.mem (s.gpr .rbp) 64 := by + rw [bpA] + apply Proof.Blake2.bytesAt_congr + intro i hi + exact (ha.frame space.bound).bytes (R := ⟨s.gpr .rbp, 64⟩) (by + intro r hr; simp only [List.mem_singleton] at hr; subst r + exact space.frameMatrix.sub_left (Region.sub_prefix (by decide))) + (show (64 : Nat) ≤ 2 ^ 64 from by decide) hi + refine WP.seq ((lanesSetup_ok a memory lanes q + (by rw [ha.rd, ha.wr, bpA]; exact memoryRead) + (by rw [ha.rd, ha.wr, bpA]; exact lanesRead) + ((ha.word space (by decide)).trans memoryWord) + ((ha.word space (by decide)).trans lanesWord) + ((ha.other .r13 (by decide) (by decide) (by decide)).trans laneLength)).mono ?_) + intro b hb + have bpB := hb.other .rbp (by decide) (by decide) (by decide) (by decide) + have bxB := hb.other .rbx (by decide) (by decide) (by decide) (by decide) + have spB := hb.other .rsp (by decide) (by decide) (by decide) (by decide) + have spaceB := spaceA.same hb.wr bpB bxB spB + refine (lanesLoop_ok v name b memory lanes q (bytesAt s.mem (s.gpr .rbp) 64) + spaceB lo lanesBound hq hb.destination hb.lane hb.remaining hb.stride ?_ ?_).mono ?_ + · rw [hb.mem, ha.mem] + exact initialized_zero s.mem memory lanes q space.bound _ + · rw [hb.mem, bpB]; exact hashA + · intro t ht + refine ⟨ht.initialized, ht.keeps.rbp.trans (bpB.trans bpA), + ht.keeps.rbx.trans (bxB.trans bxA), ht.keeps.rsp.trans (spB.trans spA), + ht.keeps.rd.trans (hb.rd.trans ha.rd), ht.keeps.wr.trans (hb.wr.trans ha.wr), ?_⟩ + have fb : Frame [⟨memory, 1024 * (lanes * q)⟩, ⟨s.gpr .rbx, 16384⟩, + below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem b.mem := by + rw [hb.mem] + exact (ha.frame space.bound).mono (by + intro r hr + simp only [List.mem_singleton] at hr + subst r + exact List.mem_cons_self ..) + apply fb.trans + have f := ht.keeps.frame + rw [bpB, bpA, bxB, bxA, spB, spA] at f + exact f + +/-- Every cell agrees with the reviewed initialization spec, in lane-major order. -/ +theorem Initialized.spec {m : Mem} {base : Addr} {p : Spec.Argon2.Params} + {h0 : List Byte} (hl : 0 < p.lanes) (hq : 0 < p.laneLen) + (h : Initialized m base p.lanes p.laneLen p.lanes h0) + (k : Nat) (hk : k < p.blocks) : + Spec.Argon2.blockAt m (base + BitVec.ofNat 64 (1024 * k)) = + (Spec.Argon2.initMemory p h0).memory[k]'(by + rw [Proof.Argon2.initMemory_size]; exact hk) := by + have blocks := Proof.Argon2.blocks_lanes p hl + have lane : k / p.laneLen < p.lanes := by + apply (Nat.div_lt_iff_lt_mul hq).mpr + simpa only [blocks] using hk + have cell := h (k / p.laneLen) lane (k % p.laneLen) (Nat.mod_lt _ hq) + rw [Nat.mul_comm (k / p.laneLen) p.laneLen, Nat.div_add_mod] at cell + simp only [lane, true_and] at cell + rw [Proof.Argon2.initMemory_cell p h0 k hk] + exact cell + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitArgs.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitArgs.lean new file mode 100644 index 000000000..18e07f600 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitArgs.lean @@ -0,0 +1,81 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.MemoryInit +import VerifiedGarbage.Proof.Argon2.X86_64.HPrime.Copy +import VerifiedGarbage.Proof.Blake2.Stream + +/-! # The 72-byte H₀, column and lane input to memory initialization -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Spec.Blake2 (bytesAt) + +def blockMem (m : Mem) (p : Addr) (column : Nat) (lane : Addr) : Mem := + (m.writeW (p + 64) (BitVec.ofNat 32 column)).writeW (p + 68) (lane.setWidth 32) + +theorem blockMem_frame (m : Mem) (p : Addr) (column : Nat) (lane : Addr) : + Frame [⟨p + 64, 8⟩] m (blockMem m p column lane) := by + unfold blockMem + have first : Frame [⟨p + 64, 8⟩] m (m.writeW (p + 64) (BitVec.ofNat 32 column)) := + (Frame.refl _ _).writeW (List.mem_singleton_self _) _ + (by simpa only [BitVec.add_zero] using + Offset.contains_base (p + 64) (d := 0) (n := 4) (k := 8) (by decide) (by decide)) + apply first.writeW (List.mem_singleton_self _) + have eq : p + 68 = (p + 64) + BitVec.ofNat 64 4 := by rw [BitVec.add_assoc]; rfl + rw [eq] + exact Offset.contains_base _ (by decide : 4 + 4 ≤ 8) (by decide) + +theorem blockMem_bytes (m : Mem) (p : Addr) (column : Nat) (lane : Addr) : + bytesAt (blockMem m p column lane) p 72 = + bytesAt m p 64 ++ Spec.Argon2.le32 column ++ Spec.Argon2.le32 lane.toNat := by + have first : bytesAt (blockMem m p column lane) p 64 = bytesAt m p 64 := by + apply Proof.Blake2.bytesAt_congr + intro i hi + apply (blockMem_frame m p column lane).bytes (R := ⟨p, 64⟩) _ + (show (64 : Nat) ≤ 2 ^ 64 from by decide) hi + · intro r hr; simp only [List.mem_singleton] at hr; subst r + exact Offset.base_disjoint _ (by decide) (by decide) + + have columnWord : (blockMem m p column lane).readW (p + 64) 32 = BitVec.ofNat 32 column := by + unfold blockMem + rw [Mem.readW_writeW_sep ?_ (by decide), Mem.readW_writeW_self32] + exact Offset.sep p (by decide) (by decide) (by decide) + have laneWord : (blockMem m p column lane).readW (p + 68) 32 = lane.setWidth 32 := + Mem.readW_writeW_self32 _ _ _ + have words := Proof.Blake2.bytesAt_add (blockMem m p column lane) (p + 64) 4 4 + have pos : p + 64 + BitVec.ofNat 64 4 = p + 68 := by rw [BitVec.add_assoc]; rfl + rw [pos, ← Proof.Blake2.wordBytes_readW _ _ (Or.inl rfl), + ← Proof.Blake2.wordBytes_readW _ _ (Or.inl rfl), columnWord, laneWord] at words + have header := Proof.Blake2.bytesAt_add (blockMem m p column lane) p 64 8 + change bytesAt (blockMem m p column lane) (p + 64) 8 = _ at words + rw [show BitVec.ofNat 64 64 = (64 : Addr) from rfl, first, words, ← BitVec.ofNat_toNat 32 lane, ← List.append_assoc] at header + exact header + +structure BlockArgs (s t : State) (column : Nat) : Prop where + input : t.gpr .rdi = s.gpr .rbp + inputLength : t.gpr .rsi = 72 + output : t.gpr .rdx = s.gpr .r14 + outputLength : t.gpr .rcx = 1024 + work : t.gpr .r8 = s.gpr .rbx + other : ∀ r, r ≠ .rax → r ≠ .rdi → r ≠ .rsi → r ≠ .rdx → r ≠ .rcx → r ≠ .r8 → + t.gpr r = s.gpr r + mem : t.mem = blockMem s.mem (s.gpr .rbp) column (s.gpr .r12) + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem blockArgs_ok (s : State) (column : Nat) + (colWrite : InRegions s.wr (s.gpr .rbp + 64) 4) + (laneWrite : InRegions s.wr (s.gpr .rbp + 68) 4) : + WP isa (.block (blockArgs column)) s (fun t => BlockArgs s t column) := by + apply WP.of_runBlock + simp only [blockArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + readSrc32, State.setReg32, State.store32, HPrime.ea_at, + RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg, + show BitVec.ofNat 64 64 = (64 : Addr) from rfl, + show BitVec.ofNat 64 68 = (68 : Addr) from rfl, + reduceCtorEq, ite_true, ite_false, colWrite, laneWrite, + Option.map_some, Option.some.injEq, exists_eq_left', + BitVec.setWidth_setWidth_of_le _ (by decide : 32 ≤ 64), BitVec.setWidth_eq] + refine ⟨rfl, rfl, rfl, rfl, rfl, fun r h1 h2 h3 h4 h5 h6 => ?_, rfl, rfl, rfl⟩ + simp only [RegUpd.gpr_setReg, h1, h2, h3, h4, h5, h6, ite_false] + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlock.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlock.lean new file mode 100644 index 000000000..d370a111c --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlock.lean @@ -0,0 +1,93 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitArgs +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitCall + +/-! # Initializing a block while preserving H₀ and the public lane counters -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Spec.Blake2 (bytesAt) + +structure BlockReady (s : State) : Prop where + input : Covers [⟨s.gpr .rbp, 72⟩] s.wr + output : Covers [⟨s.gpr .r14, 1024⟩] s.wr + work : (⟨s.gpr .rbx, 16384⟩ : Region) ∈ s.wr + frameWork : (⟨s.gpr .rbp, 72⟩ : Region).Disjoint ⟨s.gpr .rbx, 16384⟩ + frameOutput : (⟨s.gpr .rbp, 72⟩ : Region).Disjoint ⟨s.gpr .r14, 1024⟩ + outputWork : (⟨s.gpr .r14, 1024⟩ : Region).Disjoint ⟨s.gpr .rbx, 16384⟩ + stackFrame : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .rbp, 72⟩ + stackOutput : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .r14, 1024⟩ + stackWork : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .rbx, 16384⟩ + +theorem BlockArgs.regs {s t : State} {column : Nat} (h : BlockArgs s t column) + (r : Reg) (hr : r ∈ calleeSaved) : t.gpr r = s.gpr r := by + have hn : r ≠ .rax ∧ r ≠ .rdi ∧ r ≠ .rsi ∧ r ≠ .rdx ∧ r ≠ .rcx ∧ r ≠ .r8 := 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 h.other r hn.1 hn.2.1 hn.2.2.1 hn.2.2.2.1 hn.2.2.2.2.1 hn.2.2.2.2.2 + +theorem BlockReady.prefix {s : State} (h : BlockReady s) (d : Nat) + (bound : d + 4 ≤ 72) : InRegions s.wr (s.gpr .rbp + BitVec.ofNat 64 d) 4 := by + exact h.input _ _ ⟨_, List.mem_singleton_self _, Offset.contains_base _ bound (by omega)⟩ + +theorem BlockArgs.ready {s t : State} {column : Nat} (a : BlockArgs s t column) + (h : BlockReady s) : CallReady t := by + have base := a.regs .rbx (by decide) + have sp := a.regs .rsp (by decide) + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · rw [a.input, a.rd, a.wr] + intro p n ⟨r, hr, hc⟩ + simp only [List.mem_singleton] at hr; subst r + obtain ⟨r, hr, hc'⟩ := h.input p n ⟨_, List.mem_singleton_self _, hc⟩ + exact ⟨r, List.mem_append_right _ hr, hc'⟩ + · rw [a.output, a.wr]; exact h.output + · rw [a.work, a.wr]; exact h.work + · rw [a.input, a.work]; exact h.frameWork + · rw [a.output, a.work]; exact h.outputWork + · rw [sp, a.input]; exact h.stackFrame + · rw [sp, a.output]; exact h.stackOutput + · rw [sp, a.work]; exact h.stackWork + +structure BlockDone (s t : State) (column : Nat) : Prop where + digest : bytesAt t.mem (s.gpr .r14) 1024 = Spec.Argon2.hPrime 1024 + (bytesAt s.mem (s.gpr .rbp) 64 ++ Spec.Argon2.le32 column ++ Spec.Argon2.le32 (s.gpr .r12).toNat) + regs : ∀ r ∈ calleeSaved, t.gpr r = s.gpr r + rd : t.rd = s.rd + wr : t.wr = s.wr + frame : Frame [⟨s.gpr .r14, 1024⟩, ⟨s.gpr .rbx, 16384⟩, + below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem t.mem + +theorem block_ok (v : Proof.Blake2.X86_64.Backend) (name : String) + (s : State) (column : Nat) (h : BlockReady s) : + WP isa (block name (HPrime.hash v) column) s (fun t => BlockDone s t column) := by + unfold block + refine WP.seq ((blockArgs_ok s column + (by simpa only [show BitVec.ofNat 64 64 = (64 : Addr) from rfl] using h.prefix 64 (by decide)) + (by simpa only [show BitVec.ofNat 64 68 = (68 : Addr) from rfl] using h.prefix 68 (by decide))).mono ?_) + intro a ha + refine (hPrime_call_ok v name a (ha.ready h) ha.inputLength ha.outputLength).mono ?_ + intro t ht + refine ⟨?_, fun r hr => (ht.regs r hr).trans (ha.regs r hr), + ht.rd.trans ha.rd, ht.wr.trans ha.wr, ?_⟩ + · have digest := ht.digest + rw [ha.output, ha.input, ha.mem, blockMem_bytes] at digest + exact digest + · have argsFrame : Frame [⟨s.gpr .r14, 1024⟩, ⟨s.gpr .rbx, 16384⟩, + below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem a.mem := by + rw [ha.mem] + exact (blockMem_frame _ _ _ _).mono (by + intro r hr; simp only [List.mem_singleton] at hr; subst r + exact List.mem_cons_of_mem _ (List.mem_cons_of_mem _ + (List.mem_cons_of_mem _ (List.mem_singleton_self _)))) + apply argsFrame.trans + have frame := ht.frame + rw [ha.output, ha.work, ha.regs .rsp (by decide)] at frame + exact frame.mono (by + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr ⊢ + rcases hr with h | h | h + · exact Or.inl h + · exact Or.inr (Or.inl h) + · exact Or.inr (Or.inr (Or.inl h))) + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlockCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlockCT.lean new file mode 100644 index 000000000..e15069741 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitBlockCT.lean @@ -0,0 +1,57 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitBlock +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitCallCT + +/-! # Public registers survive each initialization H′ call -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit + +def AgreeSaved (s t : State) : Prop := ∀ r ∈ calleeSaved, s.gpr r = t.gpr r + +theorem blockArgs_rel (column : Nat) + (ct : ∃ hint, (taint.check (Taint.ofRegs calleeSaved) + (.block (blockArgs column)) hint).isSome = true) : + RelCT isa AgreeSaved (.block (blockArgs column)) (fun _ _ => True) := by + obtain ⟨_, check⟩ := ct + exact RelCT.taint (A := taint) (Taint.ofRegs calleeSaved) + (fun _ _ h => Taint.agree_ofRegs h) check + +theorem block_rel (v : Proof.Blake2.X86_64.Backend) (name : String) (column : Nat) + (ct : ∃ hint, (taint.check (Taint.ofRegs calleeSaved) + (.block (blockArgs column)) hint).isSome = true) : + RelCT isa (fun s t => BlockReady s ∧ BlockReady t ∧ AgreeSaved s t) + (block name (HPrime.hash v) column) AgreeSaved := by + let P := fun s t => BlockReady s ∧ BlockReady t ∧ AgreeSaved s t + have args := ((blockArgs_rel column ct).mono (P' := P) (fun _ _ h => h.2.2) + (fun _ _ h => h)).wpDep (fun s t hp => by + exact ⟨blockArgs_ok s column (hp.1.prefix 64 (by decide)) (hp.1.prefix 68 (by decide)), + blockArgs_ok t column (hp.2.1.prefix 64 (by decide)) (hp.2.1.prefix 68 (by decide))⟩) + have call := hPrime_call_rel v name (P := fun a b => + True ∧ ∃ s t, P s t ∧ BlockArgs s a column ∧ BlockArgs t b column) (by + intro a b h + obtain ⟨_, s, t, hp, ha, hb⟩ := h + refine ⟨ha.ready hp.1, hb.ready hp.2.1, ha.inputLength, hb.inputLength, + ha.outputLength, hb.outputLength, ?_, ?_, ?_, ?_⟩ + · exact ha.input.trans ((hp.2.2 .rbp (by decide)).trans hb.input.symm) + · exact ha.output.trans ((hp.2.2 .r14 (by decide)).trans hb.output.symm) + · exact ha.work.trans ((hp.2.2 .rbx (by decide)).trans hb.work.symm) + · exact (ha.regs .rsp (by decide)).trans + ((hp.2.2 .rsp (by decide)).trans (hb.regs .rsp (by decide)).symm)) + have full := (args.seq call).wpDep (fun s t hp => + ⟨block_ok v name s column hp.1, block_ok v name t column hp.2.1⟩) + exact full.mono (fun _ _ h => h) (by + intro a b h + obtain ⟨_, s, t, hp, ha, hb⟩ := h + intro r hr + exact (ha.regs r hr).trans ((hp.2.2 r hr).trans (hb.regs r hr).symm)) + +theorem blocks_rel (v : Proof.Blake2.X86_64.Backend) (name : String) : + RelCT isa (fun s t => BlockReady s ∧ BlockReady t ∧ AgreeSaved s t) + (block name (HPrime.hash v) 0) AgreeSaved ∧ + RelCT isa (fun s t => BlockReady s ∧ BlockReady t ∧ AgreeSaved s t) + (block name (HPrime.hash v) 1) AgreeSaved := + ⟨block_rel v name 0 ⟨_, by taint_decide⟩, + block_rel v name 1 ⟨_, by taint_decide⟩⟩ + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCall.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCall.lean new file mode 100644 index 000000000..d181d928f --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCall.lean @@ -0,0 +1,115 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.HPrime.Verified +import VerifiedGarbage.Impl.Argon2.X86_64.MemoryInit + +/-! # A verified H′ call to initialize a memory block -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 +open VG.Impl.Argon2.X86_64.HPrime +open VG.Spec.Blake2 (bytesAt) + +theorem hPrime_nosp (v : Proof.Blake2.X86_64.Backend) : NoSp (code (HPrime.hash v)) := by + have all (c : Prog isa) (h : NoSp c) : c.allInstrs (fun i => !Taint.clobbers i .rsp) = true := by + rw [Code.allInstrs_eq, List.all_eq_true] + intro i hi; simp only [h i hi, Bool.not_false] + have hi := all _ (HPrime.hash_ok v).initNoSp + have hu := all _ (HPrime.hash_ok v).updateNoSp + have hf := all _ (HPrime.hash_ok v).finalizeNoSp + have check : (code (HPrime.hash v)).allInstrs (fun i => !Taint.clobbers i .rsp) = true := by + simp only [code, setup, saved, first, chooseLength, init, initArgs, absorbFixed, + fixedArgs, update, updateArgs, absorbInput, inputArgs, finishInput, finalize, + finalizeArgs, finishOutput, extendDigest, emitPrefix, copy, copyByte, chain, + next, copyRemaining, restore, Code.allInstrs] + rw [hi, hu, hf] + decide +kernel + rw [Code.allInstrs_eq, List.all_eq_true] at check + intro i hi + simpa only [Bool.not_eq_true'] using check i hi + +theorem hPrime_depth (v : Proof.Blake2.X86_64.Backend) : (code (HPrime.hash v)).depth = 2 := by + simp only [code, first, chooseLength, init, absorbFixed, update, absorbInput, + finishInput, finalize, finishOutput, extendDigest, emitPrefix, copy, chain, + next, copyRemaining, Code.depth, (HPrime.hash_ok v).initDepth, + (HPrime.hash_ok v).updateDepth, (HPrime.hash_ok v).finalizeDepth] + rfl + +structure CallReady (s : State) : Prop where + input : Covers [⟨s.gpr .rdi, 72⟩] (s.rd ++ s.wr) + output : Covers [⟨s.gpr .rdx, 1024⟩] s.wr + work : (⟨s.gpr .r8, 16384⟩ : Region) ∈ s.wr + inputWork : (⟨s.gpr .rdi, 72⟩ : Region).Disjoint ⟨s.gpr .r8, 16384⟩ + outputWork : (⟨s.gpr .rdx, 1024⟩ : Region).Disjoint ⟨s.gpr .r8, 16384⟩ + stackInput : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .rdi, 72⟩ + stackOutput : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .rdx, 1024⟩ + stackWork : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .r8, 16384⟩ + +structure Called (s t : State) : Prop where + digest : bytesAt t.mem (s.gpr .rdx) 1024 = Spec.Argon2.hPrime 1024 (bytesAt s.mem (s.gpr .rdi) 72) + 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 .r8, 16384⟩, below (s.gpr .rsp) 24] s.mem t.mem + +theorem hPrime_call_hyps (s : State) (h : CallReady s) + (inputLength : s.gpr .rsi = 72) (outputLength : s.gpr .rcx = 1024) : + HPrime.localContract.pre (s.callEntry.withRegions [⟨s.gpr .rdi, 72⟩] + [⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .r8, 16384⟩]) ∧ + Covers [⟨s.gpr .rdi, 72⟩, ⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .r8, 16384⟩] (s.rd ++ s.wr) ∧ + Covers [⟨s.gpr .rdx, 1024⟩, ⟨s.gpr .r8, 16384⟩] s.wr := by + have g : ∀ r, r ≠ .rsp → s.callEntry.gpr r = s.gpr r := fun r hr => State.callEntry_gpr s hr + have inner := below_callee (s.gpr .rsp) 16 + have ret := below_sub (sp := s.gpr .rsp) (by decide : 8 ≤ 24) (by decide) + refine ⟨?_, ?_, ?_⟩ + · simp only [HPrime.localContract, HPrime.inputR, HPrime.outputR, HPrime.workR, + HPrime.stackR, HPrime.retR, 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), g _ (by decide : Reg.r8 ≠ .rsp), + State.callEntry_rsp, inputLength, outputLength] + exact ⟨rfl, rfl, by decide, by decide, by decide, h.inputWork, h.outputWork, + h.stackInput.sub_left inner, h.stackOutput.sub_left inner, h.stackWork.sub_left inner, + h.stackOutput.sub_left ret, h.stackWork.sub_left ret⟩ + · intro p n hp + rcases hp with ⟨r, hr, hc⟩ + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl + · exact h.input 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⟩ + · exact ⟨_, List.mem_append_right _ h.work, 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.work, hc⟩ + +theorem hPrime_call_ok (v : Proof.Blake2.X86_64.Backend) (name : String) + (s : State) (h : CallReady s) (inputLength : s.gpr .rsi = 72) + (outputLength : s.gpr .rcx = 1024) : + WP isa (.call name (code (HPrime.hash v))) s (Called s) := by + obtain ⟨pre, cover, writes⟩ := hPrime_call_hyps s h inputLength outputLength + refine WP.call (k := HPrime.localContract) (HPrime.code_correct v) (hPrime_nosp v) + (by rw [hPrime_depth]; decide) pre cover writes ?_ + intro t rd wr regs frame _ ⟨u, memU, regsU, digest⟩ + have inputBytes : bytesAt s.callEntry.mem (s.gpr .rdi) 72 = bytesAt s.mem (s.gpr .rdi) 72 := by + apply Proof.Blake2.bytesAt_congr + intro i hi + exact Proof.MdStream.X86_64.callEntry_byte s (h.stackInput.sub_left + (below_sub (by decide) (by decide))) (show (72 : Nat) ≤ 2 ^ 64 from by decide) hi + refine ⟨?_, regs, rd, wr, ?_⟩ + · change bytesAt u.mem (s.callEntry.gpr .rdx) (s.callEntry.gpr .rcx).toNat = + Spec.Argon2.hPrime (s.callEntry.gpr .rcx).toNat + (bytesAt s.callEntry.mem (s.callEntry.gpr .rdi) (s.callEntry.gpr .rsi).toNat) at digest + rw [State.callEntry_gpr _ (by decide : Reg.rdx ≠ .rsp), + State.callEntry_gpr _ (by decide : Reg.rcx ≠ .rsp), + State.callEntry_gpr _ (by decide : Reg.rdi ≠ .rsp), + State.callEntry_gpr _ (by decide : Reg.rsi ≠ .rsp), + memU, inputLength, outputLength, + show (72 : Addr).toNat = 72 from rfl, + show (1024 : Addr).toNat = 1024 from rfl, inputBytes] at digest + exact digest + · rw [hPrime_depth] at frame + exact frame + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCallCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCallCT.lean new file mode 100644 index 000000000..57f593b6d --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCallCT.lean @@ -0,0 +1,36 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitCall + +/-! # Initialization's H′ calls leak only their public argument registers -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 +open VG.Impl.Argon2.X86_64.HPrime (code) + +theorem hPrime_call_rel (v : Proof.Blake2.X86_64.Backend) (name : String) + {P : State → State → Prop} + (pre : ∀ s t, P s t → CallReady s ∧ CallReady t ∧ + s.gpr .rsi = 72 ∧ t.gpr .rsi = 72 ∧ s.gpr .rcx = 1024 ∧ t.gpr .rcx = 1024 ∧ + s.gpr .rdi = t.gpr .rdi ∧ s.gpr .rdx = t.gpr .rdx ∧ + s.gpr .r8 = t.gpr .r8 ∧ s.gpr .rsp = t.gpr .rsp) : + RelCT isa P (.call name (code (HPrime.hash v))) (fun _ _ => True) := by + apply RelCT.callEx (k := HPrime.localContract) (HPrime.code_correct v) (HPrime.code_ct v) + intro s t hp + obtain ⟨hs, ht, ls, lt, os, ot, di, dx, r8, sp⟩ := pre s t hp + obtain ⟨ps, cs, ws⟩ := hPrime_call_hyps s hs ls os + obtain ⟨pt, ct, wt⟩ := hPrime_call_hyps t ht lt ot + 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 ∧ + s.callEntry.gpr .r8 = t.callEntry.gpr .r8 ∧ + s.callEntry.gpr .rsp = t.callEntry.gpr .rsp + 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), + State.callEntry_gpr _ (by decide : Reg.r8 ≠ .rsp), State.callEntry_rsp] + exact ⟨di, ls.trans lt.symm, dx, os.trans ot.symm, r8, congrArg (· - 8) sp⟩ + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClear.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClear.lean new file mode 100644 index 000000000..b1b5205a0 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClear.lean @@ -0,0 +1,110 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.MemoryInit +import VerifiedGarbage.Proof.Argon2.X86_64.HPrime.Copy + +/-! # Zeroing the Argon2 matrix, independently of its initial contents -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit + +def clearMem (m : Mem) (p : Addr) : Nat → Mem + | 0 => m + | n + 1 => (clearMem m p n).writeW (p + BitVec.ofNat 64 (8 * n)) (0 : BitVec 64) + +theorem clearMem_frame (m : Mem) (p : Addr) (n : Nat) (bound : 8 * n < 2 ^ 64) : + Frame [⟨p, 8 * n⟩] m (clearMem m p n) := by + induction n with + | zero => exact Frame.refl _ _ + | succ n ih => + have smaller : Frame [⟨p, 8 * (n + 1)⟩] m (clearMem m p n) := + (ih (by omega)).sub (by + intro r hr; simp only [List.mem_singleton] at hr; subst r + exact ⟨_, List.mem_singleton_self _, Region.sub_prefix (by omega)⟩) + exact smaller.writeW (List.mem_singleton_self _) (0 : BitVec 64) + (Offset.contains_base _ (by omega) (by omega)) + +theorem clearMem_word (m : Mem) (p : Addr) (n j : Nat) + (bound : 8 * n < 2 ^ 64) (hj : j < n) : + (clearMem m p n).readW (p + BitVec.ofNat 64 (8 * j)) 64 = 0 := by + induction n with + | zero => omega + | succ n ih => + rw [clearMem] + by_cases eq : j = n + · subst j; exact Mem.readW_writeW_self64 _ _ _ + · rw [Mem.readW_writeW_sep ?_ (by decide)] + · exact ih (by omega) (by omega) + · exact Offset.sep p (by omega) (by omega) (by omega) + +theorem clearWord_ok (s : State) (hw : InRegions s.wr (s.gpr .r14) 8) : + WP isa (.block clearWord) s fun t => + t.mem = s.mem.writeW (s.gpr .r14) (s.gpr .rcx) ∧ + t.gpr .r14 = s.gpr .r14 + 8 ∧ t.gpr .rax = s.gpr .rax - 1 ∧ + t.zf = some (s.gpr .rax - 1 == 0) ∧ + (∀ r, r ≠ .rax → r ≠ .r14 → t.gpr r = s.gpr r) ∧ t.rd = s.rd ∧ t.wr = s.wr := by + apply WP.of_runBlock + simp only [clearWord, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + State.store64, execAlu, HPrime.ea_at, BitVec.add_zero, + RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg, + RegUpd.gpr_arithFlags, RegUpd.mem_arithFlags, RegUpd.rd_arithFlags, + RegUpd.wr_arithFlags, RegUpd.zf_arithFlags, RegUpd.zf_setReg, + show (BitVec.signExtend 64 (8 : BitVec 32)) = 8 from rfl, + show (BitVec.signExtend 64 (1 : BitVec 32)) = 1 from rfl, + hw, reduceCtorEq, ite_true, ite_false, + Option.bind_some, Option.some.injEq, exists_eq_left'] + exact ⟨trivial, trivial, trivial, trivial, + fun r h1 h2 => by simp only [h1, h2, ite_false], trivial, trivial⟩ + +structure ClearI (s₀ : State) (p : Addr) (n j : Nat) (s : State) : Prop where + bound : j ≤ n + destination : s.gpr .r14 = p + BitVec.ofNat 64 (8 * j) + count : s.gpr .rax = BitVec.ofNat 64 (n - j) + zero : s.gpr .rcx = 0 + other : ∀ r, r ≠ .rax → r ≠ .r14 → s.gpr r = s₀.gpr r + rd : s.rd = s₀.rd + wr : s.wr = s₀.wr + mem : s.mem = clearMem s₀.mem p j + +theorem clearLoop_ok (s₀ : State) (p : Addr) (n : Nat) (lo : 1 ≤ n) + (bound : 8 * n < 2 ^ 64) (dst : s₀.gpr .r14 = p) + (count : s₀.gpr .rax = BitVec.ofNat 64 n) (zero : s₀.gpr .rcx = 0) + (write : ∀ j < n, InRegions s₀.wr (p + BitVec.ofNat 64 (8 * j)) 8) : + WP isa (.loop (.block clearWord) .ne) s₀ (ClearI s₀ p n n) := by + refine WP.loop (M := isa) (fun k s => ∃ j, k = n - j ∧ j < n ∧ ClearI s₀ p n j s) + ?_ n s₀ ⟨0, by omega, lo, by omega, by simpa using dst, by simpa only [Nat.sub_zero] using count, + zero, fun _ _ _ => rfl, rfl, rfl, rfl⟩ + rintro k s ⟨j, rfl, hj, h⟩ + have hw : InRegions s.wr (s.gpr .r14) 8 := by + rw [h.wr, h.destination]; exact write j hj + refine (clearWord_ok s hw).mono ?_ + rintro t ⟨memT, dstT, countT, zfT, otherT, rdT, wrT⟩ + have nextCount : BitVec.ofNat 64 (n - j) - 1 = BitVec.ofNat 64 (n - (j + 1)) := by + rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl, Offset.ofNat_sub_ofNat (by omega)] + congr 1 + have next : ClearI s₀ p n (j + 1) t := by + refine ⟨by omega, ?_, ?_, (otherT _ (by decide) (by decide)).trans h.zero, + fun r h1 h2 => (otherT r h1 h2).trans (h.other r h1 h2), + rdT.trans h.rd, wrT.trans h.wr, ?_⟩ + · rw [dstT, h.destination, BitVec.add_assoc, show (8 : Addr) = BitVec.ofNat 64 8 from rfl, ← BitVec.ofNat_add] + congr 2 + · rw [countT, h.count, nextCount] + · rw [memT, h.mem, h.destination, h.zero]; rfl + have zf : t.zf = some (decide (n - (j + 1) = 0)) := by + rw [zfT, h.count, nextCount] + congr 1 + rw [Bool.eq_iff_iff, beq_iff_eq, decide_eq_true_iff] + constructor + · intro eq + have num := congrArg BitVec.toNat eq + simpa only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega : n - (j + 1) < 2 ^ 64), + show (0 : Addr).toNat = 0 from rfl] using num + · intro eq; rw [eq]; rfl + by_cases done : j + 1 = n + · refine .inl ⟨?_, done ▸ next⟩ + simp only [eval, zf, show n - (j + 1) = 0 by omega, decide_true, + Option.map_some, Bool.not_true] + · refine .inr ⟨?_, n - (j + 1), by omega, j + 1, rfl, by omega, next⟩ + simp only [eval, zf, show n - (j + 1) ≠ 0 by omega, decide_false, + Option.map_some, Bool.not_false] + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean new file mode 100644 index 000000000..1f02e16b0 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean @@ -0,0 +1,77 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitScale +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitSpace +import VerifiedGarbage.Proof.Argon2.X86_64.InitialLayout + +/-! # Clearing the complete allocation using its public block count -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Proof.Argon2.X86_64.Initial (wordAt) + +structure ClearHeader (s t : State) : Prop where + destination : t.gpr .r14 = wordAt s memoryOffset + count : t.gpr .rax = wordAt s blocksOffset + zero : t.gpr .rcx = 0 + other : ∀ r, r ≠ .r14 → r ≠ .rax → r ≠ .rcx → t.gpr r = s.gpr r + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem clearHeader_ok (s : State) + (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8) + (blocksRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 240) 8) : + WP isa (.block clearHeader) s (ClearHeader s) := by + apply WP.of_runBlock + simp only [clearHeader, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + readSrc32, State.load64, State.setReg32, HPrime.ea_at, memoryOffset, blocksOffset, + RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg, + show BitVec.ofNat 64 232 = (232 : Addr) from rfl, + show BitVec.ofNat 64 240 = (240 : Addr) from rfl, + memoryRead, blocksRead, reduceCtorEq, ite_true, ite_false, + Option.map_some, Option.some.injEq, exists_eq_left'] + refine ⟨rfl, rfl, rfl, fun r h1 h2 h3 => ?_, rfl, rfl, rfl⟩ + simp only [RegUpd.gpr_setReg, h1, h2, h3, ite_false] + +structure Cleared (s t : State) (memory : Addr) (blocks : Nat) : Prop where + destination : t.gpr .r14 = memory + BitVec.ofNat 64 (1024 * blocks) + other : ∀ r, r ≠ .r14 → r ≠ .rax → r ≠ .rcx → t.gpr r = s.gpr r + mem : t.mem = clearMem s.mem memory (128 * blocks) + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem clear_ok (s : State) (memory : Addr) (blocks : Nat) (lo : 1 ≤ blocks) + (bound : 1024 * blocks < 2 ^ 64) + (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8) + (blocksRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 240) 8) + (memoryWord : wordAt s memoryOffset = memory) + (blocksWord : wordAt s blocksOffset = BitVec.ofNat 64 blocks) + (cover : Covers [⟨memory, 1024 * blocks⟩] s.wr) : + WP isa clear s fun t => Cleared s t memory blocks := by + unfold clear clearSetup + apply WP.seq + rw [WP.block_append_iff] + refine (clearHeader_ok s memoryRead blocksRead).mono ?_ + intro a ha + refine (scale_ok a .rax 7).mono ?_ + intro b hb + have count : b.gpr .rax = BitVec.ofNat 64 (128 * blocks) := by + rw [hb.value, ha.count, blocksWord, ← BitVec.ofNat_mul, Nat.mul_comm] + have dst : b.gpr .r14 = memory := (hb.other _ (by decide)).trans (ha.destination.trans memoryWord) + have zero : b.gpr .rcx = 0 := (hb.other _ (by decide)).trans ha.zero + have mem : b.mem = s.mem := hb.mem.trans ha.mem + have rd : b.rd = s.rd := hb.rd.trans ha.rd + have wr : b.wr = s.wr := hb.wr.trans ha.wr + have other : ∀ r, r ≠ .r14 → r ≠ .rax → r ≠ .rcx → b.gpr r = s.gpr r := + fun r h1 h2 h3 => (hb.other r h2).trans (ha.other r h1 h2 h3) + refine (clearLoop_ok b memory (128 * blocks) (by omega) (by omega) dst count zero ?_).mono ?_ + · intro j hj + rw [wr] + exact cover _ _ ⟨_, List.mem_singleton_self _, Offset.contains_base _ (by omega) (by omega)⟩ + · intro t ht + refine ⟨?_, fun r h1 h2 h3 => (ht.other r h2 h1).trans (other r h1 h2 h3), ?_, + ht.rd.trans rd, ht.wr.trans wr⟩ + · rw [ht.destination, show 8 * (128 * blocks) = 1024 * blocks by omega] + · rw [ht.mem, mem] + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitFrame.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitFrame.lean new file mode 100644 index 000000000..fe879c4c1 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitFrame.lean @@ -0,0 +1,72 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitStage + +/-! # Effects allowed across the complete lane loop -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 +open VG.Spec.Blake2 (bytesAt) + +def keptRegs : List Reg := [.rbp, .rbx, .rsp, .r13] + +structure Keeps (s t : State) (memory : Addr) (bytes : Nat) : Prop where + regs : ∀ r ∈ keptRegs, t.gpr r = s.gpr r + rd : t.rd = s.rd + wr : t.wr = s.wr + frame : Frame [⟨memory, bytes⟩, ⟨s.gpr .rbx, 16384⟩, + below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem t.mem + +theorem Keeps.rbp {s t : State} {memory : Addr} {bytes : Nat} (h : Keeps s t memory bytes) : + t.gpr .rbp = s.gpr .rbp := h.regs _ (by decide) +theorem Keeps.rbx {s t : State} {memory : Addr} {bytes : Nat} (h : Keeps s t memory bytes) : + t.gpr .rbx = s.gpr .rbx := h.regs _ (by decide) +theorem Keeps.rsp {s t : State} {memory : Addr} {bytes : Nat} (h : Keeps s t memory bytes) : + t.gpr .rsp = s.gpr .rsp := h.regs _ (by decide) + +theorem Keeps.refl (s : State) (memory : Addr) (bytes : Nat) : Keeps s s memory bytes := + ⟨fun _ _ => rfl, rfl, rfl, Frame.refl _ _⟩ + +theorem Keeps.trans {s t u : State} {memory : Addr} {bytes : Nat} + (h : Keeps s t memory bytes) (k : Keeps t u memory bytes) : Keeps s u memory bytes := + ⟨fun r hr => (k.regs r hr).trans (h.regs r hr), k.rd.trans h.rd, k.wr.trans h.wr, + h.frame.trans (by simpa only [h.rbx, h.rsp, h.rbp] using k.frame)⟩ + +theorem Space.keeps {s t : State} {memory : Addr} {bytes : Nat} + (h : Space s memory bytes) (k : Keeps s t memory bytes) : Space t memory bytes := + h.same k.wr k.rbp k.rbx k.rsp + +theorem Keeps.h0 {s t : State} {memory : Addr} {bytes : Nat} + (h : Keeps s t memory bytes) (space : Space s memory bytes) : + bytesAt t.mem (t.gpr .rbp) 64 = bytesAt s.mem (s.gpr .rbp) 64 := by + rw [h.rbp] + apply Proof.Blake2.bytesAt_congr + intro i hi + apply h.frame.bytes (R := ⟨s.gpr .rbp, 64⟩) _ + (show (64 : Nat) ≤ 2 ^ 64 from by decide) hi + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact space.frameMatrix.sub_left (Region.sub_prefix (by decide)) + · exact space.frameWork.sub_left (Region.sub_prefix (by decide)) + · exact space.stackFrame.symm.sub_left (Region.sub_prefix (by decide)) + · exact Offset.base_disjoint _ (by decide) (by decide) + +theorem LaneDone.keeps {s t : State} (memory : Addr) (bytes d : Nat) + (h : LaneDone s t) (dst : s.gpr .r14 = memory + BitVec.ofNat 64 d) + (bound : d + 2048 ≤ bytes) : Keeps s t memory bytes := by + refine ⟨?_, h.rd, h.wr, ?_⟩ + · intro r hr + have facts : ∀ r ∈ keptRegs, r ∈ calleeSaved ∧ r ≠ .r14 ∧ r ≠ .r12 ∧ r ≠ .r15 := by decide + obtain ⟨cs, h14, h12, h15⟩ := facts r hr + exact h.regs r cs h14 h12 h15 + · apply h.frame.sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨_, List.mem_cons_self .., by rw [dst]; exact Offset.sub_base _ bound⟩ + · exact ⟨_, List.mem_cons_of_mem _ (List.mem_cons_self ..), fun _ h => h⟩ + · exact ⟨_, List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (List.mem_cons_self ..)), fun _ h => h⟩ + · exact ⟨_, List.mem_cons_of_mem _ (List.mem_cons_of_mem _ + (List.mem_cons_of_mem _ (List.mem_singleton_self _))), fun _ h => h⟩ + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLane.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLane.lean new file mode 100644 index 000000000..655b53e97 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLane.lean @@ -0,0 +1,108 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitSpace +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitSteps + +/-! # Initializing both leading blocks of one lane -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Spec.Blake2 (bytesAt) + +structure LaneDone (s t : State) : Prop where + first : bytesAt t.mem (s.gpr .r14) 1024 = Proof.Argon2.initialBytes + (bytesAt s.mem (s.gpr .rbp) 64) (s.gpr .r12).toNat 0 + second : bytesAt t.mem (s.gpr .r14 + 1024) 1024 = Proof.Argon2.initialBytes + (bytesAt s.mem (s.gpr .rbp) 64) (s.gpr .r12).toNat 1 + destination : t.gpr .r14 = s.gpr .r14 + s.gpr .r13 + lane : t.gpr .r12 = s.gpr .r12 + 1 + remaining : t.gpr .r15 = s.gpr .r15 - 1 + zf : t.zf = some (s.gpr .r15 - 1 == 0) + regs : ∀ r ∈ calleeSaved, r ≠ .r14 → r ≠ .r12 → r ≠ .r15 → t.gpr r = s.gpr r + rd : t.rd = s.rd + wr : t.wr = s.wr + frame : Frame [⟨s.gpr .r14, 2048⟩, ⟨s.gpr .rbx, 16384⟩, + below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem t.mem + +theorem frame_widen {m m' : Mem} {p : Addr} {d : Nat} {work stack headRegion : Region} + (h : Frame [⟨p + BitVec.ofNat 64 d, 1024⟩, work, stack, headRegion] m m') + (bound : d + 1024 ≤ 2048) : Frame [⟨p, 2048⟩, work, stack, headRegion] m m' := by + apply h.sub + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ⟨_, List.mem_cons_self .., Offset.sub_base _ bound⟩ + · exact ⟨_, List.mem_cons_of_mem _ (List.mem_cons_self ..), fun _ h => h⟩ + · exact ⟨_, List.mem_cons_of_mem _ (List.mem_cons_of_mem _ (List.mem_cons_self ..)), fun _ h => h⟩ + · exact ⟨_, List.mem_cons_of_mem _ (List.mem_cons_of_mem _ + (List.mem_cons_of_mem _ (List.mem_singleton_self _))), fun _ h => h⟩ + +theorem lane_ok (v : Proof.Blake2.X86_64.Backend) (name : String) + (s : State) (memory : Addr) (bytes d : Nat) (space : Space s memory bytes) + (dst : s.gpr .r14 = memory + BitVec.ofNat 64 d) (bound : d + 2048 ≤ bytes) : + WP isa (lane name (HPrime.hash v)) s (LaneDone s) := by + have ready := space.blockReady dst (by omega) + unfold lane + refine WP.seq ((block_ok v name s 0 ready).mono ?_) + intro a ha + have spaceA := space.same ha.wr (ha.regs .rbp (by decide)) + (ha.regs .rbx (by decide)) (ha.regs .rsp (by decide)) + refine WP.seq ((advance_ok a).mono ?_) + intro b hb + have spaceB := spaceA.same hb.wr (hb.other .rbp (by decide)) + (hb.other .rbx (by decide)) (hb.other .rsp (by decide)) + have base : b.gpr .r14 = s.gpr .r14 + 1024 := by rw [hb.destination, ha.regs .r14 (by decide)] + have bp : b.gpr .rbp = s.gpr .rbp := (hb.other _ (by decide)).trans (ha.regs _ (by decide)) + have bx : b.gpr .rbx = s.gpr .rbx := (hb.other _ (by decide)).trans (ha.regs _ (by decide)) + have sp : b.gpr .rsp = s.gpr .rsp := (hb.other _ (by decide)).trans (ha.regs _ (by decide)) + have laneB : b.gpr .r12 = s.gpr .r12 := (hb.other _ (by decide)).trans (ha.regs _ (by decide)) + have strideB : b.gpr .r13 = s.gpr .r13 := (hb.other _ (by decide)).trans (ha.regs _ (by decide)) + have remainingB : b.gpr .r15 = s.gpr .r15 := (hb.other _ (by decide)).trans (ha.regs _ (by decide)) + have dstB : b.gpr .r14 = memory + BitVec.ofNat 64 (d + 1024) := by + rw [base, dst, BitVec.ofNat_add, BitVec.add_assoc]; rfl + have readyB := spaceB.blockReady dstB (by omega) + refine WP.seq ((block_ok v name b 1 readyB).mono ?_) + intro c hc + refine (laneEnd_ok c).mono ?_ + intro t ht + have secondFrame := hc.frame + rw [base, bx, sp, bp] at secondFrame + have keptFirst : bytesAt c.mem (s.gpr .r14) 1024 = bytesAt b.mem (s.gpr .r14) 1024 := by + apply Proof.Blake2.bytesAt_congr + intro i hi + apply secondFrame.bytes (R := ⟨s.gpr .r14, 1024⟩) _ + (show (1024 : Nat) ≤ 2 ^ 64 from by decide) hi + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact Offset.base_disjoint _ (by decide) (by decide) + · rw [dst]; exact space.matrixWork.sub_left (Offset.sub_base _ (by omega)) + · rw [dst]; exact space.stackMatrix.symm.sub_left (Offset.sub_base _ (by omega)) + · rw [dst]; exact space.frameMatrix.symm.sub_left (Offset.sub_base _ (by omega)) |>.sub_right + (Offset.sub_base _ (by decide : 64 + 8 ≤ 272)) + have h0B : bytesAt b.mem (b.gpr .rbp) 64 = bytesAt s.mem (s.gpr .rbp) 64 := by + rw [hb.mem, bp]; exact ha.h0 ready + refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_, ht.rd.trans (hc.rd.trans (hb.rd.trans ha.rd)), + ht.wr.trans (hc.wr.trans (hb.wr.trans ha.wr)), ?_⟩ + · rw [ht.mem, keptFirst, hb.mem]; exact ha.digest + · have digest := hc.digest + rw [base, h0B, laneB] at digest + rw [ht.mem]; exact digest + · rw [ht.destination, hc.regs .r14 (by decide), hc.regs .r13 (by decide), base, strideB] + rw [BitVec.add_assoc, BitVec.add_comm (1024 : Addr), ← BitVec.add_assoc, + BitVec.add_sub_cancel] + · rw [ht.lane, hc.regs .r12 (by decide), laneB] + · rw [ht.remaining, hc.regs .r15 (by decide), remainingB] + · rw [ht.zf, hc.regs .r15 (by decide), remainingB] + · intro r hr h14 h12 h15 + exact (ht.other r h14 h12 h15).trans ((hc.regs r hr).trans + ((hb.other r h14).trans (ha.regs r hr))) + · rw [ht.mem] + rw [hb.mem] at secondFrame + have firstFrame := frame_widen (p := s.gpr .r14) (d := 0) + (by simpa using ha.frame) + (by decide) + have finalFrame := frame_widen (p := s.gpr .r14) (d := 1024) + (by simpa only [show BitVec.ofNat 64 1024 = (1024 : Addr) from rfl] using secondFrame) (by decide) + exact firstFrame.trans finalFrame + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLaneCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLaneCT.lean new file mode 100644 index 000000000..fed28212c --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLaneCT.lean @@ -0,0 +1,78 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitBlockCT +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLane + +/-! # The two leading blocks of a lane have a public execution trace -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit + +structure LaneReady (memory : Addr) (bytes d : Nat) (s : State) : Prop where + space : Space s memory bytes + destination : s.gpr .r14 = memory + BitVec.ofNat 64 d + +def RelatedLane (memory : Addr) (bytes d : Nat) (s t : State) : Prop := + LaneReady memory bytes d s ∧ LaneReady memory bytes d t ∧ AgreeSaved s t + +theorem BlockDone.laneReady {s t : State} {column : Nat} {memory : Addr} {bytes d : Nat} + (h : BlockDone s t column) (ready : LaneReady memory bytes d s) : + LaneReady memory bytes d t := + ⟨ready.space.same h.wr (h.regs .rbp (by decide)) (h.regs .rbx (by decide)) + (h.regs .rsp (by decide)), (h.regs .r14 (by decide)).trans ready.destination⟩ + +theorem block_lane_rel (v : Proof.Blake2.X86_64.Backend) (name : String) (column : Nat) + (ct : ∃ hint, (taint.check (Taint.ofRegs calleeSaved) + (.block (blockArgs column)) hint).isSome = true) + (memory : Addr) (bytes d : Nat) (bound : d + 1024 ≤ bytes) : + RelCT isa (RelatedLane memory bytes d) (block name (HPrime.hash v) column) + (RelatedLane memory bytes d) := by + have h := ((block_rel v name column ct).mono + (P' := RelatedLane memory bytes d) (fun _ _ hp => + ⟨hp.1.space.blockReady hp.1.destination bound, + hp.2.1.space.blockReady hp.2.1.destination bound, hp.2.2⟩) + (fun _ _ h => h)).wpDep (fun s t hp => + ⟨block_ok v name s column (hp.1.space.blockReady hp.1.destination bound), + block_ok v name t column (hp.2.1.space.blockReady hp.2.1.destination bound)⟩) + exact h.mono (fun _ _ h => h) (by + intro a b h + obtain ⟨pub, s, t, hp, ha, hb⟩ := h + exact ⟨ha.laneReady hp.1, hb.laneReady hp.2.1, pub⟩) + +theorem advance_rel : RelCT isa AgreeSaved + (.block [.alu .add .r14 (.imm 1024)]) AgreeSaved := by + apply RelCT.taintRegs (τ := Taint.ofRegs calleeSaved) + (fun _ _ h => Taint.agree_ofRegs h) calleeSaved + taint_decide + +theorem advance_lane_rel (memory : Addr) (bytes d : Nat) : + RelCT isa (RelatedLane memory bytes d) (.block [.alu .add .r14 (.imm 1024)]) + (RelatedLane memory bytes (d + 1024)) := by + have h := (advance_rel.mono (P' := RelatedLane memory bytes d) + (fun _ _ h => h.2.2) (fun _ _ h => h)).wpDep + (fun s t _ => ⟨advance_ok s, advance_ok t⟩) + have ready {s t : State} (h : Advanced s t) (hs : LaneReady memory bytes d s) : + LaneReady memory bytes (d + 1024) t := by + refine ⟨hs.space.same h.wr (h.other .rbp (by decide)) + (h.other .rbx (by decide)) (h.other .rsp (by decide)), ?_⟩ + rw [h.destination, hs.destination, BitVec.ofNat_add, BitVec.add_assoc]; rfl + exact h.mono (fun _ _ h => h) (by + intro a b h + obtain ⟨pub, s, t, hp, ha, hb⟩ := h + exact ⟨ready ha hp.1, ready hb hp.2.1, pub⟩) + +theorem laneEnd_rel : RelCT isa AgreeSaved + (.block [.alu .add .r14 (.reg .r13), .alu .sub .r14 (.imm 1024), + .alu .add .r12 (.imm 1), .alu .sub .r15 (.imm 1)]) AgreeSaved := by + apply RelCT.taintRegs (τ := Taint.ofRegs calleeSaved) + (fun _ _ h => Taint.agree_ofRegs h) calleeSaved + taint_decide + +theorem lane_rel (v : Proof.Blake2.X86_64.Backend) (name : String) + (memory : Addr) (bytes d : Nat) (bound : d + 2048 ≤ bytes) : + RelCT isa (RelatedLane memory bytes d) (lane name (HPrime.hash v)) AgreeSaved := by + exact (block_lane_rel v name 0 ⟨_, by taint_decide⟩ memory bytes d (by omega)).seq + ((advance_lane_rel memory bytes d).seq + ((block_lane_rel v name 1 ⟨_, by taint_decide⟩ memory bytes (d + 1024) (by omega)).seq + (laneEnd_rel.mono (fun _ _ h => h.2.2) (fun _ _ h => h)))) + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean new file mode 100644 index 000000000..62f737444 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean @@ -0,0 +1,74 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitFrame + +/-! # Termination and correctness of the all-lanes initialization loop -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Spec.Blake2 (bytesAt) + +structure LoopI (s₀ : State) (memory : Addr) (lanes q j : Nat) (h0 : List Byte) (s : State) : Prop where + bound : j ≤ lanes + destination : s.gpr .r14 = memory + BitVec.ofNat 64 (1024 * (j * q)) + lane : s.gpr .r12 = BitVec.ofNat 64 j + remaining : s.gpr .r15 = BitVec.ofNat 64 (lanes - j) + stride : s.gpr .r13 = BitVec.ofNat 64 (1024 * q) + keeps : Keeps s₀ s memory (1024 * (lanes * q)) + initialized : Initialized s.mem memory lanes q j h0 + hash : bytesAt s.mem (s.gpr .rbp) 64 = h0 + +theorem lanesLoop_ok (v : Proof.Blake2.X86_64.Backend) (name : String) + (s₀ : State) (memory : Addr) (lanes q : Nat) (h0 : List Byte) + (space : Space s₀ memory (1024 * (lanes * q))) (lo : 1 ≤ lanes) + (lanesBound : lanes < 2 ^ 64) (hq : 2 ≤ q) + (dst : s₀.gpr .r14 = memory) (laneReg : s₀.gpr .r12 = 0) + (remaining : s₀.gpr .r15 = BitVec.ofNat 64 lanes) + (stride : s₀.gpr .r13 = BitVec.ofNat 64 (1024 * q)) + (initialized : Initialized s₀.mem memory lanes q 0 h0) + (hash : bytesAt s₀.mem (s₀.gpr .rbp) 64 = h0) : + WP isa (.loop (lane name (HPrime.hash v)) .ne) s₀ (LoopI s₀ memory lanes q lanes h0) := by + refine WP.loop (M := isa) + (fun n s => ∃ j, n = lanes - j ∧ j < lanes ∧ LoopI s₀ memory lanes q j h0 s) + ?_ lanes s₀ ⟨0, by omega, lo, by omega, by simpa using dst, laneReg, + by simpa only [Nat.sub_zero] using remaining, stride, Keeps.refl _ _ _, initialized, hash⟩ + rintro n s ⟨j, rfl, hj, h⟩ + have spaceS := space.keeps h.keeps + have endBound : 1024 * (j * q) + 2048 ≤ 1024 * (lanes * q) := by + have mul := Nat.mul_le_mul_right q (show j + 1 ≤ lanes by omega) + rw [Nat.add_mul, Nat.one_mul] at mul + omega + refine (lane_ok v name s memory (1024 * (lanes * q)) (1024 * (j * q)) + spaceS h.destination endBound).mono ?_ + intro t ht + have kt := ht.keeps memory _ _ h.destination endBound + have nextCount : BitVec.ofNat 64 (lanes - j) - 1 = BitVec.ofNat 64 (lanes - (j + 1)) := by + rw [show (1 : Addr) = BitVec.ofNat 64 1 from rfl, Offset.ofNat_sub_ofNat (by omega)] + congr 1 + have next : LoopI s₀ memory lanes q (j + 1) h0 t := by + refine ⟨by omega, ?_, ?_, ?_, ?_, h.keeps.trans kt, + initialized_lane memory lanes q j h0 spaceS hq hj lanesBound h.destination h.lane + h.hash h.initialized ht, (kt.h0 spaceS).trans h.hash⟩ + · rw [ht.destination, h.destination, h.stride, BitVec.add_assoc, ← BitVec.ofNat_add, + Nat.add_mul, Nat.one_mul, Nat.mul_add] + · rw [ht.lane, h.lane, BitVec.ofNat_add]; rfl + · rw [ht.remaining, h.remaining, nextCount] + · exact (kt.regs .r13 (by decide)).trans h.stride + have zf : t.zf = some (decide (lanes - (j + 1) = 0)) := by + rw [ht.zf, h.remaining, nextCount] + congr 1 + rw [Bool.eq_iff_iff, beq_iff_eq, decide_eq_true_iff] + constructor + · intro eq + have num := congrArg BitVec.toNat eq + simpa only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega : lanes - (j + 1) < 2 ^ 64), + show (0 : Addr).toNat = 0 from rfl] using num + · intro eq; rw [eq]; rfl + by_cases done : j + 1 = lanes + · refine .inl ⟨?_, done ▸ next⟩ + simp only [eval, zf, show lanes - (j + 1) = 0 by omega, decide_true, + Option.map_some, Bool.not_true] + · refine .inr ⟨?_, lanes - (j + 1), by omega, j + 1, rfl, by omega, next⟩ + simp only [eval, zf, show lanes - (j + 1) ≠ 0 by omega, decide_false, + Option.map_some, Bool.not_false] + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitMatrix.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitMatrix.lean new file mode 100644 index 000000000..96e6789e3 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitMatrix.lean @@ -0,0 +1,50 @@ +import VerifiedGarbage.Proof.Argon2.MemoryInit +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitBlock +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitClear + +/-! # Matrix cells and the memory preserved by initialization calls -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Spec.Argon2 +open VG.Spec.Blake2 (bytesAt) + +theorem clearMem_block (m : Mem) (p : Addr) (blocks k : Nat) + (bound : 1024 * blocks < 2 ^ 64) (hk : k < blocks) : + blockAt (clearMem m p (128 * blocks)) (p + BitVec.ofNat 64 (1024 * k)) = zeroBlock := by + apply Vector.ext + intro j hj + simp only [blockAt, zeroBlock, Vector.getElem_ofFn, Vector.getElem_replicate] + rw [BitVec.add_assoc, ← BitVec.ofNat_add, + show 1024 * k + 8 * j = 8 * (128 * k + j) by omega] + exact clearMem_word m p (128 * blocks) (128 * k + j) (by omega) (by omega) + +theorem blockAt_frame {m m' : Mem} {rs : List Region} (frame : Frame rs m m') + (p : Addr) (sep : ∀ r ∈ rs, (⟨p, 1024⟩ : Region).Disjoint r) : + blockAt m' p = blockAt m p := by + rw [← Proof.Argon2.parseBlock_bytesAt, ← Proof.Argon2.parseBlock_bytesAt] + apply congrArg parseBlock + apply Proof.Blake2.bytesAt_congr + intro i hi + exact frame.bytes (R := ⟨p, 1024⟩) sep (show (1024 : Nat) ≤ 2 ^ 64 from by decide) hi + +theorem BlockDone.h0 {s t : State} {column : Nat} (h : BlockDone s t column) + (ready : BlockReady s) : bytesAt t.mem (s.gpr .rbp) 64 = bytesAt s.mem (s.gpr .rbp) 64 := by + apply Proof.Blake2.bytesAt_congr + intro i hi + apply h.frame.bytes (R := ⟨s.gpr .rbp, 64⟩) _ + (show (64 : Nat) ≤ 2 ^ 64 from by decide) hi + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · exact ready.frameOutput.sub_left (Region.sub_prefix (by decide)) + · exact ready.frameWork.sub_left (Region.sub_prefix (by decide)) + · exact ready.stackFrame.symm.sub_left (Region.sub_prefix (by decide)) + · exact Offset.base_disjoint _ (by decide) (by decide) + +theorem BlockDone.block {s t : State} {column : Nat} (h : BlockDone s t column) : + blockAt t.mem (s.gpr .r14) = parseBlock + (Proof.Argon2.initialBytes (bytesAt s.mem (s.gpr .rbp) 64) (s.gpr .r12).toNat column) := + Proof.Argon2.blockAt_of_initialBytes _ _ _ _ _ h.digest + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitScale.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitScale.lean new file mode 100644 index 000000000..95faa58c8 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitScale.lean @@ -0,0 +1,47 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitSteps + +/-! # Fixed public scaling by powers of two using baseline additions -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 + +structure Scaled (s t : State) (r : Reg) (n : Nat) : Prop where + value : t.gpr r = s.gpr r * BitVec.ofNat 64 (2 ^ n) + other : ∀ q, q ≠ r → t.gpr q = s.gpr q + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem double_ok (s : State) (r : Reg) : + WP isa (.block [.alu .add r (.reg r)]) s fun t => + t.gpr r = s.gpr r + s.gpr r ∧ (∀ q, q ≠ r → t.gpr q = s.gpr q) ∧ + t.mem = s.mem ∧ t.rd = s.rd ∧ t.wr = s.wr := by + apply WP.of_runBlock + simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu, + Option.bind_some, Option.some.injEq, exists_eq_left'] + refine ⟨?_, fun q hr => ?_, rfl, rfl, rfl⟩ + · simp only [RegUpd.gpr_arithFlags, RegUpd.gpr_setReg, ite_true] + · simp only [RegUpd.gpr_arithFlags, RegUpd.gpr_setReg, hr, ite_false] + +theorem scale_ok (s : State) (r : Reg) (n : Nat) : + WP isa (.block (List.replicate n (.alu .add r (.reg r)))) s fun t => Scaled s t r n := by + induction n generalizing s with + | zero => + exact WP.block_nil ⟨by rw [Nat.pow_zero]; exact (BitVec.mul_one _).symm, + fun _ _ => rfl, rfl, rfl, rfl⟩ + | succ n ih => + change WP isa (.block (([.alu .add r (.reg r)] : List Instr) ++ + List.replicate n (.alu .add r (.reg r)))) s _ + rw [WP.block_append_iff] + refine (double_ok s r).mono ?_ + rintro a ⟨value, other, mem, rd, wr⟩ + refine (ih a).mono ?_ + intro t ht + refine ⟨?_, fun q hq => (ht.other q hq).trans (other q hq), + ht.mem.trans mem, ht.rd.trans rd, ht.wr.trans wr⟩ + rw [ht.value, value, ← BitVec.mul_two, Nat.pow_succ, BitVec.ofNat_mul, + BitVec.mul_assoc] + exact congrArg (fun v => s.gpr r * v) (BitVec.mul_comm _ _) + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSetup.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSetup.lean new file mode 100644 index 000000000..351956bc8 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSetup.lean @@ -0,0 +1,65 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitClearSetup + +/-! # Set up the public lane loop after matrix clearing -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Proof.Argon2.X86_64.Initial (wordAt) + +structure LanesHeader (s t : State) : Prop where + destination : t.gpr .r14 = wordAt s memoryOffset + lane : t.gpr .r12 = 0 + remaining : t.gpr .r15 = wordAt s VG.Impl.Argon2.X86_64.Initial.lanesOffset + other : ∀ r, r ≠ .r14 → r ≠ .r12 → r ≠ .r15 → t.gpr r = s.gpr r + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem lanesHeader_ok (s : State) + (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8) + (lanesRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 184) 8) : + WP isa (.block lanesHeader) s (LanesHeader s) := by + apply WP.of_runBlock + simp only [lanesHeader, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + readSrc32, State.load64, State.setReg32, HPrime.ea_at, memoryOffset, VG.Impl.Argon2.X86_64.Initial.lanesOffset, + RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg, + show BitVec.ofNat 64 232 = (232 : Addr) from rfl, + show BitVec.ofNat 64 184 = (184 : Addr) from rfl, + memoryRead, lanesRead, reduceCtorEq, ite_true, ite_false, + Option.map_some, Option.some.injEq, exists_eq_left'] + refine ⟨rfl, rfl, rfl, fun r h1 h2 h3 => ?_, rfl, rfl, rfl⟩ + simp only [RegUpd.gpr_setReg, h1, h2, h3, ite_false] + +structure Setup (s t : State) (memory : Addr) (lanes q : Nat) : Prop where + destination : t.gpr .r14 = memory + lane : t.gpr .r12 = 0 + remaining : t.gpr .r15 = BitVec.ofNat 64 lanes + stride : t.gpr .r13 = BitVec.ofNat 64 (1024 * q) + other : ∀ r, r ≠ .r14 → r ≠ .r12 → r ≠ .r15 → r ≠ .r13 → t.gpr r = s.gpr r + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem lanesSetup_ok (s : State) (memory : Addr) (lanes q : Nat) + (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8) + (lanesRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 184) 8) + (memoryWord : wordAt s memoryOffset = memory) + (lanesWord : wordAt s VG.Impl.Argon2.X86_64.Initial.lanesOffset = BitVec.ofNat 64 lanes) + (laneLength : s.gpr .r13 = BitVec.ofNat 64 q) : + WP isa (.block lanesSetup) s fun t => Setup s t memory lanes q := by + unfold lanesSetup + rw [WP.block_append_iff] + refine (lanesHeader_ok s memoryRead lanesRead).mono ?_ + intro a ha + refine (scale_ok a .r13 10).mono ?_ + intro t ht + refine ⟨?_, ?_, ?_, ?_, fun r h1 h2 h3 h4 => (ht.other r h4).trans (ha.other r h1 h2 h3), + ht.mem.trans ha.mem, ht.rd.trans ha.rd, ht.wr.trans ha.wr⟩ + · rw [ht.other .r14 (by decide), ha.destination, memoryWord] + · rw [ht.other .r12 (by decide), ha.lane] + · rw [ht.other .r15 (by decide), ha.remaining, lanesWord] + · rw [ht.value, ha.other .r13 (by decide) (by decide) (by decide), laneLength, + ← BitVec.ofNat_mul, Nat.mul_comm] + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSpace.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSpace.lean new file mode 100644 index 000000000..b94f4c359 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSpace.lean @@ -0,0 +1,53 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitMatrix + +/-! # Permissions for the matrix, derivation frame and hash scratch -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 + +structure Space (s : State) (memory : Addr) (bytes : Nat) : Prop where + matrix : Covers [⟨memory, bytes⟩] s.wr + frame : Covers [⟨s.gpr .rbp, 72⟩] s.wr + work : (⟨s.gpr .rbx, 16384⟩ : Region) ∈ s.wr + frameMatrix : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨memory, bytes⟩ + frameWork : (⟨s.gpr .rbp, 272⟩ : Region).Disjoint ⟨s.gpr .rbx, 16384⟩ + matrixWork : (⟨memory, bytes⟩ : Region).Disjoint ⟨s.gpr .rbx, 16384⟩ + stackFrame : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .rbp, 272⟩ + stackMatrix : (below (s.gpr .rsp) 24).Disjoint ⟨memory, bytes⟩ + stackWork : (below (s.gpr .rsp) 24).Disjoint ⟨s.gpr .rbx, 16384⟩ + bound : bytes < 2 ^ 64 + +theorem Space.same {s t : State} {memory : Addr} {bytes : Nat} (h : Space s memory bytes) + (wr : t.wr = s.wr) (bp : t.gpr .rbp = s.gpr .rbp) + (bx : t.gpr .rbx = s.gpr .rbx) (sp : t.gpr .rsp = s.gpr .rsp) : Space t memory bytes := by + constructor + · rw [wr]; exact h.matrix + · rw [bp, wr]; exact h.frame + · rw [bx, wr]; exact h.work + · rw [bp]; exact h.frameMatrix + · rw [bp, bx]; exact h.frameWork + · rw [bx]; exact h.matrixWork + · rw [sp, bp]; exact h.stackFrame + · rw [sp]; exact h.stackMatrix + · rw [sp, bx]; exact h.stackWork + · exact h.bound + +theorem Space.blockReady {s : State} {memory : Addr} {bytes d : Nat} + (h : Space s memory bytes) (dst : s.gpr .r14 = memory + BitVec.ofNat 64 d) + (bound : d + 1024 ≤ bytes) : BlockReady s := by + have outputSub : Region.Sub ⟨s.gpr .r14, 1024⟩ ⟨memory, bytes⟩ := by + rw [dst]; exact Offset.sub_base _ bound + have outputCover : Covers [⟨s.gpr .r14, 1024⟩] s.wr := by + have narrow : Covers [⟨s.gpr .r14, 1024⟩] [⟨memory, bytes⟩] := Covers.of_sub (by + intro r hr; simp only [List.mem_singleton] at hr; subst r + exact ⟨_, List.mem_singleton_self _, d, dst, bound⟩) + exact fun p n hp => h.matrix p n (narrow p n hp) + exact ⟨h.frame, outputCover, h.work, + h.frameWork.sub_left (Region.sub_prefix (by decide)), + (h.frameMatrix.sub_left (Region.sub_prefix (by decide))).sub_right outputSub, + h.matrixWork.sub_left outputSub, + h.stackFrame.sub_right (Region.sub_prefix (by decide)), + h.stackMatrix.sub_right outputSub, h.stackWork⟩ + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitStage.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitStage.lean new file mode 100644 index 000000000..4429de7f8 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitStage.lean @@ -0,0 +1,123 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLane + +/-! # Matrix invariant: completed lanes contain their RFC initialization blocks -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Spec.Argon2 +open VG.Spec.Blake2 (bytesAt) + +def Initialized (m : Mem) (base : Addr) (lanes q done : Nat) (h0 : List Byte) : Prop := + ∀ lane < lanes, ∀ column < q, + blockAt m (base + BitVec.ofNat 64 (1024 * (lane * q + column))) = + if lane < done ∧ column < 2 then parseBlock (Proof.Argon2.initialBytes h0 lane column) + else zeroBlock + +theorem cell_bound (lanes q lane column : Nat) (hl : lane < lanes) (hc : column < q) : + lane * q + column < lanes * q := by + have mul := Nat.mul_le_mul_right q (show lane + 1 ≤ lanes by omega) + rw [Nat.add_mul, Nat.one_mul] at mul + omega + +theorem cell_sep (q j lane column : Nat) (hq : 2 ≤ q) (hc : column < q) + (other : lane ≠ j ∨ 2 ≤ column) : + 1024 * (lane * q + column) + 1024 ≤ 1024 * (j * q) ∨ + 1024 * (j * q) + 2048 ≤ 1024 * (lane * q + column) := by + by_cases lt : lane < j + · have mul := Nat.mul_le_mul_right q (show lane + 1 ≤ j by omega) + rw [Nat.add_mul, Nat.one_mul] at mul + omega + · by_cases gt : j < lane + · have mul := Nat.mul_le_mul_right q (show j + 1 ≤ lane by omega) + rw [Nat.add_mul, Nat.one_mul] at mul + omega + · have eq : lane = j := by omega + subst lane + have large : 2 ≤ column := other.elim (fun h => False.elim (h rfl)) id + omega + +theorem initialized_zero (m : Mem) (base : Addr) (lanes q : Nat) + (bound : 1024 * (lanes * q) < 2 ^ 64) (h0 : List Byte) : + Initialized (clearMem m base (128 * (lanes * q))) base lanes q 0 h0 := by + intro lane hl column hc + rw [clearMem_block _ _ _ _ bound (cell_bound _ _ _ _ hl hc)] + simp only [Nat.not_lt_zero, false_and, ite_false] + +theorem initialized_lane {s t : State} (memory : Addr) (lanes q j : Nat) + (h0 : List Byte) (space : Space s memory (1024 * (lanes * q))) + (hq : 2 ≤ q) (hj : j < lanes) (lanesBound : lanes < 2 ^ 64) + (dst : s.gpr .r14 = memory + BitVec.ofNat 64 (1024 * (j * q))) + (laneReg : s.gpr .r12 = BitVec.ofNat 64 j) + (hash : bytesAt s.mem (s.gpr .rbp) 64 = h0) + (initialized : Initialized s.mem memory lanes q j h0) (done : LaneDone s t) : + Initialized t.mem memory lanes q (j + 1) h0 := by + have laneValue : (s.gpr .r12).toNat = j := by + rw [laneReg, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)] + have currentEnd : 1024 * (j * q) + 2048 ≤ 2 ^ 64 := by + have mul := Nat.mul_le_mul_right q (show j + 1 ≤ lanes by omega) + rw [Nat.add_mul, Nat.one_mul] at mul + have b := space.bound + omega + have cellEnd (lane column : Nat) (hl : lane < lanes) (hc : column < q) : + 1024 * (lane * q + column) + 1024 ≤ 2 ^ 64 := by + have cell := cell_bound lanes q lane column hl hc + have b := space.bound + omega + intro lane hl column hc + by_cases same : lane = j + · subst lane + by_cases first : column = 0 + · subst column + rw [ite_eq_left (by omega)] + apply Proof.Argon2.blockAt_of_initialBytes + have eq := done.first + rw [hash, laneValue, dst] at eq + simpa only [Nat.add_zero] using eq + · by_cases second : column = 1 + · subst column + rw [ite_eq_left (by omega)] + apply Proof.Argon2.blockAt_of_initialBytes + have eq := done.second + rw [hash, laneValue, dst, BitVec.add_assoc, + show (1024 : Addr) = BitVec.ofNat 64 1024 from rfl, ← BitVec.ofNat_add] at eq + rw [Nat.mul_add, Nat.mul_one] + exact eq + · have large : 2 ≤ column := by omega + have sep := cell_sep q j j column hq hc (Or.inr large) + have kept : blockAt t.mem (memory + BitVec.ofNat 64 (1024 * (j * q + column))) = + blockAt s.mem (memory + BitVec.ofNat 64 (1024 * (j * q + column))) := by + apply blockAt_frame done.frame + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · rw [dst]; exact Offset.disjoint _ sep (cellEnd j column hj hc) currentEnd + · exact space.matrixWork.sub_left (Offset.sub_base _ + (by have := cell_bound lanes q j column hj hc; omega)) + · exact space.stackMatrix.symm.sub_left (Offset.sub_base _ + (by have := cell_bound lanes q j column hj hc; omega)) + · exact space.frameMatrix.symm.sub_left (Offset.sub_base _ + (by have := cell_bound lanes q j column hj hc; omega)) |>.sub_right + (Offset.sub_base _ (by decide : 64 + 8 ≤ 272)) + rw [kept, initialized j hj column hc] + simp only [Nat.lt_irrefl, false_and, ite_false, ite_eq_right (by omega : ¬ (j < j + 1 ∧ column < 2))] + · have kept : blockAt t.mem (memory + BitVec.ofNat 64 (1024 * (lane * q + column))) = + blockAt s.mem (memory + BitVec.ofNat 64 (1024 * (lane * q + column))) := by + apply blockAt_frame done.frame + intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + rcases hr with rfl | rfl | rfl | rfl + · rw [dst] + exact Offset.disjoint _ (cell_sep q j lane column hq hc (Or.inl same)) + (cellEnd lane column hl hc) currentEnd + · exact space.matrixWork.sub_left (Offset.sub_base _ + (by have := cell_bound lanes q lane column hl hc; omega)) + · exact space.stackMatrix.symm.sub_left (Offset.sub_base _ + (by have := cell_bound lanes q lane column hl hc; omega)) + · exact space.frameMatrix.symm.sub_left (Offset.sub_base _ + (by have := cell_bound lanes q lane column hl hc; omega)) |>.sub_right + (Offset.sub_base _ (by decide : 64 + 8 ≤ 272)) + rw [kept, initialized lane hl column hc] + by_cases before : lane < j ∧ column < 2 <;> + simp (disch := omega) only [ite_eq_left, ite_eq_right] + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSteps.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSteps.lean new file mode 100644 index 000000000..b03aad5dd --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitSteps.lean @@ -0,0 +1,49 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.MemoryInit +import VerifiedGarbage.Proof.Argon2.X86_64.HPrime.Copy + +/-! # Public pointer advances and lane countdowns -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 + +structure Advanced (s t : State) : Prop where + destination : t.gpr .r14 = s.gpr .r14 + 1024 + other : ∀ r, r ≠ .r14 → t.gpr r = s.gpr r + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem advance_ok (s : State) : + WP isa (.block [.alu .add .r14 (.imm 1024)]) s (Advanced s) := by + apply WP.of_runBlock + simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu, + Option.bind_some, Option.some.injEq, exists_eq_left', + show (BitVec.signExtend 64 (1024 : BitVec 32)) = 1024 from rfl] + refine ⟨rfl, fun r hr => ?_, rfl, rfl, rfl⟩ + simp only [RegUpd.gpr_arithFlags, RegUpd.gpr_setReg, hr, ite_false] + +structure LaneEnd (s t : State) : Prop where + destination : t.gpr .r14 = s.gpr .r14 + s.gpr .r13 - 1024 + lane : t.gpr .r12 = s.gpr .r12 + 1 + remaining : t.gpr .r15 = s.gpr .r15 - 1 + zf : t.zf = some (s.gpr .r15 - 1 == 0) + other : ∀ r, r ≠ .r14 → r ≠ .r12 → r ≠ .r15 → t.gpr r = s.gpr r + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem laneEnd_ok (s : State) : + WP isa (.block [.alu .add .r14 (.reg .r13), .alu .sub .r14 (.imm 1024), + .alu .add .r12 (.imm 1), .alu .sub .r15 (.imm 1)]) s (LaneEnd s) := by + apply WP.of_runBlock + simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu, + RegUpd.gpr_arithFlags, RegUpd.gpr_setReg, + reduceCtorEq, ite_true, ite_false, + Option.bind_some, Option.some.injEq, exists_eq_left', + show (BitVec.signExtend 64 (1024 : BitVec 32)) = 1024 from rfl, + show (BitVec.signExtend 64 (1 : BitVec 32)) = 1 from rfl] + refine ⟨rfl, rfl, rfl, rfl, fun r h1 h2 h3 => ?_, rfl, rfl, rfl⟩ + simp only [RegUpd.gpr_arithFlags, RegUpd.gpr_setReg, h1, h2, h3, ite_false] + +end VG.Proof.Argon2.X86_64.MemoryInit From 8efb98c6d395c94d6ad1d1fca94e4a349e2fbb40 Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 12:15:52 +0000 Subject: [PATCH 2/7] Argon2 on x86-64: prove the complete initialization trace --- .../Impl/Argon2/X86_64/MemoryInit.lean | 8 +- .../Proof/Argon2/X86_64/MemoryInit.lean | 2 +- .../Proof/Argon2/X86_64/MemoryInitCT.lean | 114 ++++++++++++++++++ .../Argon2/X86_64/MemoryInitClearCT.lean | 59 +++++++++ .../Argon2/X86_64/MemoryInitClearSetup.lean | 49 +++++--- .../Proof/Argon2/X86_64/MemoryInitLit.lean | 11 ++ .../Proof/Argon2/X86_64/MemoryInitLoop.lean | 41 ++++--- .../Proof/Argon2/X86_64/MemoryInitLoopCT.lean | 51 ++++++++ 8 files changed, 304 insertions(+), 31 deletions(-) create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLit.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoopCT.lean diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean index 5804c8626..ce46a463a 100644 --- a/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/MemoryInit.lean @@ -30,7 +30,9 @@ def clearHeader : List Instr := def clearSetup : List Instr := clearHeader ++ List.replicate 7 (.alu .add .rax (.reg .rax)) -def clear : Prog isa := .seq (.block clearSetup) (.loop (.block clearWord) .ne) +def clearSetupCode : Prog isa := .block clearSetup + +def clear : Prog isa := .seq clearSetupCode (.loop (.block clearWord) .ne) /-- Reset the matrix pointer and lane number, retaining the lane stride in bytes. -/ def lanesHeader : List Instr := @@ -39,6 +41,8 @@ def lanesHeader : List Instr := def lanesSetup : List Instr := lanesHeader ++ List.replicate 10 (.alu .add .r13 (.reg .r13)) +def lanesSetupCode : Prog isa := .block lanesSetup + /-- H′(1024, H₀ || LE32(column) || LE32(lane)). -/ def blockArgs (column : Nat) : List Instr := [.mov32 .rax (.imm (BitVec.ofNat 32 column)), .store32 (at_ .rbp 64) .rax, @@ -58,6 +62,6 @@ def lane (name : String) (h : Hash) : Prog isa := /-- Zero the matrix and initialize both leading blocks in every lane. -/ def code (name : String) (h : Hash) : Prog isa := - .seq clear (.seq (.block lanesSetup) (.loop (lane name h) .ne)) + .seq clear (.seq lanesSetupCode (.loop (lane name h) .ne)) end VG.Impl.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean index 90de79f62..eaf7c8ff6 100644 --- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInit.lean @@ -43,7 +43,7 @@ theorem code_ok (v : Proof.Blake2.X86_64.Backend) (name : String) t.rd = s.rd ∧ t.wr = s.wr ∧ Frame [⟨memory, 1024 * (lanes * q)⟩, ⟨s.gpr .rbx, 16384⟩, below (s.gpr .rsp) 24, ⟨s.gpr .rbp + 64, 8⟩] s.mem t.mem := by - unfold code + unfold code lanesSetupCode have blocksPositive : 1 ≤ lanes * q := by have mul := Nat.mul_le_mul_right q lo rw [Nat.one_mul] at mul; omega diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCT.lean new file mode 100644 index 000000000..90fb3755b --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitCT.lean @@ -0,0 +1,114 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitClearCT +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLoopCT + +/-! # The complete memory initialization trace depends only on public parameters -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Spec.Blake2 (bytesAt) + +structure LoopReady (memory : Addr) (lanes q : Nat) (s : State) : Prop where + space : Space s memory (1024 * (lanes * q)) + initialized : Initialized s.mem memory lanes q 0 (bytesAt s.mem (s.gpr .rbp) 64) + destination : s.gpr .r14 = memory + lane : s.gpr .r12 = 0 + remaining : s.gpr .r15 = BitVec.ofNat 64 lanes + stride : s.gpr .r13 = BitVec.ofNat 64 (1024 * q) + +theorem Cleared.ready {s t : State} {memory : Addr} {lanes q : Nat} + (h : Cleared s t memory (lanes * q)) (hs : Ready memory lanes q s) : + Ready memory lanes q t := by + have bp := h.other .rbp (by decide) (by decide) (by decide) + have bx := h.other .rbx (by decide) (by decide) (by decide) + have sp := h.other .rsp (by decide) (by decide) (by decide) + refine ⟨hs.space.same h.wr bp bx sp, ?_, ?_, ?_, ?_, ?_, ?_, ?_⟩ + · rw [h.rd, h.wr, bp]; exact hs.memoryRead + · rw [h.rd, h.wr, bp]; exact hs.lanesRead + · rw [h.rd, h.wr, bp]; exact hs.blocksRead + · exact (h.word hs.space (by decide)).trans hs.memoryWord + · exact (h.word hs.space (by decide)).trans hs.lanesWord + · exact (h.word hs.space (by decide)).trans hs.blocksWord + · exact (h.other .r13 (by decide) (by decide) (by decide)).trans hs.laneLength + +theorem Setup.loopReady {s a b : State} {memory : Addr} {lanes q : Nat} + (hs : Ready memory lanes q s) (ha : Cleared s a memory (lanes * q)) + (hb : Setup a b memory lanes q) : LoopReady memory lanes q b := by + have ready := ha.ready hs + refine ⟨ready.space.same hb.wr (hb.other .rbp (by decide) (by decide) (by decide) (by decide)) + (hb.other .rbx (by decide) (by decide) (by decide) (by decide)) + (hb.other .rsp (by decide) (by decide) (by decide) (by decide)), ?_, + hb.destination, hb.lane, hb.remaining, hb.stride⟩ + rw [hb.mem, ha.mem] + exact initialized_zero s.mem memory lanes q hs.space.bound _ + +theorem lanesSetup_rel : RelCT isa AgreeBases lanesSetupCode (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs publicBases) + (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide) + +theorem Setup.agree {s t a b : State} {memory : Addr} {lanes q : Nat} + (ha : Setup s a memory lanes q) (hb : Setup t b memory lanes q) + (hp : AgreeBases s t) : AgreeSaved a b := by + intro r hr + by_cases h14 : r = .r14 + · subst r; exact ha.destination.trans hb.destination.symm + by_cases h12 : r = .r12 + · subst r; exact ha.lane.trans hb.lane.symm + by_cases h15 : r = .r15 + · subst r; exact ha.remaining.trans hb.remaining.symm + by_cases h13 : r = .r13 + · subst r; exact ha.stride.trans hb.stride.symm + have included : ∀ r ∈ calleeSaved, r ≠ .r14 → r ≠ .r12 → r ≠ .r15 → r ≠ .r13 → + r ∈ publicBases := by decide + exact (ha.other r h14 h12 h15 h13).trans + ((hp r (included r hr h14 h12 h15 h13)).trans (hb.other r h14 h12 h15 h13).symm) + +theorem lanesLoop_ready_rel (v : Proof.Blake2.X86_64.Backend) (name : String) + (memory : Addr) (lanes q : Nat) (lo : 1 ≤ lanes) (lanesBound : lanes < 2 ^ 64) + (hq : 2 ≤ q) : + RelCT isa (fun s t => LoopReady memory lanes q s ∧ LoopReady memory lanes q t ∧ + AgreeSaved s t) (.loop (lane name (HPrime.hash v)) .ne) AgreeSaved := by + intro s t ts tt a b hp es et + have initial {s : State} (h : LoopReady memory lanes q s) : + LoopI s memory lanes q 0 (bytesAt s.mem (s.gpr .rbp) 64) s := + ⟨by omega, by simpa using h.destination, h.lane, + by simpa only [Nat.sub_zero] using h.remaining, h.stride, Keeps.refl _ _ _, + h.initialized, rfl⟩ + exact lanesLoop_rel v name s t memory lanes q _ _ hp.1.space hp.2.1.space lo + lanesBound hq _ _ _ _ _ _ ⟨initial hp.1, initial hp.2.1, hp.2.2⟩ es et + +theorem code_ct (v : Proof.Blake2.X86_64.Backend) (name : String) + (memory : Addr) (lanes q : Nat) (lo : 1 ≤ lanes) (lanesBound : lanes < 2 ^ 64) + (hq : 2 ≤ q) : + ConstantTime isa (Ready memory lanes q) AgreeBases (code name (HPrime.hash v)) := by + let P := fun s t => Ready memory lanes q s ∧ Ready memory lanes q t ∧ AgreeBases s t + have blocksPositive : 1 ≤ lanes * q := by + have mul := Nat.mul_le_mul_right q lo + rw [Nat.one_mul] at mul; omega + have cleared := (clear_rel memory lanes q).wpDep (fun s t hp => + ⟨clear_ok s memory (lanes * q) blocksPositive hp.1.space.bound hp.1.memoryRead + hp.1.blocksRead hp.1.memoryWord hp.1.blocksWord hp.1.space.matrix, + clear_ok t memory (lanes * q) blocksPositive hp.2.1.space.bound hp.2.1.memoryRead + hp.2.1.blocksRead hp.2.1.memoryWord hp.2.1.blocksWord hp.2.1.space.matrix⟩) + let R := fun a b => AgreeBases a b ∧ ∃ s t, P s t ∧ + Cleared s a memory (lanes * q) ∧ Cleared t b memory (lanes * q) + have setup := (lanesSetup_rel.mono (P' := R) (fun _ _ h => h.1) + (fun _ _ h => h)).wpDep (F := fun a b => Setup a b memory lanes q) (by + intro a b hp + obtain ⟨_, s, t, hst, ha, hb⟩ := hp + have ra := ha.ready hst.1 + have rb := hb.ready hst.2.1 + exact ⟨lanesSetup_ok a memory lanes q ra.memoryRead ra.lanesRead ra.memoryWord + ra.lanesWord ra.laneLength, + lanesSetup_ok b memory lanes q rb.memoryRead rb.lanesRead rb.memoryWord + rb.lanesWord rb.laneLength⟩) + have prepared : RelCT isa R lanesSetupCode (fun a b => + LoopReady memory lanes q a ∧ LoopReady memory lanes q b ∧ AgreeSaved a b) := setup.mono (fun _ _ h => h) (by + intro a b h + obtain ⟨_, c, d, hp, ha, hb⟩ := h + obtain ⟨pub, s, t, hst, hc, hd⟩ := hp + exact ⟨ha.loopReady hst.1 hc, hb.loopReady hst.2.1 hd, ha.agree hb pub⟩) + exact (cleared.seq (prepared.seq (lanesLoop_ready_rel v name memory lanes q lo + lanesBound hq))).constantTime + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearCT.lean new file mode 100644 index 000000000..980a48089 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearCT.lean @@ -0,0 +1,59 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInit +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitBlockCT +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLit + +/-! # Matrix clearing uses only public addresses and the public allocation size -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit +open VG.Proof.Argon2.X86_64.Initial (wordAt) + +structure Ready (memory : Addr) (lanes q : Nat) (s : State) : Prop where + space : Space s memory (1024 * (lanes * q)) + memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8 + lanesRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 184) 8 + blocksRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 240) 8 + memoryWord : wordAt s memoryOffset = memory + lanesWord : wordAt s VG.Impl.Argon2.X86_64.Initial.lanesOffset = BitVec.ofNat 64 lanes + blocksWord : wordAt s blocksOffset = BitVec.ofNat 64 (lanes * q) + laneLength : s.gpr .r13 = BitVec.ofNat 64 q + +def publicBases : List Reg := [.rbp, .rbx, .rsp, .r13] + +def AgreeBases (s t : State) : Prop := ∀ r ∈ publicBases, s.gpr r = t.gpr r + +theorem clearSetup_rel : RelCT isa AgreeBases clearSetupCode (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs publicBases) + (fun _ _ h => Taint.agree_ofRegs h) (by taint_decide) + +theorem clearLoop_rel : RelCT isa + (fun s t => VG.X86_64.Taint.Agree (Taint.ofRegs (.rax :: .r14 :: publicBases)) s t) + (.loop (.block clearWord) .ne) AgreeBases := by + apply RelCT.taintRegs (τ := Taint.ofRegs (.rax :: .r14 :: publicBases)) + (fun _ _ h => h) publicBases + taint_decide + +theorem clear_rel (memory : Addr) (lanes q : Nat) : + RelCT isa (fun s t => Ready memory lanes q s ∧ Ready memory lanes q t ∧ AgreeBases s t) + clear AgreeBases := by + let P := fun s t => Ready memory lanes q s ∧ Ready memory lanes q t ∧ AgreeBases s t + have prep := (clearSetup_rel.mono (P' := P) (fun _ _ h => h.2.2) + (fun _ _ h => h)).wpDep (fun s t h => + ⟨clearSetup_ok s h.1.memoryRead h.1.blocksRead, + clearSetup_ok t h.2.1.memoryRead h.2.1.blocksRead⟩) + refine prep.seq (clearLoop_rel.mono ?_ (fun _ _ h => h)) + intro a b h + obtain ⟨_, s, t, hp, ha, hb⟩ := h + apply Taint.agree_ofRegs + intro r hr + simp only [List.mem_cons] at hr + rcases hr with rfl | rfl | hr + · rw [ha.count, hb.count, hp.1.blocksWord, hp.2.1.blocksWord] + · rw [ha.destination, hb.destination, hp.1.memoryWord, hp.2.1.memoryWord] + · have excluded : ∀ r ∈ publicBases, r ≠ .r14 ∧ r ≠ .rax ∧ r ≠ .rcx := by decide + have hn := excluded r hr + exact (ha.other r hn.1 hn.2.1 hn.2.2).trans + ((hp.2.2 r hr).trans (hb.other r hn.1 hn.2.1 hn.2.2).symm) + +end VG.Proof.Argon2.X86_64.MemoryInit diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean index 1f02e16b0..592ab2cfa 100644 --- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitClearSetup.lean @@ -33,6 +33,31 @@ theorem clearHeader_ok (s : State) refine ⟨rfl, rfl, rfl, fun r h1 h2 h3 => ?_, rfl, rfl, rfl⟩ simp only [RegUpd.gpr_setReg, h1, h2, h3, ite_false] +structure ClearSetup (s t : State) : Prop where + destination : t.gpr .r14 = wordAt s memoryOffset + count : t.gpr .rax = wordAt s blocksOffset * 128 + zero : t.gpr .rcx = 0 + other : ∀ r, r ≠ .r14 → r ≠ .rax → r ≠ .rcx → t.gpr r = s.gpr r + mem : t.mem = s.mem + rd : t.rd = s.rd + wr : t.wr = s.wr + +theorem clearSetup_ok (s : State) + (memoryRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 232) 8) + (blocksRead : InRegions (s.rd ++ s.wr) (s.gpr .rbp + 240) 8) : + WP isa clearSetupCode s (ClearSetup s) := by + unfold clearSetupCode clearSetup + rw [WP.block_append_iff] + refine (clearHeader_ok s memoryRead blocksRead).mono ?_ + intro a ha + refine (scale_ok a .rax 7).mono ?_ + intro b hb + exact ⟨(hb.other _ (by decide)).trans ha.destination, + by rw [hb.value, ha.count]; rfl, + (hb.other _ (by decide)).trans ha.zero, + fun r h1 h2 h3 => (hb.other r h2).trans (ha.other r h1 h2 h3), + hb.mem.trans ha.mem, hb.rd.trans ha.rd, hb.wr.trans ha.wr⟩ + structure Cleared (s t : State) (memory : Addr) (blocks : Nat) : Prop where destination : t.gpr .r14 = memory + BitVec.ofNat 64 (1024 * blocks) other : ∀ r, r ≠ .r14 → r ≠ .rax → r ≠ .rcx → t.gpr r = s.gpr r @@ -48,22 +73,18 @@ theorem clear_ok (s : State) (memory : Addr) (blocks : Nat) (lo : 1 ≤ blocks) (blocksWord : wordAt s blocksOffset = BitVec.ofNat 64 blocks) (cover : Covers [⟨memory, 1024 * blocks⟩] s.wr) : WP isa clear s fun t => Cleared s t memory blocks := by - unfold clear clearSetup - apply WP.seq - rw [WP.block_append_iff] - refine (clearHeader_ok s memoryRead blocksRead).mono ?_ - intro a ha - refine (scale_ok a .rax 7).mono ?_ + unfold clear + refine WP.seq ((clearSetup_ok s memoryRead blocksRead).mono ?_) intro b hb have count : b.gpr .rax = BitVec.ofNat 64 (128 * blocks) := by - rw [hb.value, ha.count, blocksWord, ← BitVec.ofNat_mul, Nat.mul_comm] - have dst : b.gpr .r14 = memory := (hb.other _ (by decide)).trans (ha.destination.trans memoryWord) - have zero : b.gpr .rcx = 0 := (hb.other _ (by decide)).trans ha.zero - have mem : b.mem = s.mem := hb.mem.trans ha.mem - have rd : b.rd = s.rd := hb.rd.trans ha.rd - have wr : b.wr = s.wr := hb.wr.trans ha.wr - have other : ∀ r, r ≠ .r14 → r ≠ .rax → r ≠ .rcx → b.gpr r = s.gpr r := - fun r h1 h2 h3 => (hb.other r h2).trans (ha.other r h1 h2 h3) + rw [hb.count, blocksWord, show (128 : Addr) = BitVec.ofNat 64 128 from rfl, + ← BitVec.ofNat_mul, Nat.mul_comm] + have dst : b.gpr .r14 = memory := hb.destination.trans memoryWord + have zero := hb.zero + have mem := hb.mem + have rd := hb.rd + have wr := hb.wr + have other := hb.other refine (clearLoop_ok b memory (128 * blocks) (by omega) (by omega) dst count zero ?_).mono ?_ · intro j hj rw [wr] diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLit.lean new file mode 100644 index 000000000..7692b2fd3 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLit.lean @@ -0,0 +1,11 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.MemoryInit +import VerifiedGarbage.Proof.Framework.X86_64.Lit + +/-! # Checked literals for the public dimension setup blocks -/ + +namespace VG + +materialize_code Impl.Argon2.X86_64.MemoryInit.clearSetupCode +materialize_code Impl.Argon2.X86_64.MemoryInit.lanesSetupCode + +end VG diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean index 62f737444..8c10929e8 100644 --- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoop.lean @@ -17,21 +17,14 @@ structure LoopI (s₀ : State) (memory : Addr) (lanes q j : Nat) (h0 : List Byte initialized : Initialized s.mem memory lanes q j h0 hash : bytesAt s.mem (s.gpr .rbp) 64 = h0 -theorem lanesLoop_ok (v : Proof.Blake2.X86_64.Backend) (name : String) - (s₀ : State) (memory : Addr) (lanes q : Nat) (h0 : List Byte) - (space : Space s₀ memory (1024 * (lanes * q))) (lo : 1 ≤ lanes) +theorem lane_step (v : Proof.Blake2.X86_64.Backend) (name : String) + (s₀ s : State) (memory : Addr) (lanes q j : Nat) (h0 : List Byte) + (space : Space s₀ memory (1024 * (lanes * q))) (hj : j < lanes) (lanesBound : lanes < 2 ^ 64) (hq : 2 ≤ q) - (dst : s₀.gpr .r14 = memory) (laneReg : s₀.gpr .r12 = 0) - (remaining : s₀.gpr .r15 = BitVec.ofNat 64 lanes) - (stride : s₀.gpr .r13 = BitVec.ofNat 64 (1024 * q)) - (initialized : Initialized s₀.mem memory lanes q 0 h0) - (hash : bytesAt s₀.mem (s₀.gpr .rbp) 64 = h0) : - WP isa (.loop (lane name (HPrime.hash v)) .ne) s₀ (LoopI s₀ memory lanes q lanes h0) := by - refine WP.loop (M := isa) - (fun n s => ∃ j, n = lanes - j ∧ j < lanes ∧ LoopI s₀ memory lanes q j h0 s) - ?_ lanes s₀ ⟨0, by omega, lo, by omega, by simpa using dst, laneReg, - by simpa only [Nat.sub_zero] using remaining, stride, Keeps.refl _ _ _, initialized, hash⟩ - rintro n s ⟨j, rfl, hj, h⟩ + (h : LoopI s₀ memory lanes q j h0 s) : + WP isa (lane name (HPrime.hash v)) s fun t => + LoopI s₀ memory lanes q (j + 1) h0 t ∧ + t.zf = some (decide (lanes - (j + 1) = 0)) := by have spaceS := space.keeps h.keeps have endBound : 1024 * (j * q) + 2048 ≤ 1024 * (lanes * q) := by have mul := Nat.mul_le_mul_right q (show j + 1 ≤ lanes by omega) @@ -63,6 +56,26 @@ theorem lanesLoop_ok (v : Proof.Blake2.X86_64.Backend) (name : String) simpa only [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega : lanes - (j + 1) < 2 ^ 64), show (0 : Addr).toNat = 0 from rfl] using num · intro eq; rw [eq]; rfl + exact ⟨next, zf⟩ + + +theorem lanesLoop_ok (v : Proof.Blake2.X86_64.Backend) (name : String) + (s₀ : State) (memory : Addr) (lanes q : Nat) (h0 : List Byte) + (space : Space s₀ memory (1024 * (lanes * q))) (lo : 1 ≤ lanes) + (lanesBound : lanes < 2 ^ 64) (hq : 2 ≤ q) + (dst : s₀.gpr .r14 = memory) (laneReg : s₀.gpr .r12 = 0) + (remaining : s₀.gpr .r15 = BitVec.ofNat 64 lanes) + (stride : s₀.gpr .r13 = BitVec.ofNat 64 (1024 * q)) + (initialized : Initialized s₀.mem memory lanes q 0 h0) + (hash : bytesAt s₀.mem (s₀.gpr .rbp) 64 = h0) : + WP isa (.loop (lane name (HPrime.hash v)) .ne) s₀ (LoopI s₀ memory lanes q lanes h0) := by + refine WP.loop (M := isa) + (fun n s => ∃ j, n = lanes - j ∧ j < lanes ∧ LoopI s₀ memory lanes q j h0 s) + ?_ lanes s₀ ⟨0, by omega, lo, by omega, by simpa using dst, laneReg, + by simpa only [Nat.sub_zero] using remaining, stride, Keeps.refl _ _ _, initialized, hash⟩ + rintro n s ⟨j, rfl, hj, h⟩ + refine (lane_step v name s₀ s memory lanes q j h0 space hj lanesBound hq h).mono ?_ + intro t ⟨next, zf⟩ by_cases done : j + 1 = lanes · refine .inl ⟨?_, done ▸ next⟩ simp only [eval, zf, show lanes - (j + 1) = 0 by omega, decide_true, diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoopCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoopCT.lean new file mode 100644 index 000000000..c59fc1ff3 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/MemoryInitLoopCT.lean @@ -0,0 +1,51 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLoop +import VerifiedGarbage.Proof.Argon2.X86_64.MemoryInitLaneCT + +/-! # Both initialization loops count only pubNext matrix dimensions -/ + +namespace VG.Proof.Argon2.X86_64.MemoryInit + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.MemoryInit + +theorem lanesLoop_rel (v : Proof.Blake2.X86_64.Backend) (name : String) + (s₁ s₂ : State) (memory : Addr) (lanes q : Nat) (h₁ h₂ : List Byte) + (space₁ : Space s₁ memory (1024 * (lanes * q))) + (space₂ : Space s₂ memory (1024 * (lanes * q))) + (lo : 1 ≤ lanes) (lanesBound : lanes < 2 ^ 64) (hq : 2 ≤ q) : + RelCT isa (fun s t => LoopI s₁ memory lanes q 0 h₁ s ∧ + LoopI s₂ memory lanes q 0 h₂ t ∧ AgreeSaved s t) + (.loop (lane name (HPrime.hash v)) .ne) AgreeSaved := by + let I := fun n s t => ∃ j, n = lanes - j ∧ j < lanes ∧ + LoopI s₁ memory lanes q j h₁ s ∧ LoopI s₂ memory lanes q j h₂ t ∧ AgreeSaved s t + have steps : ∀ n, RelCT isa (I n) (lane name (HPrime.hash v)) fun a b => + isa.eval .ne a = isa.eval .ne b ∧ + (isa.eval .ne a = some false → AgreeSaved a b) ∧ + (isa.eval .ne a = some true → ∃ m < n, I m a b) := by + intro n s t trace₁ trace₂ a b hp e₁ e₂ + obtain ⟨j, rfl, hj, hs, ht, pub⟩ := hp + have bound : 1024 * (j * q) + 2048 ≤ 1024 * (lanes * q) := by + have mul := Nat.mul_le_mul_right q (show j + 1 ≤ lanes by omega) + rw [Nat.add_mul, Nat.one_mul] at mul + omega + have related : RelatedLane memory (1024 * (lanes * q)) (1024 * (j * q)) s t := + ⟨⟨space₁.keeps hs.keeps, hs.destination⟩, + ⟨space₂.keeps ht.keeps, ht.destination⟩, pub⟩ + obtain ⟨trace, pubNext⟩ := lane_rel v name memory _ _ bound _ _ _ _ _ _ related e₁ e₂ + obtain ⟨_, a', ea, ha⟩ := lane_step v name s₁ s memory lanes q j h₁ + space₁ hj lanesBound hq hs + obtain ⟨_, b', eb, hb⟩ := lane_step v name s₂ t memory lanes q j h₂ + space₂ hj lanesBound hq ht + obtain ⟨-, rfl⟩ := Exec.det e₁ ea + obtain ⟨-, rfl⟩ := Exec.det e₂ eb + refine ⟨trace, ?_, fun _ => pubNext, ?_⟩ + · simp only [eval, ha.2, hb.2] + · intro taken + have remaining : lanes - (j + 1) ≠ 0 := by + intro zero + simp only [eval, ha.2, zero, decide_true, Option.map_some, + Bool.not_true, Option.some.injEq, Bool.false_eq_true] at taken + exact ⟨lanes - (j + 1), by omega, j + 1, rfl, by omega, ha.1, hb.1, pubNext⟩ + exact (RelCT.loop I steps lanes).mono (fun _ _ hp => + ⟨0, by omega, lo, hp.1, hp.2.1, hp.2.2⟩) (fun _ _ h => h) + +end VG.Proof.Argon2.X86_64.MemoryInit From 19d8c62ee16322992dcf9788ea7cd9027127cc1e Mon Sep 17 00:00:00 2001 From: Paul Kehrer Date: Thu, 1 Oct 2026 22:00:53 +0800 Subject: [PATCH 3/7] Argon2 on x86-64: prove reference-index arithmetic (#457) * Argon2 on x86-64: prove reference-window arithmetic * Argon2 on x86-64: prove fixed-time reference-lane selection --------- Co-authored-by: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> --- .../Impl/Argon2/X86_64/ReferenceLane.lean | 19 ++++ .../Impl/Argon2/X86_64/Relative.lean | 19 ++++ .../Impl/Argon2/X86_64/Wrap.lean | 18 ++++ .../Proof/Argon2/Reference.lean | 95 ++++++++++++++++++ .../Proof/Argon2/X86_64/ReferenceLane.lean | 59 ++++++++++++ .../Proof/Argon2/X86_64/Relative.lean | 96 +++++++++++++++++++ .../Proof/Argon2/X86_64/Wrap.lean | 52 ++++++++++ 7 files changed, 358 insertions(+) create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceLane.lean create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/Relative.lean create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/Wrap.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/Reference.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceLane.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/Relative.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/Wrap.lean diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceLane.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceLane.lean new file mode 100644 index 000000000..a220683fd --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceLane.lean @@ -0,0 +1,19 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.Divide + +/-! # Selecting a lane from J₂ with fixed-time division + +`rdi` contains the full address word and `rsi` the positive lane count. +`r8` receives J₂ modulo the lane count; `r11` retains the address word +for the subsequent J₁ mapping. The first slice of pass zero instead uses +the current lane; the enclosing public loop selects that case separately. +-/ + +namespace VG.Impl.Argon2.X86_64.ReferenceLane + +open VG.X86_64 + +def highArgs : List Instr := [.mov .r11 (.reg .rdi), .shift .shr .rdi 32] + +def code : Prog isa := .seq (.block highArgs) Divide.code + +end VG.Impl.Argon2.X86_64.ReferenceLane diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/Relative.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/Relative.lean new file mode 100644 index 000000000..843822504 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/Relative.lean @@ -0,0 +1,19 @@ +import VerifiedGarbage.TCB.X86_64.Isa + +/-! # Argon2's squared mapping into an eligible reference window + +`rdi` contains J₁ in its low half and `rsi` contains the positive window +length. Both products fit in 64 bits for the RFC's 32-bit dimensions. The +code has no branches or memory accesses, including for secret J₁ values. +-/ + +namespace VG.Impl.Argon2.X86_64.Relative + +open VG.X86_64 + +def code : Prog isa := .block [ + .mov32 .rax (.reg .rdi), .mul .rax, .shift .shr .rax 32, + .mul .rsi, .shift .shr .rax 32, .mov .rcx (.reg .rsi), + .alu .sub .rcx (.imm 1), .alu .sub .rcx (.reg .rax), .mov .rax (.reg .rcx)] + +end VG.Impl.Argon2.X86_64.Relative diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/Wrap.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/Wrap.lean new file mode 100644 index 000000000..caefcec13 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/Wrap.lean @@ -0,0 +1,18 @@ +import VerifiedGarbage.TCB.X86_64.Isa + +/-! # Wrap a reference-column sum with one masked subtraction + +`rdi` is the sum and `rsi` the positive lane length. A sum below twice the +lane length needs at most one subtraction; the borrow mask selects the +original sum when it is already in range. No secret controls a branch. +-/ + +namespace VG.Impl.Argon2.X86_64.Wrap + +open VG.X86_64 + +def code : Prog isa := .block [ + .mov .r10 (.reg .rdi), .alu .sub .rdi (.reg .rsi), .alu .sbb .rax (.reg .rax), + .alu .xor .r10 (.reg .rdi), .alu .and .r10 (.reg .rax), .alu .xor .rdi (.reg .r10)] + +end VG.Impl.Argon2.X86_64.Wrap diff --git a/lean/VerifiedGarbage/Proof/Argon2/Reference.lean b/lean/VerifiedGarbage/Proof/Argon2/Reference.lean new file mode 100644 index 000000000..285930a20 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/Reference.lean @@ -0,0 +1,95 @@ +import VerifiedGarbage.Proof.Argon2.Dimensions + +/-! # Bounds for the quadratic reference-window mapping in RFC 9106 §3.4.2 -/ + +namespace VG.Proof.Argon2 + +theorem reference_square_bound (j : Nat) (hj : j < 2 ^ 32) : j * j < 2 ^ 64 := by + exact Nat.lt_of_lt_of_eq (Nat.mul_self_lt_mul_self hj) (by decide) + +theorem reference_scaled_bound (j : Nat) (hj : j < 2 ^ 32) : + j * j / 2 ^ 32 < 2 ^ 32 := by + apply (Nat.div_lt_iff_lt_mul (by decide : 0 < 2 ^ 32)).mpr + exact Nat.lt_of_lt_of_eq (reference_square_bound j hj) (by decide) + +theorem reference_product_bound (count j : Nat) (hc : count < 2 ^ 32) + (hj : j < 2 ^ 32) : count * (j * j / 2 ^ 32) < 2 ^ 64 := by + exact Nat.lt_of_lt_of_eq (Nat.mul_lt_mul_of_lt_of_lt hc (reference_scaled_bound j hj)) + (by decide) + +theorem reference_scale_lt_count (count j : Nat) (hc : 0 < count) (hj : j < 2 ^ 32) : + count * (j * j / 2 ^ 32) / 2 ^ 32 < count := by + apply (Nat.div_lt_iff_lt_mul (by decide : 0 < 2 ^ 32)).mpr + exact Nat.mul_lt_mul_of_pos_left (reference_scaled_bound j hj) hc + +theorem reference_relative_bound (count j : Nat) (hc : 0 < count) : + count - 1 - count * (j * j / 2 ^ 32) / 2 ^ 32 < count := by + omega + +open VG.Spec.Argon2 + +theorem reference_count_lt_lane (p : Params) (hl : 0 < p.lanes) + (hm : 8 * p.lanes ≤ p.memory) (pass slice index : Nat) (same : Bool) + (hs : slice < 4) (hi : index < p.segmentLen) : + referenceCount p pass slice index same < p.laneLen := by + have seg := segmentLen_ge_two p hl hm + have len := laneLen_segments p hl + have column := column_lt p hl hs hi + unfold referenceCount + by_cases first : pass = 0 + · rw [ite_eq_left first] + cases same + · simp only [Bool.false_eq_true, ite_false] + split <;> omega + · simp only [ite_true] + omega + · rw [ite_eq_right first] + cases same + · simp only [Bool.false_eq_true, ite_false] + split <;> omega + · simp only [ite_true] + omega + +theorem reference_count_positive (p : Params) (hl : 0 < p.lanes) + (hm : 8 * p.lanes ≤ p.memory) (pass slice index : Nat) (same : Bool) + (active : pass ≠ 0 ∨ slice ≠ 0 ∨ 2 ≤ index) + (firstLane : pass = 0 → slice = 0 → same = true) : + 0 < referenceCount p pass slice index same := by + have seg := segmentLen_ge_two p hl hm + have len := laneLen_segments p hl + unfold referenceCount + by_cases first : pass = 0 + · rw [ite_eq_left first] + by_cases zero : slice = 0 + · simp only [firstLane first zero, zero, Nat.zero_mul, ite_true] + omega + · have mul := Nat.mul_le_mul_right p.segmentLen (show 1 ≤ slice by omega) + rw [Nat.one_mul] at mul + cases same + · simp only [Bool.false_eq_true, ite_false] + split <;> omega + · simp only [ite_true] + omega + · rw [ite_eq_right first] + cases same + · simp only [Bool.false_eq_true, ite_false] + split <;> omega + · simp only [ite_true] + omega + +theorem reference_count_32 (p : Params) (hl : 0 < p.lanes) + (hm : 8 * p.lanes ≤ p.memory) (memoryBound : p.memory < 2 ^ 32) + (pass slice index : Nat) (same : Bool) (hs : slice < 4) (hi : index < p.segmentLen) : + referenceCount p pass slice index same < 2 ^ 32 := by + have laneBlocks := Nat.le_mul_of_pos_left p.laneLen hl + rw [← blocks_lanes p hl] at laneBlocks + exact Nat.lt_of_lt_of_le (reference_count_lt_lane p hl hm pass slice index same hs hi) + (Nat.le_trans laneBlocks (Nat.le_trans (blocks_le_memory p) (Nat.le_of_lt memoryBound))) + +theorem reference_wrap (sum q : Nat) (bound : sum < 2 * q) : + sum % q = if sum < q then sum else sum - q := by + by_cases small : sum < q + · rw [ite_eq_left small, Nat.mod_eq_of_lt small] + · rw [ite_eq_right small, Nat.mod_eq_sub_mod (by omega), Nat.mod_eq_of_lt (by omega)] + +end VG.Proof.Argon2 diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceLane.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceLane.lean new file mode 100644 index 000000000..6ff64dbbb --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceLane.lean @@ -0,0 +1,59 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceLane +import VerifiedGarbage.Proof.Argon2.X86_64.Divide +import VerifiedGarbage.Proof.Argon2.X86_64.DivideCT + +/-! # Secret J₂ does not affect the lane-selection trace -/ + +namespace VG.Proof.Argon2.X86_64.ReferenceLane + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceLane + +structure Prefix (s t : State) : Prop where + high : t.gpr .rdi = s.gpr .rdi >>> 32 + original : t.gpr .r11 = s.gpr .rdi + keeps : Divide.Keeps [.rdi, .r11] s t + +theorem highArgs_ok (s : State) : WP isa (.block highArgs) s (Prefix s) := by + apply WP.of_runBlock + simp only [highArgs, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + execShift, RegUpd.gpr_setReg, + show 1 ≤ (32 : Nat) ∧ (32 : Nat) ≤ 63 from by decide, + and_self, ite_true, ite_false, reduceCtorEq, + Option.map_some, Option.some.injEq, exists_eq_left'] + refine ⟨rfl, rfl, ?_⟩ + 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_setFlags, hr.1, hr.2, ite_false] + all_goals rfl + +def changed : List Reg := [.rdi, .r11] ++ Divide.changed + +theorem code_ok (s : State) (lo : 0 < (s.gpr .rsi).toNat) + (bound : (s.gpr .rsi).toNat < 2 ^ 32) : + WP isa code s fun t => + (t.gpr .r8).toNat = (s.gpr .rdi >>> 32).toNat % (s.gpr .rsi).toNat ∧ + t.gpr .r11 = s.gpr .rdi ∧ Divide.Keeps changed s t := by + unfold code + refine WP.seq ((highArgs_ok s).mono ?_) + intro a ha + have si := ha.keeps.regs .rsi (by decide) + refine (Divide.code_ok a ?_ (by rw [si]; exact lo) (by rw [si]; exact bound)).mono ?_ + · rw [ha.high] + simpa only [show 64 - 32 = (32 : Nat) from rfl] using + BitVec.toNat_ushiftRight_lt (s.gpr .rdi) 32 (by decide) + · intro t ht + refine ⟨?_, ?_, (ha.keeps.mono ?_).trans (ht.2.2.mono ?_)⟩ + · rw [ht.2.1, ha.high, si] + · exact (ht.2.2.regs .r11 (by decide)).trans ha.original + · intro r hr; exact List.mem_append_left _ hr + · intro r hr; exact List.mem_append_right _ hr + +theorem highArgs_secret_rel : RelCT isa (fun _ _ => True) (.block highArgs) (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs []) + (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide) + +theorem code_secret_rel : RelCT isa (fun _ _ => True) code (fun _ _ => True) := + highArgs_secret_rel.seq Divide.code_secret_rel + +end VG.Proof.Argon2.X86_64.ReferenceLane diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/Relative.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/Relative.lean new file mode 100644 index 000000000..e34edf4de --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/Relative.lean @@ -0,0 +1,96 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.Relative +import VerifiedGarbage.Proof.Argon2.Reference +import VerifiedGarbage.Proof.Argon2.X86_64.Mix +import VerifiedGarbage.Proof.Framework.X86_64.RelCT + +/-! # The baseline reference-window mapping is fixed time and preserves memory -/ + +namespace VG.Proof.Argon2.X86_64.Relative + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.Relative + +def value (random count : Addr) : Addr := + let j := random &&& 0xffffffff + let x := (j * j) >>> 32 + let y := (x * count) >>> 32 + count - 1 - y + +theorem code_ok (s : State) : WP isa code s fun t => + t.gpr .rax = value (s.gpr .rdi) (s.gpr .rsi) ∧ + (∀ r, r ≠ .rax → r ≠ .rdx → r ≠ .rcx → t.gpr r = s.gpr r) ∧ + t.mem = s.mem ∧ t.rd = s.rd ∧ t.wr = s.wr := by + unfold code + apply WP.of_runBlock + simp only [runBlock_cons, runStep_some, runBlock_nil, exec, + readSrc32, readSrc, State.setReg32, execMul, execAlu, execShift, + RegUpd.gpr_setReg, RegUpd.mem_setReg, RegUpd.rd_setReg, RegUpd.wr_setReg, + RegUpd.gpr_setFlags, RegUpd.mem_setFlags, RegUpd.rd_setFlags, RegUpd.wr_setFlags, + RegUpd.gpr_arithFlags, RegUpd.mem_arithFlags, RegUpd.rd_arithFlags, + RegUpd.wr_arithFlags, reduceCtorEq, and_self, ite_true, ite_false, + show 1 ≤ (32 : Nat) ∧ (32 : Nat) ≤ 63 from by decide, + Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left', + BitVec.ofNat_mul, BitVec.ofNat_toNat, BitVec.setWidth_eq, + show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl] + refine ⟨?_, ?_, trivial⟩ + · rw [VG.Proof.Argon2.X86_64.low32]; rfl + · intro r h1 h2 h3 + simp only [h1, h2, h3, ite_false] + +theorem mul_shift_toNat (x y : Addr) (bound : x.toNat * y.toNat < 2 ^ 64) : + ((x * y) >>> 32).toNat = x.toNat * y.toNat / 2 ^ 32 := by + rw [BitVec.toNat_ushiftRight, Nat.shiftRight_eq_div_pow, BitVec.toNat_mul, + Nat.mod_eq_of_lt bound] + +theorem value_nat (random count : Addr) (lo : 0 < count.toNat) + (bound : count.toNat < 2 ^ 32) : + value random count = BitVec.ofNat 64 + (count.toNat - 1 - count.toNat * ((random &&& 0xffffffff).toNat * + (random &&& 0xffffffff).toNat / 2 ^ 32) / 2 ^ 32) := by + let j := random &&& 0xffffffff + have hj : j.toNat < 2 ^ 32 := by + have h32 := (random.setWidth 32).isLt + rw [show j = (random.setWidth 32).setWidth 64 from (low32 random).symm, + BitVec.toNat_setWidth, Nat.mod_eq_of_lt (by omega)] + exact h32 + have hx := mul_shift_toNat j j (Proof.Argon2.reference_square_bound _ hj) + have product : ((j * j) >>> 32).toNat * count.toNat < 2 ^ 64 := by + rw [hx, Nat.mul_comm] + exact Proof.Argon2.reference_product_bound _ _ bound hj + have hy := mul_shift_toNat ((j * j) >>> 32) count product + rw [hx, Nat.mul_comm] at hy + have hyBound : count.toNat * (j.toNat * j.toNat / 2 ^ 32) / 2 ^ 32 < count.toNat := + Proof.Argon2.reference_scale_lt_count _ _ lo hj + have hyWord : (((j * j) >>> 32) * count) >>> 32 = BitVec.ofNat 64 + (count.toNat * (j.toNat * j.toNat / 2 ^ 32) / 2 ^ 32) := by + apply BitVec.eq_of_toNat_eq + rw [hy, BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)] + unfold value + change count - 1 - ((((j * j) >>> 32) * count) >>> 32) = _ + rw [hyWord] + change count - (1 : Addr) - BitVec.ofNat 64 + (count.toNat * (j.toNat * j.toNat / 2 ^ 32) / 2 ^ 32) = _ + have countWord : count = BitVec.ofNat 64 count.toNat := by + exact (BitVec.ofNat_toNat 64 count).symm + have countSub : count - 1 = BitVec.ofNat 64 (count.toNat - 1) := by + calc + count - 1 = BitVec.ofNat 64 count.toNat - BitVec.ofNat 64 1 := + congrArg (fun x : Addr => x - 1) countWord + _ = _ := Offset.ofNat_sub_ofNat (by omega) + rw [countSub, Offset.ofNat_sub_ofNat (by omega)] + +theorem code_nat_ok (s : State) (lo : 0 < (s.gpr .rsi).toNat) + (bound : (s.gpr .rsi).toNat < 2 ^ 32) : + WP isa code s fun t => + t.gpr .rax = BitVec.ofNat 64 + ((s.gpr .rsi).toNat - 1 - (s.gpr .rsi).toNat * + ((s.gpr .rdi &&& 0xffffffff).toNat * (s.gpr .rdi &&& 0xffffffff).toNat / 2 ^ 32) / + 2 ^ 32) ∧ + (∀ r, r ≠ .rax → r ≠ .rdx → r ≠ .rcx → t.gpr r = s.gpr r) ∧ + t.mem = s.mem ∧ t.rd = s.rd ∧ t.wr = s.wr := + (code_ok s).mono (fun _ h => ⟨h.1.trans (value_nat _ _ lo bound), h.2⟩) + +theorem code_secret_rel : RelCT isa (fun _ _ => True) code (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs []) + (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide) + +end VG.Proof.Argon2.X86_64.Relative diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/Wrap.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/Wrap.lean new file mode 100644 index 000000000..9eb7f2f13 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/Wrap.lean @@ -0,0 +1,52 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.Wrap +import VerifiedGarbage.Proof.Argon2.Reference +import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep +import VerifiedGarbage.Proof.Framework.X86_64.RelCT + +/-! # Masked subtraction agrees with wrapping the reference column -/ + +namespace VG.Proof.Argon2.X86_64.Wrap + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.Wrap + +theorem code_ok (s : State) : WP isa code s fun t => + t.gpr .rdi = (if (s.gpr .rdi).toNat < (s.gpr .rsi).toNat + then s.gpr .rdi else s.gpr .rdi - s.gpr .rsi) ∧ + Divide.Keeps [.rdi, .r10, .rax] s t := by + unfold code + apply WP.of_runBlock + simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu, + RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, RegUpd.cf_setReg, RegUpd.cf_arithFlags, + reduceCtorEq, ite_true, ite_false, Option.map_some, Option.bind_some, Option.some.injEq, + exists_eq_left', Divide.sbb_mask, Divide.select_value, decide_eq_true_eq] + refine ⟨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 + +theorem wrap_nat (x q : Addr) (bound : x.toNat < 2 * q.toNat) : + (if x.toNat < q.toNat then x else x - q) = BitVec.ofNat 64 (x.toNat % q.toNat) := by + rw [Proof.Argon2.reference_wrap _ _ bound] + by_cases small : x.toNat < q.toNat + · rw [ite_eq_left small, ite_eq_left small] + exact (BitVec.ofNat_toNat 64 x).symm + · rw [ite_eq_right small, ite_eq_right small] + calc + x - q = BitVec.ofNat 64 x.toNat - BitVec.ofNat 64 q.toNat := by + simp only [BitVec.ofNat_toNat, BitVec.setWidth_eq] + _ = _ := Offset.ofNat_sub_ofNat (by omega) + +theorem code_nat_ok (s : State) (bound : (s.gpr .rdi).toNat < 2 * (s.gpr .rsi).toNat) : + WP isa code s fun t => + t.gpr .rdi = BitVec.ofNat 64 ((s.gpr .rdi).toNat % (s.gpr .rsi).toNat) ∧ + Divide.Keeps [.rdi, .r10, .rax] s t := + (code_ok s).mono (fun _ h => ⟨h.1.trans (wrap_nat _ _ bound), h.2⟩) + +theorem code_secret_rel : RelCT isa (fun _ _ => True) code (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs []) + (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide) + +end VG.Proof.Argon2.X86_64.Wrap From 649d26f92431b8722c518815f564fcbb3fa401fe Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:34:43 +0000 Subject: [PATCH 4/7] Prove Argon2 reference-window candidate arithmetic and selection --- .../Impl/Argon2/X86_64/CountCandidates.lean | 31 +++++ .../Impl/Argon2/X86_64/ReferenceCount.lean | 16 +++ .../Impl/Argon2/X86_64/SelectWindow.lean | 20 +++ .../Proof/Argon2/X86_64/CountCandidates.lean | 123 ++++++++++++++++++ .../Argon2/X86_64/CountCandidatesCT.lean | 19 +++ .../Argon2/X86_64/CountCandidatesLit.lean | 10 ++ .../Proof/Argon2/X86_64/ReferenceCount.lean | 29 +++++ .../Proof/Argon2/X86_64/SelectWindow.lean | 45 +++++++ 8 files changed, 293 insertions(+) create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/CountCandidates.lean create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceCount.lean create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/SelectWindow.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidates.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesLit.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/SelectWindow.lean diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/CountCandidates.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/CountCandidates.lean new file mode 100644 index 000000000..3af55582c --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/CountCandidates.lean @@ -0,0 +1,31 @@ +import VerifiedGarbage.TCB.X86_64.Isa + +/-! # The two eligible reference windows + +`r9` is the pass, `r12` the lane length, `r13` the segment length, `r14` +the slice and `r15` the index within the segment. `rdx` receives the count +for the current lane; `rcx` receives the count for another lane. Only the +public pass controls a branch. The zero-index adjustment uses a borrow mask. +-/ + +namespace VG.Impl.Argon2.X86_64.CountCandidates + +open VG.X86_64 + +def first : List Instr := [ + .mov .rax (.reg .r13), .mul .r14, .mov .rcx (.reg .rax), .mov .rdx (.reg .rax), + .alu .add .rdx (.reg .r15), .alu .sub .rdx (.imm 1)] + +def later : List Instr := [ + .mov .rax (.reg .r12), .alu .sub .rax (.reg .r13), .mov .rcx (.reg .rax), + .mov .rdx (.reg .rax), .alu .add .rdx (.reg .r15), .alu .sub .rdx (.imm 1)] + +def adjust : List Instr := [ + .mov .r8 (.reg .r15), .alu .sub .r8 (.imm 1), .alu .sbb .r9 (.reg .r9), + .alu .add .rcx (.reg .r9)] + +def code : Prog isa := + .seq (.block [.alu .cmp .r9 (.imm 0)]) + (.seq (.ite .e (.block first) (.block later)) (.block adjust)) + +end VG.Impl.Argon2.X86_64.CountCandidates diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceCount.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceCount.lean new file mode 100644 index 000000000..4ee9b2b2b --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceCount.lean @@ -0,0 +1,16 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.CountCandidates +import VerifiedGarbage.Impl.Argon2.X86_64.SelectWindow + +/-! Compute both reference windows and select one without a secret branch. + +`rdi` and `rsi` are the reference and current lanes. The pass and segment +position use CountCandidates' registers. `r8` receives the selected count. +-/ + +namespace VG.Impl.Argon2.X86_64.ReferenceCount + +open VG VG.X86_64 + +def code : Prog isa := .seq CountCandidates.code SelectWindow.code + +end VG.Impl.Argon2.X86_64.ReferenceCount diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/SelectWindow.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/SelectWindow.lean new file mode 100644 index 000000000..16dd37e30 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/SelectWindow.lean @@ -0,0 +1,20 @@ +import VerifiedGarbage.TCB.X86_64.Isa + +/-! # Select the eligible window without branching on the reference lane + +`rdi,rsi` are the reference and current lanes; `rdx,rcx` hold the same-lane +and cross-lane window lengths. `r8` receives the selected length. Subtracting +one from the lanes' XOR borrows exactly when the lanes match, supplying the +mask for the selection. The counts may be secret too. +-/ + +namespace VG.Impl.Argon2.X86_64.SelectWindow + +open VG.X86_64 + +def code : Prog isa := .block [ + .mov .rax (.reg .rdi), .alu .xor .rax (.reg .rsi), .alu .sub .rax (.imm 1), + .alu .sbb .rax (.reg .rax), .mov .r8 (.reg .rcx), .alu .xor .rdx (.reg .rcx), + .alu .and .rdx (.reg .rax), .alu .xor .r8 (.reg .rdx)] + +end VG.Impl.Argon2.X86_64.SelectWindow diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidates.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidates.lean new file mode 100644 index 000000000..5a8281c4b --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidates.lean @@ -0,0 +1,123 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.CountCandidates +import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep + +/-! # Candidate window arithmetic before selecting the reference lane -/ + +namespace VG.Proof.Argon2.X86_64.CountCandidates + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.CountCandidates + +structure Candidates (s t : State) (base : Addr) : Prop where + same : t.gpr .rdx = base + s.gpr .r15 - 1 + other : t.gpr .rcx = base + keeps : Divide.Keeps [.rax, .rdx, .rcx] s t + +theorem first_ok (s : State) : WP isa (.block first) s + (Candidates s · (s.gpr .r13 * s.gpr .r14)) := by + apply WP.of_runBlock + simp only [first, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + execMul, execAlu, RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags, + reduceCtorEq, ite_true, ite_false, Option.map_some, Option.bind_some, + Option.some.injEq, exists_eq_left', BitVec.ofNat_mul, BitVec.ofNat_toNat, BitVec.setWidth_eq, + show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl] + refine ⟨rfl, rfl, ?_⟩ + 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_setFlags, RegUpd.gpr_arithFlags, + hr.1, hr.2.1, hr.2.2, ite_false] + all_goals rfl + +theorem later_ok (s : State) : WP isa (.block later) s + (Candidates s · (s.gpr .r12 - s.gpr .r13)) := by + apply WP.of_runBlock + simp only [later, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + 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 (1 : BitVec 32) = (1 : Addr) from rfl] + refine ⟨rfl, rfl, ?_⟩ + 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 + +structure Adjusted (s t : State) : Prop where + count : t.gpr .rcx = s.gpr .rcx + Divide.mask (decide ((s.gpr .r15).toNat < 1)) + keeps : Divide.Keeps [.r8, .r9, .rcx] s t + +theorem adjust_ok (s : State) : WP isa (.block adjust) s (Adjusted s) := by + apply WP.of_runBlock + simp only [adjust, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + execAlu, RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, RegUpd.cf_setReg, RegUpd.cf_arithFlags, + reduceCtorEq, ite_true, ite_false, Option.map_some, Option.bind_some, + Option.some.injEq, exists_eq_left', Divide.sbb_mask, + show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl, + show (1 : Addr).toNat = 1 from rfl] + refine ⟨rfl, ?_⟩ + 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 + +theorem compare_ok (s : State) : WP isa (.block [.alu .cmp .r9 (.imm 0)]) s + fun t => t.zf = decide (s.gpr .r9 = 0) ∧ Divide.Keeps [] s t := by + apply WP.of_runBlock + simp only [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 .r9 - (0 : Addr) == (0 : Addr)) = decide (s.gpr .r9 = 0) + apply Bool.eq_iff_iff.mpr + simp only [beq_iff_eq, decide_eq_true_eq] + change s.gpr .r9 - 0#64 = 0#64 ↔ s.gpr .r9 = 0#64 + rw [BitVec.sub_zero] + constructor + · intro r _; exact congrFun (RegUpd.gpr_arithFlags _ _ _ _) r + all_goals rfl + +def base (s : State) : Addr := + if s.gpr .r9 = 0 then s.gpr .r13 * s.gpr .r14 else s.gpr .r12 - s.gpr .r13 + +def changed : List Reg := [.rax, .rdx, .rcx, .r8, .r9] + +theorem code_ok (s : State) : WP isa code s fun t => + t.gpr .rdx = base s + s.gpr .r15 - 1 ∧ + t.gpr .rcx = base s + Divide.mask (decide ((s.gpr .r15).toNat < 1)) ∧ + Divide.Keeps changed s t := by + unfold code + refine WP.seq ((compare_ok s).mono ?_) + rintro a ⟨flag, keeps⟩ + have branches : WP isa (.ite .e (.block first) (.block later)) a + (Candidates s · (base s)) := by + refine WP.ite (decide (s.gpr .r9 = 0)) (by simp only [eval, flag]) ?_ ?_ + · intro h + have zero : s.gpr .r9 = 0 := of_decide_eq_true h + refine (first_ok a).mono ?_ + intro b hb + refine ⟨?_, ?_, keeps.mono (by simp) |>.trans hb.keeps⟩ + · simpa only [base, zero, ite_true, keeps.regs .r13 (by simp), + keeps.regs .r14 (by simp), keeps.regs .r15 (by simp)] using hb.same + · simpa only [base, zero, ite_true, keeps.regs .r13 (by simp), + keeps.regs .r14 (by simp)] using hb.other + · intro h + have nonzero : s.gpr .r9 ≠ 0 := of_decide_eq_false h + refine (later_ok a).mono ?_ + intro b hb + refine ⟨?_, ?_, keeps.mono (by simp) |>.trans hb.keeps⟩ + · simpa only [base, nonzero, ite_false, keeps.regs .r12 (by simp), + keeps.regs .r13 (by simp), keeps.regs .r15 (by simp)] using hb.same + · simpa only [base, nonzero, ite_false, keeps.regs .r12 (by simp), + keeps.regs .r13 (by simp)] using hb.other + refine WP.seq (branches.mono ?_) + intro b hb + refine (adjust_ok b).mono ?_ + intro t ht + refine ⟨?_, ?_, (hb.keeps.mono (by decide)).trans (ht.keeps.mono (by decide))⟩ + · exact (ht.keeps.regs .rdx (by decide)).trans hb.same + · rw [ht.count, hb.other, hb.keeps.regs .r15 (by decide)] + +end VG.Proof.Argon2.X86_64.CountCandidates diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesCT.lean new file mode 100644 index 000000000..744d373c2 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesCT.lean @@ -0,0 +1,19 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidatesLit +import VerifiedGarbage.Proof.Framework.X86_64.RelCT + +/-! Only the public pass affects reference-window arithmetic's trace. -/ + +namespace VG.Proof.Argon2.X86_64.CountCandidates + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.CountCandidates + +theorem code_rel : RelCT isa (fun s t => s.gpr .r9 = t.gpr .r9) code + (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs [.r9]) + (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) + +end VG.Proof.Argon2.X86_64.CountCandidates diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesLit.lean new file mode 100644 index 000000000..cec06bda1 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/CountCandidatesLit.lean @@ -0,0 +1,10 @@ +import VerifiedGarbage.Proof.Framework.X86_64.Lit +import VerifiedGarbage.Impl.Argon2.X86_64.CountCandidates + +/-! A checked literal for reference-window candidate arithmetic. -/ + +namespace VG + +materialize_code Impl.Argon2.X86_64.CountCandidates.code + +end VG diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean new file mode 100644 index 000000000..d9c488b63 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean @@ -0,0 +1,29 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceCount +import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidates +import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidatesCT +import VerifiedGarbage.Proof.Argon2.X86_64.SelectWindow + +/-! The selected reference window, with public pass control only. -/ + +namespace VG.Proof.Argon2.X86_64.ReferenceCount + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceCount + +theorem code_ok (s : State) : WP isa code s fun t => + t.gpr .r8 = (if s.gpr .rdi = s.gpr .rsi then + CountCandidates.base s + s.gpr .r15 - 1 else + CountCandidates.base s + Divide.mask (decide ((s.gpr .r15).toNat < 1))) ∧ + Divide.Keeps CountCandidates.changed s t := by + unfold code + refine WP.seq ((CountCandidates.code_ok s).mono ?_) + rintro a ⟨same, other, keeps⟩ + refine (SelectWindow.code_ok a).mono ?_ + rintro t ⟨out, tail⟩ + refine ⟨?_, keeps.trans (tail.mono (by decide))⟩ + rw [out, keeps.regs .rdi (by decide), keeps.regs .rsi (by decide), same, other] + +theorem code_rel : RelCT isa (fun s t => s.gpr .r9 = t.gpr .r9) code + (fun _ _ => True) := + CountCandidates.code_rel.seq SelectWindow.code_secret_rel + +end VG.Proof.Argon2.X86_64.ReferenceCount diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/SelectWindow.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SelectWindow.lean new file mode 100644 index 000000000..638144898 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/SelectWindow.lean @@ -0,0 +1,45 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.SelectWindow +import VerifiedGarbage.Proof.Argon2.X86_64.DivideStep +import VerifiedGarbage.Proof.Framework.X86_64.RelCT + +/-! # Same-lane window selection with no leakage from the equality test -/ + +namespace VG.Proof.Argon2.X86_64.SelectWindow + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.SelectWindow + +theorem equality_test (x y : Addr) : (x ^^^ y).toNat < 1 ↔ x = y := by + constructor + · intro h + have zero : x ^^^ y = 0 := by + apply BitVec.eq_of_toNat_eq + change (x ^^^ y).toNat = 0 + omega + exact BitVec.xor_eq_zero_iff.mp zero + · intro h + rw [h, BitVec.xor_self] + decide + +theorem code_ok (s : State) : WP isa code s fun t => + t.gpr .r8 = (if s.gpr .rdi = s.gpr .rsi then s.gpr .rdx else s.gpr .rcx) ∧ + Divide.Keeps [.rax, .r8, .rdx] s t := by + unfold code + apply WP.of_runBlock + simp only [runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, execAlu, + RegUpd.gpr_setReg, RegUpd.gpr_arithFlags, RegUpd.cf_setReg, RegUpd.cf_arithFlags, + reduceCtorEq, ite_true, ite_false, Option.map_some, Option.bind_some, + Option.some.injEq, exists_eq_left', + show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl, + show (1 : Addr).toNat = 1 from rfl, equality_test, Divide.sbb_mask, Divide.select_value, decide_eq_true_eq] + refine ⟨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 + +theorem code_secret_rel : RelCT isa (fun _ _ => True) code (fun _ _ => True) := + RelCT.taint (A := taint) (Taint.ofRegs []) + (fun _ _ _ => Taint.agree_ofRegs (by simp)) (by taint_decide) + +end VG.Proof.Argon2.X86_64.SelectWindow From 7237d273a27edb0546948282389df9ac7bf42f05 Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:36:21 +0000 Subject: [PATCH 5/7] Relate reference-window word arithmetic to natural counts --- .../Proof/Argon2/X86_64/ReferenceCount.lean | 24 +++++++++++++++++++ 1 file changed, 24 insertions(+) diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean index d9c488b63..0b55e368f 100644 --- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean @@ -1,4 +1,6 @@ import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceCount +import VerifiedGarbage.Proof.Argon2.Reference +import VerifiedGarbage.Proof.Framework.Offset import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidates import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidatesCT import VerifiedGarbage.Proof.Argon2.X86_64.SelectWindow @@ -22,6 +24,28 @@ theorem code_ok (s : State) : WP isa code s fun t => refine ⟨?_, keeps.trans (tail.mono (by decide))⟩ rw [out, keeps.regs .rdi (by decide), keeps.regs .rsi (by decide), same, other] +theorem same_word (b i : Nat) (positive : 0 < b + i) : + BitVec.ofNat 64 b + BitVec.ofNat 64 i - (1 : Addr) = + BitVec.ofNat 64 (b + i - 1) := by + rw [← BitVec.ofNat_add] + change BitVec.ofNat 64 (b + i) - BitVec.ofNat 64 1 = _ + exact Offset.ofNat_sub_ofNat (by omega) + +theorem other_word (b i : Nat) (bound : i < 2 ^ 64) (positive : i = 0 → 0 < b) : + BitVec.ofNat 64 b + Divide.mask (decide ((BitVec.ofNat 64 i).toNat < 1)) = + BitVec.ofNat 64 (b - (if i = 0 then 1 else 0)) := by + rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt bound] + by_cases zero : i = 0 + · simp only [zero, show decide ((0 : Nat) < 1) = true from rfl, Divide.mask, ite_true] + rw [BitVec.add_neg_eq_sub] + change BitVec.ofNat 64 b - BitVec.ofNat 64 1 = _ + exact Offset.ofNat_sub_ofNat (by have := positive zero; omega) + · have notSmall : ¬i < 1 := by omega + simp only [notSmall, decide_false, Divide.mask, Bool.false_eq_true, ite_false, + zero, Nat.sub_zero] + change BitVec.ofNat 64 b + 0#64 = BitVec.ofNat 64 b + rw [BitVec.add_zero] + theorem code_rel : RelCT isa (fun s t => s.gpr .r9 = t.gpr .r9) code (fun _ _ => True) := CountCandidates.code_rel.seq SelectWindow.code_secret_rel From d8d241588c4c043959edc5f79db5df6fe5cd1def Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 13:43:16 +0000 Subject: [PATCH 6/7] Prove reference-window selection matches the reviewed count specification --- .../Proof/Argon2/X86_64/ReferenceCount.lean | 64 +++++++++++++++++++ 1 file changed, 64 insertions(+) diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean index 0b55e368f..054a1e4ad 100644 --- a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceCount.lean @@ -46,6 +46,70 @@ theorem other_word (b i : Nat) (bound : i < 2 ^ 64) (positive : i = 0 → 0 < b) change BitVec.ofNat 64 b + 0#64 = BitVec.ofNat 64 b rw [BitVec.add_zero] +theorem selected_word (b i : Nat) (same : Bool) (bound : i < 2 ^ 64) + (positive : 0 < b + i) (atZero : i = 0 → 0 < b) : + (if same then BitVec.ofNat 64 b + BitVec.ofNat 64 i - (1 : Addr) else + BitVec.ofNat 64 b + Divide.mask (decide ((BitVec.ofNat 64 i).toNat < 1))) = + BitVec.ofNat 64 (if same then b + i - 1 else b - (if i = 0 then 1 else 0)) := by + cases same + · exact other_word b i bound atZero + · exact same_word b i positive + +theorem spec_count (p : Spec.Argon2.Params) (pass slice index : Nat) (same : Bool) : + Spec.Argon2.referenceCount p pass slice index same = + let b := if pass = 0 then slice * p.segmentLen else p.laneLen - p.segmentLen + if same then b + index - 1 else b - (if index = 0 then 1 else 0) := by + unfold Spec.Argon2.referenceCount + by_cases firstPass : pass = 0 <;> cases same <;> + simp only [firstPass, ite_true, ite_false, Bool.false_eq_true] + +def windowBase (p : Spec.Argon2.Params) (pass slice : Nat) : Nat := + if pass = 0 then slice * p.segmentLen else p.laneLen - p.segmentLen + +theorem base_nat (s : State) (p : Spec.Argon2.Params) (pass slice : Nat) + (passReg : (s.gpr .r9).toNat = pass) + (laneReg : s.gpr .r12 = BitVec.ofNat 64 p.laneLen) + (segmentReg : s.gpr .r13 = BitVec.ofNat 64 p.segmentLen) + (sliceReg : s.gpr .r14 = BitVec.ofNat 64 slice) + (segmentBound : p.segmentLen ≤ p.laneLen) : + CountCandidates.base s = BitVec.ofNat 64 (windowBase p pass slice) := by + have isZero : s.gpr .r9 = 0 ↔ pass = 0 := by + rw [← passReg] + constructor + · intro h; rw [h]; rfl + · intro h + apply BitVec.eq_of_toNat_eq + exact h + unfold CountCandidates.base windowBase + by_cases firstPass : pass = 0 + · simp only [isZero, firstPass, ite_true] + rw [segmentReg, sliceReg, ← BitVec.ofNat_mul, Nat.mul_comm] + · simp only [isZero, firstPass, ite_false] + rw [laneReg, segmentReg] + exact Offset.ofNat_sub_ofNat segmentBound + +theorem code_nat_ok (s : State) (p : Spec.Argon2.Params) (pass slice index : Nat) + (passReg : (s.gpr .r9).toNat = pass) + (laneReg : s.gpr .r12 = BitVec.ofNat 64 p.laneLen) + (segmentReg : s.gpr .r13 = BitVec.ofNat 64 p.segmentLen) + (sliceReg : s.gpr .r14 = BitVec.ofNat 64 slice) + (indexReg : s.gpr .r15 = BitVec.ofNat 64 index) + (segmentBound : p.segmentLen ≤ p.laneLen) (indexBound : index < 2 ^ 64) + (positive : 0 < windowBase p pass slice + index) + (atZero : index = 0 → 0 < windowBase p pass slice) : + WP isa code s fun t => + t.gpr .r8 = BitVec.ofNat 64 (Spec.Argon2.referenceCount p pass slice index + (decide (s.gpr .rdi = s.gpr .rsi))) ∧ + Divide.Keeps CountCandidates.changed s t := by + refine (code_ok s).mono ?_ + rintro t ⟨out, keeps⟩ + refine ⟨out.trans ?_, keeps⟩ + rw [base_nat s p pass slice passReg laneReg segmentReg sliceReg segmentBound, indexReg, + spec_count] + simpa only [decide_eq_true_eq, windowBase] using + selected_word (windowBase p pass slice) index + (decide (s.gpr .rdi = s.gpr .rsi)) indexBound positive atZero + theorem code_rel : RelCT isa (fun s t => s.gpr .r9 = t.gpr .r9) code (fun _ _ => True) := CountCandidates.code_rel.seq SelectWindow.code_secret_rel From 48078556e78668fe741d3414c5c32216e81b176e Mon Sep 17 00:00:00 2001 From: Paul Kehrer <161495+reaperhulk@users.noreply.github.com> Date: Thu, 1 Oct 2026 14:00:12 +0000 Subject: [PATCH 7/7] Prove the fixed-time Argon2 reference-window start --- .../Impl/Argon2/X86_64/ReferenceStart.lean | 25 +++ .../Proof/Argon2/X86_64/ReferenceStart.lean | 151 ++++++++++++++++++ .../Proof/Argon2/X86_64/ReferenceStartCT.lean | 20 +++ .../Argon2/X86_64/ReferenceStartLit.lean | 10 ++ 4 files changed, 206 insertions(+) create mode 100644 lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceStart.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStart.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartCT.lean create mode 100644 lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartLit.lean diff --git a/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceStart.lean b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceStart.lean new file mode 100644 index 000000000..27e5303b7 --- /dev/null +++ b/lean/VerifiedGarbage/Impl/Argon2/X86_64/ReferenceStart.lean @@ -0,0 +1,25 @@ +import VerifiedGarbage.TCB.X86_64.Isa + +/-! Start of the chronological reference window. + +The public pass, slice and segment length are in `r9`, `r14` and `r13`. +`r10` receives zero on pass zero or the last slice, otherwise the column +at the beginning of the next slice. No division is needed. +-/ + +namespace VG.Impl.Argon2.X86_64.ReferenceStart + +open VG.X86_64 + +def zero : List Instr := [.mov .r10 (.imm 0)] + +def advance : List Instr := [ + .mov .rax (.reg .r14), .alu .add .rax (.imm 1), .mul .r13, + .mov .r10 (.reg .rax), .alu .cmp .r14 (.imm 3)] + +def code : Prog isa := + .seq (.block [.alu .cmp .r9 (.imm 0)]) + (.ite .e (.block zero) + (.seq (.block advance) (.ite .e (.block zero) (.block [])))) + +end VG.Impl.Argon2.X86_64.ReferenceStart diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStart.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStart.lean new file mode 100644 index 000000000..ce5b6f7b8 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStart.lean @@ -0,0 +1,151 @@ +import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceStart +import VerifiedGarbage.Proof.Argon2.Dimensions +import VerifiedGarbage.Proof.Argon2.X86_64.CountCandidates + +/-! The reference window starts at the next slice on later passes. -/ + +namespace VG.Proof.Argon2.X86_64.ReferenceStart + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceStart + +theorem sub_zero_iff (x y : Addr) : x - y = 0 ↔ x = y := by + constructor + · intro h + calc + x = (x - y) + y := (BitVec.sub_add_cancel x y).symm + _ = y := by rw [h]; exact BitVec.zero_add y + · intro h; rw [h, BitVec.sub_self]; rfl + +theorem zero_ok (s : State) : WP isa (.block zero) s fun t => + t.gpr .r10 = 0 ∧ Divide.Keeps [.r10] s t := by + apply WP.of_runBlock + simp only [zero, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + RegUpd.gpr_setReg, Option.map_some, Option.some.injEq, exists_eq_left', + ite_true, show BitVec.signExtend 64 (0 : BitVec 32) = (0 : Addr) from rfl] + refine ⟨trivial, ?_⟩ + constructor + · intro r hr + simp only [List.mem_cons, List.not_mem_nil, or_false] at hr + simp only [RegUpd.gpr_setReg, hr, ite_false] + all_goals rfl + +theorem advance_ok (s : State) : WP isa (.block advance) s fun t => + t.gpr .r10 = (s.gpr .r14 + 1) * s.gpr .r13 ∧ + t.zf = decide (s.gpr .r14 = 3) ∧ Divide.Keeps [.rax, .rdx, .r10] s t := by + apply WP.of_runBlock + simp only [advance, runBlock_cons, runStep_some, runBlock_nil, exec, readSrc, + execAlu, execMul, RegUpd.gpr_setReg, RegUpd.gpr_setFlags, RegUpd.gpr_arithFlags, + RegUpd.zf_arithFlags, reduceCtorEq, ite_true, ite_false, + Option.map_some, Option.bind_some, Option.some.injEq, exists_eq_left', + BitVec.ofNat_mul, BitVec.ofNat_toNat, BitVec.setWidth_eq, + show BitVec.signExtend 64 (1 : BitVec 32) = (1 : Addr) from rfl, + show BitVec.signExtend 64 (3 : BitVec 32) = (3 : Addr) from rfl] + refine ⟨trivial, ?_, ?_⟩ + · apply Bool.eq_iff_iff.mpr + simp only [beq_iff_eq, decide_eq_true_eq, sub_zero_iff] + · 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_setFlags, RegUpd.gpr_arithFlags, + hr.1, hr.2.1, hr.2.2, ite_false] + all_goals rfl + +def changed : List Reg := [.rax, .rdx, .r10] + +def value (s : State) : Addr := + if s.gpr .r9 = 0 then 0 else + if s.gpr .r14 = 3 then 0 else (s.gpr .r14 + 1) * s.gpr .r13 + +theorem code_ok (s : State) : WP isa code s fun t => + t.gpr .r10 = value s ∧ Divide.Keeps changed s t := by + unfold code + refine WP.seq ((CountCandidates.compare_ok s).mono ?_) + rintro a ⟨flag, keeps⟩ + refine WP.ite (decide (s.gpr .r9 = 0)) (by simp only [eval, flag]) ?_ ?_ + · intro h + have firstPass : s.gpr .r9 = 0 := of_decide_eq_true h + refine (zero_ok a).mono ?_ + rintro t ⟨out, tail⟩ + refine ⟨?_, (keeps.mono (by simp)).trans (tail.mono (by decide))⟩ + simpa only [value, firstPass, ite_true] using out + · intro h + have laterPass : s.gpr .r9 ≠ 0 := of_decide_eq_false h + refine WP.seq ((advance_ok a).mono ?_) + rintro b ⟨out, flag, advanceKeeps⟩ + have sliceReg := keeps.regs .r14 (by simp) + have segmentReg := keeps.regs .r13 (by simp) + refine WP.ite (decide (s.gpr .r14 = 3)) + (by simp only [eval, flag, sliceReg]) ?_ ?_ + · intro h + have lastSlice : s.gpr .r14 = 3 := of_decide_eq_true h + refine (zero_ok b).mono ?_ + rintro t ⟨out, tail⟩ + refine ⟨?_, ((keeps.mono (by simp)).trans advanceKeeps).trans (tail.mono (by decide))⟩ + simpa only [value, laterPass, lastSlice, ite_false, ite_true] using out + · intro h + have earlierSlice : s.gpr .r14 ≠ 3 := of_decide_eq_false h + apply WP.of_runBlock + simp only [runBlock_nil, Option.some.injEq, exists_eq_left'] + refine ⟨?_, (keeps.mono (by simp)).trans advanceKeeps⟩ + simpa only [value, laterPass, earlierSlice, ite_false, sliceReg, segmentReg] using out + +theorem start_nat (p : Spec.Argon2.Params) (hl : 0 < p.lanes) + (hg : 0 < p.segmentLen) (slice : Nat) (hs : slice < 4) : + (slice + 1) * p.segmentLen % p.laneLen = + if slice = 3 then 0 else (slice + 1) * p.segmentLen := by + rw [Proof.Argon2.laneLen_segments p hl] + by_cases lastSlice : slice = 3 + · simp only [lastSlice, ite_true, show (3 : Nat) + 1 = 4 from rfl, Nat.mod_self] + · have smaller : (slice + 1) * p.segmentLen < 4 * p.segmentLen := + Nat.mul_lt_mul_of_pos_right (by omega) hg + rw [Nat.mod_eq_of_lt smaller] + simp only [lastSlice, ite_false] + +theorem value_nat (s : State) (p : Spec.Argon2.Params) (pass slice : Nat) + (hl : 0 < p.lanes) (hg : 0 < p.segmentLen) (hs : slice < 4) + (passReg : (s.gpr .r9).toNat = pass) + (sliceReg : s.gpr .r14 = BitVec.ofNat 64 slice) + (segmentReg : s.gpr .r13 = BitVec.ofNat 64 p.segmentLen) : + value s = BitVec.ofNat 64 + (if pass = 0 then 0 else (slice + 1) * p.segmentLen % p.laneLen) := by + have isZero : s.gpr .r9 = 0 ↔ pass = 0 := by + rw [← passReg] + constructor + · intro h; rw [h]; rfl + · intro h + apply BitVec.eq_of_toNat_eq + exact h + have isLast : s.gpr .r14 = 3 ↔ slice = 3 := by + rw [sliceReg] + constructor + · intro h + have hn := congrArg BitVec.toNat h + rw [BitVec.toNat_ofNat, Nat.mod_eq_of_lt (by omega)] at hn + exact hn + · intro h; rw [h]; rfl + unfold value + simp only [isZero, isLast] + by_cases firstPass : pass = 0 + · simp only [firstPass, ite_true]; rfl + · simp only [firstPass, ite_false, start_nat p hl hg slice hs] + by_cases lastSlice : slice = 3 + · simp only [lastSlice, ite_true]; rfl + · simp only [lastSlice, ite_false] + rw [sliceReg, segmentReg] + change (BitVec.ofNat 64 slice + BitVec.ofNat 64 1) * + BitVec.ofNat 64 p.segmentLen = _ + rw [← BitVec.ofNat_add, ← BitVec.ofNat_mul] + +theorem code_nat_ok (s : State) (p : Spec.Argon2.Params) (pass slice : Nat) + (hl : 0 < p.lanes) (hg : 0 < p.segmentLen) (hs : slice < 4) + (passReg : (s.gpr .r9).toNat = pass) + (sliceReg : s.gpr .r14 = BitVec.ofNat 64 slice) + (segmentReg : s.gpr .r13 = BitVec.ofNat 64 p.segmentLen) : + WP isa code s fun t => + t.gpr .r10 = BitVec.ofNat 64 + (if pass = 0 then 0 else (slice + 1) * p.segmentLen % p.laneLen) ∧ + Divide.Keeps changed s t := + (code_ok s).mono (fun _ h => + ⟨h.1.trans (value_nat s p pass slice hl hg hs passReg sliceReg segmentReg), h.2⟩) + +end VG.Proof.Argon2.X86_64.ReferenceStart diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartCT.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartCT.lean new file mode 100644 index 000000000..125a9149d --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartCT.lean @@ -0,0 +1,20 @@ +import VerifiedGarbage.Proof.Argon2.X86_64.ReferenceStartLit +import VerifiedGarbage.Proof.Framework.X86_64.RelCT + +/-! The public pass, slice and segment length determine the window start. -/ + +namespace VG.Proof.Argon2.X86_64.ReferenceStart + +open VG VG.X86_64 VG.Impl.Argon2.X86_64.ReferenceStart + +theorem code_rel : RelCT isa + (fun s t => ∀ r ∈ [Reg.r9, .r14, .r13], s.gpr r = t.gpr r) code + (fun s t => s.gpr .r10 = t.gpr .r10) := by + have h : RelCT isa + (fun s t => ∀ r ∈ [Reg.r9, .r14, .r13], s.gpr r = t.gpr r) code + (fun s t => ∀ r ∈ [Reg.r10], s.gpr r = t.gpr r) := + RelCT.taintRegs (τ := Taint.ofRegs [.r9, .r14, .r13]) + (fun _ _ h => Taint.agree_ofRegs h) [Reg.r10] (by taint_decide) + exact h.mono (fun _ _ h => h) (fun _ _ h => h .r10 (by simp)) + +end VG.Proof.Argon2.X86_64.ReferenceStart diff --git a/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartLit.lean b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartLit.lean new file mode 100644 index 000000000..361a5c537 --- /dev/null +++ b/lean/VerifiedGarbage/Proof/Argon2/X86_64/ReferenceStartLit.lean @@ -0,0 +1,10 @@ +import VerifiedGarbage.Proof.Framework.X86_64.Lit +import VerifiedGarbage.Impl.Argon2.X86_64.ReferenceStart + +/-! A checked literal for the chronological reference-window start. -/ + +namespace VG + +materialize_code Impl.Argon2.X86_64.ReferenceStart.code + +end VG