val length_aux6 (b: uint8_p) : Lemma (B.length b = DV.length (get_downview b))
let length_aux6 (b:uint8_p) : Lemma (B.length b = DV.length (get_downview b))
  = DV.length_eq (get_downview b)
val length_aux6 (b: uint8_p) : Lemma (B.length b = DV.length (get_downview b))
let length_aux6 (b: uint8_p) : Lemma (B.length b = DV.length (get_downview b)) =
DV.length_eq (get_downview b)
Vale.Wrapper.X64.GCTR.fst.checked
Vale.X64.MemoryAdapters.fsti.checked Vale.X64.Decls.fsti.checked Vale.Wrapper.X64.AES.fsti.checked Vale.Stdcalls.X64.GCTR.fst.checked Vale.SHA.Simplify_Sha.fsti.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.AsLowStar.MemoryHelpers.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.Gcm_simplify.fsti.checked Vale.AES.GCM_helpers.fsti.checked prims.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Integers.fst.checked FStar.Int.Cast.fst.checked FStar.Ghost.fsti.checked FStar.Calc.fsti.checked
Vale.Wrapper.X64.GCTR.fst
Vale.Wrapper.X64.GCTR.uint8_p LowStar.BufferView.Down.length_eq FStar.UInt8.t Vale.Interop.Types.get_downview Vale.Arch.HeapTypes_s.TUInt8 LowStar.Buffer.trivial_preorder Prims.unit Prims.l_True Prims.squash Prims.b2t Prims.op_Equality Prims.nat LowStar.Monotonic.Buffer.length LowStar.BufferView.Down.length Prims.Nil FStar.Pervasives.pattern
module Vale.Wrapper.X64.GCTR

open FStar.Mul
open Vale.Stdcalls.X64.GCTR
open Vale.AsLowStar.MemoryHelpers
open Vale.X64.MemoryAdapters
module V = Vale.X64.Decls
open Vale.SHA.Simplify_Sha
open Vale.AES.Gcm_simplify
open Vale.AES.GCM_helpers
open Vale.Arch.Types

let wrap_slice (#a:Type0) (s:Seq.seq a) (i:int) : Seq.seq a =
  Seq.slice s 0 (if 0 <= i && i <= Seq.length s then i else 0)

let length_aux3 (b:uint8_p) (n:nat) : Lemma
  (requires B.length b = 16 * n)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db;
    FStar.Math.Lemmas.cancel_mul_mod n 16

inline_for_extraction
val gctr128_bytes_stdcall':
  key:Ghost.erased (Seq.seq nat32) ->
  in_b:uint8_p ->
  num_bytes:uint64 ->
  out_b:uint8_p ->
  inout_b: uint8_p ->
  keys_b:uint8_p ->
  ctr_b:uint8_p ->
  num_blocks:uint64 ->
  Stack unit
  (requires fun h0 ->
     B.disjoint in_b out_b /\
     B.disjoint keys_b out_b /\
     (B.disjoint in_b keys_b \/ in_b == keys_b) /\
     B.disjoint ctr_b in_b /\
     B.disjoint ctr_b out_b /\
     B.disjoint ctr_b keys_b /\
     B.disjoint inout_b in_b /\ B.disjoint inout_b out_b /\
     B.disjoint inout_b keys_b /\ B.disjoint inout_b ctr_b /\

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

     B.length in_b = 16 * UInt64.v num_blocks /\
     B.length out_b = B.length in_b /\
     B.length ctr_b = 16 /\
     B.length keys_b = Vale.Wrapper.X64.AES.key_offset AES_128 /\
     B.length inout_b = 16 /\

     4096 * (UInt64.v num_blocks) * 16 < pow2_32 /\
     UInt64.v num_blocks * 128/8 <= UInt64.v num_bytes /\
     UInt64.v num_bytes < UInt64.v num_blocks * 128/8 + 128/8 /\

     aesni_enabled /\ avx_enabled /\ sse_enabled /\
     is_aes_key_LE AES_128 (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 AES_128 (Ghost.reveal key)))))
   )
   (ensures fun h0 r h1 ->
     B.modifies (B.loc_union (B.loc_buffer out_b) (B.loc_buffer inout_b)) h0 h1 /\

     (let ctr = seq_uint8_to_seq_nat8 (B.as_seq h0 ctr_b) in
       let in_d = get_downview in_b in
       length_aux3 in_b (UInt64.v num_blocks);
       let in_u = UV.mk_buffer in_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let out_d = get_downview out_b in
       length_aux3 out_b (UInt64.v num_blocks);
       let out_u = UV.mk_buffer out_d Vale.Interop.Views.up_view128 in

      let plain_quads = Seq.append (UV.as_seq h0 in_u) (UV.as_seq h0 inout_u) in
      let plain = wrap_slice (le_seq_quad32_to_bytes plain_quads) (UInt64.v num_bytes) in
      let cipher_quads = Seq.append (UV.as_seq h1 out_u) (UV.as_seq h1 inout_u) in
      let cipher = wrap_slice (le_seq_quad32_to_bytes cipher_quads) (UInt64.v num_bytes) in
      Seq.equal
        (gctr_encrypt_LE (le_bytes_to_quad32 ctr) (make_gctr_plain_LE plain) AES_128 (Ghost.reveal key))
        cipher
      )
   )

inline_for_extraction
val gctr256_bytes_stdcall':
  key:Ghost.erased (Seq.seq nat32) ->
  in_b:uint8_p ->
  num_bytes:uint64 ->
  out_b:uint8_p ->
  inout_b: uint8_p ->
  keys_b:uint8_p ->
  ctr_b:uint8_p ->
  num_blocks:uint64 ->
  Stack unit
  (requires fun h0 ->
     B.disjoint in_b out_b /\
     B.disjoint keys_b out_b /\
     (B.disjoint in_b keys_b \/ in_b == keys_b) /\
     B.disjoint ctr_b in_b /\
     B.disjoint ctr_b out_b /\
     B.disjoint ctr_b keys_b /\
     B.disjoint inout_b in_b /\ B.disjoint inout_b out_b /\
     B.disjoint inout_b keys_b /\ B.disjoint inout_b ctr_b /\

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

     B.length in_b = 16 * UInt64.v num_blocks /\
     B.length out_b = B.length in_b /\
     B.length ctr_b = 16 /\
     B.length keys_b = Vale.Wrapper.X64.AES.key_offset AES_256 /\
     B.length inout_b = 16 /\

     4096 * (UInt64.v num_blocks) * 16 < pow2_32 /\
     UInt64.v num_blocks * 128/8 <= UInt64.v num_bytes /\
     UInt64.v num_bytes < UInt64.v num_blocks * 128/8 + 128/8 /\

     aesni_enabled /\ avx_enabled /\ sse_enabled /\
     is_aes_key_LE AES_256 (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 AES_256 (Ghost.reveal key)))))
   )
   (ensures fun h0 r h1 ->
     B.modifies (B.loc_union (B.loc_buffer out_b) (B.loc_buffer inout_b)) h0 h1 /\

     (let ctr = seq_uint8_to_seq_nat8 (B.as_seq h0 ctr_b) in

       let in_d = get_downview in_b in
       length_aux3 in_b (UInt64.v num_blocks);
       let in_u = UV.mk_buffer in_d Vale.Interop.Views.up_view128 in
       let inout_d = get_downview inout_b in
       length_aux3 inout_b 1;
       let inout_u = UV.mk_buffer inout_d Vale.Interop.Views.up_view128 in
       let out_d = get_downview out_b in
       length_aux3 out_b (UInt64.v num_blocks);
       let out_u = UV.mk_buffer out_d Vale.Interop.Views.up_view128 in

      let plain_quads = Seq.append (UV.as_seq h0 in_u) (UV.as_seq h0 inout_u) in
      let plain = wrap_slice (le_seq_quad32_to_bytes plain_quads) (UInt64.v num_bytes) in
      let cipher_quads = Seq.append (UV.as_seq h1 out_u) (UV.as_seq h1 inout_u) in
      let cipher = wrap_slice (le_seq_quad32_to_bytes cipher_quads) (UInt64.v num_bytes) in
      Seq.equal
        (gctr_encrypt_LE (le_bytes_to_quad32 ctr) (make_gctr_plain_LE plain) AES_256 (Ghost.reveal key))
        cipher
      )
   )

let length_aux (b:uint8_p) : Lemma
  (requires B.length b = 176)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db

let length_aux2 (b:uint8_p) : Lemma
  (requires B.length b = 240)
  (ensures DV.length (get_downview b) % 16 = 0) =
    let db = get_downview b in
    DV.length_eq db

#push-options "--z3rlimit 200 --max_fuel 0 --max_ifuel 0 --ext compat:normalizer_memo_ignore_cfg"
inline_for_extraction
let gctr128_bytes_stdcall' key in_b num_bytes out_b inout_b keys_b ctr_b num_blocks =
  let h0 = get() in

  DV.length_eq (get_downview in_b);
  DV.length_eq (get_downview out_b);
  DV.length_eq (get_downview keys_b);
  DV.length_eq (get_downview ctr_b);
  DV.length_eq (get_downview inout_b);

  as_vale_buffer_len #TUInt8 #TUInt128 in_b;
  as_vale_buffer_len #TUInt8 #TUInt128 out_b;
  as_vale_buffer_len #TUInt8 #TUInt128 keys_b;
  as_vale_buffer_len #TUInt8 #TUInt128 ctr_b;
  as_vale_buffer_len #TUInt8 #TUInt128 inout_b;

  bounded_buffer_addrs_all TUInt8 TUInt128 h0 in_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 keys_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 out_b;

  let lemma_uv_key () : Lemma
    (let db = get_downview keys_b in
      length_aux keys_b;
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      Seq.equal (UV.as_seq h0 ub) (key_to_round_keys_LE AES_128 (Ghost.reveal key)))
    = length_aux keys_b;
      let db = get_downview keys_b in
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      le_bytes_to_seq_quad32_to_bytes (key_to_round_keys_LE AES_128 (Ghost.reveal key));
      assert (Seq.equal (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 keys_b)))
         (key_to_round_keys_LE AES_128 (Ghost.reveal key)));
      calc (==) {
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 keys_b));
        (==) { lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 keys_b h0 }
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h0 ub))));
        (==) { le_bytes_to_seq_quad32_to_bytes (UV.as_seq h0 ub) }
        UV.as_seq h0 ub;
      }

  in lemma_uv_key ();
  let (x, _) = gctr128_bytes key in_b num_bytes out_b inout_b keys_b ctr_b num_blocks () in

  let h1 = get() in

  // lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 in_b h1;
  // lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 inout_b h0;
  // lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 inout_b h1;
  // lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 out_b h1;
  le_bytes_to_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h0 ctr_b 0);
  gcm_simplify2 ctr_b h0;

  ()

inline_for_extraction
let gctr256_bytes_stdcall' key in_b num_bytes out_b inout_b keys_b ctr_b num_blocks =
  let h0 = get() in

  DV.length_eq (get_downview in_b);
  DV.length_eq (get_downview out_b);
  DV.length_eq (get_downview inout_b);
  DV.length_eq (get_downview keys_b);
  DV.length_eq (get_downview ctr_b);

  as_vale_buffer_len #TUInt8 #TUInt128 in_b;
  as_vale_buffer_len #TUInt8 #TUInt128 out_b;
  as_vale_buffer_len #TUInt8 #TUInt128 inout_b;
  as_vale_buffer_len #TUInt8 #TUInt128 keys_b;
  as_vale_buffer_len #TUInt8 #TUInt128 ctr_b;

  bounded_buffer_addrs_all TUInt8 TUInt128 h0 in_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 keys_b;
  bounded_buffer_addrs_all TUInt8 TUInt128 h0 out_b;

  let lemma_uv_key () : Lemma
    (let db = get_downview keys_b in
      length_aux2 keys_b;
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      Seq.equal (UV.as_seq h0 ub) (key_to_round_keys_LE AES_256 (Ghost.reveal key)))
    = length_aux2 keys_b;
      let db = get_downview keys_b in
      let ub = UV.mk_buffer db Vale.Interop.Views.up_view128 in
      le_bytes_to_seq_quad32_to_bytes (key_to_round_keys_LE AES_256 (Ghost.reveal key));
      assert (Seq.equal (le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 keys_b)))
         (key_to_round_keys_LE AES_256 (Ghost.reveal key)));
      calc (==) {
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (B.as_seq h0 keys_b));
        (==) { lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 keys_b h0 }
        le_bytes_to_seq_quad32 (seq_uint8_to_seq_nat8 (seq_nat8_to_seq_uint8 (le_seq_quad32_to_bytes (UV.as_seq h0 ub))));
        (==) { le_bytes_to_seq_quad32_to_bytes (UV.as_seq h0 ub) }
        UV.as_seq h0 ub;
      }

  in lemma_uv_key ();
  let (x, _) = gctr256_bytes key in_b num_bytes out_b inout_b keys_b ctr_b num_blocks () in

  let h1 = get() in

  // lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 in_b h1;
  // lemma_seq_nat8_le_seq_quad32_to_bytes_uint32 out_b h1;
  le_bytes_to_quad32_to_bytes (low_buffer_read TUInt8 TUInt128 h0 ctr_b 0);
  gcm_simplify2 ctr_b h0;

  ()

let length_aux4 (b:uint8_p) (n:nat) : Lemma
  (requires B.length b = n * 16)
  (ensures DV.length (get_downview b) % 16 = 0) =
  DV.length_eq (get_downview b)
val length_aux6 (b: uint8_p) : Lemma (B.length b = DV.length (get_downview b))
b: Vale.Wrapper.X64.GCTR.uint8_p
  -> FStar.Pervasives.Lemma
    (ensures
      LowStar.Monotonic.Buffer.length b =
      LowStar.BufferView.Down.length (Vale.Interop.Types.get_downview b))