val empty_log_framing:
  #ip:ipkg ->
  #aeadAlg_of_i:(ip.t -> aeadAlg) ->
  #index_of_i:(ip.t -> I.id) ->
  #i:ip.t{ip.registered i} ->
  a:info1 #ip aeadAlg_of_i i ->
  k:key ip index_of_i i ->
  h0:mem ->
  r:rid ->
  h1:mem ->
  Lemma
    (requires (empty_log a k h0 /\
               modifies_one r h0 h1 /\
               ~(r `Set.mem` footprint k)))
    (ensures  (empty_log a k h1))
val empty_log_framing:
  #ip:ipkg ->
  #aeadAlg_of_i:(ip.t -> aeadAlg) ->
  #index_of_i:(ip.t -> I.id) ->
  #i:ip.t{ip.registered i} ->
  a:info1 #ip aeadAlg_of_i i ->
  k:key ip index_of_i i ->
  h0:mem ->
  r:rid ->
  h1:mem ->
  Lemma
    (requires (empty_log a k h0 /\
               modifies_one r h0 h1 /\
               ~(r `Set.mem` footprint k)))
    (ensures  (empty_log a k h1))
let empty_log_framing #ip #aeadAlg_of_i #index_of_i #i a k h0 r h1 =
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal _ st ->
      if AE.safeMac (index_of_i i) then
        AE.frame_log st Seq.empty h0 r h1
      else ()
    | Real _ -> ()
(**
  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

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

let footprint #ip #index_of_i #i k =
  Set.lemma_equal_intro (Set.empty `Set.intersect` shared_footprint) Set.empty;
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal _ st -> AE.footprint st
    | Real _ -> Set.empty
  else Set.empty

let invariant #ip #index_of_i #i k h =
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal _ st -> AE.invariant st h
    | Real _ -> True
  else True

let invariant_framing #ip #index_of_i i k h0 r h1 =
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal _ st -> AE.frame_invariant st h0 r h1
    | Real _ -> ()

let empty_log #ip #aeadAlg_of_i #index_of_i #i a k h =
  if model then
    let k: _key index_of_i i = k in
    match k with
    | Ideal _ st ->
      if AE.safeMac (index_of_i i) then
        AE.log st h == Seq.empty
      else True
    | Real _ -> True
  else True
/
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

    a: MiTLS.AEAD.Pkg.info1 aeadAlg_of_i i ->
    k: MiTLS.AEAD.Pkg.key ip index_of_i i ->
    h0: FStar.Monotonic.HyperStack.mem ->
    r: FStar.Monotonic.HyperHeap.rid ->
    h1: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
      (requires
        MiTLS.AEAD.Pkg.empty_log a k h0 /\ FStar.Monotonic.HyperStack.modifies_one r h0 h1 /\
        ~(FStar.Set.mem r (MiTLS.AEAD.Pkg.footprint k))) (ensures MiTLS.AEAD.Pkg.empty_log a k h1)
MiTLS.Pkg.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.AEAD.Pkg.aeadAlg MiTLS.Crypto.Indexing.id MiTLS.Pkg.__proj__Idx__item__registered MiTLS.AEAD.Pkg.info1 MiTLS.AEAD.Pkg.key FStar.Monotonic.HyperStack.mem FStar.Monotonic.HyperHeap.rid MiTLS.Mem.model MiTLS.AEAD.Pkg.concrete_key MiTLS.AEAD.aead_state MiTLS.Crypto.Indexing.Writer MiTLS.AEAD.safeMac MiTLS.AEAD.frame_log FStar.Seq.Base.empty MiTLS.AEAD.entry Prims.bool Prims.unit MiTLS.AEAD.Pkg._key
let empty_log_framing #ip #aeadAlg_of_i #index_of_i #i a k h0 r h1 =
  
if model
then
  let k:_key index_of_i i = k in
  match k with
  | Ideal _ st -> if AE.safeMac (index_of_i i) then AE.frame_log st Seq.empty h0 r h1
  | Real _ -> ()