val lemma_pad_to_32_bits (s s'': seq4 nat8) (n: nat)
    : Lemma
      (requires
        n <= 4 /\
        (forall (i: nat). {:pattern (index s i)\/(index s'' i)}
            i < 4 ==> index s'' i == (if i < n then index s i else 0)))
      (ensures
        four_to_nat 8 (seq_to_four_BE s'') ==
        (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n)))
let lemma_pad_to_32_bits (s s'':seq4 nat8) (n:nat) : Lemma
  (requires
    n <= 4 /\
    (forall (i:nat).{:pattern (index s i) \/ (index s'' i)} i < 4 ==>
      index s'' i == (if i < n then index s i else 0))
  )
  (ensures four_to_nat 8 (seq_to_four_BE s'') == (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n)))
  =
  if n <= 2 then lemma_pad_to_32_bits_helper s s'' n else
  assert (n == 3 \/ n == 4);
  assert_norm (four_to_nat 8 (seq_to_four_BE s) == four_to_nat_unfold 8 (seq_to_four_BE s));
  assert_norm (four_to_nat 8 (seq_to_four_BE s'') == four_to_nat_unfold 8 (seq_to_four_BE s''));
  assert_norm (pow2 (0 * 8) == 1);
  assert_norm (pow2 (1 * 8) == 0x100);
  let x = four_to_nat 8 (seq_to_four_BE s'') in
  assert (n == 3 ==> x / pow2 (8 * (4 - n)) == x / 0x100);
  assert (n == 4 ==> x / pow2 (8 * (4 - n)) == x / 0x1);
  assert_norm (((x / pow2 (8 * 1)) * pow2 (8 * 1)) % pow2 (8 * 1) == 0);
  assert_norm (((x / pow2 (8 * 0)) * pow2 (8 * 0)) % pow2 (8 * 0) == 0);
  ()
val lemma_pad_to_32_bits (s s'': seq4 nat8) (n: nat)
    : Lemma
      (requires
        n <= 4 /\
        (forall (i: nat). {:pattern (index s i)\/(index s'' i)}
            i < 4 ==> index s'' i == (if i < n then index s i else 0)))
      (ensures
        four_to_nat 8 (seq_to_four_BE s'') ==
        (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n)))
let lemma_pad_to_32_bits (s s'': seq4 nat8) (n: nat)
    : Lemma
      (requires
        n <= 4 /\
        (forall (i: nat). {:pattern (index s i)\/(index s'' i)}
            i < 4 ==> index s'' i == (if i < n then index s i else 0)))
      (ensures
        four_to_nat 8 (seq_to_four_BE s'') ==
        (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n))) =
if n <= 2 then lemma_pad_to_32_bits_helper s s'' n else assert (n == 3 \/ n == 4);
assert_norm (four_to_nat 8 (seq_to_four_BE s) == four_to_nat_unfold 8 (seq_to_four_BE s));
assert_norm (four_to_nat 8 (seq_to_four_BE s'') == four_to_nat_unfold 8 (seq_to_four_BE s''));
assert_norm (pow2 (0 * 8) == 1);
assert_norm (pow2 (1 * 8) == 0x100);
let x = four_to_nat 8 (seq_to_four_BE s'') in
assert (n == 3 ==> x / pow2 (8 * (4 - n)) == x / 0x100);
assert (n == 4 ==> x / pow2 (8 * (4 - n)) == x / 0x1);
assert_norm (((x / pow2 (8 * 1)) * pow2 (8 * 1)) % pow2 (8 * 1) == 0);
assert_norm (((x / pow2 (8 * 0)) * pow2 (8 * 0)) % pow2 (8 * 0) == 0);
()
Vale.AES.GCM_helpers_BE.fst.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.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_BE_s.fst.checked Vale.AES.AES_BE_s.fst.checked prims.fst.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked
Vale.AES.GCM_helpers_BE.fst
Vale.Def.Words.Seq_s.seq4 Vale.Def.Types_s.nat8 Prims.nat Prims.unit FStar.Pervasives.assert_norm Prims.eq2 Prims.int Prims.op_Modulus FStar.Mul.op_Star Prims.op_Division Prims.pow2 Prims._assert Prims.l_imp Prims.op_Subtraction Vale.Def.Words_s.natN Prims.op_Multiply Vale.Def.Words.Four_s.four_to_nat Vale.Def.Words.Seq_s.seq_to_four_BE Vale.Def.Words.Four_s.four_to_nat_unfold Prims.op_LessThanOrEqual Vale.AES.GCM_helpers_BE.lemma_pad_to_32_bits_helper Prims.bool Prims.l_or Prims.l_and Prims.b2t Prims.l_Forall Prims.op_LessThan FStar.Seq.Base.index Prims.squash Prims.Nil FStar.Pervasives.pattern
module Vale.AES.GCM_helpers_BE

open FStar.Tactics
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.Arch.Types
open FStar.Mul
open FStar.Seq
open Vale.Def.Opaque_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.AES.AES_BE_s
open Vale.AES.GCTR_BE_s
open FStar.Math.Lemmas
open Vale.Lib.Seqs
open Vale.AES.Types_helpers

let no_extra_bytes_helper s num_bytes =
  ()

let be_seq_quad32_to_bytes_tail_prefix (s:seq quad32) (num_bytes:nat) =
  let num_extra = num_bytes % 16 in
  let num_blocks = num_bytes / 16 in
  let final = index s num_blocks in
  let x  = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) (num_blocks * 16) num_bytes in
  let x' = slice (be_quad32_to_bytes final) 0 num_extra in

  be_seq_quad32_to_bytes_of_singleton final;
  assert (be_quad32_to_bytes final == seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE (create 1 final)));
  assert (equal (create 1 final) (slice s num_blocks (length s)));

  assert (x' == slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE (slice s num_blocks (length s)))) 0 num_extra);
  slice_commutes_be_seq_quad32_to_bytes s num_blocks (length s);
  assert (x' == slice (slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) (num_blocks * 16) (length s * 16)) 0 num_extra);
  assert (x' == slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) (num_blocks * 16) num_bytes);

  assert (equal x' x);
  ()

let pad_to_128_bits_multiples (b:seq nat8) : Lemma
  (let full_blocks = (length b) / 16 * 16 in
   let full_bytes, partial_bytes = split b full_blocks in
   pad_to_128_bits b == full_bytes @| pad_to_128_bits partial_bytes)
  =
  let full_blocks = (length b) / 16 * 16 in
  let full_bytes, partial_bytes = split b full_blocks in
  if length b < 16 then (
    assert (full_bytes == empty);
    assert (partial_bytes == b);
    append_empty_l(pad_to_128_bits partial_bytes);
    ()
  ) else (
    assert (length full_bytes + length partial_bytes == length b);
    assert (length full_bytes % 16 == 0);
    let num_extra_bytes = length b % 16 in
    assert (num_extra_bytes == (length partial_bytes) % 16);
    if num_extra_bytes = 0 then (
      lemma_split b full_blocks;
      assert (b == full_bytes @| partial_bytes);
      ()
    ) else (
      let pad = create (16 - num_extra_bytes) 0 in
      assert (equal (b @| pad) (full_bytes @| (partial_bytes @| pad)));
      ()
    );
    ()
  )

let pad_to_128_bits_be_quad32_to_bytes (s:seq quad32) (num_bytes:int) =
  let num_extra = num_bytes % 16 in
  let num_blocks = num_bytes / 16 in
  let full_quads,final_quads = split s num_blocks in
  assert(length final_quads == 1);
  let final_quad = index final_quads 0 in
  let b = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) 0 num_bytes in
  pad_to_128_bits_multiples b; // ==>  pad_to_128_bits b == full_bytes @| pad_to_128_bits partial_bytes
  let full_blocks = (length b) / 16 * 16 in
  let full_bytes, partial_bytes = split b full_blocks in
  slice_commutes_be_seq_quad32_to_bytes0 s num_blocks;
  slice_slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) 0 num_bytes 0 full_blocks;
  assert (full_bytes == seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE full_quads));

  slice_slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) 0 num_bytes full_blocks num_bytes;
  be_seq_quad32_to_bytes_tail_prefix s num_bytes;
  ()

#reset-options "--smtencoding.elim_box true --z3rlimit 60 --z3refresh --initial_ifuel 0 --max_ifuel 1 --initial_fuel 1 --max_fuel 1"
let lemma_pad_to_32_bits_helper (s s'':seq4 nat8) (n:nat) : Lemma
  (requires
    n <= 2 /\
    (forall (i:nat).{:pattern (index s i) \/ (index s'' i)} i < 4 ==>
      index s'' i == (if i < n then index s i else 0))
  )
  (ensures four_to_nat 8 (seq_to_four_BE s'') == (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n)))
  =
  assert (n == 0 \/ n == 1 \/ n == 2);
  assert_norm (four_to_nat 8 (seq_to_four_BE s) == four_to_nat_unfold 8 (seq_to_four_BE s));
  assert_norm (four_to_nat 8 (seq_to_four_BE s'') == four_to_nat_unfold 8 (seq_to_four_BE s''));
  assert_norm (pow2 (2 * 8) == 0x10000);
  assert_norm (pow2 (3 * 8) == 0x1000000);
  assert_norm (pow2 (4 * 8) == 0x100000000);
  let x = four_to_nat 8 (seq_to_four_BE s'') in
  assert (n == 0 ==> x / pow2 (8 * (4 - n)) == x / 0x100000000);
  assert (n == 1 ==> x / pow2 (8 * (4 - n)) == x / 0x1000000);
  assert (n == 2 ==> x / pow2 (8 * (4 - n)) == x / 0x10000);
  assert_norm (((x / pow2 (8 * 4)) * pow2 (8 * 4)) % pow2 (8 * 4) == 0);
  assert_norm (((x / pow2 (8 * 3)) * pow2 (8 * 3)) % pow2 (8 * 3) == 0);
  assert_norm (((x / pow2 (8 * 2)) * pow2 (8 * 2)) % pow2 (8 * 2) == 0);
  ()

let lemma_pad_to_32_bits (s s'':seq4 nat8) (n:nat) : Lemma
  (requires
    n <= 4 /\
    (forall (i:nat).{:pattern (index s i) \/ (index s'' i)} i < 4 ==>
      index s'' i == (if i < n then index s i else 0))
  )
  (ensures four_to_nat 8 (seq_to_four_BE s'') == (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n)))
val lemma_pad_to_32_bits (s s'': seq4 nat8) (n: nat)
    : Lemma
      (requires
        n <= 4 /\
        (forall (i: nat). {:pattern (index s i)\/(index s'' i)}
            i < 4 ==> index s'' i == (if i < n then index s i else 0)))
      (ensures
        four_to_nat 8 (seq_to_four_BE s'') ==
        (four_to_nat 8 (seq_to_four_BE s) / pow2 (8 * (4 - n))) * pow2 (8 * (4 - n)))

    s: Vale.Def.Words.Seq_s.seq4 Vale.Def.Types_s.nat8 ->
    s'': Vale.Def.Words.Seq_s.seq4 Vale.Def.Types_s.nat8 ->
    n: Prims.nat
  -> FStar.Pervasives.Lemma
      (requires
        n <= 4 /\
        (forall (i: Prims.nat). {:pattern FStar.Seq.Base.index s i\/FStar.Seq.Base.index s'' i}
            i < 4 ==>
            FStar.Seq.Base.index s'' i ==
            (match i < n with
              | true -> FStar.Seq.Base.index s i
              | _ -> 0)))
      (ensures
        Vale.Def.Words.Four_s.four_to_nat 8 (Vale.Def.Words.Seq_s.seq_to_four_BE s'') ==
        (Vale.Def.Words.Four_s.four_to_nat 8 (Vale.Def.Words.Seq_s.seq_to_four_BE s) /
        Prims.pow2 (8 * (4 - n))) *
        Prims.pow2 (8 * (4 - n)))