val keylen (u: info) : Pkg.keylen
val keylen (u: info) : Pkg.keylen
let keylen (u:info): Pkg.keylen = Hacl.Hash.Definitions.hash_len u.alg
(**! 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

let model = Flags.model
let ideal = Flags.ideal_HMAC // secret idealization flag for the UFCMA assumption

type safe (#ip:ipkg) (i:ip.Pkg.t) = b2t ideal /\ ip.Pkg.honest i

noextract
private let is_safe (#ip:ipkg) (i:ip.Pkg.t{ip.Pkg.registered i}): ST bool 
  (requires fun h0 -> True)
  (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
  =
  let b = ip.Pkg.get_honesty i in
  ideal && b

type ha = Hashing.alg

// initial parameters
noeq type info = | Info: 
  parent: rgn {~ (is_tls_rgn parent)} -> 
  alg: HMAC.ha -> 
  good: (Hashing.macable alg -> bool) ->  //TODO: should be Type0 instead of bool, and erased, but hard to propagate
  info

//18-02-25 should we index by i instead?
type text (u:info) = Hashing.macable u.alg
type tag (u:info) = lbytes32 (Hacl.Hash.Definitions.hash_len u.alg)
/
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
u37: MiTLS.HMAC.UFCMA.info -> MiTLS.Pkg.keylen
MiTLS.HMAC.UFCMA.info Hacl.Hash.Definitions.hash_len MiTLS.HMAC.UFCMA.__proj__Info__item__alg MiTLS.Pkg.keylen
let keylen (u: info) : Pkg.keylen =
  
Hacl.Hash.Definitions.hash_len u.alg