val hash_block_length_fits (a: hash_alg)
    : Lemma
    (if is_keccak a
      then True
      else hash_length a + pow2 32 + block_length a < Some?.v (max_input_length a))
let hash_block_length_fits (a:hash_alg) :
  Lemma (if is_keccak a then True else hash_length a + pow2 32 + block_length a < Some?.v(max_input_length a))
=
  let open FStar.Mul in
  assert_norm (8 * 16 + 8 * 8 + pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125)
val hash_block_length_fits (a: hash_alg)
    : Lemma
    (if is_keccak a
      then True
      else hash_length a + pow2 32 + block_length a < Some?.v (max_input_length a))
let hash_block_length_fits (a: hash_alg)
    : Lemma
    (if is_keccak a
      then True
      else hash_length a + pow2 32 + block_length a < Some?.v (max_input_length a)) =
let open FStar.Mul in
assert_norm (8 * 16 + 8 * 8 + pow2 32 < pow2 61);
assert_norm (pow2 61 < pow2 125)
EverCrypt.HKDF.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.HKDF.fsti.checked prims.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked EverCrypt.HMAC.fsti.checked
EverCrypt.HKDF.fsti
Spec.Hash.Definitions.hash_alg FStar.Pervasives.assert_norm Prims.b2t Prims.op_LessThan Prims.pow2 Prims.unit Prims.op_Addition FStar.Mul.op_Star Prims.l_True Prims.squash Spec.Hash.Definitions.is_keccak Prims.bool Spec.Hash.Definitions.hash_length Spec.Hash.Definitions.block_length FStar.Pervasives.Native.__proj__Some__item__v Prims.pos Spec.Hash.Definitions.max_input_length Prims.Nil FStar.Pervasives.pattern
(** Agile HKDF *)
module EverCrypt.HKDF

module B = LowStar.Buffer

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

open FStar.HyperStack.ST
open Lib.IntTypes

#set-options "--max_ifuel 0 --max_fuel 0 --z3rlimit 20"

/// Auxiliary lemmas

let key_and_data_fits (a:hash_alg) :
  Lemma ((block_length a + pow2 32) `less_than_max_input_length` a)
=
  let open FStar.Mul in
  assert_norm (8 * 16 + pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125)

let hash_block_length_fits (a:hash_alg) :
  Lemma (if is_keccak a then True else hash_length a + pow2 32 + block_length a < Some?.v(max_input_length a))
val hash_block_length_fits (a: hash_alg)
    : Lemma
    (if is_keccak a
      then True
      else hash_length a + pow2 32 + block_length a < Some?.v (max_input_length a))
a: Spec.Hash.Definitions.hash_alg
  -> FStar.Pervasives.Lemma
    (ensures
      ((match Spec.Hash.Definitions.is_keccak a with
          | true -> Prims.l_True
          | _ ->
            Spec.Hash.Definitions.hash_length a + Prims.pow2 32 +
            Spec.Hash.Definitions.block_length a <
            Some?.v (Spec.Hash.Definitions.max_input_length a))
        <:
        Type0))