SHA-256 on PPC64LE: verified compress/init/update/finalize

README.md

@@ -166,7 +166,7 @@ yours to keep:
 
 <td>✅ SHA extensions</td>
 
-<td>❌</td>
+<td>✅</td>
 
 </tr>
 

bench/benches/primitives/sha256.rs

@@ -8,20 +8,6 @@ use crate::hash_group;
 
 pub const USES: &[&str] = &["sha256"];
 
-#[cfg(not(any(
-    target_arch = "x86_64",
-    target_arch = "aarch64",
-    target_arch = "arm",
-    target_arch = "x86"
-)))]
-pub fn bench(_: &mut Criterion) {}
-
-#[cfg(any(
-    target_arch = "x86_64",
-    target_arch = "aarch64",
-    target_arch = "arm",
-    target_arch = "x86"
-))]
 pub fn bench(c: &mut Criterion) {
     hash_group(c, "sha256", Sha256::digest, MessageDigest::sha256());
 }

lean/VerifiedGarbage/Artifacts/Sha256/PPC64LE.lean

@@ -0,0 +1,51 @@
+import VerifiedGarbage.TCB.PPC64LE.Target
+import VerifiedGarbage.Proof.Sha256.PPC64LE.Shared
+
+/-!
+# SHA-256 (FIPS 180-4) on PPC64LE
+
+A registration file (see `TCB/Emit.lean`): the artifacts it lists are
+emitted. **Review note**: `sig` and `doc` are trusted, as they tie the Rust
+caller to the contract; check them against the contract's `pre`/`post`. An
+artifact made from a function's `Api` (in `Spec/`, reviewed with the
+contract) takes them from there, and this file adds only notes on the
+implementation. The emitter adds the `# Safety` items that depend on the
+target (`Sig.layoutDoc`), from `stack` and `writeArgs`, which `ofSig` checks
+against the contract.
+-/
+
+namespace VG.Artifacts.Sha256.PPC64LE
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.compressApi with
+    target := PPC64LE.target
+    doc := Spec.Sha256.compressApi.doc
+    code := Impl.Sha256.PPC64LE.compress
+    contract := Spec.Sha256.compressContract PPC64LE.abi
+    verified := Proof.Sha256.PPC64LE.Shared.compress
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Sha256.initApi with
+    target := PPC64LE.target
+    doc := Spec.Sha256.initApi.doc
+    code := Impl.Sha256.PPC64LE.Stream.init
+    contract := Spec.Sha256.initContract PPC64LE.abi
+    verified := Proof.Sha256.PPC64LE.Shared.init
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Sha256.updateApi with
+    target := PPC64LE.target
+    doc := Spec.Sha256.updateApi.doc
+    code := Impl.Sha256.PPC64LE.Stream.update
+    contract := Spec.Sha256.updateContract PPC64LE.abi 48
+    stack := 48
+    verified := Proof.Sha256.PPC64LE.Shared.update
+    spSafe := Code.all_of_forall (fun _ => rfl) _ },
+  { Spec.Sha256.finalizeApi with
+    target := PPC64LE.target
+    doc := Spec.Sha256.finalizeApi.doc
+    code := Impl.Sha256.PPC64LE.Stream.finalize
+    contract := Spec.Sha256.finalizeContract PPC64LE.abi 48
+    stack := 48
+    verified := Proof.Sha256.PPC64LE.Shared.finalize
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.Sha256.PPC64LE

lean/VerifiedGarbage/Impl/Sha256/PPC64LE.lean

@@ -0,0 +1,149 @@
+import VerifiedGarbage.Spec.Sha256
+import VerifiedGarbage.TCB.PPC64LE.Isa
+
+/-!
+# SHA-256 compression function: PPC64LE implementation
+
+`vg_sha256_compress(state = r3, blocks = r4, n = r5, scratch = r6)`.
+
+The same structure as the AArch64 implementation:
+* The working variables `a … h` live in the low words of `r7`–`r12`, `r14`
+  and `r15`; the fully unrolled rounds rename them: in round `t`, variable
+  `k` is in `var t k`. The additions act on all 64 bits, so the high words
+  hold carries, which the word rotates, shifts and stores ignore.
+* The message schedule is a 16-word window in `scratch[0..64)`. The words
+  of a block are loaded big-endian with `lwbrx`, indexed by `r0`.
+* `r14`–`r19` are nonvolatile: they are saved in `scratch[64..112)` first and
+  restored last.
+* `r3`–`r6` (the pointers and the block count) are public; no address and
+  no branch depends on anything else.
+-/
+
+namespace VG.Impl.Sha256.PPC64LE
+
+open VG.PPC64LE
+open VG.Spec.Sha256 (K)
+
+/-- The registers holding the working variables. -/
+def work : List Reg := [.r7, .r8, .r9, .r10, .r11, .r12, .r14, .r15]
+
+/-- The register holding working variable `k` (`a = 0, …, h = 7`) at the start of round `t`. -/
+def var (t k : Nat) : Reg := work.getD ((k + 8 - t % 8) % 8) .r7
+
+/-- Temporaries; `T0` holds `Wₜ` at the start of each round. -/
+def T0 : Reg := .r16
+def T1 : Reg := .r17
+def T2 : Reg := .r18
+def T3 : Reg := .r19
+
+/-- The nonvolatile registers used, in the order they are saved. -/
+def saved (i : Nat) : Reg := [.r14, .r15, .r16, .r17, .r18, .r19].getD i .r14
+
+/-- Save them in `scratch[64..112)`. -/
+def save : List Instr := (List.range 6).flatMap fun i => [.store .d (saved i) .r6 (64 + 8 * i)]
+
+/-- Restore them. -/
+def restore : List Instr := (List.range 6).flatMap fun i => [.load .d (saved i) .r6 (64 + 8 * i)]
+
+/-- The offset of `W[i mod 16]` in the scratch buffer. -/
+def slot (i : Nat) : Nat := 4 * (i % 16)
+
+/-- Leave `Wₜ` in the low word of `T0` and in its slot. The additions are in
+the order of the specification. -/
+def schedule (t : Nat) : List Instr :=
+  if t < 16 then [
+    .li .r0 (4 * t),
+    .loadRev .w T0 .r4 .r0,
+    .store .w T0 .r6 (slot t)]
+  else [
+    -- T0 := σ₁(Wₜ₋₂)
+    .load .w T1 .r6 (slot (t + 14)),
+    .rotr .w T0 T1 17,
+    .rotr .w T2 T1 19,
+    .logic .xor T0 T0 T2,
+    .lsr .w T2 T1 10,
+    .logic .xor T0 T0 T2,
+    -- T0 := T0 + Wₜ₋₇
+    .load .w T2 .r6 (slot (t + 9)),
+    .add T0 T0 T2,
+    -- T0 := T0 + σ₀(Wₜ₋₁₅)
+    .load .w T1 .r6 (slot (t + 1)),
+    .rotr .w T2 T1 7,
+    .rotr .w T3 T1 18,
+    .logic .xor T2 T2 T3,
+    .lsr .w T3 T1 3,
+    .logic .xor T2 T2 T3,
+    .add T0 T0 T2,
+    -- T0 := T0 + Wₜ₋₁₆
+    .load .w T2 .r6 (slot t),
+    .add T0 T0 T2,
+    .store .w T0 .r6 (slot t)]
+
+/-- Round `t`, with `Wₜ` in `T0`. The additions are in the order of the
+specification. -/
+def round (t : Nat) : List Instr :=
+  let a := var t 0; let b := var t 1; let c := var t 2; let d := var t 3
+  let e := var t 4; let f := var t 5; let g := var t 6; let h := var t 7
+  [ -- h := h + Σ₁(e)
+    .rotr .w T1 e 6,
+    .rotr .w T2 e 11,
+    .logic .xor T1 T1 T2,
+    .rotr .w T2 e 25,
+    .logic .xor T1 T1 T2,
+    .add h h T1,
+    -- h := h + Ch(e, f, g), as ((f ⊕ g) ∧ e) ⊕ g
+    .logic .xor T1 f g,
+    .logic .and T1 T1 e,
+    .logic .xor T1 T1 g,
+    .add h h T1,
+    -- h := h + Kₜ + Wₜ, which is T₁
+    .lis T1 ((K t).extractLsb' 16 16),
+    .ori T1 T1 ((K t).extractLsb' 0 16),
+    .add h h T1,
+    .add h h T0,
+    -- e' := d + T₁
+    .add d d h,
+    -- h := h + Σ₀(a)
+    .rotr .w T1 a 2,
+    .rotr .w T2 a 13,
+    .logic .xor T1 T1 T2,
+    .rotr .w T2 a 22,
+    .logic .xor T1 T1 T2,
+    .add h h T1,
+    -- h := h + Maj(a, b, c), as ((a ∨ b) ∧ c) ∨ (a ∧ b); now h = a' = T₁ + T₂
+    .logic .or T1 a b,
+    .logic .and T1 T1 c,
+    .logic .and T2 a b,
+    .logic .or T1 T1 T2,
+    .add h h T1]
+
+/-- Rounds `0 … n-1`. -/
+def rounds : Nat → Prog isa
+  | 0 => .block []
+  | n + 1 => .seq (rounds n) (.block (schedule n ++ round n))
+
+/-- Load the hash value (`64 % 8 = 0`, so the variables are in the same
+registers after the 64 rounds). -/
+def load : List Instr := (List.range 8).map fun k => .load .w (var 0 k) .r3 (4 * k)
+
+/-- Add the hash value into the working variables (loading all of it before
+storing any of it), and store the result. -/
+def update : List Instr :=
+  (List.range 4).map (fun k => .load .w ([T0, T1, T2, T3].getD k T0) .r3 (4 * k)) ++
+  (List.range 4).map (fun k => .add (var 0 k) (var 0 k) ([T0, T1, T2, T3].getD k T0)) ++
+  (List.range 4).map (fun k => .load .w ([T0, T1, T2, T3].getD k T0) .r3 (4 * (k + 4))) ++
+  (List.range 4).map (fun k => .add (var 0 (k + 4)) (var 0 (k + 4)) ([T0, T1, T2, T3].getD k T0)) ++
+  (List.range 8).map (fun k => .store .w (var 0 k) .r3 (4 * k))
+
+/-- Advance to the next block and decrement the count. -/
+def advance : List Instr := [.addi .r4 .r4 64, .subi .r5 .r5 1]
+
+/-- One block. -/
+def body : Prog isa := .seq (.block load) (.seq (rounds 64) (.block (update ++ advance)))
+
+/-- The blocks. -/
+def blocks : Prog isa := .ite (.zero .d .r5) (.block []) (.loop body (.nonzero .d .r5))
+
+def compress : Prog isa := .seq (.block save) (.seq blocks (.block restore))
+
+end VG.Impl.Sha256.PPC64LE

lean/VerifiedGarbage/Impl/Sha256/PPC64LE/Stream.lean

@@ -0,0 +1,147 @@
+import VerifiedGarbage.Impl.Sha256.PPC64LE
+
+/-!
+# Streaming SHA-256: PPC64LE implementation
+
+The streaming state (96 bytes at `state`) is the hash value followed by a
+64-byte buffer (see `VG.Spec.Sha256.Repr`).
+
+* `init(state = r3)` stores `H⁽⁰⁾`.
+* `update(state = r3, count = r4, data = r5, len = r6, scratch = r7)`
+  processes one block per iteration: straight from `data` while the buffer is
+  empty and a whole block remains, otherwise by copying bytes into the buffer,
+  compressing it once it is full.
+* `finalize(state = r3, count = r4, out = r5, scratch = r6)` pads the
+  buffered bytes (one or two blocks), compresses them and writes the digest.
+
+`update` and `finalize` call the compression function (`vg_sha256_compress`)
+with `scratch[0..112)` as its scratch space. It preserves `r14`–`r31`, so our
+own variables live in `r26`–`r31` (`r26` = `state`, `r27` = `scratch`), and
+our caller's values of those registers are saved in `scratch[112..160)`. Our
+return address (the link register), which each call replaces, is moved to
+`r0` and saved in a stack frame around the whole function.
+
+Only register-plus-displacement addressing is used, so byte `r` of the buffer
+is addressed as `32(r11)` with `r11 = state + r` computed just before the
+access, and `data` is consumed through a pointer that advances. Every
+comparison is a shift (`len ≥ 64` iff `len >> 6 ≠ 0`) or a subtraction
+tested against zero. Every address and branch depends only on the pointers,
+`count` and `len`.
+-/
+
+namespace VG.Impl.Sha256.PPC64LE.Stream
+
+open VG.PPC64LE
+open VG.Impl.Sha256.PPC64LE (compress)
+
+/-- `mr d, n` (as `addi d, n, 0`; `n` is not `r0`). -/
+def mov (d n : Reg) : Instr := .addi d n 0
+
+def init : Prog isa :=
+  .block ((List.range 8).flatMap fun k =>
+    [.lis .r8 (Spec.Sha256.H0[k]!.extractLsb' 16 16),
+     .ori .r8 .r8 (Spec.Sha256.H0[k]!.extractLsb' 0 16),
+     .store .w .r8 .r3 (4 * k)])
+
+/-- The nonvolatile registers we use, and where they are saved in `scratch`. -/
+def saved : List (Reg × Nat) :=
+  [(.r26, 112), (.r27, 120), (.r28, 128), (.r29, 136), (.r30, 144), (.r31, 152)]
+
+/-- Save them, with `scratch` in `b`. -/
+def save (b : Reg) : List Instr := saved.map fun (r, d) => .store .d r b d
+
+/-- Restore them from `scratch` in `r27` (`r27`, the base, last). -/
+def restore : List Instr :=
+  (saved.filter (·.1 != .r27)).map (fun (r, d) => .load .d r .r27 d) ++ [.load .d .r27 .r27 120]
+
+/-- Compress the block at `r4` into the hash value at `r26`, with scratch
+space `r27`. -/
+def compressAt : Prog isa :=
+  .seq (.block [mov .r3 .r26, .li .r5 1, mov .r6 .r27]) (.call "vg_sha256_compress" compress)
+
+/-! ## `update`
+
+Registers: `r28` = `data`, `r29` = bytes of `data` left, `r30` = bytes in the
+buffer (`r`), `r9` = whether this iteration compresses a block (at `r4`).
+The loop runs while `r29 ≠ 0`, so each iteration starts with `r29 ≥ 1` and
+`r30 < 64`. -/
+
+/-- A whole block straight from `data`. -/
+def direct : List Instr :=
+  [mov .r4 .r28, .addi .r28 .r28 64, .subi .r29 .r29 64, .li .r9 1]
+
+/-- Copy `n = min(64 - r, len) ≥ 1` bytes of `data` into the buffer; if that
+fills it, compress it. -/
+def fill : Prog isa :=
+  -- r10 := 64 - r; if len < 64 and len + r < 64 (i.e. len < 64 - r), r10 := len.
+  .seq (.block [.li .r10 64, .sub .r10 .r10 .r30, .lsr .d .r8 .r29 6])
+  (.seq (.ite (.zero .d .r8)
+      (.seq (.block [.add .r8 .r29 .r30, .lsr .d .r8 .r8 6])
+        (.ite (.zero .d .r8) (.block [mov .r10 .r29]) (.block [])))
+      (.block []))
+  (.seq (.block [.sub .r29 .r29 .r10])
+  (.seq (.loop (.block [.lbz .r8 .r28 0, .add .r11 .r26 .r30, .stb .r8 .r11 32,
+      .addi .r28 .r28 1, .addi .r30 .r30 1, .subi .r10 .r10 1]) (.nonzero .d .r10))
+  -- Full: compress the buffer.
+  (.seq (.block [.subi .r8 .r30 64])
+    (.ite (.zero .d .r8) (.block [.addi .r4 .r26 32, .li .r30 0, .li .r9 1])
+      (.block []))))))
+
+def updateBody : Prog isa :=
+  .seq (.block [.li .r9 0])
+  (.seq (.ite (.zero .d .r30)
+      (.seq (.block [.lsr .d .r8 .r29 6]) (.ite (.zero .d .r8) fill (.block direct)))
+      fill)
+    (.ite (.zero .d .r9) (.block []) compressAt))
+
+/-- `update`, but for saving the link register. -/
+def updateMain : Prog isa :=
+  .seq (.block (save .r7 ++ [mov .r26 .r3, mov .r27 .r7, mov .r28 .r5, mov .r29 .r6,
+      .li .r8 63, .logic .and .r30 .r4 .r8]))
+  (.seq (.ite (.zero .d .r29) (.block []) (.loop updateBody (.nonzero .d .r29)))
+    (.block restore))
+
+def update : Prog isa :=
+  .seq (.block [.mflr .r0])
+    (.seq (.frame (.push .r0) updateMain (.pop .r0)) (.block [.mtlr .r0]))
+
+/-! ## `finalize`
+
+Registers: `r28` = `out`, `r29` = `count`, `r30` = bytes in the buffer (`r`),
+`r31` = 1 while the block being padded is not the last one (then 0). -/
+
+def finalizeBody : Prog isa :=
+  -- Zero the buffer from `r` to 64, or to 56 in the last block.
+  .seq (.block [.li .r10 64])
+  (.seq (.ite (.zero .d .r31) (.block [.li .r10 56]) (.block []))
+  (.seq (.block [.li .r8 0, .sub .r10 .r10 .r30])
+  (.seq (.ite (.zero .d .r10) (.block [])
+      (.loop (.block [.add .r11 .r26 .r30, .stb .r8 .r11 32, .addi .r30 .r30 1,
+        .subi .r10 .r10 1]) (.nonzero .d .r10)))
+  -- In the last block, the message length in bits (`8 * count`), big-endian.
+  (.seq (.ite (.zero .d .r31)
+      (.block [.add .r8 .r29 .r29, .add .r8 .r8 .r8, .add .r8 .r8 .r8, .li .r11 88,
+        .storeRev .d .r8 .r26 .r11])
+      (.block []))
+  (.seq (.block [.addi .r4 .r26 32])
+  (.seq compressAt
+    (.block [.li .r30 0, .subi .r31 .r31 1])))))))
+
+/-- `finalize`, but for saving the link register. -/
+def finalizeMain : Prog isa :=
+  .seq (.block (save .r6 ++ [mov .r26 .r3, mov .r27 .r6, mov .r28 .r5, mov .r29 .r4,
+      .li .r8 63, .logic .and .r30 .r29 .r8,
+      -- The `0x80` byte.
+      .li .r8 0x80, .add .r11 .r26 .r30, .stb .r8 .r11 32, .addi .r30 .r30 1,
+      -- Two blocks iff that leaves fewer than 8 bytes for the length (r ≥ 57).
+      .addi .r31 .r30 7, .lsr .d .r31 .r31 6]))
+  (.seq (.loop finalizeBody (.zero .d .r31))
+    (.block ((List.range 8).flatMap (fun k =>
+        [.load .w .r8 .r26 (4 * k), .li .r11 (4 * k), .storeRev .w .r8 .r28 .r11]) ++
+      restore)))
+
+def finalize : Prog isa :=
+  .seq (.block [.mflr .r0])
+    (.seq (.frame (.push .r0) finalizeMain (.pop .r0)) (.block [.mtlr .r0]))
+
+end VG.Impl.Sha256.PPC64LE.Stream

lean/VerifiedGarbage/Proof/Framework/PPC64LE/Inline.lean

@@ -472,14 +472,13 @@ theorem Verified.widen {c : Prog isa} {k k' : Contract isa} (h : Verified target
       k.post (s.withRegions s.rd (wr s)) (s'.withRegions s.rd (wr s)) → k'.post s s')
     (hpub : ∀ s₁ s₂, k'.pre s₁ → k'.pre s₂ → k'.pub s₁ s₂ →
       k.pub (s₁.withRegions s₁.rd (wr s₁)) (s₂.withRegions s₂.rd (wr s₂)))
-    (hsat : ∃ s, k'.pre s) (hn : c.noFrames = true := by decide +kernel) :
-    Verified target c k' := by
+    (hsat : ∃ s, k'.pre s) : Verified target c k' := by
   refine h.of_narrow (fun s => s.withRegions s.rd (wr s)) (fun s s₁ => s₁.withRegions s.rd s.wr)
     hpre (fun s t s₁ hs he => ?_) (fun s t s₁ hs he ha hq => ?_) hpub hsat
   · have hw : Covers (wr s) s.wr := fun _ _ => InRegions.of_prefix (hwr s hs)
     have := Exec.widen (rd := s.rd) (wr := s.wr) he (Covers.append (fun _ _ h => h) hw) hw
     rwa [State.withRegions_withRegions, State.withRegions_self] at this
-  · obtain ⟨hr, hw, -⟩ := Exec.regions he hn
+  · obtain ⟨hr, hw, -⟩ := Exec.rdwr he
     simp only [State.withRegions_rd, State.withRegions_wr] at hr hw
     have : (s₁.withRegions s.rd s.wr).withRegions s.rd (wr s) = s₁ := by
       rw [State.withRegions_withRegions, ← hr, ← hw]; rfl