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
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
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.Spec.SHA2.Vec.state_spec Hacl.Spec.SHA2.Vec.M32 Lib.Sequence.eq_intro Spec.Hash.Definitions.word Lib.Sequence.op_String_Access Hacl.Spec.SHA2.Vec.words_state' Hacl.Spec.SHA2.Vec.lanes Hacl.Spec.SHA2.Vec.state_spec_v Prims.unit Lib.IntVector.reveal_vec_1 Spec.Hash.Definitions.word_t Lib.IntVector.reveal_vec_v_1 Hacl.Spec.SHA2.Vec.element_t
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)
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)
a: Spec.Hash.Definitions.sha2_alg -> st: Hacl.Spec.SHA2.Vec.state_spec a Hacl.Spec.SHA2.Vec.M32
  -> FStar.Pervasives.Lemma
    (ensures
      ([@@ FStar.Pervasives.inline_let ]let _ =
          Lib.IntVector.reveal_vec_1 (Spec.Hash.Definitions.word_t a)
        in
        FStar.Seq.Base.equal st (Lib.Sequence.index (Hacl.Spec.SHA2.Vec.state_spec_v st) 0)))