val token:
  #ip:ipkg -> #i:ip.Pkg.t{ip.Pkg.registered i} -> k:key ip i ->
  ST (tag (usage k))
  (requires fun _ -> (usage k).good \/ ~(safe i))
  (ensures fun h0 t h1 -> modifies (footprint k) h0 h1)
val token:
  #ip:ipkg -> #i:ip.Pkg.t{ip.Pkg.registered i} -> k:key ip i ->
  ST (tag (usage k))
  (requires fun _ -> (usage k).good \/ ~(safe i))
  (ensures fun h0 t h1 -> modifies (footprint k) h0 h1)
let token #ip #i k =
  let MAC _ t = get_key k in
  if is_safe i then
    (let IdealKey _ _ log = k <: ir_key ip i in
    log := Some ());
  t
(* 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

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


let coerce ip _ _ i u kv =
  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
/
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
k: MiTLS.Token.UF1CMA.key ip i
  -> FStar.HyperStack.ST.ST (MiTLS.Token.UF1CMA.tag (MiTLS.Token.UF1CMA.usage k))
MiTLS.Token.UF1CMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.__proj__Idx__item__registered MiTLS.Token.UF1CMA.key MiTLS.Token.UF1CMA.info MiTLS.Token.UF1CMA.keyrepr MiTLS.Token.UF1CMA.tag MiTLS.Token.UF1CMA.usage Prims.unit MiTLS.Token.UF1CMA.concrete_key MiTLS.Mem.subrgn MiTLS.Token.UF1CMA.__proj__Mkinfo__item__parent MiTLS.Token.UF1CMA.concrete_key_info Prims.l_not Prims.b2t MiTLS.Mem.is_tls_rgn MiTLS.Token.UF1CMA.log_t FStar.HyperStack.ST.op_Colon_Equals FStar.Pervasives.Native.option MiTLS.Token.UF1CMA.goodish MiTLS.Mem.ssa FStar.Pervasives.Native.Some MiTLS.Token.UF1CMA.ir_key Prims.bool MiTLS.Token.UF1CMA.is_safe MiTLS.Token.UF1CMA.get_key
let token #ip #i k =
  
let MAC _ t = get_key k in
if is_safe i
then
  (let IdealKey _ _ log = k <: ir_key ip i in
    log := Some ());
t