val 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)
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
val 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)
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
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
Vale.AES.AES_common_s.algorithm FStar.Seq.Base.seq Vale.Def.Types_s.quad32 Vale.Def.Types_s.nat32 Vale.AES.GCTR.gctr_partial_completed Prims.unit Vale.AES.GCTR.gctr_partial_reveal Prims.l_and Vale.AES.AES_s.is_aes_key_LE Prims.eq2 Prims.nat FStar.Seq.Base.length Prims.b2t Prims.op_LessThan Vale.Def.Words_s.pow2_32 Vale.AES.GCTR.gctr_partial Prims.squash Vale.AES.GCTR_s.gctr_encrypt_recursive Prims.Nil FStar.Pervasives.pattern
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)
val 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)

    alg: Vale.AES.AES_common_s.algorithm ->
    plain: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    cipher: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    key: FStar.Seq.Base.seq Vale.Def.Types_s.nat32 ->
    icb: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
      (requires
        Vale.AES.AES_s.is_aes_key_LE alg key /\
        FStar.Seq.Base.length plain == FStar.Seq.Base.length cipher /\
        FStar.Seq.Base.length plain < Vale.Def.Words_s.pow2_32 /\
        Vale.AES.GCTR.gctr_partial alg (FStar.Seq.Base.length cipher) plain cipher key icb)
      (ensures cipher == Vale.AES.GCTR_s.gctr_encrypt_recursive icb plain alg key 0)