val lemma_be_bytes_to_quad32_prefix_equality
      (b0: seq nat8 {length b0 == 16})
      (b1: seq nat8 {length b1 == 16})
    : Lemma (requires slice b0 0 12 == slice b1 0 12)
      (ensures upper3_equal (be_bytes_to_quad32 b0) (be_bytes_to_quad32 b1))
let lemma_be_bytes_to_quad32_prefix_equality (b0:seq nat8 {length b0 == 16}) (b1:seq nat8 {length b1 == 16}) : Lemma
  (requires slice b0 0 12 == slice b1 0 12)
  (ensures upper3_equal (be_bytes_to_quad32 b0) (be_bytes_to_quad32 b1))
  =
  let q0 = be_bytes_to_quad32 b0 in
  let q1 = be_bytes_to_quad32 b1 in
  be_bytes_to_quad32_reveal ();

  reveal_opaque (`%seq_to_seq_four_BE) (seq_to_seq_four_BE #nat8);

  assert (forall (i:int). (0 <= i /\ i < 12) ==> (index b0 i == index (slice b0 0 12) i /\
                                         index b1 i == index (slice b1 0 12) i))
val lemma_be_bytes_to_quad32_prefix_equality
      (b0: seq nat8 {length b0 == 16})
      (b1: seq nat8 {length b1 == 16})
    : Lemma (requires slice b0 0 12 == slice b1 0 12)
      (ensures upper3_equal (be_bytes_to_quad32 b0) (be_bytes_to_quad32 b1))
let lemma_be_bytes_to_quad32_prefix_equality
      (b0: seq nat8 {length b0 == 16})
      (b1: seq nat8 {length b1 == 16})
    : Lemma (requires slice b0 0 12 == slice b1 0 12)
      (ensures upper3_equal (be_bytes_to_quad32 b0) (be_bytes_to_quad32 b1)) =
let q0 = be_bytes_to_quad32 b0 in
let q1 = be_bytes_to_quad32 b1 in
be_bytes_to_quad32_reveal ();
reveal_opaque (`%seq_to_seq_four_BE) (seq_to_seq_four_BE #nat8);
assert (forall (i: int).
      (0 <= i /\ i < 12) ==>
      (index b0 i == index (slice b0 0 12) i /\ index b1 i == index (slice b1 0 12) i))
Vale.AES.GCM_BE.fst.checked
Vale.Lib.Seqs.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.GHash_BE_s.fst.checked Vale.AES.GCTR_BE_s.fst.checked Vale.AES.GCTR_BE.fsti.checked Vale.AES.GCM_helpers_BE.fsti.checked Vale.AES.GCM_BE_s.fst.checked Vale.AES.AES_BE_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Calc.fsti.checked
Vale.AES.GCM_BE.fst
FStar.Seq.Base.seq Vale.Def.Words_s.nat8 Prims.eq2 Prims.int FStar.Seq.Base.length Prims._assert Prims.l_Forall Prims.l_imp Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan FStar.Seq.Base.index FStar.Seq.Base.slice Prims.unit FStar.Pervasives.reveal_opaque Prims.op_Modulus Vale.Def.Words_s.four Prims.op_Division Vale.Def.Words.Seq_s.seq_to_seq_four_BE Vale.Def.Types_s.be_bytes_to_quad32_reveal Vale.Def.Types_s.quad32 Vale.Def.Types_s.be_bytes_to_quad32 Prims.squash Vale.AES.GCM_BE.upper3_equal Prims.Nil FStar.Pervasives.pattern
module Vale.AES.GCM_BE

open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.AES.GCM_BE_s
open Vale.AES.AES_BE_s
open Vale.AES.GCM_helpers_BE
open Vale.AES.GCTR_BE_s
open Vale.AES.GCTR_BE
open Vale.AES.GHash_BE_s
open FStar.Mul
open FStar.Seq
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open FStar.Calc

let upper3_equal (q0 q1:quad32) : bool = 
  q0.lo1 = q1.lo1 &&
  q0.hi2 = q1.hi2 &&
  q0.hi3 = q1.hi3

let lemma_be_bytes_to_quad32_prefix_equality (b0:seq nat8 {length b0 == 16}) (b1:seq nat8 {length b1 == 16}) : Lemma
  (requires slice b0 0 12 == slice b1 0 12)
val lemma_be_bytes_to_quad32_prefix_equality
      (b0: seq nat8 {length b0 == 16})
      (b1: seq nat8 {length b1 == 16})
    : Lemma (requires slice b0 0 12 == slice b1 0 12)
      (ensures upper3_equal (be_bytes_to_quad32 b0) (be_bytes_to_quad32 b1))

    b0: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 {FStar.Seq.Base.length b0 == 16} ->
    b1: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 {FStar.Seq.Base.length b1 == 16}
  -> FStar.Pervasives.Lemma (requires FStar.Seq.Base.slice b0 0 12 == FStar.Seq.Base.slice b1 0 12)
      (ensures
        Vale.AES.GCM_BE.upper3_equal (Vale.Def.Types_s.be_bytes_to_quad32 b0)
          (Vale.Def.Types_s.be_bytes_to_quad32 b1))