val decrypt_expand_aes128_gcm: decrypt_expand_st true AES128_GCM
let decrypt_expand_aes128_gcm : decrypt_expand_st true AES128_GCM =
  fun k iv iv_len ad ad_len cipher cipher_len tag dst ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    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
    let has_aesni = EverCrypt.AutoConfig2.has_aesni () in
    if  (has_aesni && has_pclmulqdq && has_avx && has_sse && has_movbe) then
      decrypt_expand_aes_gcm Vale_AES128 k iv iv_len ad ad_len cipher cipher_len tag dst
    else
      UnsupportedAlgorithm
  else
    UnsupportedAlgorithm
val decrypt_expand_aes128_gcm: decrypt_expand_st true AES128_GCM
let decrypt_expand_aes128_gcm:decrypt_expand_st true AES128_GCM =
fun k iv iv_len ad ad_len cipher cipher_len tag dst ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale
  then
    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
    let has_aesni = EverCrypt.AutoConfig2.has_aesni () in
    if (has_aesni && has_pclmulqdq && has_avx && has_sse && has_movbe)
    then decrypt_expand_aes_gcm Vale_AES128 k iv iv_len ad ad_len cipher cipher_len tag dst
    else UnsupportedAlgorithm
  else UnsupportedAlgorithm
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
LowStar.Buffer.buffer EverCrypt.CTR.Keys.uint8 Prims.b2t Prims.op_Equality Prims.int Prims.l_or Prims.op_GreaterThanOrEqual FStar.Integers.op_Greater_Equals FStar.Integers.Signed FStar.Integers.Winfinite LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Spec.Agile.AEAD.key_length Spec.Agile.AEAD.AES128_GCM EverCrypt.AEAD.iv_p FStar.UInt32.t Prims.l_and FStar.Integers.within_bounds FStar.Integers.Unsigned FStar.Integers.W32 FStar.Integers.v FStar.Integers.op_Greater EverCrypt.AEAD.ad_p FStar.Integers.op_Less_Equals Prims.pow2 EverCrypt.AEAD.cipher_p Spec.Agile.AEAD.tag_length Prims.nat EverCrypt.TargetConfig.hacl_can_compile_vale Prims.op_AmpAmp EverCrypt.AEAD.decrypt_expand_aes_gcm Spec.Cipher.Expansion.Vale_AES128 EverCrypt.Error.error_code Prims.bool EverCrypt.Error.UnsupportedAlgorithm EverCrypt.AutoConfig2.has_aesni EverCrypt.AutoConfig2.has_movbe EverCrypt.AutoConfig2.has_sse EverCrypt.AutoConfig2.has_avx EverCrypt.AutoConfig2.has_pclmulqdq EverCrypt.AEAD.decrypt_expand_st
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
  

let create_in_aes128_gcm: create_in_st AES128_GCM = create_in_aes_gcm Vale_AES128
let create_in_aes256_gcm: create_in_st AES256_GCM = create_in_aes_gcm Vale_AES256

let create_in #a r dst k =
  match a with
  | AES128_GCM -> create_in_aes128_gcm r dst k
  | AES256_GCM -> create_in_aes256_gcm r dst k
  | CHACHA20_POLY1305 -> create_in_chacha20_poly1305 r dst k
  | _ -> UnsupportedAlgorithm

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

inline_for_extraction noextract
let alloca_chacha20_poly1305: alloca_st CHACHA20_POLY1305 =
  fun k ->
  let h0 = ST.get () in
  let ek = B.alloca 0uy 32ul in
  let p = B.alloca (Ek Hacl_CHACHA20 (G.hide (B.as_seq h0 k)) ek) 1ul in
  B.blit k 0ul ek 0ul 32ul;
  let h3 = ST.get() in
  B.modifies_only_not_unused_in B.loc_none h0 h3;
  p

#pop-options

inline_for_extraction noextract
let alloca_aes_gcm (i: vale_impl):
  alloca_st (alg_of_vale_impl i) =
  fun 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
  let ek = B.alloca 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.alloca (Ek i (G.hide (B.as_seq h0 k)) ek) 1ul in
  p

inline_for_extraction noextract
let alloca_aes128_gcm: alloca_st AES128_GCM =
  alloca_aes_gcm Vale_AES128

inline_for_extraction noextract
let alloca_aes256_gcm: alloca_st AES256_GCM =
  alloca_aes_gcm Vale_AES256

let alloca #a k =
  match a with
  | AES128_GCM -> alloca_aes128_gcm k
  | AES256_GCM -> alloca_aes256_gcm k
  | CHACHA20_POLY1305 -> alloca_chacha20_poly1305 k

inline_for_extraction noextract
let aes_gcm_encrypt (i: vale_impl):
  Vale.Wrapper.X64.GCMencryptOpt.encrypt_opt_stdcall_st (vale_alg_of_vale_impl i) =
  match i with
  | Vale_AES128 -> Vale.Wrapper.X64.GCMencryptOpt.gcm128_encrypt_opt_stdcall
  | Vale_AES256 -> Vale.Wrapper.X64.GCMencryptOpt256.gcm256_encrypt_opt_stdcall

#reset-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Seq.Properties.slice_slice'"
inline_for_extraction noextract
let encrypt_aes_gcm (i: vale_impl): encrypt_st (alg_of_vale_impl i) =
fun s iv iv_len ad ad_len plain plain_len cipher tag ->
  if B.is_null s then
    InvalidKey
  else
    let a = alg_of_vale_impl i in
    // This condition is never satisfied in F* because of the iv_length precondition on iv.
    // We keep it here to be defensive when extracting to C
    if iv_len = 0ul then
      InvalidIVLength
    else
      let open LowStar.BufferOps in
      let Ek _ kv ek = !*s in
      assert (
        let k = G.reveal kv in
        let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
        let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in
        Vale.AES.AES_s.is_aes_key_LE (vale_alg_of_alg a) k_w);

      push_frame();
      let scratch_b = B.sub ek (concrete_xkey_len i) 176ul in

      let ek = B.sub ek 0ul (concrete_xkey_len i) in
      let keys_b = B.sub ek 0ul (key_offset i) in
      let hkeys_b = B.sub ek (key_offset i) 128ul in

      let h0 = get() in

      // The iv can be arbitrary length, hence we need to allocate a new one to perform the hashing
      let tmp_iv = B.alloca 0uy 16ul in

      // There is no SMTPat on le_bytes_to_seq_quad32_to_bytes and the converse,
      // so we need an explicit lemma
      let lemma_hkeys_reqs () : Lemma
        (let k = G.reveal kv in
        let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
        let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in
        Vale.AES.OptPublic.hkeys_reqs_pub
          (Vale.Def.Types_s.le_bytes_to_seq_quad32 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b)))
          (Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.AES_s.aes_encrypt_LE (vale_alg_of_alg a) k_w (Vale.Def.Words_s.Mkfour 0 0 0 0))))
      = let k = G.reveal kv in
          let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
          let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in
          let hkeys_quad = Vale.AES.OptPublic.get_hkeys_reqs (Vale.Def.Types_s.reverse_bytes_quad32 (
            Vale.AES.AES_s.aes_encrypt_LE (vale_alg_of_alg a) k_w (Vale.Def.Words_s.Mkfour 0 0 0 0))) in
          let hkeys = Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 (Vale.Def.Types_s.le_seq_quad32_to_bytes hkeys_quad) in
          assert (Seq.equal (B.as_seq h0 hkeys_b) hkeys);
          calc (==) {
            Vale.Def.Types_s.le_bytes_to_seq_quad32 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 hkeys);
            (==) { Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes hkeys_quad }
            hkeys_quad;
          }

      in lemma_hkeys_reqs ();

      // We perform the hashing of the iv. The extra buffer and the hashed iv are the same
      Vale.Wrapper.X64.GCM_IV.compute_iv (vale_alg_of_alg a)
      (let k = G.reveal kv in
        let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
        let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in G.hide k_w )
        iv iv_len
        tmp_iv tmp_iv
        hkeys_b;

      let h0 = get() in

      aes_gcm_encrypt i
        (let k = G.reveal kv in
        let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
        let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in G.hide k_w)
        (Ghost.hide (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 iv)))
        plain
        (uint32_to_uint64 plain_len)
        ad
        (uint32_to_uint64 ad_len)
        tmp_iv
        cipher
        tag
        keys_b
        hkeys_b
        scratch_b;

      let h1 = get() in

      // This assert is needed for z3 to pick up sequence equality for ciphertext
      // and tag. It could be avoided if the spec returned both instead of appending them
      assert (
        let kv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (G.reveal kv) in
        let iv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 iv) in
        // `ad` is called `auth` in Vale world; "additional data", "authenticated
        // data", potato, potato
        let ad_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 ad) in
        let plain_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 plain) in
        let cipher_nat, tag_nat =
          Vale.AES.GCM_s.gcm_encrypt_LE (vale_alg_of_alg a) kv_nat iv_nat plain_nat ad_nat
        in
        Seq.equal (B.as_seq h1 cipher) (Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 cipher_nat) /\
        Seq.equal (B.as_seq h1 tag) (Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 tag_nat));


      pop_frame();
      Success

let encrypt_aes128_gcm (_: squash (EverCrypt.TargetConfig.hacl_can_compile_vale)):
  encrypt_st AES128_GCM =
  fun s iv iv_len ad ad_len plain plain_len cipher tag ->
    if EverCrypt.TargetConfig.hacl_can_compile_vale then
      encrypt_aes_gcm Vale_AES128 s iv iv_len ad ad_len plain plain_len cipher tag
    else
      let () = false_elim () in
      LowStar.Failure.failwith "statically unreachable"

let encrypt_aes256_gcm (_: squash (EverCrypt.TargetConfig.hacl_can_compile_vale)):
  encrypt_st AES256_GCM =
  fun s iv iv_len ad ad_len plain plain_len cipher tag ->
    if EverCrypt.TargetConfig.hacl_can_compile_vale then
      encrypt_aes_gcm Vale_AES256 s iv iv_len ad ad_len plain plain_len cipher tag
    else
      let () = false_elim () in
      LowStar.Failure.failwith "statically unreachable"

let encrypt #a s iv iv_len ad ad_len plain plain_len cipher tag =
  if B.is_null s then
    InvalidKey
  else
    let open LowStar.BufferOps in
    let Ek i kv ek = !*s in
    match i with
    | Vale_AES128 ->
        encrypt_aes128_gcm () s iv iv_len ad ad_len plain plain_len cipher tag
    | Vale_AES256 ->
        encrypt_aes256_gcm () s iv iv_len ad ad_len plain plain_len cipher tag
    | Hacl_CHACHA20 ->
        // This condition is never satisfied in F* because of the iv_length precondition on iv.
        // We keep it here to be defensive when extracting to C
        if iv_len <> 12ul then
          InvalidIVLength
        else begin
          // Length restrictions
          assert_norm (pow2 31 + pow2 32 / 64 <= pow2 32 - 1);
          EverCrypt.Chacha20Poly1305.aead_encrypt
            ek iv ad_len ad plain_len plain cipher tag;
          Success
        end

inline_for_extraction noextract
let encrypt_expand_aes_gcm (i: vale_impl): encrypt_expand_st false (alg_of_vale_impl i) =
  fun k iv iv_len ad ad_len plain plain_len cipher tag ->
  push_frame ();
  (* Allocate the state *)
  let s : B.pointer_or_null (state_s (alg_of_vale_impl i)) = alloca k in
  let r = encrypt_aes_gcm i s iv iv_len ad ad_len plain plain_len cipher tag in
  assert(r == Success);
  pop_frame ();
  Success

let encrypt_expand_aes128_gcm_no_check : encrypt_expand_st false AES128_GCM =
  fun k iv iv_len ad ad_len plain plain_len cipher tag ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    encrypt_expand_aes_gcm Vale_AES128 k iv iv_len ad ad_len plain plain_len cipher tag
  else
    LowStar.Failure.failwith "EverCrypt was compiled on a system which doesn't support Vale"

let encrypt_expand_aes256_gcm_no_check : encrypt_expand_st false AES256_GCM =
  fun k iv iv_len ad ad_len plain plain_len cipher tag ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    encrypt_expand_aes_gcm Vale_AES256 k iv iv_len ad ad_len plain plain_len cipher tag
  else
    LowStar.Failure.failwith "EverCrypt was compiled on a system which doesn't support Vale"

let encrypt_expand_aes128_gcm : encrypt_expand_st true AES128_GCM =
  fun k iv iv_len ad ad_len plain plain_len cipher tag  ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    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
    let has_aesni = EverCrypt.AutoConfig2.has_aesni () in
    if  (has_aesni && has_pclmulqdq && has_avx && has_sse && has_movbe) then
      encrypt_expand_aes_gcm Vale_AES128 k iv iv_len ad ad_len plain plain_len cipher tag
    else
      UnsupportedAlgorithm
  else
    UnsupportedAlgorithm

let encrypt_expand_aes256_gcm : encrypt_expand_st true AES256_GCM =
  fun k iv iv_len ad ad_len plain plain_len cipher tag  ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    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
    let has_aesni = EverCrypt.AutoConfig2.has_aesni () in
    if  (has_aesni && has_pclmulqdq && has_avx && has_sse && has_movbe) then
      encrypt_expand_aes_gcm Vale_AES256 k iv iv_len ad ad_len plain plain_len cipher tag
    else
      UnsupportedAlgorithm
  else
    UnsupportedAlgorithm

let encrypt_expand_chacha20_poly1305 : encrypt_expand_st false CHACHA20_POLY1305 =
  fun k iv iv_len ad ad_len plain plain_len cipher tag ->
  push_frame ();
  (* Allocate the state *)
  let s : B.pointer_or_null (state_s CHACHA20_POLY1305) = alloca k in
  let open LowStar.BufferOps in
  let Ek i kv ek = !*s in
  EverCrypt.Chacha20Poly1305.aead_encrypt ek iv ad_len ad plain_len plain cipher tag;
  pop_frame ();
  Success

let encrypt_expand #a k iv iv_len ad ad_len plain plain_len cipher tag =
  match a with
  | AES128_GCM ->
    encrypt_expand_aes128_gcm k iv iv_len ad ad_len plain plain_len cipher tag
  | AES256_GCM ->
    encrypt_expand_aes256_gcm k iv iv_len ad ad_len plain plain_len cipher tag
  | CHACHA20_POLY1305 ->
    encrypt_expand_chacha20_poly1305 k iv iv_len ad ad_len plain plain_len cipher tag

inline_for_extraction noextract
let aes_gcm_decrypt (i: vale_impl):
  Vale.Wrapper.X64.GCMdecryptOpt.decrypt_opt_stdcall_st (vale_alg_of_vale_impl i) =
  match i with
  | Vale_AES128 -> Vale.Wrapper.X64.GCMdecryptOpt.gcm128_decrypt_opt_stdcall
  | Vale_AES256 -> Vale.Wrapper.X64.GCMdecryptOpt256.gcm256_decrypt_opt_stdcall

#reset-options "--z3rlimit 100 --max_fuel 0 --max_ifuel 0 --using_facts_from '* -FStar.Seq.Properties.slice_slice'"
inline_for_extraction noextract
let decrypt_aes_gcm (i: vale_impl): decrypt_st (alg_of_vale_impl i) =
fun s iv iv_len ad ad_len cipher cipher_len tag dst ->
  if B.is_null s then
    InvalidKey
  else
    // This condition is never satisfied in F* because of the iv_length precondition on iv.
    // We keep it here to be defensive when extracting to C
    if iv_len = 0ul then
      InvalidIVLength
    else
      let a = alg_of_vale_impl i in
      let open LowStar.BufferOps in
      let Ek _ kv ek = !*s in
        assert (
          let k = G.reveal kv in
          let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
          let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in
          Vale.AES.AES_s.is_aes_key_LE (vale_alg_of_alg a) k_w);

        push_frame();
        let scratch_b = B.sub ek (concrete_xkey_len i) 176ul in

        let ek = B.sub ek 0ul (concrete_xkey_len i) in
        let keys_b = B.sub ek 0ul (key_offset i) in
        let hkeys_b = B.sub ek (key_offset i) 128ul in

        let h0 = get() in

        // The iv can be arbitrary length, hence we need to allocate a new one to perform the hashing
        let tmp_iv = B.alloca 0uy 16ul in

        // There is no SMTPat on le_bytes_to_seq_quad32_to_bytes and the converse,
        // so we need an explicit lemma
        let lemma_hkeys_reqs () : Lemma
          (let k = G.reveal kv in
          let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
          let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in
          Vale.AES.OptPublic.hkeys_reqs_pub
            (Vale.Def.Types_s.le_bytes_to_seq_quad32 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 hkeys_b)))
            (Vale.Def.Types_s.reverse_bytes_quad32 (Vale.AES.AES_s.aes_encrypt_LE (vale_alg_of_alg a) k_w (Vale.Def.Words_s.Mkfour 0 0 0 0))))
        = let k = G.reveal kv in
              let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
              let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in
              let hkeys_quad = Vale.AES.OptPublic.get_hkeys_reqs (Vale.Def.Types_s.reverse_bytes_quad32 (
              Vale.AES.AES_s.aes_encrypt_LE (vale_alg_of_alg a) k_w (Vale.Def.Words_s.Mkfour 0 0 0 0))) in
              let hkeys = Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 (Vale.Def.Types_s.le_seq_quad32_to_bytes hkeys_quad) in
              assert (Seq.equal (B.as_seq h0 hkeys_b) hkeys);
              calc (==) {
              Vale.Def.Types_s.le_bytes_to_seq_quad32 (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 hkeys);
              (==) { Vale.Arch.Types.le_bytes_to_seq_quad32_to_bytes hkeys_quad }
              hkeys_quad;
              }

        in lemma_hkeys_reqs ();

        // We perform the hashing of the iv. The extra buffer and the hashed iv are the same
        Vale.Wrapper.X64.GCM_IV.compute_iv (vale_alg_of_alg a)
        (let k = G.reveal kv in
          let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
          let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in G.hide k_w )
          iv iv_len
          tmp_iv tmp_iv
          hkeys_b;

        let r = aes_gcm_decrypt i
          (let k = G.reveal kv in
          let k_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 k in
          let k_w = Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE k_nat in G.hide k_w)
          (Ghost.hide (Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 iv)))
          cipher
          (uint32_to_uint64 cipher_len)
          ad
          (uint32_to_uint64 ad_len)
          tmp_iv
          dst
          tag
          keys_b
          hkeys_b
          scratch_b in

        let h1 = get() in

        // This assert is needed for z3 to pick up sequence equality for ciphertext
        // It could be avoided if the spec returned both instead of appending them
        assert (
          let kv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (G.reveal kv) in
          let iv_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 iv) in
          // `ad` is called `auth` in Vale world; "additional data", "authenticated
          // data", potato, potato
          let ad_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 ad) in
          let cipher_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 cipher) in
          let tag_nat = Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8 (B.as_seq h0 tag) in
          let plain_nat, success =
            Vale.AES.GCM_s.gcm_decrypt_LE (vale_alg_of_alg a) kv_nat iv_nat cipher_nat ad_nat tag_nat
          in
          Seq.equal (B.as_seq h1 dst) (Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 plain_nat) /\
          (UInt64.v r = 0) == success);

        assert (
          let kv = G.reveal kv in
          let cipher_tag = B.as_seq h0 cipher `S.append` B.as_seq h0 tag in
          Seq.equal (Seq.slice cipher_tag (S.length cipher_tag - tag_length a) (S.length cipher_tag))
            (B.as_seq h0 tag) /\
          Seq.equal (Seq.slice cipher_tag 0 (S.length cipher_tag - tag_length a)) (B.as_seq h0 cipher));

        pop_frame();

        if r = 0uL then
          Success
        else
          AuthenticationFailure

let decrypt_aes128_gcm (_: squash (EverCrypt.TargetConfig.hacl_can_compile_vale)):
  decrypt_st AES128_GCM =
  fun s iv iv_len ad ad_len cipher cipher_len tag dst ->
    if EverCrypt.TargetConfig.hacl_can_compile_vale then
      decrypt_aes_gcm Vale_AES128 s iv iv_len ad ad_len cipher cipher_len tag dst
    else
      let () = false_elim () in
      LowStar.Failure.failwith "statically unreachable"

let decrypt_aes256_gcm (_: squash (EverCrypt.TargetConfig.hacl_can_compile_vale)):
  decrypt_st AES256_GCM =
  fun s iv iv_len ad ad_len cipher cipher_len tag dst ->
    if EverCrypt.TargetConfig.hacl_can_compile_vale then
      decrypt_aes_gcm Vale_AES256 s iv iv_len ad ad_len cipher cipher_len tag dst
    else
      let () = false_elim () in
      LowStar.Failure.failwith "statically unreachable"

let decrypt_chacha20_poly1305 : decrypt_st CHACHA20_POLY1305 =
  fun s iv iv_len ad ad_len cipher cipher_len tag dst ->
  if B.is_null s then
    InvalidKey
  else
    // This condition is never satisfied in F* because of the iv_length precondition on iv.
    // We keep it here to be defensive when extracting to C
    if iv_len <> 12ul then
      InvalidIVLength
    else begin
      let open LowStar.BufferOps in
      let Ek i kv ek = !*s in
      [@ inline_let ] let bound = pow2 32 - 1 - 16 in
      assert (v cipher_len <= bound);
      assert_norm (bound + 16 <= pow2 32 - 1);
      assert_norm (pow2 31 + bound / 64 <= pow2 32 - 1);

      let h0 = ST.get () in
      let r = EverCrypt.Chacha20Poly1305.aead_decrypt
        ek iv ad_len ad cipher_len dst cipher tag
      in
      assert (
        let cipher_tag = B.as_seq h0 cipher `S.append` B.as_seq h0 tag in
        let tag_s = S.slice cipher_tag (S.length cipher_tag - tag_length CHACHA20_POLY1305) (S.length cipher_tag) in
        let cipher_s = S.slice cipher_tag 0 (S.length cipher_tag - tag_length CHACHA20_POLY1305) in
        S.equal cipher_s (B.as_seq h0 cipher) /\ S.equal tag_s (B.as_seq h0 tag));

      if r = 0ul then
        Success
      else
        AuthenticationFailure
    end

let decrypt #a s iv iv_len ad ad_len cipher cipher_len tag dst =
  if B.is_null s then
     InvalidKey
  else
    let open LowStar.BufferOps in
    let Ek i kv ek = !*s in
    match i with
    | Vale_AES128 ->
        decrypt_aes128_gcm () s iv iv_len ad ad_len cipher cipher_len tag dst
    | Vale_AES256 ->
        decrypt_aes256_gcm () s iv iv_len ad ad_len cipher cipher_len tag dst
    | Hacl_CHACHA20 ->
        decrypt_chacha20_poly1305 s iv iv_len ad ad_len cipher cipher_len tag dst

inline_for_extraction noextract
let decrypt_expand_aes_gcm (i: vale_impl): decrypt_expand_st false (alg_of_vale_impl i) =
  fun k iv iv_len ad ad_len cipher cipher_len tag dst ->
  push_frame ();
  (* Allocate the state *)
  let s : B.pointer_or_null (state_s (alg_of_vale_impl i)) = alloca k in
  let r = decrypt_aes_gcm i s iv iv_len ad ad_len cipher cipher_len tag dst in
  pop_frame ();
  r

let decrypt_expand_aes128_gcm_no_check : decrypt_expand_st false AES128_GCM =
  fun k iv iv_len ad ad_len cipher cipher_len tag dst ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    decrypt_expand_aes_gcm Vale_AES128 k iv iv_len ad ad_len cipher cipher_len tag dst
  else
    LowStar.Failure.failwith "EverCrypt was compiled on a system which doesn't support Vale"

let decrypt_expand_aes256_gcm_no_check : decrypt_expand_st false AES256_GCM =
  fun k iv iv_len ad ad_len cipher cipher_len tag dst ->
  if EverCrypt.TargetConfig.hacl_can_compile_vale then
    decrypt_expand_aes_gcm Vale_AES256 k iv iv_len ad ad_len cipher cipher_len tag dst
  else
    LowStar.Failure.failwith "EverCrypt was compiled on a system which doesn't support Vale"
val decrypt_expand_aes128_gcm: decrypt_expand_st true AES128_GCM
EverCrypt.AEAD.decrypt_expand_st true Spec.Agile.AEAD.AES128_GCM