val be_seq_quad32_to_bytes_tail_prefix (s:seq quad32) (num_bytes:nat) : Lemma
  (requires (1 <= num_bytes /\
             num_bytes < 16 * length s /\
             16 * (length s - 1) < num_bytes /\
             num_bytes % 16 <> 0))
  (ensures (let num_extra = num_bytes % 16 in
            let num_blocks = num_bytes / 16 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 (index s num_blocks)) 0 num_extra in
            x == x'))
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);
  ()
val be_seq_quad32_to_bytes_tail_prefix (s:seq quad32) (num_bytes:nat) : Lemma
  (requires (1 <= num_bytes /\
             num_bytes < 16 * length s /\
             16 * (length s - 1) < num_bytes /\
             num_bytes % 16 <> 0))
  (ensures (let num_extra = num_bytes % 16 in
            let num_blocks = num_bytes / 16 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 (index s num_blocks)) 0 num_extra in
            x == x'))
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);
()
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.nat Prims.unit Prims._assert FStar.Seq.Base.equal Vale.Def.Words_s.nat8 Prims.eq2 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 Vale.Def.Types_s.nat32 FStar.Mul.op_Star FStar.Seq.Base.length Vale.Arch.Types.slice_commutes_be_seq_quad32_to_bytes FStar.Seq.Base.create Vale.Arch.Types.be_quad32_to_bytes Vale.Def.Words_s.nat32 Vale.Def.Words_s.four Vale.Arch.Types.be_seq_quad32_to_bytes_of_singleton FStar.Seq.Base.index Prims.int Prims.op_Division 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 =
  ()
val be_seq_quad32_to_bytes_tail_prefix (s:seq quad32) (num_bytes:nat) : Lemma
  (requires (1 <= num_bytes /\
             num_bytes < 16 * length s /\
             16 * (length s - 1) < num_bytes /\
             num_bytes % 16 <> 0))
  (ensures (let num_extra = num_bytes % 16 in
            let num_blocks = num_bytes / 16 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 (index s num_blocks)) 0 num_extra in
            x == x'))
s: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 -> num_bytes: Prims.nat
  -> 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)
      (ensures
        (let num_extra = num_bytes % 16 in
          let num_blocks = num_bytes / 16 in
          let x =
            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))
              (num_blocks * 16)
              num_bytes
          in
          let x' =
            FStar.Seq.Base.slice (Vale.Arch.Types.be_quad32_to_bytes (FStar.Seq.Base.index s
                      num_blocks))
              0
              num_extra
          in
          x == x'))