val alloca: alloca_st (|Blake2S, M128|)
val alloca: alloca_st (|Blake2S, M128|)
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
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
/
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.alloca_st (| Spec.Hash.Definitions.Blake2S, Hacl.Impl.Blake2.Core.M128 |)
Prims.unit Prims._assert LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.modifies_only_not_unused_in 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 FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get Hacl.Blake2s_128.init FStar.UInt32.__uint_to_t Lib.Buffer.lbuffer_t Lib.Buffer.MUT Hacl.Impl.Blake2.Core.element_t Spec.Blake2.Definitions.Blake2S Lib.IntTypes.mul_mod Lib.IntTypes.U32 Lib.IntTypes.PUB 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
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