let pow2_24 = 0x1000000
let pow2_24 =
0x1000000
Vale.AES.GCTR.fst.checked
Vale.Poly1305.Bitvectors.fsti.checked Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.TypesNative_s.fst.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.Types_helpers.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.UInt.fsti.checked FStar.Seq.Properties.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.AES.GCTR.fst
module Vale.AES.GCTR

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Mul
open FStar.Seq
open Vale.AES.AES_s
open Vale.AES.GCTR_s
open Vale.AES.GCM_helpers
open FStar.Math.Lemmas
open Vale.Lib.Seqs
open Vale.AES.Types_helpers

#set-options "--z3rlimit 20 --max_fuel 1 --max_ifuel 0"

let lemma_counter_init x low64 low8 =
  Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1 low64;
  Vale.Def.TypesNative_s.reveal_iand 64 low64 0xff;
  assert (low8 == low64 % 256);
  lo64_reveal ();
  assert_norm (pow2_norm 32 == pow2_32);      // OBSERVE
  assert (low64 == x.lo0 + x.lo1 * pow2_32);  // OBSERVE
  assert (low64 % 256 == x.lo0 % 256);
  ()

let gctr_encrypt_block_offset (icb_BE:quad32) (plain_LE:quad32) (alg:algorithm) (key:seq nat32) (i:int) =
  ()

let gctr_encrypt_empty (icb_BE:quad32) (plain_LE cipher_LE:seq quad32) (alg:algorithm) (key:seq nat32) =
  reveal_opaque (`%le_bytes_to_seq_quad32) le_bytes_to_seq_quad32;
  gctr_encrypt_LE_reveal ();
  let plain = slice (le_seq_quad32_to_bytes plain_LE) 0 0 in
  let cipher = slice (le_seq_quad32_to_bytes cipher_LE) 0 0 in
  assert (plain == empty);
  assert (cipher == empty);
  assert (length plain == 0);
  assert (make_gctr_plain_LE plain == empty);
  let num_extra = (length (make_gctr_plain_LE plain)) % 16 in
  assert (num_extra == 0);
  let plain_quads_LE = le_bytes_to_seq_quad32 plain in
  let cipher_quads_LE = gctr_encrypt_recursive icb_BE plain_quads_LE alg key 0 in
  assert (equal plain_quads_LE empty);     // OBSERVE
  assert (plain_quads_LE == empty);
  assert (cipher_quads_LE == empty);
  assert (equal (le_seq_quad32_to_bytes cipher_quads_LE) empty);  // OBSERVEs
  ()

let gctr_partial_opaque_init alg plain cipher key icb =
  gctr_partial_reveal ();
  ()

#restart-solver
let lemma_gctr_partial_append alg b1 b2 p1 c1 p2 c2 key icb1 icb2 =
  gctr_partial_reveal ();
  ()

let gctr_partial_opaque_ignores_postfix alg bound plain plain' cipher cipher' key icb =
  gctr_partial_reveal ();
  // OBSERVE:
  assert (forall i . 0 <= i /\ i < bound ==> index plain i == index (slice plain 0 bound) i);
  assert (forall i . 0 <= i /\ i < bound ==> index plain' i == index (slice plain' 0 bound) i);
  assert (forall i . 0 <= i /\ i < bound ==> index cipher i == index (slice cipher 0 bound) i);
  assert (forall i . 0 <= i /\ i < bound ==> index cipher' i == index (slice cipher' 0 bound) i);
  ()

let gctr_partial_extend6 (alg:algorithm) (bound:nat) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32)
  =
  gctr_partial_reveal ();
  ()

(*
let rec seq_map_i_indexed' (#a:Type) (#b:Type) (f:int->a->b) (s:seq a) (i:int) :
  Tot (s':seq b { length s' == length s /\
                  (forall j . {:pattern index s' j} 0 <= j /\ j < length s ==> index s' j == f (i + j) (index s j))
                })
      (decreases (length s))
  =
  if length s = 0 then empty
  else cons (f i (head s)) (seq_map_i_indexed f (tail s) (i + 1))

let rec test (icb_BE:quad32) (plain_LE:gctr_plain_internal_LE)
         (alg:algorithm) (key:aes_key_LE alg) (i:int) :
  Lemma (ensures
     (let gctr_encrypt_block_curried (j:int) (p:quad32) = gctr_encrypt_block icb_BE p alg key j in

      gctr_encrypt_recursive icb_BE plain_LE alg key i == seq_map_i_indexed' gctr_encrypt_block_curried plain_LE i))
     (decreases (length plain_LE))
  =
  let gctr_encrypt_block_curried (j:int) (p:quad32) = gctr_encrypt_block icb_BE p alg key j in
  let g = gctr_encrypt_recursive icb_BE plain_LE alg key i in
  let s = seq_map_i_indexed' gctr_encrypt_block_curried plain_LE i in
  if length plain_LE = 0 then (
    assert(equal (g) (s));
    ()
  ) else (
    test icb_BE (tail plain_LE) alg key (i+1);
    assert (gctr_encrypt_recursive icb_BE (tail plain_LE) alg key (i+1) == seq_map_i_indexed' gctr_encrypt_block_curried (tail plain_LE) (i+1))
  )
*)

let rec gctr_encrypt_recursive_length (icb:quad32) (plain:gctr_plain_internal_LE)
                                      (alg:algorithm) (key:aes_key_LE alg) (i:int) : Lemma
  (requires True)
  (ensures length (gctr_encrypt_recursive icb plain alg key i) == length plain)
  (decreases %[length plain])
  [SMTPat (length (gctr_encrypt_recursive icb plain alg key i))]
  =
  if length plain = 0 then ()
  else gctr_encrypt_recursive_length icb (tail plain) alg key (i + 1)

#reset-options "--z3rlimit 40"
let gctr_encrypt_length (icb_BE:quad32) (plain:gctr_plain_LE)
                             (alg:algorithm) (key:aes_key_LE alg) :
  Lemma(length (gctr_encrypt_LE icb_BE plain alg key) == length plain)
  [SMTPat (length (gctr_encrypt_LE icb_BE plain alg key))]
  =
  reveal_opaque (`%le_bytes_to_seq_quad32) le_bytes_to_seq_quad32;
  gctr_encrypt_LE_reveal ();
  let num_extra = (length plain) % 16 in
  let result = gctr_encrypt_LE icb_BE plain alg key in
  if num_extra = 0 then (
    let plain_quads_LE = le_bytes_to_seq_quad32 plain in
    gctr_encrypt_recursive_length icb_BE plain_quads_LE alg key 0
  ) else (
    let full_bytes_len = (length plain) - num_extra in
    let full_blocks, final_block = split plain full_bytes_len in

    let full_quads_LE = le_bytes_to_seq_quad32 full_blocks in
    let final_quad_LE = le_bytes_to_quad32 (pad_to_128_bits final_block) in

    let cipher_quads_LE = gctr_encrypt_recursive icb_BE full_quads_LE alg key 0 in
    let final_cipher_quad_LE = gctr_encrypt_block icb_BE final_quad_LE alg key (full_bytes_len / 16) in

    let cipher_bytes_full_LE = le_seq_quad32_to_bytes cipher_quads_LE in
    let final_cipher_bytes_LE = slice (le_quad32_to_bytes final_cipher_quad_LE) 0 num_extra in

    gctr_encrypt_recursive_length icb_BE full_quads_LE alg key 0;
    assert (length result == length cipher_bytes_full_LE + length final_cipher_bytes_LE);
    assert (length cipher_quads_LE == length full_quads_LE);
    assert (length cipher_bytes_full_LE == 16 * length cipher_quads_LE);
    assert (16 * length full_quads_LE == length full_blocks);
    assert (length cipher_bytes_full_LE == length full_blocks);
    ()
  )
#reset-options

let rec gctr_indexed_helper (icb:quad32) (plain:gctr_plain_internal_LE)
                            (alg:algorithm) (key:aes_key_LE alg) (i:int) : Lemma
  (requires True)
  (ensures (let cipher = gctr_encrypt_recursive icb plain alg key i in
            length cipher == length plain /\
           (forall j . {:pattern index cipher j} 0 <= j /\ j < length plain ==>
           index cipher j == quad32_xor (index plain j) (aes_encrypt_BE alg key (inc32 icb (i + j)) ))))
  (decreases %[length plain])
=
  if length plain = 0 then ()
  else
      let tl = tail plain in
      let cipher = gctr_encrypt_recursive icb plain alg key i in
      let r_cipher = gctr_encrypt_recursive icb tl alg key (i+1) in
      let helper (j:int) :
        Lemma ((0 <= j /\ j < length plain) ==> (index cipher j == quad32_xor (index plain j) (aes_encrypt_BE alg key (inc32 icb (i + j)) )))
        =
        aes_encrypt_LE_reveal ();
        if 0 < j && j < length plain then (
          gctr_indexed_helper icb tl alg key (i+1);
          assert(index r_cipher (j-1) == quad32_xor (index tl (j-1)) (aes_encrypt_BE alg key (inc32 icb (i + 1 + j - 1)) )) // OBSERVE
        ) else ()
      in
      FStar.Classical.forall_intro helper

let gctr_indexed (icb:quad32) (plain:gctr_plain_internal_LE)
                     (alg:algorithm) (key:aes_key_LE alg) (cipher:seq quad32) : Lemma
  (requires  length cipher == length plain /\
             (forall i . {:pattern index cipher i} 0 <= i /\ i < length cipher ==>
             index cipher i == quad32_xor (index plain i) (aes_encrypt_BE alg key (inc32 icb i) )))
  (ensures  cipher == gctr_encrypt_recursive icb plain alg key 0)
=
  gctr_indexed_helper icb plain alg key 0;
  let c = gctr_encrypt_recursive icb plain alg key 0 in
  assert(equal cipher c)  // OBSERVE: Invoke extensionality lemmas


let gctr_partial_completed (alg:algorithm) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32) =
  gctr_indexed icb plain alg key cipher;
  ()

let gctr_partial_opaque_completed (alg:algorithm) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires
    is_aes_key_LE alg key /\
    length plain == length cipher /\
    length plain < pow2_32 /\
    gctr_partial alg (length cipher) plain cipher key icb
  )
  (ensures cipher == gctr_encrypt_recursive icb plain alg key 0)
  =
  gctr_partial_reveal ();
  gctr_partial_completed alg plain cipher key icb

let gctr_partial_to_full_basic (icb_BE:quad32) (plain:seq quad32) (alg:algorithm) (key:seq nat32) (cipher:seq quad32) =
  gctr_encrypt_LE_reveal ();
  let p = le_seq_quad32_to_bytes plain in
  assert (length p % 16 == 0);
  let plain_quads_LE = le_bytes_to_seq_quad32 p in
  let cipher_quads_LE = gctr_encrypt_recursive icb_BE plain_quads_LE alg key 0 in
  let cipher_bytes = le_seq_quad32_to_bytes cipher_quads_LE in
  le_bytes_to_seq_quad32_to_bytes plain;
  ()


(*
Want to show that:
   slice (le_seq_quad32_to_bytes (buffer128_as_seq(mem, out_b))) 0 num_bytes
   ==
   gctr_encrypt_LE icb_BE (slice (le_seq_quad32_to_bytes (buffer128_as_seq(mem, in_b))) 0 num_bytes) ...

We know that
   slice (buffer128_as_seq(mem, out_b) 0 num_blocks
   ==
   gctr_encrypt_recursive icb_BE (slice buffer128_as_seq(mem, in_b) 0 num_blocks) ...

And we know that:
  get_mem out_b num_blocks
  ==
  gctr_encrypt_block(icb_BE, (get_mem inb num_blocks), alg, key, num_blocks);


Internally gctr_encrypt_LE will compute:
  full_blocks, final_block = split (slice (le_seq_quad32_to_bytes (buffer128_as_seq(mem, in_b))) 0 num_bytes) (num_blocks * 16)

  We'd like to show that
  Step1:  le_bytes_to_seq_quad32 full_blocks == slice buffer128_as_seq(mem, in_b) 0 num_blocks
    and
  Step2:  final_block == slice (le_quad32_to_bytes (get_mem inb num_blocks)) 0 num_extra

  Then we need to break down the byte-level effects of gctr_encrypt_block to show that even though the
  padded version of final_block differs from (get_mem inb num_blocks), after we slice it at the end,
  we end up with the same value
*)


let step1 (p:seq quad32) (num_bytes:nat{ num_bytes < 16 * length p }) : Lemma
  (let num_extra = num_bytes % 16 in
   let num_blocks = num_bytes / 16 in
   let full_blocks, final_block = split (slice (le_seq_quad32_to_bytes p) 0 num_bytes) (num_blocks * 16) in
   let full_quads_LE = le_bytes_to_seq_quad32 full_blocks in
   let p_prefix = slice p 0 num_blocks in
   p_prefix == full_quads_LE)
  =
  let num_extra = num_bytes % 16 in
  let num_blocks = num_bytes / 16 in
  let full_blocks, final_block = split (slice (le_seq_quad32_to_bytes p) 0 num_bytes) (num_blocks * 16) in
  let full_quads_LE = le_bytes_to_seq_quad32 full_blocks in
  let p_prefix = slice p 0 num_blocks in
  assert (length full_blocks == num_blocks * 16);
  assert (full_blocks == slice (slice (le_seq_quad32_to_bytes p) 0 num_bytes) 0 (num_blocks * 16));
  assert (full_blocks == slice (le_seq_quad32_to_bytes p) 0 (num_blocks * 16));
  slice_commutes_le_seq_quad32_to_bytes0 p num_blocks;
  assert (full_blocks == le_seq_quad32_to_bytes (slice p 0 num_blocks));
  le_bytes_to_seq_quad32_to_bytes (slice p 0 num_blocks);
  assert (full_quads_LE == (slice p 0 num_blocks));
  ()

#reset-options "--smtencoding.elim_box true --z3rlimit 30"
let lemma_slice_orig_index (#a:Type) (s s':seq a) (m n:nat) : Lemma
  (requires length s == length s' /\ m <= n /\ n <= length s /\ slice s m n == slice s' m n)
  (ensures (forall (i:int).{:pattern (index s i) \/ (index s' i)} m <= i /\ i < n ==> index s i == index s' i))
  =
  let aux (i:nat{m <= i /\ i < n}) : Lemma (index s i == index s' i) =
    lemma_index_slice s m n (i - m);
    lemma_index_slice s' m n (i - m)
  in Classical.forall_intro aux

let lemma_ishl_32 (x:nat32) (k:nat) : Lemma
  (ensures ishl #pow2_32 x k == x * pow2 k % pow2_32)
  =
  Vale.Def.TypesNative_s.reveal_ishl 32 x k;
  FStar.UInt.shift_left_value_lemma #32 x k;
  ()

let lemma_ishl_ixor_32 (x y:nat32) (k:nat) : Lemma
  (ensures ishl #pow2_32 (ixor x y) k == ixor (ishl x k) (ishl y k))
  =
  Vale.Def.TypesNative_s.reveal_ishl 32 x k;
  Vale.Def.TypesNative_s.reveal_ishl 32 y k;
  Vale.Def.TypesNative_s.reveal_ishl 32 (ixor x y) k;
  Vale.Def.TypesNative_s.reveal_ixor 32 x y;
  Vale.Def.TypesNative_s.reveal_ixor 32 (ishl x k) (ishl y k);
  FStar.UInt.shift_left_logxor_lemma #32 x y k;
  ()
val pow2_24 : Prims.int
Prims.int