val update_multi_blake2s_128: update_multi_st (|Blake2S, M128|)
let update_multi_blake2s_128 s ev blocks n =
  ST.push_frame ();
  let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M128 in
  BlS128.blake2s_update_multi #(n `FStar.UInt32.mul` block_len Blake2S) wv s (secret ev) blocks n;
  ST.pop_frame ()
val update_multi_blake2s_128: update_multi_st (|Blake2S, M128|)
let update_multi_blake2s_128 s ev blocks n =
ST.push_frame ();
let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M128 in
BlS128.blake2s_update_multi #(n `FStar.UInt32.mul` (block_len Blake2S)) wv s (secret ev) blocks n;
ST.pop_frame ()
Hacl.Hash.Blake2.fst.checked
Spec.Blake2.fst.checked Spec.Agile.Hash.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Lib.Buffer.fsti.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Blake2s_32.fst.checked Hacl.Blake2s_128.fst.checked Hacl.Blake2b_32.fst.checked Hacl.Blake2b_256.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
Hacl.Hash.Blake2.fst
Hacl.Hash.Definitions.state Prims.Mkdtuple2 Spec.Hash.Definitions.hash_alg Hacl.Hash.Definitions.m_spec Spec.Hash.Definitions.Blake2S Hacl.Impl.Blake2.Core.M128 Hacl.Hash.Definitions.extra_state Hacl.Hash.Definitions.get_alg Hacl.Hash.Definitions.blocks_t 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.HyperStack.ST.pop_frame Prims.unit Hacl.Blake2s_128.blake2s_update_multi FStar.UInt32.mul Hacl.Hash.Definitions.block_len Lib.IntTypes.secret Spec.Blake2.limb_inttype Spec.Blake2.Blake2S Lib.Buffer.lbuffer_t Lib.Buffer.MUT Hacl.Impl.Blake2.Core.element_t Lib.IntTypes.mul_mod FStar.UInt32.uint_to_t FStar.UInt32.t Hacl.Impl.Blake2.Core.row_len Hacl.Impl.Blake2.Core.alloc_state Hacl.Impl.Blake2.Core.state_p FStar.HyperStack.ST.push_frame
module Hacl.Hash.Blake2

module B = LowStar.Buffer
module ST = FStar.HyperStack.ST
module BlB32 = Hacl.Blake2b_32
module BlB256 = Hacl.Blake2b_256
module BlS32 = Hacl.Blake2s_32
module BlS128 = Hacl.Blake2s_128
open Lib.IntTypes
open Lib.Buffer

#push-options "--fuel 0 --ifuel 0 --z3rlimit 20"

friend Spec.Agile.Hash

// Blake2b_32

let malloc_blake2b_32 = BlB32.blake2b_malloc

let alloca_blake2b_32 () =
  let h0 = ST.get() in
  let s = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2B M32 in
  BlB32.blake2b_init s 0ul 64ul;
  let h1 = ST.get () in
  B.modifies_only_not_unused_in (B.loc_none) h0 h1;
  assert (B.modifies B.loc_none h0 h1);
  s

let init_blake2b_32 s = BlB32.blake2b_init s 0ul 64ul

let update_multi_blake2b_32 s ev blocks n =
  ST.push_frame ();
  let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2B M32 in
  BlB32.blake2b_update_multi #(n `FStar.UInt32.mul` block_len Blake2B) wv s (secret ev) blocks n;
  ST.pop_frame ()

let update_last_blake2b_32 s prev input input_len =
  ST.push_frame ();
  let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2B M32 in
  BlB32.blake2b_update_last #input_len wv s (secret prev) input_len input;
  ST.pop_frame()

let finish_blake2b_32 s dst = BlB32.blake2b_finish (hash_len Blake2B) dst s

let hash_blake2b_32 input input_len dst = BlB32.blake2b 64ul dst input_len input 0ul (null #MUT uint8)

// Blake2s_32

let malloc_blake2s_32 = BlS32.blake2s_malloc

let alloca_blake2s_32 () =
  let h0 = ST.get() in
  let s = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M32 in
  BlS32.blake2s_init s 0ul 32ul;
  let h1 = ST.get () in
  B.modifies_only_not_unused_in (B.loc_none) h0 h1;
  assert (B.modifies B.loc_none h0 h1);
  s

let init_blake2s_32 s = BlS32.blake2s_init s 0ul 32ul

let update_multi_blake2s_32 s ev blocks n =
  ST.push_frame ();
  let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M32 in
  BlS32.blake2s_update_multi #(n `FStar.UInt32.mul` block_len Blake2S) wv s (secret ev) blocks n;
  ST.pop_frame ()

let update_last_blake2s_32 s prev input input_len =
  ST.push_frame ();
  let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M32 in
  BlS32.blake2s_update_last #input_len wv s (secret prev) input_len input;
  ST.pop_frame()

let finish_blake2s_32 s dst = BlS32.blake2s_finish (hash_len Blake2S) dst s

let hash_blake2s_32 input input_len dst = BlS32.blake2s 32ul dst input_len input 0ul (null #MUT uint8)

// Blake2s_128

let malloc_blake2s_128 = BlS128.blake2s_malloc

let alloca_blake2s_128 () =
  let h0 = ST.get() in
  let s = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M128 in
  BlS128.blake2s_init s 0ul 32ul;
  let h1 = ST.get () in
  B.modifies_only_not_unused_in (B.loc_none) h0 h1;
  assert (B.modifies B.loc_none h0 h1);
  s

let init_blake2s_128 s = BlS128.blake2s_init s 0ul 32ul
val update_multi_blake2s_128: update_multi_st (|Blake2S, M128|)
Hacl.Hash.Definitions.update_multi_st (|
    Spec.Hash.Definitions.Blake2S,
    Hacl.Impl.Blake2.Core.M128
  |)