val mk_init: a:sha2_alg -> init_st (| a, () |)
let mk_init a st =
  [@inline_let]
  let st: mb_state_32 a = coerce_to_mb_state a st in

  Lib.IntVector.reveal_vec_1 (word_t a);
  Hacl.SHA2.Scalar32.init #a st;
  Hacl.Spec.SHA2.Equiv.init_lemma_l a Vec.M32 0;
  state_spec_v_lemma a (Vec.init a Vec.M32)
val mk_init: a:sha2_alg -> init_st (| a, () |)
let mk_init a st =
[@@ inline_let ]let st:mb_state_32 a = coerce_to_mb_state a st in
Lib.IntVector.reveal_vec_1 (word_t a);
Hacl.SHA2.Scalar32.init #a st;
Hacl.Spec.SHA2.Equiv.init_lemma_l a Vec.M32 0;
state_spec_v_lemma a (Vec.init a Vec.M32)
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.Definitions.state Prims.Mkdtuple2 Spec.Hash.Definitions.hash_alg Hacl.Hash.Definitions.m_spec Hacl.Hash.SHA2.state_spec_v_lemma Hacl.Spec.SHA2.Vec.init Hacl.Spec.SHA2.Vec.M32 Prims.unit Hacl.Spec.SHA2.Equiv.init_lemma_l Hacl.SHA2.Scalar32.init Lib.IntVector.reveal_vec_1 Spec.Hash.Definitions.word_t Hacl.Hash.SHA2.mb_state_32 Hacl.Hash.SHA2.coerce_to_mb_state
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
let coerce_to_state (a:sha2_alg) (b:mb_state_32 a) : state (| a, () |)
  = Lib.IntVector.reveal_vec_1 (word_t a);
    b

inline_for_extraction noextract
let coerce_to_mb_state (a:sha2_alg) (b:state (| a, () |)) : mb_state_32 a
  = Lib.IntVector.reveal_vec_1 (word_t a);
    b

val state_spec_v_lemma (a:sha2_alg) (st:Vec.state_spec a Vec.M32) : Lemma
  (Lib.IntVector.reveal_vec_1 (word_t a);
   st `Seq.equal` Lib.Sequence.index (Vec.state_spec_v st) 0)

let state_spec_v_lemma a st =
  let open Lib.Sequence in
  let open Lib.IntVector in
  reveal_vec_v_1 st.[0];
  reveal_vec_v_1 st.[1];
  reveal_vec_v_1 st.[2];
  reveal_vec_v_1 st.[3];
  reveal_vec_v_1 st.[4];
  reveal_vec_v_1 st.[5];
  reveal_vec_v_1 st.[6];
  reveal_vec_v_1 st.[7];
  reveal_vec_1 (word_t a);
  eq_intro #(word a) #8 (Vec.state_spec_v st).[0] st

inline_for_extraction noextract
val mk_init: a:sha2_alg -> init_st (| a, () |)
val mk_init: a:sha2_alg -> init_st (| a, () |)
a: Spec.Hash.Definitions.sha2_alg -> Hacl.Hash.Definitions.init_st (| a, () |)