let gctr_bytes_st (a: algorithm { a = AES_128 \/ a = AES_256 }) =
 key:Ghost.erased (Seq.seq nat32) ->
 in_b:uint8_p ->
 num_bytes:uint64 ->
 out_b:uint8_p ->
 keys_b:uint8_p ->
 ctr_b:uint8_p ->
 Stack unit
   (requires fun h0 ->
     B.disjoint in_b out_b /\
     B.disjoint keys_b out_b /\
     B.disjoint in_b keys_b /\
     B.disjoint ctr_b in_b /\
     B.disjoint ctr_b out_b /\
     B.disjoint ctr_b keys_b /\

     B.live h0 keys_b /\ B.live h0 in_b /\
     B.live h0 out_b /\ B.live h0 ctr_b /\

     B.length in_b = UInt64.v num_bytes /\
     B.length out_b = B.length in_b /\
     B.length ctr_b = 16 /\
     B.length keys_b = Vale.Wrapper.X64.AES.key_offset a /\

     4096 * (UInt64.v num_bytes) < pow2_32 /\

     aesni_enabled /\ avx_enabled /\ sse_enabled /\
     is_aes_key_LE a (Ghost.reveal key) /\
     (Seq.equal (B.as_seq h0 keys_b)
       (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (key_to_round_keys_LE a (Ghost.reveal key)))))
   )
   (ensures fun h0 r h1 ->
     B.modifies (B.loc_buffer out_b) h0 h1 /\

     (let ctr = seq_uint8_to_seq_nat8 (B.as_seq h0 ctr_b) in
      let plain = seq_uint8_to_seq_nat8 (B.as_seq h0 in_b) in
      let cipher = seq_uint8_to_seq_nat8 (B.as_seq h1 out_b) in
      Seq.equal
        (gctr_encrypt_LE (le_bytes_to_quad32 ctr) (make_gctr_plain_LE plain) a (Ghost.reveal key))
        cipher
      )
   )
let gctr_bytes_st (a: algorithm{a = AES_128 \/ a = AES_256}) =

    key: Ghost.erased (Seq.seq nat32) ->
    in_b: uint8_p ->
    num_bytes: uint64 ->
    out_b: uint8_p ->
    keys_b: uint8_p ->
    ctr_b: uint8_p
  -> Stack unit
      (requires
        fun h0 ->
          B.disjoint in_b out_b /\ B.disjoint keys_b out_b /\ B.disjoint in_b keys_b /\
          B.disjoint ctr_b in_b /\ B.disjoint ctr_b out_b /\ B.disjoint ctr_b keys_b /\
          B.live h0 keys_b /\ B.live h0 in_b /\ B.live h0 out_b /\ B.live h0 ctr_b /\
          B.length in_b = UInt64.v num_bytes /\ B.length out_b = B.length in_b /\
          B.length ctr_b = 16 /\ B.length keys_b = Vale.Wrapper.X64.AES.key_offset a /\
          4096 * (UInt64.v num_bytes) < pow2_32 /\ aesni_enabled /\ avx_enabled /\ sse_enabled /\
          is_aes_key_LE a (Ghost.reveal key) /\
          (Seq.equal (B.as_seq h0 keys_b)
              (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (key_to_round_keys_LE a
                          (Ghost.reveal key))))))
      (ensures
        fun h0 r h1 ->
          B.modifies (B.loc_buffer out_b) h0 h1 /\
          (let ctr = seq_uint8_to_seq_nat8 (B.as_seq h0 ctr_b) in
            let plain = seq_uint8_to_seq_nat8 (B.as_seq h0 in_b) in
            let cipher = seq_uint8_to_seq_nat8 (B.as_seq h1 out_b) in
            Seq.equal (gctr_encrypt_LE (le_bytes_to_quad32 ctr)
                  (make_gctr_plain_LE plain)
                  a
                  (Ghost.reveal key))
              cipher))
Vale.Wrapper.X64.GCTR.fsti.checked
Vale.X64.CPU_Features_s.fst.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Interop.Base.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked
Vale.Wrapper.X64.GCTR.fsti
Vale.AES.AES_common_s.algorithm Prims.l_or Prims.b2t Prims.op_Equality Vale.AES.AES_common_s.AES_128 Vale.AES.AES_common_s.AES_256 FStar.Ghost.erased FStar.Seq.Base.seq Vale.Def.Types_s.nat32 Vale.Wrapper.X64.GCTR.uint8_p Vale.Wrapper.X64.GCTR.uint64 Prims.unit FStar.Monotonic.HyperStack.mem Prims.l_and LowStar.Monotonic.Buffer.disjoint FStar.UInt8.t LowStar.Buffer.trivial_preorder LowStar.Monotonic.Buffer.live Prims.int Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt64.n LowStar.Monotonic.Buffer.length FStar.UInt64.v Prims.nat Vale.Wrapper.X64.AES.key_offset Prims.op_LessThan FStar.Mul.op_Star Vale.Def.Words_s.pow2_32 Vale.X64.CPU_Features_s.aesni_enabled Vale.X64.CPU_Features_s.avx_enabled Vale.X64.CPU_Features_s.sse_enabled Vale.AES.AES_s.is_aes_key_LE FStar.Ghost.reveal FStar.Seq.Base.equal LowStar.Monotonic.Buffer.as_seq Vale.Def.Words.Seq_s.seq_nat8_to_seq_uint8 Vale.Def.Types_s.le_seq_quad32_to_bytes Vale.AES.AES_s.key_to_round_keys_LE LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer Vale.Def.Types_s.nat8 Vale.AES.GCTR_s.gctr_encrypt_LE Vale.Def.Types_s.le_bytes_to_quad32 Vale.AES.GCTR.make_gctr_plain_LE Vale.Def.Words_s.nat8 Vale.Def.Words.Seq_s.seq_uint8_to_seq_nat8
module Vale.Wrapper.X64.GCTR

open Vale.X64.CPU_Features_s
open FStar.HyperStack.ST
module B = LowStar.Buffer
module HS = FStar.HyperStack
module DV = LowStar.BufferView.Down
module UV = LowStar.BufferView.Up
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.AES.AES_s
open Vale.AES.GCTR
open Vale.AES.GCTR_s
open Vale.Interop.Base
open Vale.Def.Types_s

unfold
let uint8_p = B.buffer UInt8.t
let uint64 = UInt64.t

inline_for_extraction noextract
val gctr_bytes_st : a:
      Vale.AES.AES_common_s.algorithm
        {a = Vale.AES.AES_common_s.AES_128 \/ a = Vale.AES.AES_common_s.AES_256}
  -> Type0

    a:
      Vale.AES.AES_common_s.algorithm
        {a = Vale.AES.AES_common_s.AES_128 \/ a = Vale.AES.AES_common_s.AES_256}
  -> Type0