diff --git a/README.md b/README.md
index 25b339af4..97f86bd67 100644
--- a/README.md
+++ b/README.md
@@ -125,6 +125,22 @@ yours to keep:
 
 <tr>
 
+<td>SHA-224</td>
+
+<td>✅</td>
+
+<td>❌</td>
+
+<td>❌</td>
+
+<td>❌</td>
+
+<td>❌</td>
+
+</tr>
+
+<tr>
+
 <td>SHA-256</td>
 
 <td>✅</td>
diff --git a/docs/algorithms/sha224.toml b/docs/algorithms/sha224.toml
new file mode 100644
index 000000000..4b3c87af3
--- /dev/null
+++ b/docs/algorithms/sha224.toml
@@ -0,0 +1,5 @@
+name = "SHA-224"
+family = "Hashes"
+specs = ["Sha256"]
+modules = ["src/hashes/sha224.rs"]
+asm = ["sha256"]
diff --git a/lean/VerifiedGarbage/Proof/Hmac/Arm/Finalize.lean b/lean/VerifiedGarbage/Proof/Hmac/Arm/Finalize.lean
index 72b2e27aa..4fd8c8e7c 100644
--- a/lean/VerifiedGarbage/Proof/Hmac/Arm/Finalize.lean
+++ b/lean/VerifiedGarbage/Proof/Hmac/Arm/Finalize.lean
@@ -167,7 +167,7 @@ theorem fin_ok {s₀ : State} (hp : Pre s₀) {s : State} (hrd : s.rd = s₀.rd)
     · exact ⟨scR s₀, by simp, 0, by simp, by simp⟩
   · intro s' h₁ h₂ h₃ h₄ hg hpost
     simp only [Proof.Sha256.finalizeArm, State.withRegions_gpr, State.withRegions_mem, h0, e0] at hpost
-    exact hQ s' h₁ h₂ h₃ h₄ (by rw [hg _ r0_ok (by decide), h0]) hpost
+    exact hQ s' h₁ h₂ h₃ h₄ (by rw [hg _ r0_ok (by decide), h0]) fun m hr hc => hpost Spec.Sha256.H0 m hr hc
 
 /-! ## Saving the outer hash value -/
 
diff --git a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/Hashes/Sha256.lean b/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/Hashes/Sha256.lean
index 0f75c37f0..38e6e8007 100644
--- a/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/Hashes/Sha256.lean
+++ b/lean/VerifiedGarbage/Proof/Pbkdf2/Md/AArch64/Hashes/Sha256.lean
@@ -98,13 +98,17 @@ def streamOK : Hmac.Generic.AArch64.HashOK (hash v).stream where
   hW := by simp only [hash, Hash.stream] <;> decide
   repr := sha256_repr
   init := Proof.Sha256.AArch64.Stream.init_verified
-  upd := v.update_verified
+  upd := v.update_verified.of_implies
+    { pre := fun _ h => h
+      post := fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc
+      pub := fun _ _ _ _ h => h
+      sat := v.update_verified.2.2 }
   fin := v.finalize_verified.of_implies
     { pre := fun _ h => h
       post := fun s s' _ h m hr _ hc => by
         show List.take 32 (Spec.Sha256.bytesAt s'.mem _ 32) = _
         rw [List.take_of_length_le (by simp [Spec.Sha256.bytesAt])]
-        exact h m hr hc
+        exact h Spec.Sha256.H0 m hr hc
       pub := fun _ _ _ _ h => h
       sat := v.finalize_verified.2.2 }
   initDepth := by simp only [hash, Hash.stream] <;> decide +kernel
diff --git a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean
index 46279def1..8666c554a 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Contract.lean
@@ -56,8 +56,8 @@ open AArch64 in
 /-- AArch64 contract for
 `vg_sha256_update(state: *mut [u8; 96], count: u64, data: *const u8, len: usize, scratch: *mut [u64; 20])`:
 if the streaming state at `state` represents a message `m` of `count` bytes
-(modulo 2⁶⁴), then afterwards it represents `m` followed by the `len` bytes at
-`data`.
+(modulo 2⁶⁴), hashed from any initial hash value `iv`, then afterwards it
+represents `m` followed by the `len` bytes at `data`, from `iv`.
 
 The code may read `data` (`len` bytes) and read and write `state` (96
 bytes) and `scratch` (160 bytes, whose contents on exit are unspecified).
@@ -73,8 +73,8 @@ def updateAArch64 : Contract AArch64.isa where
     s.rd = [data] ∧ s.wr = [state, scratch] ∧
     state.Disjoint scratch ∧ data.Disjoint state ∧ data.Disjoint scratch ∧
     16 ≤ s.sp.toNat ∧ stack.Disjoint state ∧ stack.Disjoint data ∧ stack.Disjoint scratch
-  post s s' := ∀ m, Repr s.mem (s.gpr .x0) m → s.gpr .x1 = BitVec.ofNat 64 m.length →
-    Repr s'.mem (s.gpr .x0) (m ++ bytesAt s.mem (s.gpr .x2) (s.gpr .x3).toNat)
+  post s s' := ∀ iv m, ReprFrom iv s.mem (s.gpr .x0) m → s.gpr .x1 = BitVec.ofNat 64 m.length →
+    ReprFrom iv s'.mem (s.gpr .x0) (m ++ bytesAt s.mem (s.gpr .x2) (s.gpr .x3).toNat)
   pub s₁ s₂ :=
     s₁.gpr .x0 = s₂.gpr .x0 ∧ s₁.gpr .x1 = s₂.gpr .x1 ∧ s₁.gpr .x2 = s₂.gpr .x2 ∧
     s₁.gpr .x3 = s₂.gpr .x3 ∧ s₁.gpr .x4 = s₂.gpr .x4 ∧ s₁.sp = s₂.sp
@@ -83,7 +83,8 @@ open AArch64 in
 /-- AArch64 contract for
 `vg_sha256_finalize(state: *mut [u8; 96], count: u64, out: *mut [u8; 32], scratch: *mut [u64; 20])`:
 if the streaming state at `state` represents a message `m` of `count` bytes
-(modulo 2⁶⁴), writes the SHA-256 digest of `m` to `out`.
+(modulo 2⁶⁴), hashed from the initial hash value `iv`, writes the final hash
+value of `m` from `iv` to `out` (the SHA-256 digest if `iv` is `H0`).
 
 The code may read and write `state` (96 bytes, whose contents on exit are
 unspecified), `out` (32 bytes) and `scratch` (160 bytes, whose contents on
@@ -99,8 +100,8 @@ def finalizeAArch64 : Contract AArch64.isa where
     s.rd = [] ∧ s.wr = [state, out, scratch] ∧
     state.Disjoint out ∧ state.Disjoint scratch ∧ out.Disjoint scratch ∧
     16 ≤ s.sp.toNat ∧ stack.Disjoint state ∧ stack.Disjoint out ∧ stack.Disjoint scratch
-  post s s' := ∀ m, Repr s.mem (s.gpr .x0) m → s.gpr .x1 = BitVec.ofNat 64 m.length →
-    bytesAt s'.mem (s.gpr .x2) 32 = Spec.Sha256.hash m
+  post s s' := ∀ iv m, ReprFrom iv s.mem (s.gpr .x0) m → s.gpr .x1 = BitVec.ofNat 64 m.length →
+    bytesAt s'.mem (s.gpr .x2) 32 = Spec.Sha256.finalHash iv m
   pub s₁ s₂ :=
     s₁.gpr .x0 = s₂.gpr .x0 ∧ s₁.gpr .x1 = s₂.gpr .x1 ∧ s₁.gpr .x2 = s₂.gpr .x2 ∧
     s₁.gpr .x3 = s₂.gpr .x3 ∧ s₁.sp = s₂.sp
diff --git a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Md.lean b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Md.lean
index 1201fa1b0..71c27ce1e 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Md.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Stream/Md.lean
@@ -46,7 +46,7 @@ theorem update_verified : Verified AArch64.target Impl.Sha256.AArch64.Stream.upd
     (VG.Taint.constantTime (A := taint) (Taint.ofRegs [.x0, .x1, .x2, .x3, .x4])
       (fun _ _ _ _ hp => MdStream.AArch64.Update.agree₀ hp) (by taint_decide))
     (instrs_keeps (by lit_decide)) (by lit_decide)
-  Verified.of_implies h ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc, fun _ _ _ _ h => h, h.2.2⟩
+  Verified.of_implies h ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr hc, fun _ _ _ _ h => h, h.2.2⟩
 
 /-- A state satisfying `update`'s precondition. -/
 abbrev sat : State := MdStream.AArch64.Update.sat params
@@ -61,7 +61,7 @@ theorem finalize_verified : Verified AArch64.target Impl.Sha256.AArch64.Stream.f
       (fun _ _ _ _ hp => MdStream.AArch64.Finalize.agree₀ hp) (by taint_decide))
     (instrs_keeps (by lit_decide)) (by lit_decide)
   Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
 
 /-- A state satisfying `finalize`'s precondition. -/
 abbrev sat : State := MdStream.AArch64.Finalize.sat params
diff --git a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Variant.lean b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Variant.lean
index efbbb427b..21e2e4ac0 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/AArch64/Variant.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/AArch64/Variant.lean
@@ -46,13 +46,13 @@ theorem callee : CalleeOk (P := Stream.params) md v.code := ⟨v.verified.1, v.n
 theorem update_verified : Verified AArch64.target v.update Proof.Sha256.updateAArch64 := by
   have h := MdStream.AArch64.Update.verified Stream.dims v.callee v.updateCT v.updateKeeps
     (by rw [v.updateDepth]; decide)
-  exact h.of_implies ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc,
+  exact h.of_implies ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr hc,
     fun _ _ _ _ h => h, h.2.2⟩
 
 theorem finalize_verified : Verified AArch64.target v.finalize Proof.Sha256.finalizeAArch64 := by
   have h := MdStream.AArch64.Finalize.verified Stream.dims Stream.shape v.callee v.finalizeCT
     v.finalizeKeeps (by rw [v.finalizeDepth]; decide)
-  exact h.of_implies ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc,
+  exact h.of_implies ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr trivial hc,
     fun _ _ _ _ h => h, h.2.2⟩
 
 end Compress
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean
index 0a255d856..883dc5d61 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Arm/Contract.lean
@@ -65,8 +65,8 @@ open Arm in
 /-- 32-bit ARM contract for
 `vg_sha256_update(state: *mut [u8; 96], count: u64, data: *const u8, len: usize, scratch: *mut [u64; 20])`:
 if the streaming state at `state` represents a message `m` of `count` bytes
-(modulo 2⁶⁴), then afterwards it represents `m` followed by the `len` bytes at
-`data`.
+(modulo 2⁶⁴), hashed from any initial hash value `iv`, then afterwards it
+represents `m` followed by the `len` bytes at `data`, from `iv`.
 
 Under AAPCS, `state` is in `r0`, `count` in `r2:r3`, and `data`, `len` and
 `scratch` are the stack arguments 0, 1 and 2. The code may read those
@@ -87,8 +87,8 @@ def updateArm : Contract Arm.isa where
     args.Disjoint state ∧ args.Disjoint scratch ∧
     (s.gpr .r0).toNat + 96 ≤ 2 ^ 32 ∧ (stackArg s 0).toNat + (stackArg s 1).toNat ≤ 2 ^ 32 ∧
     (stackArg s 2).toNat + 160 ≤ 2 ^ 32 ∧ s.sp.toNat + 12 ≤ 2 ^ 32
-  post s s' := ∀ m, Repr s.mem (State.addr (s.gpr .r0)) m → countArm s = BitVec.ofNat 64 m.length →
-    Repr s'.mem (State.addr (s.gpr .r0))
+  post s s' := ∀ iv m, ReprFrom iv s.mem (State.addr (s.gpr .r0)) m → countArm s = BitVec.ofNat 64 m.length →
+    ReprFrom iv s'.mem (State.addr (s.gpr .r0))
       (m ++ bytesAt s.mem (State.addr (stackArg s 0)) (stackArg s 1).toNat)
   pub s₁ s₂ :=
     s₁.sp = s₂.sp ∧ s₁.gpr .r0 = s₂.gpr .r0 ∧ s₁.gpr .r2 = s₂.gpr .r2 ∧ s₁.gpr .r3 = s₂.gpr .r3 ∧
@@ -98,7 +98,8 @@ open Arm in
 /-- 32-bit ARM contract for
 `vg_sha256_finalize(state: *mut [u8; 96], count: u64, out: *mut [u8; 32], scratch: *mut [u64; 20])`:
 if the streaming state at `state` represents a message `m` of `count` bytes
-(modulo 2⁶⁴), writes the SHA-256 digest of `m` to `out`.
+(modulo 2⁶⁴), hashed from the initial hash value `iv`, writes the final hash
+value of `m` from `iv` to `out` (the SHA-256 digest if `iv` is `H0`).
 
 Under AAPCS, `state` is in `r0`, `count` in `r2:r3`, and `out` and `scratch`
 are the stack arguments 0 and 1. The code may read those arguments (8 bytes
@@ -118,8 +119,8 @@ def finalizeArm : Contract Arm.isa where
     args.Disjoint state ∧ args.Disjoint out ∧ args.Disjoint scratch ∧
     (s.gpr .r0).toNat + 96 ≤ 2 ^ 32 ∧ (stackArg s 0).toNat + 32 ≤ 2 ^ 32 ∧
     (stackArg s 1).toNat + 160 ≤ 2 ^ 32 ∧ s.sp.toNat + 8 ≤ 2 ^ 32
-  post s s' := ∀ m, Repr s.mem (State.addr (s.gpr .r0)) m → countArm s = BitVec.ofNat 64 m.length →
-    bytesAt s'.mem (State.addr (stackArg s 0)) 32 = Spec.Sha256.hash m
+  post s s' := ∀ iv m, ReprFrom iv s.mem (State.addr (s.gpr .r0)) m → countArm s = BitVec.ofNat 64 m.length →
+    bytesAt s'.mem (State.addr (stackArg s 0)) 32 = Spec.Sha256.finalHash iv m
   pub s₁ s₂ :=
     s₁.sp = s₂.sp ∧ s₁.gpr .r0 = s₂.gpr .r0 ∧ s₁.gpr .r2 = s₂.gpr .r2 ∧ s₁.gpr .r3 = s₂.gpr .r3 ∧
     stackArg s₁ 0 = stackArg s₂ 0 ∧ stackArg s₁ 1 = stackArg s₂ 1
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Md.lean b/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Md.lean
index 068ffd2c3..5527c5e33 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Md.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Arm/Stream/Md.lean
@@ -43,7 +43,7 @@ theorem update_verified : Verified Arm.target Impl.Sha256.Arm.Stream.update Proo
   have h := MdStream.Arm.Update.verified (name := "vg_sha256_compress") dims callee
     (VG.Taint.constantTime (A := taint) (MdStream.Arm.Update.τ₀ params)
       (fun _ _ h₁ h₂ hp => MdStream.Arm.Update.agree₀ h₁ h₂ hp) (by taint_decide))
-  Verified.of_implies h ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc, fun _ _ _ _ h => h, h.2.2⟩
+  Verified.of_implies h ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr hc, fun _ _ _ _ h => h, h.2.2⟩
 
 /-- A state satisfying `update`'s precondition. -/
 abbrev sat : State := MdStream.Arm.Update.sat params
@@ -57,7 +57,7 @@ theorem finalize_verified : Verified Arm.target Impl.Sha256.Arm.Stream.finalize
     (VG.Taint.constantTime (A := taint) (MdStream.Arm.Finalize.τ₀ params)
       (fun _ _ h₁ h₂ hp => MdStream.Arm.Finalize.agree₀ h₁ h₂ hp) (by taint_decide))
   Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
 
 /-- A state satisfying `finalize`'s precondition. -/
 abbrev sat : State := MdStream.Arm.Finalize.sat params
diff --git a/lean/VerifiedGarbage/Proof/Sha256/Stream.lean b/lean/VerifiedGarbage/Proof/Sha256/Stream.lean
index b63de7fbe..b1fa38fe3 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/Stream.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/Stream.lean
@@ -114,7 +114,7 @@ theorem bytesAt_writeBytes (m : Mem) (p : Addr) (r : Nat) (xs : List Byte) (h :
 /-! ## `Repr` -/
 
 theorem repr_nil {mem : Mem} {p : Addr} (h : stateAt mem p = H0) : Spec.Sha256.Repr mem p [] := by
-  simp [Spec.Sha256.Repr, h, compressList_zero, bytesAt]
+  simp [Spec.Sha256.Repr, Spec.Sha256.ReprFrom, h, compressList_zero, bytesAt]
 
 /-- Appending bytes that stay within the buffer. -/
 theorem repr_append_buf {mem mem' : Mem} {p : Addr} {m xs : List Byte} (hr : Spec.Sha256.Repr mem p m)
@@ -219,7 +219,7 @@ theorem hash_eq (m : List Byte) (nt : Nat)
   have hlen : (pad m).length / 64 = m.length / 64 + nt := by
     rw [hp]; simp only [List.length_append, List.length_replicate, lenBytes_length, List.length_singleton]
     omega
-  simp only [Spec.Sha256.hash]
+  simp only [Spec.Sha256.hash, Spec.Sha256.finalHash]
   rw [hlen, compressList_add, hp, compressList_append (by omega),
     List.drop_append_of_le_length (by omega)]
   simp only [List.append_assoc]
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean
index e2bb8ea28..9e9b7e509 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Contract.lean
@@ -6,7 +6,7 @@ import VerifiedGarbage.TCB.X86.Target
 
 **Untrusted**: the contracts the proofs are written against; the artifacts are emitted with the shared contracts of `Spec/`, which imply these (`Contract.Implies`). The contracts of the x86 (32-bit)
 implementations of the compression function and of streaming SHA-256
-(`init`/`update`/`finalize`, on the representation `Repr`), in terms of
+(`init`/`update`/`finalize`, on the representation `ReprFrom`), in terms of
 `Spec/Sha256.lean`.
 
 The shared contracts let the streaming functions write their own argument
@@ -83,8 +83,9 @@ open X86 in
 `vg_sha256_update(state: *mut [u8; 96], count: u64, data: *const u8, len: usize, scratch: *mut [u64; 20])`,
 whose arguments are on the stack (cdecl: `state`, the low and high words of
 `count`, `data`, `len`, `scratch`): if the streaming state at `state`
-represents a message `m` of `count` bytes (modulo 2⁶⁴), then afterwards it
-represents `m` followed by the `len` bytes at `data`.
+represents a message `m` of `count` bytes (modulo 2⁶⁴), hashed from any
+initial hash value `iv`, then afterwards it represents `m` followed by the
+`len` bytes at `data`, from `iv`.
 
 The code may read the arguments (24 bytes above the return address) and
 `data` (`len` bytes), and read and write `state` (96 bytes) and `scratch`
@@ -108,8 +109,8 @@ def updateX86 : Contract X86.isa where
     stack.Disjoint data ∧
     (arg s 0).toNat + 96 ≤ 2 ^ 32 ∧ (arg s 3).toNat + (arg s 4).toNat ≤ 2 ^ 32 ∧
     (arg s 5).toNat + 160 ≤ 2 ^ 32 ∧ 20 ≤ (s.gpr .esp).toNat ∧ (s.gpr .esp).toNat + 28 ≤ 2 ^ 32
-  post s s' := ∀ m, Repr s.mem ((arg s 0).setWidth 64) m → countX86 s = BitVec.ofNat 64 m.length →
-    Repr s'.mem ((arg s 0).setWidth 64)
+  post s s' := ∀ iv m, ReprFrom iv s.mem ((arg s 0).setWidth 64) m → countX86 s = BitVec.ofNat 64 m.length →
+    ReprFrom iv s'.mem ((arg s 0).setWidth 64)
       (m ++ bytesAt s.mem ((arg s 3).setWidth 64) (arg s 4).toNat)
   pub s₁ s₂ :=
     s₁.gpr .esp = s₂.gpr .esp ∧ ∀ i < 6, arg s₁ i = arg s₂ i
@@ -119,8 +120,9 @@ open X86 in
 `vg_sha256_finalize(state: *mut [u8; 96], count: u64, out: *mut [u8; 32], scratch: *mut [u64; 20])`,
 whose arguments are on the stack (cdecl: `state`, the low and high words of
 `count`, `out`, `scratch`): if the streaming state at `state` represents a
-message `m` of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of `m`
-to `out`.
+message `m` of `count` bytes (modulo 2⁶⁴), hashed from the initial hash value
+`iv`, writes the final hash value of `m` from `iv` to `out` (the SHA-256
+digest if `iv` is `H0`).
 
 The code may read and write the arguments (20 bytes above the return
 address, whose contents on exit are unspecified), `state` (96 bytes, whose
@@ -145,8 +147,8 @@ def finalizeX86 : Contract X86.isa where
     stack.Disjoint state ∧ stack.Disjoint out ∧ stack.Disjoint scratch ∧
     (arg s 0).toNat + 96 ≤ 2 ^ 32 ∧ (arg s 3).toNat + 32 ≤ 2 ^ 32 ∧
     (arg s 4).toNat + 160 ≤ 2 ^ 32 ∧ 20 ≤ (s.gpr .esp).toNat ∧ (s.gpr .esp).toNat + 24 ≤ 2 ^ 32
-  post s s' := ∀ m, Repr s.mem ((arg s 0).setWidth 64) m → countX86 s = BitVec.ofNat 64 m.length →
-    bytesAt s'.mem ((arg s 3).setWidth 64) 32 = Spec.Sha256.hash m
+  post s s' := ∀ iv m, ReprFrom iv s.mem ((arg s 0).setWidth 64) m → countX86 s = BitVec.ofNat 64 m.length →
+    bytesAt s'.mem ((arg s 3).setWidth 64) 32 = Spec.Sha256.finalHash iv m
   pub s₁ s₂ :=
     s₁.gpr .esp = s₂.gpr .esp ∧ ∀ i < 5, arg s₁ i = arg s₂ i
 
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean
index 98d5a4d79..d15d84ac9 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Shared.lean
@@ -210,7 +210,7 @@ theorem update_verified : Verified X86.target Impl.Sha256.X86.Stream.update Proo
   rw [update_eq] at ct ⊢
   have h := MdStream.X86.Update.verified (name := "vg_sha256_compress") dims callee ct
   exact Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc, fun _ _ _ _ h => h, h.2.2⟩
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr hc, fun _ _ _ _ h => h, h.2.2⟩
 
 /-- A state satisfying `update`'s precondition. -/
 abbrev sat : State := MdStream.X86.Update.sat params 160
@@ -227,7 +227,7 @@ theorem finalize_verified : Verified X86.target Impl.Sha256.X86.Stream.finalize
   rw [finalize_eq] at ct ⊢
   have h := MdStream.X86.Finalize.verified (name := "vg_sha256_compress") dims shape callee ct
   exact Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
 
 /-- A state satisfying `finalize`'s precondition. -/
 abbrev sat : State := MdStream.X86.Finalize.sat params 160
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean
index 824da9bd9..e1689f077 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86/Stream/Variant.lean
@@ -22,7 +22,7 @@ theorem update_of (ct : ConstantTime isa (updK (P := params) md 160).pre
     Verified X86.target (Impl.MdStream.X86.update params name code) Proof.Sha256.updateX86 := by
   have h := MdStream.X86.Update.verified (name := name) dims hcomp ct
   exact Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc,
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr hc,
       fun _ _ _ _ h => h, h.2.2⟩
 
 /-- Any verified compressor gives the same SHA-256 finalization contract. -/
@@ -31,7 +31,7 @@ theorem finalize_of (ct : ConstantTime isa (finK (P := params) md 160).pre
     Verified X86.target (Impl.MdStream.X86.finalize params name code) Proof.Sha256.finalizeX86 := by
   have h := MdStream.X86.Finalize.verified (name := name) dims shape hcomp ct
   exact Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc,
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr trivial hc,
       fun _ _ _ _ h => h, h.2.2⟩
 
 end VG.Proof.Sha256.X86.Stream
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean
index 9fbdceb39..36584fdad 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Contract.lean
@@ -56,8 +56,8 @@ open X86_64 in
 /-- x86-64 contract for
 `vg_sha256_update(state: *mut [u8; 96], count: u64, data: *const u8, len: usize, scratch: *mut [u64; 76])`:
 if the streaming state at `state` represents a message `m` of `count` bytes
-(modulo 2⁶⁴), then afterwards it represents `m` followed by the `len` bytes at
-`data`.
+(modulo 2⁶⁴), hashed from any initial hash value `iv`, then afterwards it
+represents `m` followed by the `len` bytes at `data`, from `iv`.
 
 The code may read `data` (`len` bytes) and read and write `state` (96
 bytes) and `scratch` (608 bytes, whose contents on exit are unspecified).
@@ -77,8 +77,8 @@ def updateX86_64 : Contract X86_64.isa where
     state.Disjoint scratch ∧ data.Disjoint state ∧ data.Disjoint scratch ∧
     ret.Disjoint state ∧ ret.Disjoint scratch ∧
     stack.Disjoint state ∧ stack.Disjoint data ∧ stack.Disjoint scratch
-  post s s' := ∀ m, Repr s.mem (s.gpr .rdi) m → s.gpr .rsi = BitVec.ofNat 64 m.length →
-    Repr s'.mem (s.gpr .rdi) (m ++ bytesAt s.mem (s.gpr .rdx) (s.gpr .rcx).toNat)
+  post s s' := ∀ iv m, ReprFrom iv s.mem (s.gpr .rdi) m → s.gpr .rsi = BitVec.ofNat 64 m.length →
+    ReprFrom iv s'.mem (s.gpr .rdi) (m ++ bytesAt s.mem (s.gpr .rdx) (s.gpr .rcx).toNat)
   pub s₁ s₂ :=
     s₁.gpr .rdi = s₂.gpr .rdi ∧ s₁.gpr .rsi = s₂.gpr .rsi ∧ s₁.gpr .rdx = s₂.gpr .rdx ∧
     s₁.gpr .rcx = s₂.gpr .rcx ∧ s₁.gpr .r8 = s₂.gpr .r8 ∧ s₁.gpr .rsp = s₂.gpr .rsp
@@ -87,7 +87,8 @@ open X86_64 in
 /-- x86-64 contract for
 `vg_sha256_finalize(state: *mut [u8; 96], count: u64, out: *mut [u8; 32], scratch: *mut [u64; 76])`:
 if the streaming state at `state` represents a message `m` of `count` bytes
-(modulo 2⁶⁴), writes the SHA-256 digest of `m` to `out`.
+(modulo 2⁶⁴), hashed from the initial hash value `iv`, writes the final hash
+value of `m` from `iv` to `out` (the SHA-256 digest if `iv` is `H0`).
 
 The code may read and write `state` (96 bytes, whose contents on exit are
 unspecified), `out` (32 bytes) and `scratch` (608 bytes, whose contents on
@@ -106,8 +107,8 @@ def finalizeX86_64 : Contract X86_64.isa where
     state.Disjoint out ∧ state.Disjoint scratch ∧ out.Disjoint scratch ∧
     ret.Disjoint state ∧ ret.Disjoint out ∧ ret.Disjoint scratch ∧
     stack.Disjoint state ∧ stack.Disjoint out ∧ stack.Disjoint scratch
-  post s s' := ∀ m, Repr s.mem (s.gpr .rdi) m → s.gpr .rsi = BitVec.ofNat 64 m.length →
-    bytesAt s'.mem (s.gpr .rdx) 32 = Spec.Sha256.hash m
+  post s s' := ∀ iv m, ReprFrom iv s.mem (s.gpr .rdi) m → s.gpr .rsi = BitVec.ofNat 64 m.length →
+    bytesAt s'.mem (s.gpr .rdx) 32 = Spec.Sha256.finalHash iv m
   pub s₁ s₂ :=
     s₁.gpr .rdi = s₂.gpr .rdi ∧ s₁.gpr .rsi = s₂.gpr .rsi ∧ s₁.gpr .rdx = s₂.gpr .rdx ∧
     s₁.gpr .rcx = s₂.gpr .rcx ∧ s₁.gpr .rsp = s₂.gpr .rsp
diff --git a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Stream/Md.lean b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Stream/Md.lean
index 72db32e5b..b8ba26155 100644
--- a/lean/VerifiedGarbage/Proof/Sha256/X86_64/Stream/Md.lean
+++ b/lean/VerifiedGarbage/Proof/Sha256/X86_64/Stream/Md.lean
@@ -52,7 +52,7 @@ include hf
 theorem verified_of (hm : (update f).allInstrs (fun i => !loadsMxcsr i) = true) :
     Verified X86_64.target (update f) Proof.Sha256.updateX86_64 :=
   have h := MdStream.X86_64.Update.verified dims taints (callee hf) hm
-  Verified.of_implies h ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr hc, fun _ _ _ _ h => h, h.2.2⟩
+  Verified.of_implies h ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr hc, fun _ _ _ _ h => h, h.2.2⟩
 
 omit hf
 
@@ -73,7 +73,7 @@ theorem correct {s₀ : State} (hp : MdStream.X86_64.Finalize.Pre params s₀) :
     WP isa (finalize f) s₀ fun s' => gprPreserved s₀ s' ∧ Proof.Sha256.finalizeX86_64.post s₀ s' ∧
       s'.gpr .rdi = s₀.gpr .rdi ∧ s'.gpr .rcx = s₀.gpr .rcx :=
   (MdStream.X86_64.Finalize.correct dims shape (callee hf) hp).mono fun _ ⟨g, h, di, cx⟩ =>
-    ⟨g, fun m hr hc => h Spec.Sha256.H0 m hr trivial hc, di, cx⟩
+    ⟨g, fun iv m hr hc => h iv m hr trivial hc, di, cx⟩
 
 theorem constantTime :
     ConstantTime isa Proof.Sha256.finalizeX86_64.pre Proof.Sha256.finalizeX86_64.pub (finalize f) :=
@@ -84,7 +84,7 @@ theorem verified_of (hm : (finalize f).allInstrs (fun i => !loadsMxcsr i) = true
     Verified X86_64.target (finalize f) Proof.Sha256.finalizeX86_64 :=
   have h := MdStream.X86_64.Finalize.verified dims shape taints (callee hf) hm
   Verified.of_implies h
-    ⟨fun _ h => h, fun _ _ _ h m hr hc => h Spec.Sha256.H0 m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
+    ⟨fun _ h => h, fun _ _ _ h iv m hr hc => h iv m hr trivial hc, fun _ _ _ _ h => h, h.2.2⟩
 
 omit hf
 
diff --git a/lean/VerifiedGarbage/Spec/Sha256.lean b/lean/VerifiedGarbage/Spec/Sha256.lean
index 0f48217c4..373cf36c2 100644
--- a/lean/VerifiedGarbage/Spec/Sha256.lean
+++ b/lean/VerifiedGarbage/Spec/Sha256.lean
@@ -1,19 +1,23 @@
 import VerifiedGarbage.TCB.Mem
 
 /-!
-# SHA-256 (FIPS 180-4)
-
-**Trusted** (as every file in `Spec/`). The hash function SHA-256, transcribed
-from FIPS 180-4, *Secure Hash Standard* (August 2015); section numbers below
-refer to it. Messages are sequences of bytes (the standard allows any number
-of bits); every multi-byte quantity is big-endian (§3.1).
-
-The primitives implemented in assembly are the compression function over a
-run of whole blocks (`compressBlocks`), and the streaming (incremental)
-interface: initialize, absorb message bytes, pad and output the digest, on a
-streaming state that `Repr` relates to the message absorbed so far. Their
-contracts on each target, which say how the code's arguments and memory
-relate to these definitions, are in `Spec/Sha256/<Target>.lean`.
+# SHA-224 and SHA-256 (FIPS 180-4)
+
+**Trusted** (as every file in `Spec/`). The hash functions SHA-224 and
+SHA-256, transcribed from FIPS 180-4, *Secure Hash Standard* (August 2015);
+section numbers below refer to it. Messages are sequences of bytes (the
+standard allows any number of bits); every multi-byte quantity is big-endian
+(§3.1).
+
+Both functions share the SHA-256 compression function and differ only in the
+initial hash value and in how much of the final hash value is output (§6.2,
+§6.3). The primitives implemented in assembly are the compression function
+over a run of whole blocks (`compressBlocks`), and the streaming
+(incremental) interface: initialize with either initial hash value, absorb
+message bytes, and pad and output the final hash value, on a streaming state
+that `ReprFrom` relates to the message absorbed so far. Their contracts,
+which say how the code's arguments and memory relate to these definitions,
+are in `Spec/Sha256/Contract.lean`.
 -/
 
 namespace VG.Spec.Sha256
@@ -48,7 +52,7 @@ def ssig0 (x : Word) : Word := x.rotateRight 7 ^^^ x.rotateRight 18 ^^^ x >>> 3
 /-- `σ₁(x) = ROTR¹⁷(x) ⊕ ROTR¹⁹(x) ⊕ SHR¹⁰(x)` -/
 def ssig1 (x : Word) : Word := x.rotateRight 17 ^^^ x.rotateRight 19 ^^^ x >>> 10
 
-/-! ## Constants (§4.2.2) and the initial hash value (§5.3.3) -/
+/-! ## Constants (§4.2.2) and initial hash values (§5.3.2, §5.3.3) -/
 
 /-- The sixty-four constants `K₀ … K₆₃`. -/
 def Ks : List Word := [
@@ -64,10 +68,14 @@ def Ks : List Word := [
 /-- `Kₜ` -/
 def K (t : Nat) : Word := Ks.getD t 0
 
-/-- `H⁽⁰⁾` -/
+/-- `H⁽⁰⁾` for SHA-256 (§5.3.3). -/
 def H0 : HashValue :=
   #v[0x6a09e667, 0xbb67ae85, 0x3c6ef372, 0xa54ff53a, 0x510e527f, 0x9b05688c, 0x1f83d9ab, 0x5be0cd19]
 
+/-- `H⁽⁰⁾` for SHA-224 (§5.3.2). -/
+def H0_224 : HashValue :=
+  #v[0xc1059ed8, 0x367cd507, 0x3070dd17, 0xf70e5939, 0xffc00b31, 0x68581511, 0x64f98fa7, 0xbefa4fa4]
+
 /-! ## Preprocessing (§5.1.1, §5.2.1) -/
 
 /-- The big-endian bytes of a word. -/
@@ -77,7 +85,8 @@ def wordBytes (x : Word) : List Byte :=
 /-- §5.1.1: append the bit `1`, then the least number of `0` bits that makes
 the length `≡ 448 (mod 512)`, then the message length `ℓ` in bits as a 64-bit
 big-endian integer. For a message of bytes, the `1` bit and the first seven
-`0` bits are the byte `0x80`. (SHA-256 is only defined for `ℓ < 2⁶⁴`.) -/
+`0` bits are the byte `0x80`. (SHA-224 and SHA-256 are only defined for
+`ℓ < 2⁶⁴`.) -/
 def pad (m : List Byte) : List Byte :=
   let ℓ : BitVec 64 := BitVec.ofNat 64 (8 * m.length)
   m ++ [0x80] ++ List.replicate ((119 - m.length % 64) % 64) 0 ++
@@ -126,10 +135,17 @@ def compress (H : HashValue) (M : Block) : HashValue :=
 def compressList (H : HashValue) (p : List Byte) (n : Nat) : HashValue :=
   (List.range n).foldl (fun H i => compress H (parseBlock fun k => p.getD (64 * i + k) 0)) H
 
-/-- The SHA-256 digest of a message: `H⁽ᴺ⁾` as 32 big-endian bytes. -/
-def hash (m : List Byte) : List Byte :=
+/-- §6.2: the final hash value `H⁽ᴺ⁾` of a message, starting from `iv`, as
+32 big-endian bytes. -/
+def finalHash (iv : HashValue) (m : List Byte) : List Byte :=
   let p := pad m
-  (compressList H0 p (p.length / 64)).toList.flatMap wordBytes
+  (compressList iv p (p.length / 64)).toList.flatMap wordBytes
+
+/-- The SHA-256 digest (§6.2): all of `H⁽ᴺ⁾`, 32 bytes. -/
+def hash (m : List Byte) : List Byte := finalHash H0 m
+
+/-- The SHA-224 digest (§6.3): the left-most 224 bits of `H⁽ᴺ⁾`, 28 bytes. -/
+def sha224 (m : List Byte) : List Byte := (finalHash H0_224 m).take 28
 
 /-! ## The compression function on memory
 
@@ -157,18 +173,25 @@ def bytesAt (m : Mem) (p : Addr) (n : Nat) : List Byte :=
 The streaming primitives hash a message given in pieces. Their state is 96
 bytes: the hash value after the message's whole blocks (stored as by
 `stateAt`), followed by a 64-byte buffer holding the bytes of the message
-after its last whole block. The length of the message is not part of the
-state: the caller keeps it (in bytes, modulo 2⁶⁴) and passes it to every
-call. (Lengths are public, so it may live anywhere; and `pad` only uses the
-length modulo 2⁶⁴ bits, so this suffices even beyond SHA-256's limit of
-`ℓ < 2⁶⁴` bits.) -/
-
-/-- The streaming state at `p` (96 bytes) represents the message `m`: its hash
-value is `H⁽⁰⁾` updated with the `⌊|m| / 64⌋` whole blocks of `m`, and its
-buffer starts with the remaining `|m| mod 64` bytes of `m`. The rest of the
-buffer is unspecified. -/
-def Repr (mem : Mem) (p : Addr) (m : List Byte) : Prop :=
-  stateAt mem p = compressList H0 m (m.length / 64) ∧
+after its last whole block. SHA-224 and SHA-256 share the state and differ
+only in the initial hash value it starts from, and in how much of the final
+hash value is output.
+
+The length of the message is not part of the state: the caller keeps it (in
+bytes, modulo 2⁶⁴) and passes it to every call. (Lengths are public, so it
+may live anywhere; and `pad` only uses the length modulo 2⁶⁴ bits, so this
+suffices even beyond the limit of `ℓ < 2⁶⁴` bits.) -/
+
+/-- The streaming state at `p` (96 bytes) represents the message `m`, hashed
+from the initial hash value `iv`: its hash value is `iv` updated with the
+`⌊|m| / 64⌋` whole blocks of `m`, and its buffer starts with the remaining
+`|m| mod 64` bytes of `m`. The rest of the buffer is unspecified. -/
+def ReprFrom (iv : HashValue) (mem : Mem) (p : Addr) (m : List Byte) : Prop :=
+  stateAt mem p = compressList iv m (m.length / 64) ∧
   bytesAt mem (p + 32) (m.length % 64) = m.drop (64 * (m.length / 64))
 
+/-- The streaming state at `p` represents the message `m`, hashed by SHA-256
+(from `H0`). -/
+def Repr (mem : Mem) (p : Addr) (m : List Byte) : Prop := ReprFrom H0 mem p m
+
 end VG.Spec.Sha256
diff --git a/lean/VerifiedGarbage/Spec/Sha256/Contract.lean b/lean/VerifiedGarbage/Spec/Sha256/Contract.lean
index 870695793..deb98b3c4 100644
--- a/lean/VerifiedGarbage/Spec/Sha256/Contract.lean
+++ b/lean/VerifiedGarbage/Spec/Sha256/Contract.lean
@@ -5,8 +5,9 @@ import VerifiedGarbage.TCB.Artifact
 # SHA-256: the contracts, on every target
 
 **Trusted** (as every file in `Spec/`). The contracts of the compression
-function and of streaming SHA-256 (`init`/`update`/`finalize`, on the
-representation `Repr`), in terms of `Spec/Sha256.lean`, for any target:
+function and of streaming SHA-224 and SHA-256 (`init`/`update`/`finalize`,
+on the representation `ReprFrom`), in terms of `Spec/Sha256.lean`, for any
+target:
 `A` is the target's calling convention. The signatures fix where the
 arguments are, the memory each function may access, disjointness, and that
 the pointers and lengths are public (see `TCB/Sig.lean`); the contracts add
@@ -15,6 +16,9 @@ the postconditions and which other arguments are public. `update` and
 convention allows it (`writeArgs`), to pass arguments to the code they
 inline.
 
+SHA-224 and SHA-256 share `update` and `finalize`, which hold for a state
+hashed from any initial hash value; each has its own `init`.
+
 `update` and `finalize` take the number of bytes of stack below the stack pointer that
 an implementation's calls use (`stack`, see `Sig.contract`), 0 for one that
 makes no call: it depends on the target, and on which functions the
@@ -71,6 +75,26 @@ def initApi : Api where
     buffered partial block (`VG.Spec.Sha256.Repr`)."
   safety := []
 
+/-- `vg_sha224_init(state: *mut [u8; 96])`, with `vg_sha256_init`'s signature
+(`initSig`): makes the streaming state at `state` represent the empty message,
+hashed from SHA-224's initial hash value `H0_224`. -/
+def init224Contract {M : ISA} (A : Abi M) : Contract M :=
+  initSig.contract A (post := fun state _ m' _ => ReprFrom H0_224 m' state [])
+
+/-- `vg_sha224_init` on every target. -/
+def init224Api : Api where
+  module := "sha256"
+  name := "vg_sha224_init"
+  sig := initSig
+  contracts := some fun A _ => init224Contract A
+  summary := "Starts a SHA-224 computation: makes the SHA-256 streaming state `*state` represent \
+    the empty message, hashed from the initial hash value of SHA-224 \
+    (`VG.Spec.Sha256.H0_224`). Continue with `vg_sha256_update` and `vg_sha256_finalize`, and \
+    take the first 28 bytes of the final hash value as the digest.\n\n\
+    Contract: `VG.Spec.Sha256.init224Contract`. The streaming state is the hash value followed by \
+    a buffered partial block (`VG.Spec.Sha256.ReprFrom`)."
+  safety := []
+
 /-- `vg_sha256_update(state: *mut [u8; 96], count: u64, data: *const u8, len: usize, scratch: *mut [u64; 76])`.
 `count` is public; `scratch` is working space. -/
 def updateSig : Sig where
@@ -78,12 +102,13 @@ def updateSig : Sig where
     ("data", .slice false .u8 "len"), ("scratch", .array true .u64 76)]
 
 /-- If the streaming state at `state` represents a message `msg` of `count`
-bytes (modulo 2⁶⁴), then afterwards it represents `msg` followed by the `len`
-bytes at `data`. The state and the data are secret. -/
+bytes (modulo 2⁶⁴), hashed from any initial hash value, then afterwards it
+represents `msg` followed by the `len` bytes at `data`, from the same one.
+The state and the data are secret. -/
 def updateContract {M : ISA} (A : Abi M) (stack : Nat := 0) : Contract M :=
   updateSig.contract A (post := fun state count data len _scratch m m' _ =>
-    ∀ msg, Repr m state msg → count = BitVec.ofNat 64 msg.length →
-      Repr m' state (msg ++ bytesAt m data len.toNat))
+    ∀ iv msg, ReprFrom iv m state msg → count = BitVec.ofNat 64 msg.length →
+      ReprFrom iv m' state (msg ++ bytesAt m data len.toNat))
     (writeArgs := true)
     (stack := stack)
 
@@ -94,9 +119,9 @@ def updateApi : Api where
   sig := updateSig
   writeArgs := true
   contracts := some fun A stack => updateContract A stack
-  summary := "Absorbs data into a SHA-256 computation: if the streaming state `*state` represents \
-    a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` \
-    bytes at `data`.\n\n\
+  summary := "Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` \
+    represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed \
+    by the `len` bytes at `data`.\n\n\
     Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` \
     may affect timing, not the state or the data."
   safety := ["The contents of `scratch` on return are unspecified."]
@@ -109,11 +134,14 @@ def finalizeSig : Sig where
     ("out", .array true .u8 32), ("scratch", .array true .u64 76)]
 
 /-- If the streaming state at `state` represents a message `msg` of `count`
-bytes (modulo 2⁶⁴), writes the SHA-256 digest of `msg` to `out`. The state is
-secret. -/
+bytes (modulo 2⁶⁴), hashed from the initial hash value `iv`, writes the final
+hash value `H⁽ᴺ⁾` of `msg` from `iv` (32 bytes; `finalHash iv msg`) to `out`:
+the SHA-256 digest of `msg` if `iv` is `H0`, and the SHA-224 digest followed
+by four more bytes if `iv` is `H0_224`. The state is secret. -/
 def finalizeContract {M : ISA} (A : Abi M) (stack : Nat := 0) : Contract M :=
   finalizeSig.contract A (post := fun state count out _scratch m m' _ =>
-    ∀ msg, Repr m state msg → count = BitVec.ofNat 64 msg.length → bytesAt m' out 32 = hash msg)
+    ∀ iv msg, ReprFrom iv m state msg → count = BitVec.ofNat 64 msg.length →
+      bytesAt m' out 32 = finalHash iv msg)
     (writeArgs := true)
     (stack := stack)
 
@@ -124,8 +152,10 @@ def finalizeApi : Api where
   sig := finalizeSig
   writeArgs := true
   contracts := some fun A stack => finalizeContract A stack
-  summary := "Finishes a SHA-256 computation: if the streaming state `*state` represents a message \
-    of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.\n\n\
+  summary := "Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` \
+    represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes \
+    the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of \
+    it; the SHA-224 digest is its first 28 bytes.\n\n\
     Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may \
     affect timing, not the state."
   safety := [
diff --git a/src/asm/aarch64/sha256.rs b/src/asm/aarch64/sha256.rs
index 3d9336e81..f632e6240 100644
--- a/src/asm/aarch64/sha256.rs
+++ b/src/asm/aarch64/sha256.rs
@@ -3007,7 +3007,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_compress_sha2(state: *mut [u32; 8], bl
     )
 }
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -3138,7 +3138,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_update(state: *mut [u8; 96], count: u6
     )
 }
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///
@@ -3248,7 +3248,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_finalize(state: *mut [u8; 96], count:
 /// The CPU features `vg_sha256_update_sha2` requires (`Artifact.features`).
 pub(crate) const VG_SHA256_UPDATE_SHA2_FEATURES: &[&str] = &["sha2"];
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -3385,7 +3385,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_update_sha2(state: *mut [u8; 96], coun
 /// The CPU features `vg_sha256_finalize_sha2` requires (`Artifact.features`).
 pub(crate) const VG_SHA256_FINALIZE_SHA2_FEATURES: &[&str] = &["sha2"];
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///
diff --git a/src/asm/arm/sha256.rs b/src/asm/arm/sha256.rs
index 674959dd0..ce598e523 100644
--- a/src/asm/arm/sha256.rs
+++ b/src/asm/arm/sha256.rs
@@ -2407,7 +2407,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_init(state: *mut [u8; 96]) {
     )
 }
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -2548,7 +2548,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_update(state: *mut [u8; 96], count: u6
     )
 }
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///
diff --git a/src/asm/x86/sha256.rs b/src/asm/x86/sha256.rs
index c8a1f786c..73703777b 100644
--- a/src/asm/x86/sha256.rs
+++ b/src/asm/x86/sha256.rs
@@ -3397,7 +3397,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_compress(state: *mut [u32; 8], blocks:
     )
 }
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -3538,7 +3538,7 @@ pub(crate) unsafe extern "C" fn vg_sha256_update(state: *mut [u8; 96], count: u6
     )
 }
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///
diff --git a/src/asm/x86_64/sha256.rs b/src/asm/x86_64/sha256.rs
index 38e09d3ae..3a8af49b2 100644
--- a/src/asm/x86_64/sha256.rs
+++ b/src/asm/x86_64/sha256.rs
@@ -6966,7 +6966,7 @@ pub(crate) unsafe extern "sysv64" fn vg_sha256_compress_avx2(state: *mut [u32; 8
     )
 }
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -7098,7 +7098,7 @@ pub(crate) unsafe extern "sysv64" fn vg_sha256_update(state: *mut [u8; 96], coun
     )
 }
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///
@@ -7215,7 +7215,7 @@ pub(crate) unsafe extern "sysv64" fn vg_sha256_finalize(state: *mut [u8; 96], co
 /// The CPU features `vg_sha256_update_avx2` requires (`Artifact.features`).
 pub(crate) const VG_SHA256_UPDATE_AVX2_FEATURES: &[&str] = &["avx", "avx2", "bmi1", "bmi2"];
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -7351,7 +7351,7 @@ pub(crate) unsafe extern "sysv64" fn vg_sha256_update_avx2(state: *mut [u8; 96],
 /// The CPU features `vg_sha256_finalize_avx2` requires (`Artifact.features`).
 pub(crate) const VG_SHA256_FINALIZE_AVX2_FEATURES: &[&str] = &["avx", "avx2", "bmi1", "bmi2"];
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///
@@ -7469,7 +7469,7 @@ pub(crate) unsafe extern "sysv64" fn vg_sha256_finalize_avx2(state: *mut [u8; 96
 /// The CPU features `vg_sha256_update_shani` requires (`Artifact.features`).
 pub(crate) const VG_SHA256_UPDATE_SHANI_FEATURES: &[&str] = &["sha", "ssse3"];
 
-/// Absorbs data into a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
+/// Absorbs data into a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), it then represents that message followed by the `len` bytes at `data`.
 ///
 /// Contract: `VG.Spec.Sha256.updateContract`. Constant time: only the pointers, `count` and `len` may affect timing, not the state or the data.
 ///
@@ -7605,7 +7605,7 @@ pub(crate) unsafe extern "sysv64" fn vg_sha256_update_shani(state: *mut [u8; 96]
 /// The CPU features `vg_sha256_finalize_shani` requires (`Artifact.features`).
 pub(crate) const VG_SHA256_FINALIZE_SHANI_FEATURES: &[&str] = &["sha", "ssse3"];
 
-/// Finishes a SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), writes the SHA-256 digest of that message to `*out`.
+/// Finishes a SHA-224 or SHA-256 computation: if the streaming state `*state` represents a message of `count` bytes (modulo 2⁶⁴), hashed from an initial hash value, writes the final hash value `H⁽ᴺ⁾` of that message (32 bytes) to `*out`. The SHA-256 digest is all of it; the SHA-224 digest is its first 28 bytes.
 ///
 /// Contract: `VG.Spec.Sha256.finalizeContract`. Constant time: only the pointers and `count` may affect timing, not the state.
 ///