val ideal : MiTLS.Flags.t
let ideal = Flags.ideal_HMAC
(**! Idealizing agile HMAC; independent of TLS, used for TLS 1.3 Finished message payloads and Binders. *)
module MiTLS.HMAC.UFCMA
open MiTLS

open FStar.Bytes
open MiTLS.Mem

module MDM = FStar.Monotonic.DependentMap

#set-options "--initial_fuel 1 --max_fuel 1 --initial_ifuel 1 --max_ifuel 1"

type lbytes32 n = FStar.Bytes.lbytes (UInt32.v n)

let ipkg = Pkg.ipkg
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked MiTLS.Random.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked MiTLS.Flags.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.IO.fst.checked FStar.Bytes.fsti.checked
MiTLS.HMAC.UFCMA.fst
MiTLS.Flags.t
MiTLS.Flags.ideal_HMAC
let ideal =
  
Flags.ideal_HMAC