val hash_blake2b_32: hash_st Blake2B
let hash_blake2b_32 input input_len dst = BlB32.blake2b 64ul dst input_len input 0ul (null #MUT uint8)
val hash_blake2b_32: hash_st Blake2B
let hash_blake2b_32 input input_len dst =
BlB32.blake2b 64ul dst input_len input 0ul (null #MUT uint8)
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
LowStar.Buffer.buffer Lib.IntTypes.uint8 Lib.IntTypes.size_t Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual Lib.IntTypes.range Lib.IntTypes.U32 LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Lib.IntTypes.v Lib.IntTypes.PUB Hacl.Hash.Definitions.hash_t Spec.Hash.Definitions.Blake2B Hacl.Blake2b_32.blake2b FStar.UInt32.__uint_to_t Lib.Buffer.null Lib.Buffer.MUT Prims.unit
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
val hash_blake2b_32: hash_st Blake2B
Hacl.Hash.Definitions.hash_st Spec.Hash.Definitions.Blake2B