val supported_alg_of_impl (i: impl) : supported_alg
let supported_alg_of_impl (i: impl): supported_alg =
  match i with
  | Vale_AES128 -> AES128_GCM
  | Vale_AES256 -> AES256_GCM
  | Hacl_CHACHA20 -> CHACHA20_POLY1305
val supported_alg_of_impl (i: impl) : supported_alg
let supported_alg_of_impl (i: impl) : supported_alg =
match i with
| Vale_AES128 -> AES128_GCM
| Vale_AES256 -> AES256_GCM
| Hacl_CHACHA20 -> CHACHA20_POLY1305
EverCrypt.AEAD.fst.checked
Vale.Wrapper.X64.GCMencryptOpt256.fsti.checked Vale.Wrapper.X64.GCMencryptOpt.fsti.checked Vale.Wrapper.X64.GCMdecryptOpt256.fsti.checked Vale.Wrapper.X64.GCMdecryptOpt.fsti.checked Vale.Wrapper.X64.GCM_IV.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.OptPublic.fsti.checked Vale.AES.GCM_s.fst.checked Vale.AES.AES_s.fst.checked Spec.Cipher.Expansion.fst.checked Spec.Cipher.Expansion.fst.checked Spec.Agile.AEAD.fst.checked Spec.Agile.AEAD.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.Failure.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked EverCrypt.TargetConfig.fsti.checked EverCrypt.CTR.Keys.fst.checked EverCrypt.CTR.Keys.fst.checked EverCrypt.Chacha20Poly1305.fsti.checked EverCrypt.AutoConfig2.fsti.checked
EverCrypt.AEAD.fst
Spec.Cipher.Expansion.impl Spec.Agile.AEAD.AES128_GCM Spec.Agile.AEAD.AES256_GCM Spec.Agile.AEAD.CHACHA20_POLY1305 Spec.Agile.AEAD.supported_alg
module EverCrypt.AEAD

module S = FStar.Seq
module G = FStar.Ghost

module HS = FStar.HyperStack
module ST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module B = LowStar.Buffer

open FStar.HyperStack.ST
open FStar.Integers
open FStar.Int.Cast

open Spec.Agile.AEAD
open Spec.Cipher.Expansion
open EverCrypt.CTR.Keys

friend Spec.Agile.AEAD
friend Spec.Cipher.Expansion
friend EverCrypt.CTR.Keys

#set-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0"

/// Defining abstract predicates, invariants, footprint, etc.
/// ---------------------------------------------------------

let _: squash (inversion impl) = allow_inversion impl

/// We now distinguish between an expanded key (as mandated by NIST spec) and a
/// **concrete** expanded key, which may contain implementation-specific details
/// and extra precomputations. In the rest of this module, we rely on concrete
/// expanded keys, which are parameterized over an implementation, instead of
/// regular expanded keys, which are parameterized over an algorithm. Helpers
/// allow us to move from one notion to the other.
val supported_alg_of_impl (i: impl) : supported_alg
i: Spec.Cipher.Expansion.impl -> Spec.Agile.AEAD.supported_alg