val malloc: malloc_st (|Blake2S, M128|)
val malloc: malloc_st (|Blake2S, M128|)
let malloc = BlS128.malloc_with_key
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
/
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.malloc_st (| Spec.Hash.Definitions.Blake2S, Hacl.Impl.Blake2.Core.M128 |)
Hacl.Blake2s_128.malloc_with_key
let malloc =
  
BlS128.malloc_with_key