SHA-224 on x86-64, x86, AArch64 and ARMv7: vg_sha224_init and the Rust API

README.md

@@ -129,13 +129,13 @@ yours to keep:
 
 <td>✅</td>
 
-<td>❌</td>
+<td>✅ SHA extensions, AVX2, BMI1, BMI2</td>
 
-<td>❌</td>
+<td>✅ SHA extensions</td>
 
-<td>❌</td>
+<td>✅</td>
 
-<td>❌</td>
+<td>✅</td>
 
 </tr>
 

bench/benches/primitives/main.rs

@@ -40,6 +40,7 @@ mod poly1305;
 mod rc2_cbc;
 mod scrypt;
 mod sha1;
+mod sha224;
 mod sha256;
 mod sha3;
 mod sha512;
@@ -211,6 +212,7 @@ const BENCHES: &[Bench] = &[
     (rc2_cbc::USES, rc2_cbc::bench),
     (scrypt::USES, scrypt::bench),
     (sha1::USES, sha1::bench),
+    (sha224::USES, sha224::bench),
     (sha256::USES, sha256::bench),
     (sha3::USES, sha3::bench),
     (sha512::USES, sha512::bench),

bench/benches/primitives/sha224.rs

@@ -0,0 +1,15 @@
+//! SHA-224.
+
+use criterion::Criterion;
+use openssl::hash::MessageDigest;
+use verified_garbage::hashes::sha224::Sha224;
+
+use crate::hash_group;
+
+/// The library modules whose code these benchmarks run (see
+/// `ci/bench_arches.py`).
+pub const USES: &[&str] = &["sha224", "sha256"];
+
+pub fn bench(c: &mut Criterion) {
+    hash_group(c, "sha224", Sha224::digest, MessageDigest::sha224());
+}

lean/VerifiedGarbage/Artifacts/Sha224/AArch64.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.AArch64.Target
+import VerifiedGarbage.Proof.Sha256.AArch64.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on AArch64
+
+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.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.AArch64
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := AArch64.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.AArch64.Stream.init224
+    contract := Spec.Sha256.init224Contract AArch64.abi
+    verified := Proof.Sha256.AArch64.Shared.init224
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.Sha224.AArch64

lean/VerifiedGarbage/Artifacts/Sha224/Arm.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.Arm.Target
+import VerifiedGarbage.Proof.Sha256.Arm.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on ARMv7
+
+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.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.Arm
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := Arm.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.Arm.Stream.init224
+    contract := Spec.Sha256.init224Contract Arm.abi
+    verified := Proof.Sha256.Arm.Shared.init224
+    spSafe := Code.all_of_forall (fun _ => rfl) _ }]
+
+end VG.Artifacts.Sha224.Arm

lean/VerifiedGarbage/Artifacts/Sha224/X86.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.X86.Target
+import VerifiedGarbage.Proof.Sha256.X86.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on x86 (32-bit)
+
+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.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.X86
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := X86.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.X86.Stream.init224
+    contract := Spec.Sha256.init224Contract X86.abi
+    verified := Proof.Sha256.X86.Shared.init224
+    spSafe := Code.all_of_allInstrs (by lit_decide) }]
+
+end VG.Artifacts.Sha224.X86

lean/VerifiedGarbage/Artifacts/Sha224/X86_64.lean

@@ -0,0 +1,32 @@
+import VerifiedGarbage.TCB.X86_64.Target
+import VerifiedGarbage.Proof.Sha256.X86_64.Shared
+
+/-!
+# SHA-224 (FIPS 180-4) on x86-64
+
+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.
+
+SHA-224 is SHA-256 from another initial hash value: only its `init` is its
+own, and it continues with SHA-256's `update` and `finalize`
+(`Artifacts/Sha256/`).
+-/
+
+namespace VG.Artifacts.Sha224.X86_64
+
+def artifacts : List Artifact := [
+  { Spec.Sha256.init224Api with
+    target := X86_64.target
+    doc := Spec.Sha256.init224Api.doc
+    code := Impl.Sha256.X86_64.Stream.init224
+    contract := Spec.Sha256.init224Contract X86_64.abi
+    verified := Proof.Sha256.X86_64.Shared.init224
+    spSafe := Code.all_of_allInstrs (by lit_decide) }]
+
+end VG.Artifacts.Sha224.X86_64

lean/VerifiedGarbage/Impl/Sha256/AArch64/Stream.lean

@@ -7,7 +7,7 @@ import VerifiedGarbage.Impl.MdStream.AArch64
 The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`).
 
-* `init(state = x0)` stores `H⁽⁰⁾`.
+* `init(state = x0)` stores `H⁽⁰⁾` (`init224`, SHA-224's).
 * `update` and `finalize` are the generic streaming code
   (`Impl/MdStream/AArch64.lean`), calling the compression function
   (`vg_sha256_compress`) with `scratch[0..112)` as its scratch space, and
@@ -25,12 +25,19 @@ open VG.Impl.Sha256.AArch64 (compress)
 /-- `mov d, n` (as `add d, n, #0`). -/
 def mov (d n : Reg) : Instr := .addImm .x d n 0
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap fun k =>
-    [.movz .w .x9 (Spec.Sha256.H0[k]!.extractLsb' 0 16) 0,
-     .movk .w .x9 (Spec.Sha256.H0[k]!.extractLsb' 16 16) 1,
+    [.movz .w .x9 (iv[k]!.extractLsb' 0 16) 0,
+     .movk .w .x9 (iv[k]!.extractLsb' 16 16) 1,
      .str .w .x9 .x0 (4 * k)])
 
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
+
 /-- The callee-saved registers we use, and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) :=
   [(.x19, 112), (.x20, 120), (.x21, 128), (.x22, 136), (.x23, 144), (.x24, 152)]

lean/VerifiedGarbage/Impl/Sha256/Arm/Stream.lean

@@ -7,7 +7,7 @@ import VerifiedGarbage.Impl.MdStream.Arm
 The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`).
 
-* `init(state = r0)` stores the initial hash value.
+* `init(state = r0)` stores the initial hash value (`init224`, SHA-224's).
 * `update` and `finalize` are the generic streaming code
   (`Impl/MdStream/Arm.lean`), calling the compression function
   (`vg_sha256_compress`) with `scratch[0..112)` as its scratch space, and saving our
@@ -22,12 +22,19 @@ namespace VG.Impl.Sha256.Arm.Stream
 open VG.Arm
 open VG.Impl.Sha256.Arm (compress)
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap fun k =>
-    [.movw .r12 (Spec.Sha256.H0[k]!.extractLsb' 0 16),
-     .movt .r12 (Spec.Sha256.H0[k]!.extractLsb' 16 16),
+    [.movw .r12 (iv[k]!.extractLsb' 0 16),
+     .movt .r12 (iv[k]!.extractLsb' 16 16),
      .str .r12 .r0 (4 * k)])
 
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
+
 /-- The callee-saved registers we use (and `lr`), and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) :=
   [(.r4, 112), (.r5, 116), (.r6, 120), (.r7, 124), (.r8, 128), (.r9, 132), (.r10, 136), (.r11, 140),

lean/VerifiedGarbage/Impl/Sha256/X86/Stream.lean

@@ -8,7 +8,7 @@ The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`). Every argument is on the stack
 (cdecl).
 
-* `init(state)` stores `H⁽⁰⁾`.
+* `init(state)` stores `H⁽⁰⁾` (`init224`, SHA-224's).
 * `update(state, count, data, len, scratch)` is the generic streaming code
   (`Impl/MdStream/X86.lean`): it compresses every whole block left in `data`
   with one call if the buffer is empty, and otherwise copies bytes into the
@@ -33,10 +33,17 @@ namespace VG.Impl.Sha256.X86.Stream
 open VG.X86
 open VG.Impl.Sha256.X86 (at_ compress)
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .seq (.block [.mov .eax (.mem (at_ .esp 4))])
     (.block ((List.range 8).flatMap fun k =>
-      [.mov .ecx (.imm Spec.Sha256.H0[k]!), .store (at_ .eax (4 * k)) .ecx]))
+      [.mov .ecx (.imm iv[k]!), .store (at_ .eax (4 * k)) .ecx]))
+
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
 
 /-- The callee-saved registers, and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) := [(.ebx, 112), (.esi, 116), (.edi, 120), (.ebp, 124)]

lean/VerifiedGarbage/Impl/Sha256/X86_64/Stream.lean

@@ -9,7 +9,7 @@ import VerifiedGarbage.Impl.MdStream.X86_64
 The streaming state (96 bytes at `state`) is the hash value followed by a
 64-byte buffer (see `VG.Spec.Sha256.Repr`).
 
-* `init(state = rdi)` stores `H⁽⁰⁾`.
+* `init(state = rdi)` stores `H⁽⁰⁾` (`init224`, SHA-224's).
 * `update(state = rdi, count = rsi, data = rdx, len = rcx, scratch = r8)`
   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,
@@ -42,9 +42,16 @@ def Callee.scalar : Callee := ⟨"vg_sha256_compress", compress⟩
 def Callee.shani : Callee := ⟨"vg_sha256_compress_shani", ShaNi.compress⟩
 def Callee.avx2 : Callee := ⟨"vg_sha256_compress_avx2", Avx2.compress⟩
 
-def init : Prog isa :=
+/-- Stores the initial hash value `iv`. -/
+def initWith (iv : Spec.Sha256.HashValue) : Prog isa :=
   .block ((List.range 8).flatMap fun k =>
-    [.mov32 .rax (.imm Spec.Sha256.H0[k]!), .store32 (at_ .rdi (4 * k)) .rax])
+    [.mov32 .rax (.imm iv[k]!), .store32 (at_ .rdi (4 * k)) .rax])
+
+/-- `vg_sha256_init`. -/
+def init : Prog isa := initWith Spec.Sha256.H0
+
+/-- `vg_sha224_init`. -/
+def init224 : Prog isa := initWith Spec.Sha256.H0_224
 
 /-- The callee-saved registers, and where they are saved in `scratch`. -/
 def saved : List (Reg × Nat) := [(.rbx, 560), (.rbp, 568), (.r12, 576), (.r13, 584), (.r14, 592), (.r15, 600)]

lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean

@@ -41,15 +41,16 @@ def compressAArch64 : Contract AArch64.isa where
     s₁.gpr .x2 = s₂.gpr .x2 ∧ s₁.gpr .x3 = s₂.gpr .x3 ∧ s₁.sp = s₂.sp
 
 open AArch64 in
-/-- AArch64 contract for `vg_sha256_init(state: *mut [u8; 96])`: makes the
-streaming state at `state` represent the empty message.
+/-- AArch64 contract for `vg_sha256_init(state: *mut [u8; 96])` and
+`vg_sha224_init`, which store the initial hash value `iv`: makes the
+streaming state at `state` represent the empty message, hashed from `iv`.
 
 The code may write `state` (96 bytes). The pointer is public. -/
-def initAArch64 : Contract AArch64.isa where
+def initAArch64 (iv : HashValue) : Contract AArch64.isa where
   pre s :=
     let state : Region := ⟨s.gpr .x0, 96⟩
     s.rd = [] ∧ s.wr = [state]
-  post s s' := Repr s'.mem (s.gpr .x0) []
+  post s s' := ReprFrom iv s'.mem (s.gpr .x0) []
   pub s₁ s₂ := s₁.gpr .x0 = s₂.gpr .x0 ∧ s₁.sp = s₂.sp
 
 open AArch64 in

lean/VerifiedGarbage/Proof/Sha256/AArch64/Shared.lean

@@ -117,6 +117,13 @@ theorem init :
       AArch64.abi, AArch64.argRegs]
       [Proof.Sha256.AArch64.Stream.initSat] using Proof.Sha256.AArch64.Stream.initSat)
 
+theorem init224 :
+    Verified AArch64.target Impl.Sha256.AArch64.Stream.init224 (Spec.Sha256.init224Contract AArch64.abi) :=
+  Proof.Sha256.AArch64.Stream.init224_verified.of_implies (by
+    contract_implies [Spec.Sha256.init224Contract, Spec.Sha256.initSig, Proof.Sha256.initAArch64,
+      AArch64.abi, AArch64.argRegs]
+      [Proof.Sha256.AArch64.Stream.initSat] using Proof.Sha256.AArch64.Stream.initSat)
+
 theorem update_of {code : Prog isa} (hv : Verified AArch64.target code Proof.Sha256.updateAArch64) :
     Verified AArch64.target code (Spec.Sha256.updateContract AArch64.abi 16) := by
   have hi : updateWide.Implies (Spec.Sha256.updateContract AArch64.abi 16) := by