val create_in_aes128_gcm:create_in_st AES128_GCM
let create_in_aes128_gcm: create_in_st AES128_GCM = create_in_aes_gcm Vale_AES128
val create_in_aes128_gcm:create_in_st AES128_GCM
let create_in_aes128_gcm:create_in_st AES128_GCM =
create_in_aes_gcm Vale_AES128
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
EverCrypt.AEAD.create_in_aes_gcm Spec.Cipher.Expansion.Vale_AES128
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

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)

let invariant_loc_in_footprint #a s m =
  ()

let frame_invariant #a l s h0 h1 =
  ()


/// Actual stateful API
/// -------------------

let alg_of_state a s =
  let open LowStar.BufferOps in
  let Ek impl _ _ = !*s in
  match impl with
  | Hacl_CHACHA20 -> CHACHA20_POLY1305
  | Vale_AES128 -> AES128_GCM
  | Vale_AES256 -> AES256_GCM

let as_kv #a (Ek _ kv _) =
  G.reveal kv

#push-options "--z3rlimit 10 --max_fuel 0 --max_ifuel 0 --z3cliopt smt.QI.EAGER_THRESHOLD=5"

let create_in_chacha20_poly1305: create_in_st CHACHA20_POLY1305 = fun r dst k ->
  let h0 = ST.get () in
  let ek = B.malloc r 0uy 32ul in
  let p = B.malloc r (Ek Hacl_CHACHA20 (G.hide (B.as_seq h0 k)) ek) 1ul in
  B.blit k 0ul ek 0ul 32ul;
  B.upd dst 0ul p;
  let h2 = ST.get() in
  B.modifies_only_not_unused_in B.(loc_buffer dst) h0 h2;
  Success

#pop-options

inline_for_extraction noextract
let create_in_aes_gcm (i: vale_impl):
  create_in_st (alg_of_vale_impl i) =
fun r dst k ->
  let a = alg_of_vale_impl i in
  let h0 = ST.get () in
  let kv: G.erased (kv a) = G.hide (B.as_seq h0 k) in 
  if EverCrypt.TargetConfig.hacl_can_compile_vale then (
    let has_aesni = EverCrypt.AutoConfig2.has_aesni () in
    let has_pclmulqdq = EverCrypt.AutoConfig2.has_pclmulqdq () in
    let has_avx = EverCrypt.AutoConfig2.has_avx() in
    let has_sse = EverCrypt.AutoConfig2.has_sse() in
    let has_movbe = EverCrypt.AutoConfig2.has_movbe() in
    if (has_aesni && has_pclmulqdq && has_avx && has_sse && has_movbe) then (
      let ek = B.malloc r 0uy (concrete_xkey_len i + 176ul) in

      vale_expand i k ek;

      let h2 = ST.get () in
      B.modifies_only_not_unused_in B.loc_none h0 h2;
      let p = B.malloc r (Ek i (G.hide (B.as_seq h0 k)) ek) 1ul in
      let open LowStar.BufferOps in
      dst *= p;
      let h3 = ST.get() in
      B.modifies_only_not_unused_in B.(loc_buffer dst) h2 h3;
      Success

    ) else
      UnsupportedAlgorithm
  ) else
      UnsupportedAlgorithm
val create_in_aes128_gcm:create_in_st AES128_GCM
EverCrypt.AEAD.create_in_st Spec.Agile.AEAD.AES128_GCM