val mk_extract:
  a: fixed_len_alg ->
  hmac: Hacl.HMAC.compute_st a ->
  extract_st a
let mk_extract a hmac prk salt saltlen ikm ikmlen =
  hmac prk salt saltlen ikm ikmlen
val mk_extract:
  a: fixed_len_alg ->
  hmac: Hacl.HMAC.compute_st a ->
  extract_st a
let mk_extract a hmac prk salt saltlen ikm ikmlen =
hmac prk salt saltlen ikm ikmlen
Hacl.HKDF.fst.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HKDF.fst.checked Spec.Agile.HKDF.fst.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.Sequence.fsti.checked Lib.IntTypes.fst.checked Lib.Buffer.fsti.checked Hacl.HMAC.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked
Hacl.HKDF.fst
Spec.Hash.Definitions.fixed_len_alg Hacl.HMAC.compute_st LowStar.Buffer.buffer Lib.IntTypes.uint8 Lib.IntTypes.pub_uint32 Prims.unit
module Hacl.HKDF

open FStar.Seq

module B = Lib.Buffer
module LB = LowStar.Buffer

open Spec.Hash.Definitions
open Spec.Agile.HKDF

open FStar.Mul
open FStar.HyperStack
open FStar.HyperStack.ST
open Lib.Buffer

friend Spec.Agile.HKDF
friend Lib.IntTypes

module Seq = Lib.Sequence

// TODO: proofs break mysteriously when not befriending Lib.IntTypes and
// declassifying uint8; investigate
// assume val declassify8: squash (uint8 == UInt8.t)

module ST = FStar.HyperStack.ST

#set-options "--max_fuel 0 --max_ifuel 0 --z3rlimit 100"
val mk_extract:
  a: fixed_len_alg ->
  hmac: Hacl.HMAC.compute_st a ->
  extract_st a
a: Spec.Hash.Definitions.fixed_len_alg -> hmac: Hacl.HMAC.compute_st a -> Hacl.HKDF.extract_st a