val alloca_512: alloca_st (|SHA2_512, ()|)
let alloca_512 = mk_alloca SHA2_512
val alloca_512: alloca_st (|SHA2_512, ()|)
let alloca_512 =
mk_alloca SHA2_512
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
Hacl.Hash.SHA2.mk_alloca Spec.Hash.Definitions.SHA2_512
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, () |)

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)

let init_224 = mk_init SHA2_224
let init_256 = mk_init SHA2_256
let init_384 = mk_init SHA2_384
let init_512 = mk_init SHA2_512

inline_for_extraction noextract
val mk_alloca: a:sha2_alg -> alloca_st (| a, () |)

let mk_alloca a () =
  let h0 = ST.get () in
  let st = Hacl.Impl.SHA2.Generic.alloc a Vec.M32 in
  Hacl.Impl.SHA2.Generic.init st;
  let h1 = ST.get () in
  Hacl.Spec.SHA2.Equiv.init_lemma_l a Vec.M32 0;
  Lib.IntVector.reveal_vec_1 (word_t a);
  state_spec_v_lemma a (Vec.init a Vec.M32);
  LowStar.Buffer.(modifies_only_not_unused_in loc_none h0 h1);
  coerce_to_state a st

let alloca_224 = mk_alloca SHA2_224
let alloca_256 = mk_alloca SHA2_256
val alloca_512: alloca_st (|SHA2_512, ()|)
Hacl.Hash.Definitions.alloca_st (| Spec.Hash.Definitions.SHA2_512, () |)