val lemma_counter_init (x:quad32) (low64 low8:nat64) : Lemma
  (requires low64 == lo64 x /\
            low8  == iand64 low64 0xff)
  (ensures  low8 == x.lo0 % 256)
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);
  ()
val lemma_counter_init (x:quad32) (low64 low8:nat64) : Lemma
  (requires low64 == lo64 x /\
            low8  == iand64 low64 0xff)
  (ensures  low8 == x.lo0 % 256)
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);
assert (low64 == x.lo0 + x.lo1 * pow2_32);
assert (low64 % 256 == x.lo0 % 256);
()
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.Def.Types_s.quad32 Vale.Def.Types_s.nat64 Prims.unit Prims._assert Prims.eq2 Prims.int Prims.op_Modulus Vale.Def.Words_s.__proj__Mkfour__item__lo0 Vale.Def.Types_s.nat32 Prims.op_Addition FStar.Mul.op_Star Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.pow2_32 FStar.Pervasives.assert_norm Vale.Def.Words_s.pow2_norm Vale.Arch.Types.lo64_reveal Vale.Def.TypesNative_s.reveal_iand Vale.Poly1305.Bitvectors.lemma_bytes_and_mod1
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"
val lemma_counter_init (x:quad32) (low64 low8:nat64) : Lemma
  (requires low64 == lo64 x /\
            low8  == iand64 low64 0xff)
  (ensures  low8 == x.lo0 % 256)
x: Vale.Def.Types_s.quad32 -> low64: Vale.Def.Types_s.nat64 -> low8: Vale.Def.Types_s.nat64
  -> FStar.Pervasives.Lemma
      (requires low64 == Vale.Arch.Types.lo64 x /\ low8 == Vale.Arch.Types.iand64 low64 0xff)
      (ensures low8 == Mkfour?.lo0 x % 256)