val key_and_data_fits (a: hash_alg)
    : Lemma (ensures ((block_length a + pow2 32) `less_than_max_input_length` a))
let key_and_data_fits (a: hash_alg): Lemma
  (ensures ((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)
val key_and_data_fits (a: hash_alg)
    : Lemma (ensures ((block_length a + pow2 32) `less_than_max_input_length` a))
let key_and_data_fits (a: hash_alg)
    : Lemma (ensures ((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)
Hacl.HMAC.fsti.checked
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fsti.checked Hacl.Hash.Definitions.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked EverCrypt.Helpers.fsti.checked
Hacl.HMAC.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.less_than_max_input_length Spec.Hash.Definitions.block_length Prims.Nil FStar.Pervasives.pattern
module Hacl.HMAC

/// A generic, meta-programmed HMAC module. This one provides one concrete
/// instantiation, namely HMAC-SHA2-256 instantiated with the HACL*
/// implementation. In the future, this module may provide more implementations
/// of HMAC, using optimized HACL versions of SHA2-256. For more algorithms, and
/// for an assembly-optimized HMAC version that may call into Vale, see
/// EverCrypt.HMAC.

module B = LowStar.Buffer
module D = Hacl.Hash.Definitions

open Spec.Agile.HMAC
open Spec.Hash.Definitions
open FStar.HyperStack.ST
open Lib.IntTypes

open EverCrypt.Helpers

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

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