val create:
  ip:ipkg -> ha_of_i: (ip.Pkg.t -> ha) -> good_of_i: (ip.Pkg.t -> bool) ->
  i:ip.Pkg.t {ip.Pkg.registered i} ->
  u:info {u.alg = ha_of_i i /\ u.good == good_of_i i} -> ST (k:key ip i)
  (requires fun _ -> model)
  (ensures fun h0 k h1 ->
    modifies Set.empty h0 h1 /\
    usage k == u /\
    Pkg.fresh_regions (footprint k) h0 h1)
val create:
  ip:ipkg -> ha_of_i: (ip.Pkg.t -> ha) -> good_of_i: (ip.Pkg.t -> bool) ->
  i:ip.Pkg.t {ip.Pkg.registered i} ->
  u:info {u.alg = ha_of_i i /\ u.good == good_of_i i} -> ST (k:key ip i)
  (requires fun _ -> model)
  (ensures fun h0 k h1 ->
    modifies Set.empty h0 h1 /\
    usage k == u /\
    Pkg.fresh_regions (footprint k) h0 h1)
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
(* 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
/
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} ->
    u180:
      u184:
      MiTLS.Token.UF1CMA.info{Mkinfo?.alg u184 = ha_of_i i /\ Mkinfo?.good u184 == good_of_i i}
  -> FStar.HyperStack.ST.ST (MiTLS.Token.UF1CMA.key ip i)
MiTLS.Token.UF1CMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Token.UF1CMA.ha Prims.bool MiTLS.Pkg.__proj__Idx__item__registered MiTLS.Token.UF1CMA.info Prims.l_and 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 MiTLS.Token.UF1CMA.key MiTLS.Token.UF1CMA.ir_key MiTLS.Token.UF1CMA.IdealKey MiTLS.Token.UF1CMA.log_t FStar.HyperStack.ST.ralloc FStar.Pervasives.Native.option MiTLS.Token.UF1CMA.goodish MiTLS.Mem.ssa FStar.Pervasives.Native.None FStar.HyperStack.ST.mref Prims.unit Prims._assert Prims.l_not MiTLS.Mem.is_tls_rgn MiTLS.Token.UF1CMA.__proj__Mkinfo__item__parent MiTLS.Mem.subrgn FStar.HyperStack.ST.new_region FStar.Monotonic.HyperHeap.rid MiTLS.Token.UF1CMA.RealKey MiTLS.Token.UF1CMA.is_safe MiTLS.Token.UF1CMA.concrete_key MiTLS.Token.UF1CMA.MAC MiTLS.Token.UF1CMA.keyrepr MiTLS.Random.sample32 Hacl.Hash.Definitions.hash_len FStar.Bytes.lbytes FStar.UInt32.v Spec.Agile.HMAC.keysized Spec.Hash.Definitions.hash_length FStar.Pervasives.assert_norm Prims.op_LessThan Prims.pow2
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