val gctr_partial_extend6 (alg:algorithm) (bound:nat) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires length plain >= bound + 6 /\
            length cipher >= bound + 6 /\
            is_aes_key_LE alg key /\
            bound + 6 < pow2_32 /\
            gctr_partial alg bound plain cipher key icb /\
            index cipher (bound + 0) == quad32_xor (index plain (bound + 0)) (aes_encrypt_BE alg key (inc32lite icb (bound + 0))) /\
            index cipher (bound + 1) == quad32_xor (index plain (bound + 1)) (aes_encrypt_BE alg key (inc32lite icb (bound + 1))) /\
            index cipher (bound + 2) == quad32_xor (index plain (bound + 2)) (aes_encrypt_BE alg key (inc32lite icb (bound + 2))) /\
            index cipher (bound + 3) == quad32_xor (index plain (bound + 3)) (aes_encrypt_BE alg key (inc32lite icb (bound + 3))) /\
            index cipher (bound + 4) == quad32_xor (index plain (bound + 4)) (aes_encrypt_BE alg key (inc32lite icb (bound + 4))) /\
            index cipher (bound + 5) == quad32_xor (index plain (bound + 5)) (aes_encrypt_BE alg key (inc32lite icb (bound + 5)))
  )
  (ensures gctr_partial alg (bound + 6) plain cipher key icb)
let gctr_partial_extend6 (alg:algorithm) (bound:nat) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32)
  =
  gctr_partial_reveal ();
  ()
val gctr_partial_extend6 (alg:algorithm) (bound:nat) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires length plain >= bound + 6 /\
            length cipher >= bound + 6 /\
            is_aes_key_LE alg key /\
            bound + 6 < pow2_32 /\
            gctr_partial alg bound plain cipher key icb /\
            index cipher (bound + 0) == quad32_xor (index plain (bound + 0)) (aes_encrypt_BE alg key (inc32lite icb (bound + 0))) /\
            index cipher (bound + 1) == quad32_xor (index plain (bound + 1)) (aes_encrypt_BE alg key (inc32lite icb (bound + 1))) /\
            index cipher (bound + 2) == quad32_xor (index plain (bound + 2)) (aes_encrypt_BE alg key (inc32lite icb (bound + 2))) /\
            index cipher (bound + 3) == quad32_xor (index plain (bound + 3)) (aes_encrypt_BE alg key (inc32lite icb (bound + 3))) /\
            index cipher (bound + 4) == quad32_xor (index plain (bound + 4)) (aes_encrypt_BE alg key (inc32lite icb (bound + 4))) /\
            index cipher (bound + 5) == quad32_xor (index plain (bound + 5)) (aes_encrypt_BE alg key (inc32lite icb (bound + 5)))
  )
  (ensures gctr_partial alg (bound + 6) plain cipher key icb)
let gctr_partial_extend6
      (alg: algorithm)
      (bound: nat)
      (plain cipher: seq quad32)
      (key: seq nat32)
      (icb: quad32)
     =
gctr_partial_reveal ();
()
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 Prims.nat FStar.Seq.Base.seq Vale.Def.Types_s.quad32 Vale.Def.Types_s.nat32 Prims.unit Vale.AES.GCTR.gctr_partial_reveal
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)
val gctr_partial_extend6 (alg:algorithm) (bound:nat) (plain cipher:seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires length plain >= bound + 6 /\
            length cipher >= bound + 6 /\
            is_aes_key_LE alg key /\
            bound + 6 < pow2_32 /\
            gctr_partial alg bound plain cipher key icb /\
            index cipher (bound + 0) == quad32_xor (index plain (bound + 0)) (aes_encrypt_BE alg key (inc32lite icb (bound + 0))) /\
            index cipher (bound + 1) == quad32_xor (index plain (bound + 1)) (aes_encrypt_BE alg key (inc32lite icb (bound + 1))) /\
            index cipher (bound + 2) == quad32_xor (index plain (bound + 2)) (aes_encrypt_BE alg key (inc32lite icb (bound + 2))) /\
            index cipher (bound + 3) == quad32_xor (index plain (bound + 3)) (aes_encrypt_BE alg key (inc32lite icb (bound + 3))) /\
            index cipher (bound + 4) == quad32_xor (index plain (bound + 4)) (aes_encrypt_BE alg key (inc32lite icb (bound + 4))) /\
            index cipher (bound + 5) == quad32_xor (index plain (bound + 5)) (aes_encrypt_BE alg key (inc32lite icb (bound + 5)))
  )
  (ensures gctr_partial alg (bound + 6) plain cipher key icb)

    alg: Vale.AES.AES_common_s.algorithm ->
    bound: Prims.nat ->
    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
        FStar.Seq.Base.length plain >= bound + 6 /\ FStar.Seq.Base.length cipher >= bound + 6 /\
        Vale.AES.AES_s.is_aes_key_LE alg key /\ bound + 6 < Vale.Def.Words_s.pow2_32 /\
        Vale.AES.GCTR.gctr_partial alg bound plain cipher key icb /\
        FStar.Seq.Base.index cipher (bound + 0) ==
        Vale.Def.Types_s.quad32_xor (FStar.Seq.Base.index plain (bound + 0))
          (Vale.AES.GCTR.aes_encrypt_BE alg key (Vale.AES.GCTR.inc32lite icb (bound + 0))) /\
        FStar.Seq.Base.index cipher (bound + 1) ==
        Vale.Def.Types_s.quad32_xor (FStar.Seq.Base.index plain (bound + 1))
          (Vale.AES.GCTR.aes_encrypt_BE alg key (Vale.AES.GCTR.inc32lite icb (bound + 1))) /\
        FStar.Seq.Base.index cipher (bound + 2) ==
        Vale.Def.Types_s.quad32_xor (FStar.Seq.Base.index plain (bound + 2))
          (Vale.AES.GCTR.aes_encrypt_BE alg key (Vale.AES.GCTR.inc32lite icb (bound + 2))) /\
        FStar.Seq.Base.index cipher (bound + 3) ==
        Vale.Def.Types_s.quad32_xor (FStar.Seq.Base.index plain (bound + 3))
          (Vale.AES.GCTR.aes_encrypt_BE alg key (Vale.AES.GCTR.inc32lite icb (bound + 3))) /\
        FStar.Seq.Base.index cipher (bound + 4) ==
        Vale.Def.Types_s.quad32_xor (FStar.Seq.Base.index plain (bound + 4))
          (Vale.AES.GCTR.aes_encrypt_BE alg key (Vale.AES.GCTR.inc32lite icb (bound + 4))) /\
        FStar.Seq.Base.index cipher (bound + 5) ==
        Vale.Def.Types_s.quad32_xor (FStar.Seq.Base.index plain (bound + 5))
          (Vale.AES.GCTR.aes_encrypt_BE alg key (Vale.AES.GCTR.inc32lite icb (bound + 5))))
      (ensures Vale.AES.GCTR.gctr_partial alg (bound + 6) plain cipher key icb)