val copy_or_expand
      (i: impl)
      (k: B.buffer uint8 {B.length k = Spec.key_length (cipher_alg_of_impl i)})
      (ek: B.buffer uint8 {B.len ek = concrete_xkey_len i})
    : Stack unit
      (requires
        (fun h0 -> B.live h0 k /\ B.live h0 ek /\ B.disjoint k ek /\ cpu_features_invariant i))
      (ensures
        (fun h0 _ h1 ->
            B.(modifies (loc_buffer ek) h0 h1) /\
            (B.as_seq h1 ek) `Seq.equal` (concrete_expand i (B.as_seq h0 k))))
let copy_or_expand (i: impl)
  (k: B.buffer uint8 { B.length k = Spec.key_length (cipher_alg_of_impl i) })
  (ek: B.buffer uint8 { B.len ek = concrete_xkey_len i }):
  Stack unit
    (requires (fun h0 ->
      B.live h0 k /\ B.live h0 ek /\
      B.disjoint k ek /\
      cpu_features_invariant i))
    (ensures (fun h0 _ h1 ->
      B.(modifies (loc_buffer ek) h0 h1) /\
      B.as_seq h1 ek `Seq.equal` concrete_expand i (B.as_seq h0 k)))
=
  match i with
  | Vale_AES128 ->
    if EverCrypt.TargetConfig.hacl_can_compile_vale then
        vale_expand Vale_AES128 k ek
  | Vale_AES256 ->
    if EverCrypt.TargetConfig.hacl_can_compile_vale then
        vale_expand Vale_AES256 k ek
  | Hacl_CHACHA20 ->
      B.blit k 0ul ek 0ul 32ul
val copy_or_expand
      (i: impl)
      (k: B.buffer uint8 {B.length k = Spec.key_length (cipher_alg_of_impl i)})
      (ek: B.buffer uint8 {B.len ek = concrete_xkey_len i})
    : Stack unit
      (requires
        (fun h0 -> B.live h0 k /\ B.live h0 ek /\ B.disjoint k ek /\ cpu_features_invariant i))
      (ensures
        (fun h0 _ h1 ->
            B.(modifies (loc_buffer ek) h0 h1) /\
            (B.as_seq h1 ek) `Seq.equal` (concrete_expand i (B.as_seq h0 k))))
let copy_or_expand
      (i: impl)
      (k: B.buffer uint8 {B.length k = Spec.key_length (cipher_alg_of_impl i)})
      (ek: B.buffer uint8 {B.len ek = concrete_xkey_len i})
    : Stack unit
      (requires
        (fun h0 -> B.live h0 k /\ B.live h0 ek /\ B.disjoint k ek /\ cpu_features_invariant i))
      (ensures
        (fun h0 _ h1 ->
            B.(modifies (loc_buffer ek) h0 h1) /\
            (B.as_seq h1 ek) `Seq.equal` (concrete_expand i (B.as_seq h0 k)))) =
match i with
| Vale_AES128 -> if EverCrypt.TargetConfig.hacl_can_compile_vale then vale_expand Vale_AES128 k ek
| Vale_AES256 -> if EverCrypt.TargetConfig.hacl_can_compile_vale then vale_expand Vale_AES256 k ek
| Hacl_CHACHA20 -> B.blit k 0ul ek 0ul 32ul
NotEverCrypt.CTR.fst.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.GCTR.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.BufferFriend.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.AES_s.fst.checked Spec.Loops.fst.checked Spec.Cipher.Expansion.fst.checked Spec.Agile.CTR.fst.checked Spec.Agile.Cipher.fst.checked Spec.AES.fst.checked prims.fst.checked LowStar.Endianness.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked Lib.IntTypes.fst.checked Hacl.Impl.Chacha20.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Int.Cast.Full.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverCrypt.TargetConfig.fsti.checked EverCrypt.CTR.Keys.fst.checked EverCrypt.AutoConfig2.fsti.checked
NotEverCrypt.CTR.fst
Spec.Cipher.Expansion.impl LowStar.Buffer.buffer NotEverCrypt.CTR.uint8 Prims.b2t Prims.op_Equality Prims.nat LowStar.Monotonic.Buffer.length LowStar.Buffer.trivial_preorder Spec.Agile.Cipher.key_length Spec.Cipher.Expansion.cipher_alg_of_impl FStar.UInt32.t LowStar.Monotonic.Buffer.len EverCrypt.CTR.Keys.concrete_xkey_len EverCrypt.TargetConfig.hacl_can_compile_vale EverCrypt.CTR.Keys.vale_expand Spec.Cipher.Expansion.Vale_AES128 Prims.unit Prims.bool Spec.Cipher.Expansion.Vale_AES256 LowStar.Monotonic.Buffer.blit FStar.UInt32.__uint_to_t FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.disjoint NotEverCrypt.CTR.cpu_features_invariant LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq Spec.Cipher.Expansion.concrete_expand
module NotEverCrypt.CTR

module ST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module B = LowStar.Buffer
module G = FStar.Ghost

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

open EverCrypt.CTR.Keys
open FStar.HyperStack.ST
open LowStar.BufferOps
open Spec.Cipher.Expansion
open Spec.Agile.CTR

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

noextract
let nonce_upper_bound a =
  match a with
  | AES128 | AES256 -> block_length a
  | CHACHA20 -> 12

noeq
type state_s (a: Spec.cipher_alg) =
| State:
    i:impl ->
    g_iv: G.erased (Spec.nonce a) ->
    iv: B.buffer uint8 { B.length iv = nonce_upper_bound a } ->
    iv_len: UInt32.t { UInt32.v iv_len = Seq.length (G.reveal g_iv) } ->
    g_key: G.erased (Spec.key a) ->
    xkey: B.buffer uint8 { B.length xkey = concrete_xkey_length i } ->
    ctr: UInt32.t ->
    state_s a

let freeable_s #a s =
  let State _ _ iv _ _ key _ = s in
  B.freeable iv /\ B.freeable key

let footprint_s #a s =
  let State _ _ iv _ _ key _ = s in
  B.(loc_addr_of_buffer iv `loc_union` loc_addr_of_buffer key)

let cpu_features_invariant (i: impl): Type0 =
  match i with
  | Vale_AES128 | Vale_AES256 ->
      EverCrypt.TargetConfig.hacl_can_compile_vale /\
      Vale.X64.CPU_Features_s.(aesni_enabled /\ pclmulqdq_enabled /\ avx_enabled /\ sse_enabled)
  | Hacl_CHACHA20 ->
      True

let invariant_s #a h s =
  let State i g_iv iv _ g_key ek _ = s in
  let g_iv = G.reveal g_iv in
  a = cipher_alg_of_impl i /\
  B.live h iv /\ B.live h ek /\
  B.disjoint ek iv /\
  g_iv `Seq.equal` Seq.slice (B.as_seq h iv) 0 (Seq.length g_iv) /\
  concrete_expand i (G.reveal g_key) `Seq.equal` B.as_seq h ek /\
  cpu_features_invariant i

let _: squash (inversion impl) = allow_inversion impl
let _: squash (inversion cipher_alg) = allow_inversion cipher_alg

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

let invariant_loc_in_footprint #_ _ _ = ()

let frame_invariant #_ _ _ _ _ = ()

let kv #a (s: state_s a) =
  let State _ _ _ _ g_key _ _ = s in
  G.reveal g_key

let iv #a (s: state_s a) =
  let State _ g_iv _ _ _ _ _ = s in
  G.reveal g_iv

let ctr #a (h: HS.mem) (s: state a) =
  UInt32.v (State?.ctr (B.deref h s))

let alg_of_state _ s =
  let State i _ _ _ _ _ _ = !*s in
  cipher_alg_of_impl i

let vale_impl_of_alg (a: vale_cipher_alg): vale_impl =
  match a with
  | AES128 -> Vale_AES128
  | AES256 -> Vale_AES256

friend Lib.IntTypes

#push-options "--z3rlimit 100"

inline_for_extraction noextract
let create_in_vale (i: vale_impl): create_in_st (cipher_alg_of_impl i) =
fun r dst k iv iv_len c ->
  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
  [@inline_let]
  let a = cipher_alg_of_impl i in

  if iv_len `UInt32.lt` 12ul then
    InvalidIVLength

  else if EverCrypt.TargetConfig.hacl_can_compile_vale && (has_aesni && has_pclmulqdq && has_avx && has_sse) then
    (**) let h0 = ST.get () in
    (**) let g_iv = G.hide (B.as_seq h0 iv) in
    (**) let g_key: G.erased (key a) = G.hide (B.as_seq h0 (k <: B.buffer uint8)) in

    let ek = B.malloc r 0uy (concrete_xkey_len i) in
    vale_expand i k ek;
    (**) let h1 = ST.get () in
    (**) B.modifies_only_not_unused_in B.loc_none h0 h1;

    let iv' = B.malloc r 0uy 16ul in
    B.blit iv 0ul iv' 0ul iv_len;
    (**) let h2 = ST.get () in
    (**) B.modifies_only_not_unused_in B.loc_none h0 h2;

    let p = B.malloc r (State (vale_impl_of_alg a) g_iv iv' iv_len g_key ek c) 1ul in
    (**) let h3 = ST.get () in
    (**) B.modifies_only_not_unused_in B.loc_none h0 h3;
    assert (B.fresh_loc (footprint h3 p) h0 h3);

    dst *= p;
    (**) let h4 = ST.get () in
    (**) B.modifies_only_not_unused_in B.(loc_buffer dst) h0 h4;

    Success

  else
    UnsupportedAlgorithm

let create_in a r dst k iv iv_len c =
  match a with
  | AES128 ->
      create_in_vale Vale_AES128 r dst k iv iv_len c
  | AES256 ->
      create_in_vale Vale_AES256 r dst k iv iv_len c
  | CHACHA20 ->
      (**) let h0 = ST.get () in
      (**) let g_iv = G.hide (B.as_seq h0 iv) in
      (**) let g_key: G.erased (key a) = G.hide (B.as_seq h0 (k <: B.buffer uint8)) in

      [@inline_let]
      let l = concrete_xkey_len Hacl_CHACHA20 in
      let ek = B.malloc r 0uy l in
      B.blit k 0ul ek 0ul l;
      (**) let h1 = ST.get () in
      (**) B.modifies_only_not_unused_in B.loc_none h0 h1;

      let iv' = B.malloc r 0uy iv_len in
      B.blit iv 0ul iv' 0ul iv_len;
      (**) let h2 = ST.get () in
      (**) B.modifies_only_not_unused_in B.loc_none h0 h2;

      let p = B.malloc r (State Hacl_CHACHA20 g_iv iv' 12ul g_key ek c) 1ul in
      (**) let h3 = ST.get () in
      (**) B.modifies_only_not_unused_in B.loc_none h0 h3;
      assert (B.fresh_loc (footprint h3 p) h0 h3);

      dst *= p;
      (**) let h4 = ST.get () in
      (**) B.modifies_only_not_unused_in B.(loc_buffer dst) h0 h4;

      Success

inline_for_extraction noextract
let copy_or_expand (i: impl)
  (k: B.buffer uint8 { B.length k = Spec.key_length (cipher_alg_of_impl i) })
  (ek: B.buffer uint8 { B.len ek = concrete_xkey_len i }):
  Stack unit
    (requires (fun h0 ->
      B.live h0 k /\ B.live h0 ek /\
      B.disjoint k ek /\
      cpu_features_invariant i))
    (ensures (fun h0 _ h1 ->
      B.(modifies (loc_buffer ek) h0 h1) /\
      B.as_seq h1 ek `Seq.equal` concrete_expand i (B.as_seq h0 k)))
val copy_or_expand
      (i: impl)
      (k: B.buffer uint8 {B.length k = Spec.key_length (cipher_alg_of_impl i)})
      (ek: B.buffer uint8 {B.len ek = concrete_xkey_len i})
    : Stack unit
      (requires
        (fun h0 -> B.live h0 k /\ B.live h0 ek /\ B.disjoint k ek /\ cpu_features_invariant i))
      (ensures
        (fun h0 _ h1 ->
            B.(modifies (loc_buffer ek) h0 h1) /\
            (B.as_seq h1 ek) `Seq.equal` (concrete_expand i (B.as_seq h0 k))))

    i: Spec.Cipher.Expansion.impl ->
    k:
      LowStar.Buffer.buffer NotEverCrypt.CTR.uint8
        { LowStar.Monotonic.Buffer.length k =
          Spec.Agile.Cipher.key_length (Spec.Cipher.Expansion.cipher_alg_of_impl i) } ->
    ek:
      LowStar.Buffer.buffer NotEverCrypt.CTR.uint8
        {LowStar.Monotonic.Buffer.len ek = EverCrypt.CTR.Keys.concrete_xkey_len i}
  -> FStar.HyperStack.ST.Stack Prims.unit