val create_in_vale (i: vale_impl) : create_in_st (cipher_alg_of_impl i)
val create_in_vale (i: vale_impl) : create_in_st (cipher_alg_of_impl i)
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
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"
/
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
i: EverCrypt.CTR.Keys.vale_impl
  -> NotEverCrypt.CTR.create_in_st (Spec.Cipher.Expansion.cipher_alg_of_impl i)
EverCrypt.CTR.Keys.vale_impl FStar.Monotonic.HyperHeap.rid LowStar.Buffer.pointer LowStar.Buffer.pointer_or_null NotEverCrypt.CTR.state_s Spec.Cipher.Expansion.cipher_alg_of_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 FStar.UInt32.t Prims.l_and Spec.Agile.Cipher.nonce_bound FStar.UInt32.v LowStar.Monotonic.Buffer.len FStar.UInt32.lt FStar.UInt32.__uint_to_t EverCrypt.Error.InvalidIVLength EverCrypt.Error.error_code Prims.bool Prims.op_AmpAmp EverCrypt.TargetConfig.hacl_can_compile_vale EverCrypt.Error.Success Prims.unit LowStar.Monotonic.Buffer.modifies_only_not_unused_in LowStar.Monotonic.Buffer.loc_buffer FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowStar.BufferOps.op_Star_Equals Prims._assert LowStar.Monotonic.Buffer.fresh_loc NotEverCrypt.CTR.footprint LowStar.Monotonic.Buffer.loc_none LowStar.Monotonic.Buffer.mbuffer Prims.eq2 FStar.UInt32.uint_to_t Prims.op_Negation LowStar.Monotonic.Buffer.g_is_null LowStar.Monotonic.Buffer.frameOf LowStar.Monotonic.Buffer.freeable LowStar.Buffer.malloc NotEverCrypt.CTR.State NotEverCrypt.CTR.vale_impl_of_alg LowStar.Monotonic.Buffer.blit FStar.UInt8.__uint_to_t EverCrypt.CTR.Keys.vale_expand EverCrypt.CTR.Keys.uint8 EverCrypt.CTR.Keys.concrete_xkey_len FStar.Ghost.erased Spec.Agile.Cipher.key FStar.Ghost.hide LowStar.Monotonic.Buffer.as_seq Spec.Agile.Cipher.nonce EverCrypt.Error.UnsupportedAlgorithm Spec.Agile.Cipher.cipher_alg EverCrypt.AutoConfig2.has_sse EverCrypt.AutoConfig2.has_avx EverCrypt.AutoConfig2.has_pclmulqdq EverCrypt.AutoConfig2.has_aesni NotEverCrypt.CTR.create_in_st
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