val get_key (#ip: ipkg) (#i: ip.Pkg.t{ip.Pkg.registered i}) (k: key ip i) : concrete_key
val get_key (#ip: ipkg) (#i: ip.Pkg.t{ip.Pkg.registered i}) (k: key ip i) : concrete_key
let get_key (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i)
  : concrete_key
  =
  if model then
    let k' : ir_key ip i = k in
    match k' with
    | IdealKey rk _ _ -> rk
    | RealKey rk -> rk
  else k
(* 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

// this file is adapted from HMAC.UFCMA but simpler, and yield
// probabilistic security: the advantage of an adversary guessing the
// random token is just 1/#tokens. (Do we need to enforce a single
// verification attempt?)

let ipkg = Pkg.ipkg
let model = Flags.model
let ideal = Flags.ideal_HMAC
// secret idealization flag for the UF1CMA assumption
//TODO use a separate flag

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

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

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

// formally agile in the KDF algorithm, which controls the token length.
type ha = Hashing.Spec.alg

// initial parameters
noeq type info = {
  parent: r:rgn {~ (is_tls_rgn r)};
  alg: Hashing.Spec.alg; //too loose? Pkg.kdfa;
  good: bool //TODO: should be Type0 instead of bool, and erased, but hard to propagate
}

type tag (u:info) = lbytes32 (Hacl.Hash.Definitions.hash_len u.alg)

let keylen (u:info): Pkg.keylen = Hacl.Hash.Definitions.hash_len u.alg
type keyrepr (u:info) = lbytes (Hashing.Spec.hash_length u.alg)

let goodish (#ip:ipkg) (i:ip.Pkg.t) (u:info) = _: unit{~(safe i) \/ u.good}

private type log_t (#ip:ipkg) (i:ip.Pkg.t) (u:info) (r:rgn) =
  m_rref r (option (goodish #ip i u)) ssa

// runtime (concrete) type of MAC instances
val concrete_key : Type0

val concrete_key_info (k:concrete_key) : info
val concrete_key_repr (k:concrete_key) : keyrepr (concrete_key_info k)

// The model type of instances - either ideal, or real
// The real and concrete version are related by the functional correctness of HMAC
noeq (* abstract *) type ir_key (ip:ipkg) (i:ip.Pkg.t) =
  | IdealKey:
    ck: concrete_key ->
    region: Mem.subrgn (concrete_key_info ck).parent {~(is_tls_rgn region)} ->  // intuitively, the writer's region
    log: log_t i (concrete_key_info ck) region ->
    ir_key ip i
  | RealKey: ck:concrete_key -> ir_key ip i

type key (ip:ipkg) (i:ip.Pkg.t{ip.Pkg.registered i}) =
  (if model
  then k:ir_key ip i{IdealKey? k <==> safe i}
  else concrete_key)

let usage (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i): GTot info =
  if model then
    let k' : ir_key ip i = k in
    match k' with
    | IdealKey ck _ _ -> concrete_key_info ck
    | RealKey ck -> concrete_key_info ck
  else (concrete_key_info k)

let keyval (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i): GTot (keyrepr (usage k)) =
  if model then
    let k' : ir_key ip i = k in
    match k' with
    | IdealKey ck _ _ -> concrete_key_repr ck
    | RealKey ck -> concrete_key_repr ck
  else concrete_key_repr k

let region (#ip:ipkg) (#i:ip.Pkg.t{ip.Pkg.registered i}) (k:key ip i):
  Ghost (subrgn (usage k).parent)
  (requires safe i)
  (ensures fun _ -> True)
  = let IdealKey _ r _ = k <: ir_key ip i in r

let shared_footprint: rset = Set.empty

let footprint (#ip:ipkg) (#i:ip.Pkg.t {ip.Pkg.registered i}) (k:key ip i):
  s:rset{s `Set.disjoint` shared_footprint}
  =
  assume false; //TODO downwards closed set
  if model then
    let k' : ir_key ip i = k in
    match k' with
    | IdealKey _ r _ -> Set.singleton r
    | RealKey _ -> Set.empty
  else Set.empty

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 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 coerce:
  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) -> ST (k:key ip i)
  (requires fun _ -> True)
  (ensures fun h0 k h1 ->
    modifies_none h0 h1 /\
    k == coerceT ip ha_of_i good_of_i i u kv /\
    usage k == u /\
    Pkg.fresh_regions (footprint k) h0 h1)


// not quite doable without reification?
// assert_norm(forall ip i u. (create #ip i u == coerce #ip i u (CoreCrypto.random (UInt32.v (keylen u)))))
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked MiTLS.Flags.fst.checked Hacl.Hash.Definitions.fst.checked FStar.Tactics.fst.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.Token.UF1CMA.fsti
k: MiTLS.Token.UF1CMA.key ip i -> MiTLS.Token.UF1CMA.concrete_key
MiTLS.Token.UF1CMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.__proj__Idx__item__registered MiTLS.Token.UF1CMA.key MiTLS.Token.UF1CMA.model 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 MiTLS.Token.UF1CMA.ir_key Prims.bool
let get_key (#ip: ipkg) (#i: ip.Pkg.t{ip.Pkg.registered i}) (k: key ip i) : concrete_key =
  
if model
then
  let k':ir_key ip i = k in
  match k' with
  | IdealKey rk _ _ -> rk
  | RealKey rk -> rk
else k