val coerceT (ip: ipkg) (ha_of_i: ip.Pkg.t -> ha) (good_of_i: ip.Pkg.t -> bool)
  (i: ip.Pkg.t {ip.Pkg.registered i /\ ~(safe i)})
  (u: info {u.alg = ha_of_i i /\ u.good == good_of_i i})
  (kv: lbytes32 (keylen u)) : GTot (key ip i)
val coerceT (ip: ipkg) (ha_of_i: ip.Pkg.t -> ha) (good_of_i: ip.Pkg.t -> bool)
  (i: ip.Pkg.t {ip.Pkg.registered i /\ ~(safe i)})
  (u: info {u.alg = ha_of_i i /\ u.good == good_of_i i})
  (kv: lbytes32 (keylen u)) : GTot (key ip i)
let coerceT (ip: ipkg) (ha_of_i: ip.Pkg.t -> ha) (good_of_i: ip.Pkg.t -> bool)
  (i: ip.Pkg.t {ip.Pkg.registered i /\ ~(safe i)})
  (u: info {u.alg = ha_of_i i /\ u.good == good_of_i i})
  (kv: lbytes32 (keylen u)) : GTot (key ip i)
  =
  assert_norm (pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125);
  assert(Spec.Agile.HMAC.keysized u.alg (Spec.Hash.Definitions.hash_length u.alg));
  let ck = MAC u kv in
  if model then
    let k : ir_key ip i = RealKey ck in k
  else ck
(* Idealizing derived authentication tokens; independent of TLS, used for TLS 1.2 Finished message payloads. *)
module MiTLS.Token.UF1CMA
open MiTLS

//TODO use this file instead of TLSPRF

open FStar.Bytes
open MiTLS.Mem

noeq type concrete_key =
  | MAC: u:info -> k:keyrepr u -> concrete_key

let concrete_key_info k = k.u
let concrete_key_repr k = k.k

let create ip _ _ i u =
  assert_norm (pow2 32 < pow2 61);
  assert_norm (pow2 61 < pow2 125);
  assert(Spec.Agile.HMAC.keysized u.alg (Spec.Hash.Definitions.hash_length u.alg));
  let kv: keyrepr u = Random.sample32 (Hacl.Hash.Definitions.hash_len u.alg) in
  let ck = MAC u kv in
  let k : ir_key ip i =
    if is_safe i then
      let region: Mem.subrgn u.parent = new_region u.parent in
      assert(~(is_tls_rgn u.parent));
      let log: log_t #ip i u region = ralloc region None in
      IdealKey ck region log
    else
      RealKey ck in
  k <: key ip i
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked prims.fst.checked MiTLS.Random.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Token.UF1CMA.fst

    ip: MiTLS.Token.UF1CMA.ipkg ->
    ha_of_i: (_: Idx?.t ip -> MiTLS.Token.UF1CMA.ha) ->
    good_of_i: (_: Idx?.t ip -> Prims.bool) ->
    i: Idx?.t ip {Idx?.registered ip i /\ ~(MiTLS.Token.UF1CMA.safe i)} ->
    u198:
      u203:
      MiTLS.Token.UF1CMA.info{Mkinfo?.alg u203 = ha_of_i i /\ Mkinfo?.good u203 == good_of_i i} ->
    kv: FStar.Bytes.lbytes32 (MiTLS.Token.UF1CMA.keylen u198)
  -> Prims.GTot (MiTLS.Token.UF1CMA.key ip i)
MiTLS.Token.UF1CMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Token.UF1CMA.ha Prims.bool Prims.l_and MiTLS.Pkg.__proj__Idx__item__registered Prims.l_not MiTLS.Token.UF1CMA.safe MiTLS.Token.UF1CMA.info Prims.b2t Prims.op_Equality MiTLS.Hashing.Spec.alg MiTLS.Token.UF1CMA.__proj__Mkinfo__item__alg Prims.eq2 MiTLS.Token.UF1CMA.__proj__Mkinfo__item__good FStar.Bytes.lbytes32 MiTLS.Token.UF1CMA.keylen MiTLS.Mem.model MiTLS.Token.UF1CMA.ir_key MiTLS.Token.UF1CMA.RealKey MiTLS.Token.UF1CMA.key MiTLS.Token.UF1CMA.concrete_key MiTLS.Token.UF1CMA.MAC Prims.unit Prims._assert Spec.Agile.HMAC.keysized Spec.Hash.Definitions.hash_length FStar.Pervasives.assert_norm Prims.op_LessThan Prims.pow2
let coerceT
      (ip: ipkg)
      (ha_of_i: (ip.Pkg.t -> ha))
      (good_of_i: (ip.Pkg.t -> bool))
      (i: ip.Pkg.t{ip.Pkg.registered i /\ ~(safe i)})
      (u: info{u.alg = ha_of_i i /\ u.good == good_of_i i})
      (kv: lbytes32 (keylen u))
    : GTot (key ip i) =
  
assert_norm (pow2 32 < pow2 61);
assert_norm (pow2 61 < pow2 125);
assert (Spec.Agile.HMAC.keysized u.alg (Spec.Hash.Definitions.hash_length u.alg));
let ck = MAC u kv in
if model
then
  let k:ir_key ip i = RealKey ck in
  k
else ck