val hmac_input_fits: a:fixed_len_alg -> Lemma
  ((pow2 32 + block_length a) `less_than_max_input_length` a)
let hmac_input_fits a =
  allow_inversion fixed_len_alg;
  match a with
  | MD5 ->
    assert_norm (pow2 32 + block_length MD5 <= Some?.v (max_input_length MD5))
  | SHA1 ->
    assert_norm (pow2 32 + block_length SHA1 <= Some?.v (max_input_length SHA1))
  | SHA2_224 ->
    assert_norm (pow2 32 + block_length SHA2_224 <= Some?.v (max_input_length SHA2_224))
  | SHA2_256 ->
    assert_norm (pow2 32 + block_length SHA2_256 <= Some?.v (max_input_length SHA2_256))
  | SHA2_384 ->
    assert_norm (pow2 32 + block_length SHA2_384 <= Some?.v (max_input_length SHA2_384))
  | SHA2_512 ->
    assert_norm (pow2 32 + block_length SHA2_512 <= Some?.v (max_input_length SHA2_512))
  | Blake2S ->
    assert_norm (pow2 32 + block_length Blake2S <= Some?.v (max_input_length Blake2S))
  | Blake2B ->
    assert_norm (pow2 32 + block_length Blake2B <= Some?.v (max_input_length Blake2B))
  | SHA3_224 -> ()
  | SHA3_256 -> ()
  | SHA3_384 -> ()
  | SHA3_512 -> ()
val hmac_input_fits: a:fixed_len_alg -> Lemma
  ((pow2 32 + block_length a) `less_than_max_input_length` a)
let hmac_input_fits a =
allow_inversion fixed_len_alg;
match a with
| MD5 -> assert_norm (pow2 32 + block_length MD5 <= Some?.v (max_input_length MD5))
| SHA1 -> assert_norm (pow2 32 + block_length SHA1 <= Some?.v (max_input_length SHA1))
| SHA2_224 -> assert_norm (pow2 32 + block_length SHA2_224 <= Some?.v (max_input_length SHA2_224))
| SHA2_256 -> assert_norm (pow2 32 + block_length SHA2_256 <= Some?.v (max_input_length SHA2_256))
| SHA2_384 -> assert_norm (pow2 32 + block_length SHA2_384 <= Some?.v (max_input_length SHA2_384))
| SHA2_512 -> assert_norm (pow2 32 + block_length SHA2_512 <= Some?.v (max_input_length SHA2_512))
| Blake2S -> assert_norm (pow2 32 + block_length Blake2S <= Some?.v (max_input_length Blake2S))
| Blake2B -> assert_norm (pow2 32 + block_length Blake2B <= Some?.v (max_input_length Blake2B))
| SHA3_224 -> ()
| SHA3_256 -> ()
| SHA3_384 -> ()
| SHA3_512 -> ()
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 FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition Prims.pow2 Spec.Hash.Definitions.block_length Spec.Hash.Definitions.MD5 FStar.Pervasives.Native.__proj__Some__item__v Prims.pos Spec.Hash.Definitions.max_input_length Spec.Hash.Definitions.SHA1 Spec.Hash.Definitions.SHA2_224 Spec.Hash.Definitions.SHA2_256 Spec.Hash.Definitions.SHA2_384 Spec.Hash.Definitions.SHA2_512 Spec.Hash.Definitions.Blake2S Spec.Hash.Definitions.Blake2B Prims.unit FStar.Pervasives.allow_inversion
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"

let mk_extract a hmac prk salt saltlen ikm ikmlen =
  hmac prk salt saltlen ikm ikmlen

val hmac_input_fits: a:fixed_len_alg -> Lemma
  ((pow2 32 + block_length a) `less_than_max_input_length` a)
val hmac_input_fits: a:fixed_len_alg -> Lemma
  ((pow2 32 + block_length a) `less_than_max_input_length` a)
a: Spec.Hash.Definitions.fixed_len_alg
  -> FStar.Pervasives.Lemma
    (ensures
      Spec.Hash.Definitions.less_than_max_input_length (Prims.pow2 32 +
          Spec.Hash.Definitions.block_length a)
        a)