Spec: SHA-224, and SHA-256's update and finalize for any initial hash value

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>

docs/algorithms/sha224.toml

@@ -0,0 +1,5 @@
+name = "SHA-224"
+family = "Hashes"
+specs = ["Sha256"]
+modules = ["src/hashes/sha224.rs"]
+asm = ["sha256"]

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 -/
 

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

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

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

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

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

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

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]

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
 

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

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