val is_safe (#ip: ipkg) (i: ip.t{ip.registered i})
    : ST bool
      (requires fun _ -> True)
      (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
val is_safe (#ip: ipkg) (i: ip.t{ip.registered i})
    : ST bool
      (requires fun _ -> True)
      (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i))
let is_safe (#ip:ipkg) (i:ip.t{ip.registered i}) : ST bool
  (requires fun _ -> True)
  (ensures  fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i)) =
  let honest = ip.get_honesty i in
  ideal && honest
(**
  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

/// TODO package instead StAE? what to do with the algorithm?

type aeadAlg =
  | AES_GCM128
  | AES_GCM256

let ideal : (b:bool{b ==> model}) =
  assume (b2t Flags.ideal_AEAD ==> model);
  Flags.ideal_AEAD

type safe (#ip:ipkg) (i:ip.t) = ideal /\ ip.honest i
/
prims.fst.checked MiTLS.Pkg.fst.checked MiTLS.Mem.fst.checked MiTLS.Flags.fst.checked MiTLS.Crypto.Indexing.fst.checked MiTLS.AEAD.fsti.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Pervasives.fsti.checked FStar.Bytes.fsti.checked
MiTLS.AEAD.Pkg.fsti
i: Idx?.t ip {Idx?.registered ip i} -> FStar.HyperStack.ST.ST Prims.bool
MiTLS.Pkg.ipkg MiTLS.Pkg.__proj__Idx__item__t MiTLS.Pkg.__proj__Idx__item__registered Prims.op_AmpAmp MiTLS.AEAD.Pkg.ideal Prims.bool MiTLS.Pkg.__proj__Idx__item__get_honesty FStar.Monotonic.HyperStack.mem Prims.l_True Prims.l_and FStar.HyperStack.ST.modifies_none Prims.l_iff Prims.b2t MiTLS.AEAD.Pkg.safe
let is_safe (#ip: ipkg) (i: ip.t{ip.registered i})
    : ST bool
      (requires fun _ -> True)
      (ensures fun h0 b h1 -> modifies_none h0 h1 /\ (b <==> safe i)) =
  
let honest = ip.get_honesty i in
ideal && honest