val 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)
val 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 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
(**! Idealizing agile HMAC; independent of TLS, used for TLS 1.3 Finished message payloads and Binders. *)
module MiTLS.HMAC.UFCMA
open MiTLS

open FStar.Bytes
open MiTLS.Mem

module MDM = FStar.Monotonic.DependentMap

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

type lbytes32 n = FStar.Bytes.lbytes (UInt32.v n)

let ipkg = Pkg.ipkg

let model = Flags.model
let ideal = Flags.ideal_HMAC // secret idealization flag for the UFCMA assumption

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

noextract
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

type ha = Hashing.alg

// initial parameters
noeq type info = | Info: 
  parent: rgn {~ (is_tls_rgn parent)} -> 
  alg: HMAC.ha -> 
  good: (Hashing.macable alg -> bool) ->  //TODO: should be Type0 instead of bool, and erased, but hard to propagate
  info

//18-02-25 should we index by i instead?
type text (u:info) = Hashing.macable u.alg
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) = Hashing.hkey u.alg

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

[@unifier_hint_injective]
private type log_t (#ip:ipkg) (i:ip.Pkg.t) (u:info) (r:rgn) =
  MDM.t r (tag u * text u) (fun (t,v) -> goodish i u v) (fun _ -> True) // could constrain size

// runtime (concrete) type of MAC instances
noeq (* abstract *) type concrete_key =
  | MAC: u:info -> k:keyrepr u -> concrete_key

// 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 ck.u.parent {~(is_tls_rgn region)} ->  // intuitively, the writer's region
    log: log_t i ck.u 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)

// 18-02-25 we probably miss indexing by ha_of_i and good_of_i...
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 _ _ -> ck.u
    | RealKey ck      -> ck.u
  else k.u

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 _ _ -> ck.k
    | RealKey ck -> ck.k
  else k.k
/
Spec.Hash.Definitions.fst.checked Spec.Agile.HMAC.fsti.checked Spec.Agile.Hash.fsti.checked prims.fst.checked MiTLS.Random.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.HMAC.fsti.checked MiTLS.Hashing.Spec.fst.checked MiTLS.Hashing.fsti.checked MiTLS.Flags.fst.checked Hacl.Hash.Definitions.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Monotonic.DependentMap.fsti.checked FStar.IO.fst.checked FStar.Bytes.fsti.checked
MiTLS.HMAC.UFCMA.fst
k: MiTLS.HMAC.UFCMA.key ip i
  -> Prims.Ghost (MiTLS.Mem.subrgn (Info?.parent (MiTLS.HMAC.UFCMA.usage k)))
MiTLS.HMAC.UFCMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.__proj__Idx__item__registered MiTLS.HMAC.UFCMA.key MiTLS.HMAC.UFCMA.concrete_key MiTLS.Mem.subrgn MiTLS.HMAC.UFCMA.__proj__Info__item__parent MiTLS.HMAC.UFCMA.__proj__MAC__item__u Prims.l_not Prims.b2t MiTLS.Mem.is_tls_rgn MiTLS.HMAC.UFCMA.log_t MiTLS.HMAC.UFCMA.usage MiTLS.HMAC.UFCMA.ir_key MiTLS.HMAC.UFCMA.safe Prims.l_True
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