val malloc_blake2b_32: malloc_st (|Blake2B, M32|)
let malloc_blake2b_32 = BlB32.blake2b_malloc
val malloc_blake2b_32: malloc_st (|Blake2B, M32|)
let malloc_blake2b_32 =
BlB32.blake2b_malloc
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.Blake2b_32.blake2b_malloc
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
val malloc_blake2b_32: malloc_st (|Blake2B, M32|)
Hacl.Hash.Definitions.malloc_st (| Spec.Hash.Definitions.Blake2B, Hacl.Impl.Blake2.Core.M32 |)