val gctr_partial_opaque_ignores_postfix (alg:algorithm) (bound:nat32) (plain plain' cipher cipher':seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires is_aes_key_LE alg key /\
            length plain >= bound /\
            length cipher >= bound /\
            length plain' >= bound /\
            length cipher' >= bound /\
            slice plain  0 bound == slice plain'  0 bound /\
            slice cipher 0 bound == slice cipher' 0 bound)
  (ensures gctr_partial alg bound plain cipher key icb <==> gctr_partial alg bound plain' cipher' key icb)
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);
  ()
val gctr_partial_opaque_ignores_postfix (alg:algorithm) (bound:nat32) (plain plain' cipher cipher':seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires is_aes_key_LE alg key /\
            length plain >= bound /\
            length cipher >= bound /\
            length plain' >= bound /\
            length cipher' >= bound /\
            slice plain  0 bound == slice plain'  0 bound /\
            slice cipher 0 bound == slice cipher' 0 bound)
  (ensures gctr_partial alg bound plain cipher key icb <==> gctr_partial alg bound plain' cipher' key icb)
let gctr_partial_opaque_ignores_postfix alg bound plain plain' cipher cipher' key icb =
gctr_partial_reveal ();
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);
()
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 Vale.Def.Types_s.nat32 FStar.Seq.Base.seq Vale.Def.Types_s.quad32 Prims.unit Prims._assert Prims.l_Forall Prims.int Prims.l_and Prims.b2t Prims.op_GreaterThanOrEqual Prims.op_LessThan FStar.Seq.Base.length FStar.Seq.Base.slice Prims.l_imp Prims.op_LessThanOrEqual Prims.eq2 FStar.Seq.Base.index 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 ();
  ()
val gctr_partial_opaque_ignores_postfix (alg:algorithm) (bound:nat32) (plain plain' cipher cipher':seq quad32) (key:seq nat32) (icb:quad32) : Lemma
  (requires is_aes_key_LE alg key /\
            length plain >= bound /\
            length cipher >= bound /\
            length plain' >= bound /\
            length cipher' >= bound /\
            slice plain  0 bound == slice plain'  0 bound /\
            slice cipher 0 bound == slice cipher' 0 bound)
  (ensures gctr_partial alg bound plain cipher key icb <==> gctr_partial alg bound plain' cipher' key icb)

    alg: Vale.AES.AES_common_s.algorithm ->
    bound: Vale.Def.Types_s.nat32 ->
    plain: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    plain': FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    cipher: 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 >= bound /\
        FStar.Seq.Base.length cipher >= bound /\ FStar.Seq.Base.length plain' >= bound /\
        FStar.Seq.Base.length cipher' >= bound /\
        FStar.Seq.Base.slice plain 0 bound == FStar.Seq.Base.slice plain' 0 bound /\
        FStar.Seq.Base.slice cipher 0 bound == FStar.Seq.Base.slice cipher' 0 bound)
      (ensures
        Vale.AES.GCTR.gctr_partial alg bound plain cipher key icb <==>
        Vale.AES.GCTR.gctr_partial alg bound plain' cipher' key icb)