val pad_to_128_bits_be_quad32_to_bytes (s:seq quad32) (num_bytes:int) : Lemma
  (requires 1 <= num_bytes /\
             num_bytes < 16 * length s /\
             16 * (length s - 1) < num_bytes /\
             num_bytes % 16 <> 0 /\
             length s == bytes_to_quad_size num_bytes)
  (ensures (let num_blocks = num_bytes / 16 in
            let full_quads,final_quads = split s num_blocks in
            length final_quads == 1 /\
            (let final_quad = index final_quads 0 in
             pad_to_128_bits (slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) 0 num_bytes)
             ==
             seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE full_quads) @| pad_to_128_bits (slice (be_quad32_to_bytes final_quad) 0 (num_bytes % 16)))))
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;
  ()
val pad_to_128_bits_be_quad32_to_bytes (s:seq quad32) (num_bytes:int) : Lemma
  (requires 1 <= num_bytes /\
             num_bytes < 16 * length s /\
             16 * (length s - 1) < num_bytes /\
             num_bytes % 16 <> 0 /\
             length s == bytes_to_quad_size num_bytes)
  (ensures (let num_blocks = num_bytes / 16 in
            let full_quads,final_quads = split s num_blocks in
            length final_quads == 1 /\
            (let final_quad = index final_quads 0 in
             pad_to_128_bits (slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) 0 num_bytes)
             ==
             seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE full_quads) @| pad_to_128_bits (slice (be_quad32_to_bytes final_quad) 0 (num_bytes % 16)))))
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;
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;
()
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.quad32 Prims.int Vale.Def.Words_s.nat8 Prims.unit Vale.AES.GCM_helpers_BE.be_seq_quad32_to_bytes_tail_prefix FStar.Seq.Properties.slice_slice Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE Vale.Def.Words.Seq_s.seq_four_to_seq_BE Vale.Def.Types_s.nat32 Prims._assert Prims.eq2 Vale.Arch.Types.slice_commutes_be_seq_quad32_to_bytes0 FStar.Pervasives.Native.tuple2 FStar.Seq.Properties.split FStar.Mul.op_Star Prims.op_Division FStar.Seq.Base.length Vale.AES.GCM_helpers_BE.pad_to_128_bits_multiples FStar.Seq.Base.slice FStar.Seq.Base.index Prims.op_Modulus
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)));
      ()
    );
    ()
  )
val pad_to_128_bits_be_quad32_to_bytes (s:seq quad32) (num_bytes:int) : Lemma
  (requires 1 <= num_bytes /\
             num_bytes < 16 * length s /\
             16 * (length s - 1) < num_bytes /\
             num_bytes % 16 <> 0 /\
             length s == bytes_to_quad_size num_bytes)
  (ensures (let num_blocks = num_bytes / 16 in
            let full_quads,final_quads = split s num_blocks in
            length final_quads == 1 /\
            (let final_quad = index final_quads 0 in
             pad_to_128_bits (slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE s)) 0 num_bytes)
             ==
             seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE full_quads) @| pad_to_128_bits (slice (be_quad32_to_bytes final_quad) 0 (num_bytes % 16)))))
s: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 -> num_bytes: Prims.int
  -> FStar.Pervasives.Lemma
      (requires
        1 <= num_bytes /\ num_bytes < 16 * FStar.Seq.Base.length s /\
        16 * (FStar.Seq.Base.length s - 1) < num_bytes /\ num_bytes % 16 <> 0 /\
        FStar.Seq.Base.length s == Vale.AES.GCM_helpers_BE.bytes_to_quad_size num_bytes)
      (ensures
        (let num_blocks = num_bytes / 16 in
          let _ = FStar.Seq.Properties.split s num_blocks in
          (let FStar.Pervasives.Native.Mktuple2 #_ #_ full_quads final_quads = _ in
            FStar.Seq.Base.length final_quads == 1 /\
            (let final_quad = FStar.Seq.Base.index final_quads 0 in
              Vale.AES.GCTR_BE_s.pad_to_128_bits (FStar.Seq.Base.slice (Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE
                        (Vale.Def.Words.Seq_s.seq_four_to_seq_BE s))
                    0
                    num_bytes) ==
              Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE (Vale.Def.Words.Seq_s.seq_four_to_seq_BE
                    full_quads) @|
              Vale.AES.GCTR_BE_s.pad_to_128_bits (FStar.Seq.Base.slice (Vale.Arch.Types.be_quad32_to_bytes
                        final_quad)
                    0
                    (num_bytes % 16))))
          <:
          Type0))