val expand_blake2b_256:expand_st Blake2B
let expand_blake2b_256: expand_st Blake2B =
  mk_expand Blake2B Hacl.HMAC.Blake2b_256.compute_blake2b_256
val expand_blake2b_256:expand_st Blake2B
let expand_blake2b_256:expand_st Blake2B =
mk_expand Blake2B Hacl.HMAC.Blake2b_256.compute_blake2b_256
Hacl.HKDF.Blake2b_256.fst.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Hacl.HMAC.Blake2b_256.fst.checked Hacl.HKDF.fsti.checked FStar.Pervasives.fsti.checked
Hacl.HKDF.Blake2b_256.fst
Hacl.HKDF.mk_expand Spec.Hash.Definitions.Blake2B Hacl.HMAC.Blake2b_256.compute_blake2b_256
module Hacl.HKDF.Blake2b_256

open Spec.Hash.Definitions
open Hacl.HKDF

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

[@@ Comment "Expand pseudorandom key to desired length.

@param okm Pointer to `len` bytes of memory where output keying material is written to.
@param prk Pointer to at least `HashLen` bytes of memory where pseudorandom key is read from. Usually, this points to the output from the extract step.
@param prklen Length of pseudorandom key.
@param info Pointer to `infolen` bytes of memory where context and application specific information is read from. Can be a zero-length string.
@param infolen Length of context and application specific information.
@param len Length of output keying material."]
val expand_blake2b_256:expand_st Blake2B
Hacl.HKDF.expand_st Spec.Hash.Definitions.Blake2B