val create:
  ip:ipkg -> ha_of_i: (ip.Pkg.t -> ha) -> good_of_i: (i:ip.Pkg.t -> Hashing.macable (ha_of_i i) -> 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_none 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: (i:ip.Pkg.t -> Hashing.macable (ha_of_i i) -> 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_none 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_norm(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 = MDM.alloc #_ #_ #_ #_ () in
      IdealKey ck region log
    else
      RealKey ck in
  k <: key ip i
(**! 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

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 = rset_empty ()

let footprint (#ip:ipkg) (#i:ip.Pkg.t {ip.Pkg.registered i}) (k:key ip i): 
  GTot (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 _ -> rset_empty ()
  else rset_empty ()

noextract
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

noextract
val create:
  ip:ipkg -> ha_of_i: (ip.Pkg.t -> ha) -> good_of_i: (i:ip.Pkg.t -> Hashing.macable (ha_of_i i) -> 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_none h0 h1 /\
    usage k == u /\
    Pkg.fresh_regions (footprint k) h0 h1)

#reset-options "--z3rlimit 100 --initial_fuel 1 --max_fuel 1 --initial_ifuel 0 --max_ifuel 0"
/
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

    ip: MiTLS.HMAC.UFCMA.ipkg ->
    ha_of_i: (_: Idx?.t ip -> MiTLS.HMAC.UFCMA.ha) ->
    good_of_i: (i: Idx?.t ip -> _: MiTLS.Hashing.Spec.macable (ha_of_i i) -> Prims.bool) ->
    i: Idx?.t ip {Idx?.registered ip i} ->
    u192: u197: MiTLS.HMAC.UFCMA.info{Info?.alg u197 = ha_of_i i /\ Info?.good u197 == good_of_i i}
  -> FStar.HyperStack.ST.ST (MiTLS.HMAC.UFCMA.key ip i)
MiTLS.HMAC.UFCMA.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.HMAC.UFCMA.ha MiTLS.Hashing.Spec.macable Prims.bool MiTLS.Pkg.__proj__Idx__item__registered MiTLS.HMAC.UFCMA.info Prims.l_and Prims.b2t Prims.op_Equality Spec.Hash.Definitions.hash_alg Prims.l_or EverCrypt.HMAC.is_supported_alg Spec.Hash.Definitions.is_md Prims.op_Negation Spec.Hash.Definitions.is_shake MiTLS.HMAC.UFCMA.__proj__Info__item__alg Prims.eq2 MiTLS.HMAC.UFCMA.__proj__Info__item__good MiTLS.HMAC.UFCMA.key MiTLS.HMAC.UFCMA.ir_key MiTLS.HMAC.UFCMA.IdealKey MiTLS.HMAC.UFCMA.log_t FStar.Monotonic.DependentMap.alloc FStar.Pervasives.Native.tuple2 MiTLS.HMAC.UFCMA.tag MiTLS.HMAC.UFCMA.text MiTLS.HMAC.UFCMA.goodish FStar.DependentMap.t FStar.Monotonic.DependentMap.opt Prims.l_True FStar.Monotonic.DependentMap.t Prims.unit Prims._assert Prims.l_not MiTLS.Mem.is_tls_rgn MiTLS.HMAC.UFCMA.__proj__Info__item__parent MiTLS.Mem.subrgn FStar.HyperStack.ST.new_region FStar.Monotonic.HyperHeap.rid MiTLS.HMAC.UFCMA.RealKey MiTLS.HMAC.UFCMA.is_safe MiTLS.HMAC.UFCMA.concrete_key MiTLS.HMAC.UFCMA.MAC MiTLS.HMAC.UFCMA.keyrepr MiTLS.Random.sample32 Hacl.Hash.Definitions.hash_len FStar.Bytes.lbytes FStar.UInt32.v FStar.Pervasives.assert_norm Spec.Agile.HMAC.keysized Spec.Hash.Definitions.hash_length Prims.op_LessThan Prims.pow2
let create ip _ _ i u =
  
assert_norm (pow2 32 < pow2 61);
assert_norm (pow2 61 < pow2 125);
assert_norm (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 = MDM.alloc #_ #_ #_ #_ () in
    IdealKey ck region log
  else RealKey ck
in
k <: key ip i