val finish: finish_st (|Blake2S, M128|)
val finish: finish_st (|Blake2S, M128|)
let finish s dst = BlS128.finish (hash_len Blake2S) dst s
module Hacl.Hash.Blake2s_128

module B = LowStar.Buffer
module ST = FStar.HyperStack.ST
module BlS128 = Hacl.Blake2s_128
open Lib.IntTypes
open Lib.Buffer

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

friend Spec.Agile.Hash

let malloc = BlS128.malloc_with_key

let alloca () =
  let h0 = ST.get() in
  let s = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M128 in
  BlS128.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 s = BlS128.init s 0ul 32ul

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

let update_last s prev input input_len =
  ST.push_frame ();
  let wv = Hacl.Impl.Blake2.Core.alloc_state Spec.Blake2.Blake2S M128 in
  BlS128.update_last #input_len wv s (secret prev) input_len input;
  ST.pop_frame()
/
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.Streaming.Blake2s_128.fst.checked Hacl.Impl.Blake2.Core.fsti.checked Hacl.Blake2s_128.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked
Hacl.Hash.Blake2s_128.fst
Hacl.Hash.Definitions.finish_st (| Spec.Hash.Definitions.Blake2S, Hacl.Impl.Blake2.Core.M128 |)
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.hash_t Hacl.Hash.Definitions.get_alg Hacl.Blake2s_128.finish Hacl.Hash.Definitions.hash_len Prims.unit
let finish s dst =
  
BlS128.finish (hash_len Blake2S) dst s