let sha224_update8 = update #SHA2_224 #M256
let sha224_update8 =
update #SHA2_224 #M256
Hacl.SHA2.Vec256.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fsti.checked prims.fst.checked Lib.NTuple.fsti.checked Lib.MultiBuffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.SHA2.Vec.fst.checked Hacl.Spec.SHA2.Equiv.fst.checked Hacl.Impl.SHA2.Generic.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.All.fst.checked FStar.HyperStack.fst.checked
Hacl.SHA2.Vec256.fst
Hacl.Impl.SHA2.Generic.update Spec.Hash.Definitions.SHA2_224 Hacl.Spec.SHA2.Vec.M256
module Hacl.SHA2.Vec256

open FStar.HyperStack
open FStar.HyperStack.All
open FStar.Mul

open Lib.IntTypes
open Lib.NTuple
open Lib.Buffer
open Lib.MultiBuffer

open Spec.Hash.Definitions
open Hacl.Spec.SHA2.Vec
open Hacl.Impl.SHA2.Generic

module ST = FStar.HyperStack.ST
module Spec = Spec.Agile.Hash
module SpecVec = Hacl.Spec.SHA2.Vec

#set-options "--z3rlimit 50 --fuel 0 --ifuel 0"
val sha224_update8 : Hacl.Impl.SHA2.Generic.update_vec_t Spec.Hash.Definitions.SHA2_224 Hacl.Spec.SHA2.Vec.M256
Hacl.Impl.SHA2.Generic.update_vec_t Spec.Hash.Definitions.SHA2_224 Hacl.Spec.SHA2.Vec.M256