val keyval:
  #ip:ipkg ->
  #index_of_i:(ip.t -> I.id) ->
  #i:ip.t{ip.registered i} ->
  k:key ip index_of_i i ->
  GTot (keyrepr (usage k))
val keyval:
  #ip:ipkg ->
  #index_of_i:(ip.t -> I.id) ->
  #i:ip.t{ip.registered i} ->
  k:key ip index_of_i i ->
  GTot (keyrepr (usage k))
let keyval #ip #index_of_i #i k =
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal ck _ -> ck.k
    | Real ck -> ck.k
  else k.k
(**
  This modules packages AEAD.fsti as a "local package" and provides
  a functor for constructing an AEAD package from an index package

  TODO:
  The next step is to restore AEADProvider using a compile-time flag to multiplex
  between the 3 different providers: Low (verified), LowC (verification lost in translation)
  and OpenSSL. This compile-time flag is such that ~Low ==> ~model
  (we only idealize if the provider is Low).

  TODO:
  As a verification unit-test, we may show how to package two
  instances of AEAD (for both directions) from the same create/coerce
  on their concatenated keys, in TLS 1.2 style.
*)
module MiTLS.AEAD.Pkg
open MiTLS

open FStar.Bytes

open MiTLS.Mem
open MiTLS.Pkg

module AE = MiTLS.AEAD
module I  = MiTLS.Crypto.Indexing

noeq type concrete_key =
  | AEAD: u:info -> k:keyrepr u -> concrete_key

noeq type _key (#ip:ipkg) (index_of_i:ip.t -> I.id) (i:ip.t) =
  | Ideal:
    ck: concrete_key ->
//    region: subrgn ck.u.parent{~(is_tls_rgn region)} ->
    state: AE.aead_state (index_of_i i) I.Writer ->
    _key #ip index_of_i i
  | Real:
    ck: concrete_key -> _key #ip index_of_i i

let is_ideal #_ #_ #_ k = Ideal? k

let usage #ip #index_of_i #i k =
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal ck _ -> ck.u
    | Real ck -> ck.u
  else k.u
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Crypto.Indexing.fst.checked MiTLS.AEAD.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.AEAD.Pkg.fst
k: MiTLS.AEAD.Pkg.key ip index_of_i i
  -> Prims.GTot (MiTLS.AEAD.Pkg.keyrepr (MiTLS.AEAD.Pkg.usage k))
MiTLS.Pkg.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Crypto.Indexing.id MiTLS.Pkg.__proj__Idx__item__registered MiTLS.AEAD.Pkg.key MiTLS.Mem.model MiTLS.AEAD.Pkg.concrete_key MiTLS.AEAD.aead_state MiTLS.Crypto.Indexing.Writer MiTLS.AEAD.Pkg.__proj__AEAD__item__k MiTLS.AEAD.Pkg.keyrepr MiTLS.AEAD.Pkg.usage MiTLS.AEAD.Pkg._key Prims.bool
let keyval #ip #index_of_i #i k =
  
if model
then
  let k:_key index_of_i i = k in
  match k with
  | Ideal ck _ -> ck.k
  | Real ck -> ck.k
else k.k