let keysized (a:hash_alg) (l:nat) =
  l `less_than_max_input_length` a /\
  l + block_length a < pow2 32
let keysized (a: hash_alg) (l: nat) =
l `less_than_max_input_length` a /\ l + block_length a < pow2 32
Spec.Agile.HMAC.fsti.checked
Spec.Hash.Definitions.fst.checked prims.fst.checked Lib.IntTypes.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked
Spec.Agile.HMAC.fsti
Spec.Hash.Definitions.hash_alg Prims.nat Prims.l_and Prims.b2t Spec.Hash.Definitions.less_than_max_input_length Prims.op_LessThan Prims.op_Addition Spec.Hash.Definitions.block_length Prims.pow2 Prims.logical
module Spec.Agile.HMAC

open Spec.Hash.Definitions
open Lib.IntTypes

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

let lbytes (l:nat) = b:bytes {Seq.length b = l}
val keysized : a: Spec.Hash.Definitions.hash_alg -> l: Prims.nat -> Prims.logical
a: Spec.Hash.Definitions.hash_alg -> l: Prims.nat -> Prims.logical