val invariant_s: (#a:alg) -> HS.mem -> state_s a -> Type0
let invariant_s #a h (Ek i kv ek) =
  is_supported_alg a /\
  a = supported_alg_of_impl i /\
  B.live h ek /\
  B.length ek >= concrete_xkey_length i /\
  B.as_seq h (B.gsub ek 0ul (UInt32.uint_to_t (concrete_xkey_length i)))
    `S.equal` concrete_expand i (G.reveal kv) /\
  config_pre a /\ (
  match i with
  | Vale_AES128
  | Vale_AES256 ->
      // Expanded key length + precomputed stuff + scratch space (AES-GCM specific)
      B.length ek =
        vale_xkey_length (cipher_alg_of_supported_alg a) + 176
  | Hacl_CHACHA20 ->
      B.length ek = concrete_xkey_length i)
val invariant_s: (#a:alg) -> HS.mem -> state_s a -> Type0
let invariant_s #a h (Ek i kv ek) =
is_supported_alg a /\ a = supported_alg_of_impl i /\ B.live h ek /\
B.length ek >= concrete_xkey_length i /\
(B.as_seq h (B.gsub ek 0ul (UInt32.uint_to_t (concrete_xkey_length i))))
`S.equal`
(concrete_expand i (G.reveal kv)) /\ config_pre a /\
(match i with
  | Vale_AES128
  | Vale_AES256 -> B.length ek = vale_xkey_length (cipher_alg_of_supported_alg a) + 176
  | Hacl_CHACHA20 -> B.length ek = concrete_xkey_length i)
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.Agile.AEAD.alg FStar.Monotonic.HyperStack.mem EverCrypt.AEAD.state_s Spec.Cipher.Expansion.impl FStar.Ghost.erased Spec.Agile.AEAD.kv LowStar.Buffer.buffer FStar.UInt8.t Prims.l_and Prims.b2t Spec.Agile.AEAD.is_supported_alg Prims.op_Equality EverCrypt.AEAD.supported_alg_of_impl LowStar.Monotonic.Buffer.live LowStar.Buffer.trivial_preorder FStar.Integers.op_Greater_Equals FStar.Integers.Signed FStar.Integers.Winfinite LowStar.Monotonic.Buffer.length Spec.Cipher.Expansion.concrete_xkey_length FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq LowStar.Buffer.gsub FStar.UInt32.__uint_to_t FStar.UInt32.uint_to_t Spec.Cipher.Expansion.concrete_expand FStar.Ghost.reveal EverCrypt.AEAD.config_pre Prims.int FStar.Integers.op_Plus Spec.Cipher.Expansion.vale_xkey_length Spec.Agile.AEAD.cipher_alg_of_supported_alg Prims.nat Prims.logical
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.

let supported_alg_of_impl (i: impl): supported_alg =
  match i with
  | Vale_AES128 -> AES128_GCM
  | Vale_AES256 -> AES256_GCM
  | Hacl_CHACHA20 -> CHACHA20_POLY1305

inline_for_extraction noextract
let alg_of_vale_impl (i: vale_impl) =
  match i with
  | Vale_AES128 -> AES128_GCM
  | Vale_AES256 -> AES256_GCM

noeq
type state_s a =
| Ek: impl:impl ->
    kv:G.erased (kv a) ->
    ek:B.buffer UInt8.t -> // concrete expanded key
    state_s a

let invert_state_s (a: alg): Lemma
  (requires True)
  (ensures (inversion (state_s a)))
  [ SMTPat (state_s a) ]
=
  allow_inversion (state_s a)

let freeable_s #a (Ek _ _ ek) = B.freeable ek

let footprint_s #a (Ek _ _ ek) = B.loc_addr_of_buffer ek
val invariant_s: (#a:alg) -> HS.mem -> state_s a -> Type0
h: FStar.Monotonic.HyperStack.mem -> _: EverCrypt.AEAD.state_s a -> Type0