val coerce_to_state (a: sha2_alg) (b: mb_state_32 a) : state (| a, () |)
let coerce_to_state (a:sha2_alg) (b:mb_state_32 a) : state (| a, () |)
  = Lib.IntVector.reveal_vec_1 (word_t a);
    b
val coerce_to_state (a: sha2_alg) (b: mb_state_32 a) : state (| a, () |)
let coerce_to_state (a: sha2_alg) (b: mb_state_32 a) : state (| a, () |) =
Lib.IntVector.reveal_vec_1 (word_t a);
b
Hacl.Hash.SHA2.fst.checked
Spec.SHA2.fst.checked Spec.Hash.MD.fst.checked Spec.Hash.Incremental.fst.checked Spec.Hash.Definitions.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.UpdateMulti.Lemmas.fsti.checked Lib.UpdateMulti.fst.checked Lib.Sequence.Lemmas.fsti.checked Lib.Sequence.fsti.checked Lib.NTuple.fsti.checked Lib.MultiBuffer.fst.checked Lib.IntVector.fsti.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Spec.SHA2.Vec.fst.checked Hacl.Spec.SHA2.EquivScalar.fsti.checked Hacl.Spec.SHA2.Equiv.fst.checked Hacl.Spec.SHA2.fst.checked Hacl.SHA2.Scalar32.fst.checked Hacl.Impl.SHA2.Generic.fst.checked Hacl.Impl.SHA2.Core.fst.checked Hacl.Hash.PadFinish.fsti.checked Hacl.Hash.MD.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Hacl.Hash.SHA2.fst
Spec.Hash.Definitions.sha2_alg Hacl.Hash.SHA2.mb_state_32 Prims.unit Lib.IntVector.reveal_vec_1 Spec.Hash.Definitions.word_t Hacl.Hash.Definitions.state Prims.Mkdtuple2 Spec.Hash.Definitions.hash_alg Hacl.Hash.Definitions.m_spec
module Hacl.Hash.SHA2

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack

module B = LowStar.Buffer

open Hacl.Hash.Definitions
open Spec.Hash.Definitions

open Lib.MultiBuffer
open Lib.NTuple

module Vec = Hacl.Spec.SHA2.Vec

// To prove we are properly defining init
friend Spec.Agile.Hash
// To prove we are properly defining update_last
friend Spec.Hash.Incremental
// To know the definition of init
friend Spec.SHA2

#set-options "--fuel 0 --ifuel 0 --z3rlimit 100"

inline_for_extraction noextract
let mb_state_32 a = Hacl.Impl.SHA2.Core.state_t a Hacl.Spec.SHA2.Vec.M32

#push-options "--ifuel 1"

inline_for_extraction noextract
val coerce_to_state (a: sha2_alg) (b: mb_state_32 a) : state (| a, () |)
a: Spec.Hash.Definitions.sha2_alg -> b: Hacl.Hash.SHA2.mb_state_32 a
  -> Hacl.Hash.Definitions.state (| a, () |)