val lemma_be_seq_quad32_to_bytes_prefix_equality (q: quad32)
    : Lemma
    (slice (be_quad32_to_bytes q) 0 12 ==
      slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
let lemma_be_seq_quad32_to_bytes_prefix_equality (q:quad32) : Lemma
  (slice (be_quad32_to_bytes q) 0 12 == slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
  =
  assert (equal (slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
                (slice (be_quad32_to_bytes q) 0 12));
  ()
val lemma_be_seq_quad32_to_bytes_prefix_equality (q: quad32)
    : Lemma
    (slice (be_quad32_to_bytes q) 0 12 ==
      slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
let lemma_be_seq_quad32_to_bytes_prefix_equality (q: quad32)
    : Lemma
    (slice (be_quad32_to_bytes q) 0 12 ==
      slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12) =
assert (equal (slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
      (slice (be_quad32_to_bytes q) 0 12));
()
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
Vale.Def.Types_s.quad32 Prims.unit Prims._assert FStar.Seq.Base.equal Vale.Def.Types_s.nat8 FStar.Seq.Base.slice Vale.AES.GCTR_BE_s.pad_to_128_bits Vale.Def.Words_s.nat8 Vale.Arch.Types.be_quad32_to_bytes Prims.l_True Prims.squash Prims.eq2 FStar.Seq.Base.seq 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)
  (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))

let lemma_be_seq_quad32_to_bytes_prefix_equality (q:quad32) : Lemma
  (slice (be_quad32_to_bytes q) 0 12 == slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
val lemma_be_seq_quad32_to_bytes_prefix_equality (q: quad32)
    : Lemma
    (slice (be_quad32_to_bytes q) 0 12 ==
      slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12)
q: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
    (ensures
      FStar.Seq.Base.slice (Vale.Arch.Types.be_quad32_to_bytes q) 0 12 ==
      FStar.Seq.Base.slice (Vale.AES.GCTR_BE_s.pad_to_128_bits (FStar.Seq.Base.slice (Vale.Arch.Types.be_quad32_to_bytes
                    q)
                0
                12))
        0
        12)