val mk_update_multi: a:sha2_alg -> update_multi_st (| a, () |)
let mk_update_multi a st () blocks n_blocks =
  Lib.IntVector.reveal_vec_1 (word_t a);

  [@inline_let]
  let len_blocks = n_blocks `FStar.UInt32.mul` block_len a in
  [@inline_let]
  let blocks_multi = ntup1 #(Lib.Buffer.lbuffer Lib.IntTypes.uint8 len_blocks) #1 blocks in
  let h0 = ST.get () in
  [@inline_let]
  let st' = coerce_to_mb_state a st in
  begin match a with
  | SHA2_224 -> Hacl.SHA2.Scalar32.sha224_update_nblocks len_blocks blocks_multi st'
  | SHA2_256 -> Hacl.SHA2.Scalar32.sha256_update_nblocks len_blocks blocks_multi st'
  | SHA2_384 -> Hacl.SHA2.Scalar32.sha384_update_nblocks len_blocks blocks_multi st'
  | SHA2_512 -> Hacl.SHA2.Scalar32.sha512_update_nblocks len_blocks blocks_multi st'
  end;

  let h1 = ST.get () in

  begin (* ghost *)
  assert_norm (pow2 32 < pow2 61);
  assert_norm (pow2 32 < pow2 125);
  let st0' = as_seq #(| a, () |) h0 st' in
  let st0 = as_seq h0 st in
  let blocks0 = LowStar.Buffer.as_seq h0 blocks in
  let length_blocks = UInt32.v len_blocks in
  assert (Lib.Sequence.length blocks0 = length_blocks);
  let blocks0_multi = as_seq_multi #1 #len_blocks h0 blocks_multi in
  let st0_raw = LowStar.Buffer.as_seq h0 st in

  calc (==) {
    as_seq h1 st;
  (==) { }
    as_seq #(| a, () |) h1 st';
  (==) { }
    Vec.update_nblocks #a #Vec.M32 length_blocks blocks0_multi st0';
  (==) { state_spec_v_lemma a (Vec.update_nblocks #a #Vec.M32 length_blocks blocks0_multi st0') }
    Lib.Sequence.index (Vec.state_spec_v (Vec.update_nblocks #a #Vec.M32 length_blocks blocks0_multi st0')) 0;
  (==) { Hacl.Spec.SHA2.Equiv.update_nblocks_lemma_l #a #Vec.M32 length_blocks blocks0_multi st0_raw 0 }
    Hacl.Spec.SHA2.update_nblocks a length_blocks blocks0_multi.(|0|)
      (Lib.Sequence.index (Vec.state_spec_v #a #Vec.M32 (as_seq h0 st)) 0);
  (==) { state_spec_v_lemma a (as_seq h0 st) }
    Hacl.Spec.SHA2.update_nblocks a length_blocks blocks0_multi.(|0|) (as_seq h0 st);
  (==) { }
    Hacl.Spec.SHA2.update_nblocks a length_blocks blocks0 st0;
  (==) { Hacl.Spec.SHA2.EquivScalar.update_nblocks_is_repeat_blocks_multi a length_blocks blocks0 st0 } (
    let b = blocks0 in
    let open Lib.Sequence in
    let bl = block_length a in
    repeat_blocks_multi #Lib.IntTypes.uint8 #(words_state a) bl
      (Seq.slice b 0 (Seq.length b - Seq.length b % bl)) (Hacl.Spec.SHA2.update a) st0);
  (==) { }
    Lib.Sequence.repeat_blocks_multi #Lib.IntTypes.uint8 #(words_state a)
      (block_length a) blocks0 (Hacl.Spec.SHA2.update a) st0;
  (==) {
    FStar.Classical.forall_intro_2 (Hacl.Spec.SHA2.EquivScalar.update_lemma a);
    Lib.Sequence.Lemmas.repeat_blocks_multi_extensionality
      #Lib.IntTypes.uint8 #(words_state a)
      (block_length a) blocks0 (Hacl.Spec.SHA2.update a)
      (Lib.UpdateMulti.Lemmas.repeat_f (block_length a) (Spec.Agile.Hash.update a))
      st0
  }
    Lib.Sequence.repeat_blocks_multi #Lib.IntTypes.uint8 #(words_state a)
      (block_length a) blocks0 (Lib.UpdateMulti.Lemmas.repeat_f (block_length a) (Spec.Agile.Hash.update a)) st0;
  (==) {
    Lib.UpdateMulti.Lemmas.update_multi_is_repeat_blocks_multi #(words_state a)
      (block_length a) (Spec.Agile.Hash.update a) st0 blocks0
  }
    Lib.UpdateMulti.mk_update_multi #(words_state a) (block_length a) (Spec.Agile.Hash.update a) st0 blocks0;
  (==) { }
    Spec.Agile.Hash.update_multi a st0 () blocks0;
  }
  end
val mk_update_multi: a:sha2_alg -> update_multi_st (| a, () |)
let mk_update_multi a st () blocks n_blocks =
Lib.IntVector.reveal_vec_1 (word_t a);
[@@ inline_let ]let len_blocks = n_blocks `FStar.UInt32.mul` (block_len a) in
[@@ inline_let ]let blocks_multi =
  ntup1 #(Lib.Buffer.lbuffer Lib.IntTypes.uint8 len_blocks) #1 blocks
in
let h0 = ST.get () in
[@@ inline_let ]let st' = coerce_to_mb_state a st in
(match a with
  | SHA2_224 -> Hacl.SHA2.Scalar32.sha224_update_nblocks len_blocks blocks_multi st'
  | SHA2_256 -> Hacl.SHA2.Scalar32.sha256_update_nblocks len_blocks blocks_multi st'
  | SHA2_384 -> Hacl.SHA2.Scalar32.sha384_update_nblocks len_blocks blocks_multi st'
  | SHA2_512 -> Hacl.SHA2.Scalar32.sha512_update_nblocks len_blocks blocks_multi st');
let h1 = ST.get () in
assert_norm (pow2 32 < pow2 61);
assert_norm (pow2 32 < pow2 125);
let st0' = as_seq #(| a, () |) h0 st' in
let st0 = as_seq h0 st in
let blocks0 = LowStar.Buffer.as_seq h0 blocks in
let length_blocks = UInt32.v len_blocks in
assert (Lib.Sequence.length blocks0 = length_blocks);
let blocks0_multi = as_seq_multi #1 #len_blocks h0 blocks_multi in
let st0_raw = LowStar.Buffer.as_seq h0 st in
calc ( == ) {
  as_seq h1 st;
  ( == ) { () }
  as_seq #(| a, () |) h1 st';
  ( == ) { () }
  Vec.update_nblocks #a #Vec.M32 length_blocks blocks0_multi st0';
  ( == ) { state_spec_v_lemma a (Vec.update_nblocks #a #Vec.M32 length_blocks blocks0_multi st0') }
  Lib.Sequence.index (Vec.state_spec_v (Vec.update_nblocks #a
            #Vec.M32
            length_blocks
            blocks0_multi
            st0'))
    0;
  ( == ) { Hacl.Spec.SHA2.Equiv.update_nblocks_lemma_l #a
    #Vec.M32
    length_blocks
    blocks0_multi
    st0_raw
    0 }
  Hacl.Spec.SHA2.update_nblocks a
    length_blocks
    blocks0_multi.(| 0 |)
    (Lib.Sequence.index (Vec.state_spec_v #a #Vec.M32 (as_seq h0 st)) 0);
  ( == ) { state_spec_v_lemma a (as_seq h0 st) }
  Hacl.Spec.SHA2.update_nblocks a length_blocks blocks0_multi.(| 0 |) (as_seq h0 st);
  ( == ) { () }
  Hacl.Spec.SHA2.update_nblocks a length_blocks blocks0 st0;
  ( == ) { Hacl.Spec.SHA2.EquivScalar.update_nblocks_is_repeat_blocks_multi a
    length_blocks
    blocks0
    st0 }
  (let b = blocks0 in
    let open Lib.Sequence in
    let bl = block_length a in
    repeat_blocks_multi #Lib.IntTypes.uint8
      #(words_state a)
      bl
      (Seq.slice b 0 (Seq.length b - Seq.length b % bl))
      (Hacl.Spec.SHA2.update a)
      st0);
  ( == ) { () }
  Lib.Sequence.repeat_blocks_multi #Lib.IntTypes.uint8
    #(words_state a)
    (block_length a)
    blocks0
    (Hacl.Spec.SHA2.update a)
    st0;
  ( == ) { (FStar.Classical.forall_intro_2 (Hacl.Spec.SHA2.EquivScalar.update_lemma a);
    Lib.Sequence.Lemmas.repeat_blocks_multi_extensionality #Lib.IntTypes.uint8
      #(words_state a)
      (block_length a)
      blocks0
      (Hacl.Spec.SHA2.update a)
      (Lib.UpdateMulti.Lemmas.repeat_f (block_length a) (Spec.Agile.Hash.update a))
      st0) }
  Lib.Sequence.repeat_blocks_multi #Lib.IntTypes.uint8
    #(words_state a)
    (block_length a)
    blocks0
    (Lib.UpdateMulti.Lemmas.repeat_f (block_length a) (Spec.Agile.Hash.update a))
    st0;
  ( == ) { Lib.UpdateMulti.Lemmas.update_multi_is_repeat_blocks_multi #(words_state a)
    (block_length a)
    (Spec.Agile.Hash.update a)
    st0
    blocks0 }
  Lib.UpdateMulti.mk_update_multi #(words_state a)
    (block_length a)
    (Spec.Agile.Hash.update a)
    st0
    blocks0;
  ( == ) { () }
  Spec.Agile.Hash.update_multi a st0 () blocks0;
}
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 Prims.unit Hacl.Hash.Definitions.blocks_t Hacl.Hash.Definitions.get_alg Lib.IntTypes.size_t Prims.b2t Prims.op_Equality Prims.int LowStar.Monotonic.Buffer.length Lib.IntTypes.uint8 LowStar.Buffer.trivial_preorder FStar.Mul.op_Star Spec.Hash.Definitions.block_length Lib.IntTypes.v Lib.IntTypes.U32 Lib.IntTypes.PUB FStar.Calc.calc_finish Spec.Hash.Definitions.words_state Prims.eq2 Hacl.Hash.Definitions.as_seq Spec.Agile.Hash.update_multi Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Lib.UpdateMulti.mk_update_multi Spec.Agile.Hash.update Lib.Sequence.repeat_blocks_multi Lib.UpdateMulti.Lemmas.repeat_f Hacl.Spec.SHA2.update FStar.Seq.Base.slice Prims.op_Subtraction FStar.Seq.Base.length Prims.op_Modulus Prims.nonzero FStar.Seq.Base.seq Lib.IntTypes.int_t Lib.IntTypes.U8 Lib.IntTypes.SEC Hacl.Spec.SHA2.update_nblocks Lib.NTuple.op_Lens_Access FStar.Seq.Properties.lseq Lib.Sequence.index Hacl.Spec.SHA2.Vec.words_state' Hacl.Spec.SHA2.Vec.lanes Hacl.Spec.SHA2.Vec.M32 Hacl.Spec.SHA2.Vec.state_spec_v Hacl.Spec.SHA2.Vec.update_nblocks FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Hacl.Hash.SHA2.state_spec_v_lemma Hacl.Spec.SHA2.Equiv.update_nblocks_lemma_l Hacl.Spec.SHA2.EquivScalar.update_nblocks_is_repeat_blocks_multi Lib.Sequence.Lemmas.repeat_blocks_multi_extensionality FStar.Classical.forall_intro_2 Hacl.Spec.SHA2.block_t Hacl.Spec.SHA2.EquivScalar.update_lemma Lib.UpdateMulti.Lemmas.update_multi_is_repeat_blocks_multi Hacl.Hash.Definitions.impl_word LowStar.Monotonic.Buffer.as_seq Lib.MultiBuffer.multiseq Lib.MultiBuffer.as_seq_multi Prims._assert Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n Lib.Sequence.length FStar.UInt.uint_t FStar.UInt32.v FStar.Pervasives.assert_norm Prims.op_LessThan Prims.pow2 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.SHA2.Scalar32.sha224_update_nblocks Hacl.SHA2.Scalar32.sha256_update_nblocks Hacl.SHA2.Scalar32.sha384_update_nblocks Hacl.SHA2.Scalar32.sha512_update_nblocks Hacl.Hash.SHA2.mb_state_32 Hacl.Hash.SHA2.coerce_to_mb_state Lib.NTuple.ntuple Lib.Buffer.lbuffer_t Lib.Buffer.MUT Lib.NTuple.ntup1 Lib.Buffer.lbuffer FStar.UInt32.t FStar.UInt32.mul Hacl.Hash.Definitions.block_len Lib.IntVector.reveal_vec_1 Spec.Hash.Definitions.word_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)

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
let alloca_384 = mk_alloca SHA2_384
let alloca_512 = mk_alloca SHA2_512

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