let compute_st (a: fixed_len_alg) =
  tag: B.buffer uint8 {B.length tag == hash_length a} ->
  key: B.buffer uint8{ keysized a (B.length key) /\ B.disjoint key tag } ->
  keylen: UInt32.t{ UInt32.v keylen = B.length key } ->
  data: B.buffer uint8{ B.length data + block_length a < pow2 32 } ->
  datalen: UInt32.t{ UInt32.v datalen = B.length data } ->
  Stack unit
  (requires fun h0 -> B.live h0 tag /\ B.live h0 key /\ B.live h0 data)
  (ensures fun h0 _ h1 ->
    key_and_data_fits a;
    LowStar.Modifies.(modifies (loc_buffer tag) h0 h1) /\
    B.as_seq h1 tag == hmac a (B.as_seq h0 key) (B.as_seq h0 data))
let compute_st (a: fixed_len_alg) =

    tag: B.buffer uint8 {B.length tag == hash_length a} ->
    key: B.buffer uint8 {keysized a (B.length key) /\ B.disjoint key tag} ->
    keylen: UInt32.t{UInt32.v keylen = B.length key} ->
    data: B.buffer uint8 {B.length data + block_length a < pow2 32} ->
    datalen: UInt32.t{UInt32.v datalen = B.length data}
  -> Stack unit
      (requires fun h0 -> B.live h0 tag /\ B.live h0 key /\ B.live h0 data)
      (ensures
        fun h0 _ h1 ->
          key_and_data_fits a;
          LowStar.Modifies.(modifies (loc_buffer tag) h0 h1) /\
          B.as_seq h1 tag == hmac a (B.as_seq h0 key) (B.as_seq h0 data))
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.fixed_len_alg LowStar.Buffer.buffer Lib.IntTypes.uint8 Prims.eq2 Prims.nat LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Spec.Hash.Definitions.hash_length Prims.l_and Spec.Agile.HMAC.keysized LowStar.Monotonic.Buffer.disjoint FStar.UInt32.t Prims.b2t Prims.op_Equality Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_GreaterThanOrEqual FStar.UInt32.v Prims.op_LessThan Prims.op_Addition Spec.Hash.Definitions.block_length Prims.pow2 Prims.unit FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer FStar.Seq.Base.seq LowStar.Monotonic.Buffer.as_seq Spec.Agile.HMAC.hmac Hacl.HMAC.key_and_data_fits
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))
=
  let open FStar.Mul in
  assert_norm (8 * 16 + pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125)

inline_for_extraction noextract
val compute_st : a: Spec.Hash.Definitions.fixed_len_alg -> Type0
a: Spec.Hash.Definitions.fixed_len_alg -> Type0