val ip:ipkg
val ip:ipkg
let ip : ipkg = Pkg.Idx id (fun _ -> True) (fun _ -> True) (fun _ -> true)
(* 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)))))

private 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

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)
  // we may be more precise to prove ideal functional correctness,

val verify:
  #ip:ipkg -> #i:ip.Pkg.t {ip.Pkg.registered i} -> k:key ip i ->
  t: tag (usage k) -> ST bool
  (requires fun _ -> True)
  (ensures fun h0 b h1 ->
    modifies_none h0 h1 /\
    (b /\ safe i ==> (usage k).good))

type info1 (ip: ipkg) (ha_of_i: ip.Pkg.t -> ha)
  (good_of_i: ip.Pkg.t -> bool) (i: ip.Pkg.t)
  =
  a:info{a.alg = ha_of_i i /\ a.good == good_of_i i}

unfold let localpkg (ip: ipkg) (ha_of_i: (i:ip.Pkg.t -> ha)) (good_of_i: ip.Pkg.t -> bool)
  : Pure (Pkg.local_pkg ip)
  (requires True) (ensures fun p -> p.Pkg.key == key ip /\ p.Pkg.info == info1 ip ha_of_i good_of_i)
  =
  Pkg.LocalPkg
    (key ip)
    (info1 ip ha_of_i good_of_i)
    (fun #_ u -> keylen u )
    (b2t ideal)
    shared_footprint
    footprint // local footprint
    (fun #_ k h -> True) // local invariant
    (fun r i h0 k h1 -> ()) // Local invariant framing
    (fun #i u k h1 -> usage k == u) // create/coerce postcondition
    (fun #i u k h1 r h2 -> ())
    (create ip ha_of_i good_of_i)
    (coerceT ip ha_of_i good_of_i)
    (coerce ip ha_of_i good_of_i)

//TODO (later) support dynamic key compromise


(** The rest of the file is a unit test for the packaging of UFCMA *)

let coerce_eq2 (a:nat -> Type0) (b: (nat -> Type0)) (v:a 0) : Pure (b 0)
  (requires a == b) (ensures fun _ -> True) = v

#set-options "--initial_fuel 1 --max_fuel 2 --initial_ifuel 1 --max_ifuel 2"
open FStar.Tactics
/
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
MiTLS.Token.UF1CMA.ipkg
MiTLS.Pkg.Idx MiTLS.Token.UF1CMA.id Prims.l_True Prims.bool
let ip:ipkg =
  
Pkg.Idx id (fun _ -> True) (fun _ -> True) (fun _ -> true)