val 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 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)));
      ()
    );
    ()
  )
val 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 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)));
        ());
    ())
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
FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.op_LessThan FStar.Seq.Base.length Prims.unit FStar.Seq.Base.append_empty_l Vale.AES.GCTR_BE_s.pad_to_128_bits Prims._assert Prims.eq2 FStar.Seq.Base.empty Prims.bool Prims.op_Equality Prims.int FStar.Seq.Base.op_At_Bar FStar.Seq.Properties.lemma_split FStar.Seq.Base.equal Vale.Def.Words_s.nat8 FStar.Seq.Base.create Prims.op_Subtraction Prims.op_Modulus Prims.op_Addition FStar.Pervasives.Native.tuple2 FStar.Seq.Properties.split FStar.Mul.op_Star Prims.op_Division Prims.l_True 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
val 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)
b: FStar.Seq.Base.seq Vale.Def.Types_s.nat8
  -> FStar.Pervasives.Lemma
    (ensures
      (let full_blocks = (FStar.Seq.Base.length b / 16) * 16 in
        let _ = FStar.Seq.Properties.split b full_blocks in
        (let FStar.Pervasives.Native.Mktuple2 #_ #_ full_bytes partial_bytes = _ in
          Vale.AES.GCTR_BE_s.pad_to_128_bits b ==
          full_bytes @| Vale.AES.GCTR_BE_s.pad_to_128_bits partial_bytes)
        <:
        Type0))