val evercrypt_aeadAlg_option_of_aead_cipher: aeadAlg -> option EverCrypt.aead_alg
val evercrypt_aeadAlg_option_of_aead_cipher: aeadAlg -> option EverCrypt.aead_alg
let evercrypt_aeadAlg_option_of_aead_cipher : aeadAlg -> option EverCrypt.aead_alg =
  let open MiTLS.EverCrypt in 
  function
  | AES128_GCM        -> Some AES128_GCM
  | AES256_GCM        -> Some AES256_GCM
  | CHACHA20_POLY1305 -> Some CHACHA20_POLY1305
  | _                 -> None
module MiTLS.AEADProvider
open MiTLS

open FStar.Heap
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Seq
open FStar.Bytes

open MiTLS.Mem
open MiTLS.TLSConstants
module TInfo = MiTLS.TLSInfo
open FStar.UInt32

module HS = FStar.HyperStack
module U8 = FStar.UInt8
module U32 = FStar.UInt32
module E = MiTLS.EverCrypt
module LB = LowStar.Buffer
module CI = MiTLS.Crypto.Indexing
module Plain = MiTLS.Crypto.Plain
module CB = MiTLS.Crypto.Symmetric.Bytes

let discard (b:bool) : ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1)) = ()
let print (s:string) : ST unit (requires fun _ -> True) (ensures (fun h0 _ h1 -> h0 == h1)) =
  discard (IO.debug_print_string ("AEP| "^s^"\n"))
unfold let dbg : string -> ST unit (requires (fun _ -> True)) (ensures (fun h0 _ h1 -> h0 == h1)) =
  if DebugFlags.debug_AEP then print else (fun _ -> ())

(***********************************************************************)

type id = i:TInfo.id{~(TInfo.PlaintextID? i) /\ AEAD? (TInfo.aeAlg_of_id i)}
let alg (i:id): aeadAlg = let AEAD aead _ = TInfo.aeAlg_of_id i in aead

//18-09-04  unclear what's shadowing alg below
let alg' (i:id): aeadAlg = let AEAD aead _ = TInfo.aeAlg_of_id i in aead
/
prims.fst.checked MiTLS.TLSInfo.fst.checked MiTLS.TLSConstants.fsti.checked MiTLS.Random.fst.checked MiTLS.Mem.fst.checked MiTLS.Flag.fst.checked MiTLS.EverCrypt.Specs.fsti.checked MiTLS.EverCrypt.fsti.checked MiTLS.DebugFlags.fst.checked MiTLS.Crypto.Symmetric.Bytes.fst.checked MiTLS.Crypto.Plain.fsti.checked MiTLS.Crypto.Indexing.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.IO.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Bytes.fsti.checked EverCrypt.Helpers.fsti.checked
MiTLS.AEADProvider.fsti
_: MiTLS.CipherSuite.aeadAlg -> FStar.Pervasives.Native.option MiTLS.EverCrypt.aead_alg
MiTLS.CipherSuite.aeadAlg FStar.Pervasives.Native.Some MiTLS.EverCrypt.aead_alg MiTLS.EverCrypt.AES128_GCM MiTLS.EverCrypt.AES256_GCM MiTLS.EverCrypt.CHACHA20_POLY1305 FStar.Pervasives.Native.None FStar.Pervasives.Native.option
let evercrypt_aeadAlg_option_of_aead_cipher: aeadAlg -> option EverCrypt.aead_alg =
  
let open MiTLS.EverCrypt in
function
| AES128_GCM -> Some AES128_GCM
| AES256_GCM -> Some AES256_GCM
| CHACHA20_POLY1305 -> Some CHACHA20_POLY1305
| _ -> None