val lemma_compute_iv_easy (iv_b iv_extra_b:seq quad32) (iv:supported_iv_BE) (num_bytes:nat64) (h_BE j0:quad32) : Lemma
  (requires
    length iv_extra_b == 1 /\
    length iv_b * (128/8) <= num_bytes /\ num_bytes < length iv_b * (128/8) + 128/8 /\
    num_bytes == 96/8 /\
    (let iv_BE = index iv_extra_b 0 in
     j0 == Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3) /\
    (let raw_quads = append iv_b iv_extra_b in
     let iv_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE raw_quads)) 0 num_bytes in
     iv_bytes == iv))
  (ensures j0 == compute_iv_BE h_BE iv)
let lemma_compute_iv_easy (iv_b iv_extra_b:seq quad32) (iv:supported_iv_BE) (num_bytes:nat64) (h_BE j0:quad32) : Lemma
  (requires
    length iv_extra_b == 1 /\
    length iv_b * (128/8) <= num_bytes /\ num_bytes < length iv_b * (128/8) + 128/8 /\
    num_bytes == 96/8 /\
    (let iv_BE = index iv_extra_b 0 in
     j0 == Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3) /\
    (let raw_quads = append iv_b iv_extra_b in
     let iv_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE raw_quads)) 0 num_bytes in
     iv_bytes == iv))
  (ensures j0 == compute_iv_BE h_BE iv)
  =
  assert (length iv == 12);
  assert (length iv_b == 0);
  lemma_empty iv_b;
  append_empty_l iv_extra_b;
  assert (append iv_b iv_extra_b == iv_extra_b);
  let q = index iv_extra_b 0 in
  be_seq_quad32_to_bytes_of_singleton q;
  assert (equal iv_extra_b (create 1 q));
  assert (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE iv_extra_b) == be_quad32_to_bytes q);

  calc (==) {
    slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12;
    == {}
    slice (pad_to_128_bits iv) 0 12;
  };

  calc (==) {
    be_bytes_to_quad32 (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 num_bytes));
    == {}
    be_bytes_to_quad32 (pad_to_128_bits (slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE iv_extra_b)) 0 num_bytes));
    == {}
    be_bytes_to_quad32 (pad_to_128_bits iv);
  };
  
  calc (==) {
    j0;
    == {}
    set_to_one q;
    == {  be_bytes_to_quad32_to_bytes q }
    set_to_one (be_bytes_to_quad32 (be_quad32_to_bytes q));
    == { 
         lemma_be_seq_quad32_to_bytes_prefix_equality q;
         lemma_be_bytes_to_quad32_prefix_equality 
           (be_quad32_to_bytes q)
           (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12))
       }
    set_to_one (be_bytes_to_quad32 (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)));
    == { lemma_be_bytes_to_quad32_prefix_equality 
           (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 
           (pad_to_128_bits iv) }
    set_to_one (be_bytes_to_quad32 (pad_to_128_bits iv));
    == {compute_iv_BE_reveal ()}
    compute_iv_BE h_BE iv;
  };
  ()
val lemma_compute_iv_easy (iv_b iv_extra_b:seq quad32) (iv:supported_iv_BE) (num_bytes:nat64) (h_BE j0:quad32) : Lemma
  (requires
    length iv_extra_b == 1 /\
    length iv_b * (128/8) <= num_bytes /\ num_bytes < length iv_b * (128/8) + 128/8 /\
    num_bytes == 96/8 /\
    (let iv_BE = index iv_extra_b 0 in
     j0 == Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3) /\
    (let raw_quads = append iv_b iv_extra_b in
     let iv_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE raw_quads)) 0 num_bytes in
     iv_bytes == iv))
  (ensures j0 == compute_iv_BE h_BE iv)
let lemma_compute_iv_easy
      (iv_b iv_extra_b: seq quad32)
      (iv: supported_iv_BE)
      (num_bytes: nat64)
      (h_BE j0: quad32)
    : Lemma
      (requires
        length iv_extra_b == 1 /\ length iv_b * (128 / 8) <= num_bytes /\
        num_bytes < length iv_b * (128 / 8) + 128 / 8 /\ num_bytes == 96 / 8 /\
        (let iv_BE = index iv_extra_b 0 in
          j0 == Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3) /\
        (let raw_quads = append iv_b iv_extra_b in
          let iv_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE raw_quads)) 0 num_bytes
          in
          iv_bytes == iv)) (ensures j0 == compute_iv_BE h_BE iv) =
assert (length iv == 12);
assert (length iv_b == 0);
lemma_empty iv_b;
append_empty_l iv_extra_b;
assert (append iv_b iv_extra_b == iv_extra_b);
let q = index iv_extra_b 0 in
be_seq_quad32_to_bytes_of_singleton q;
assert (equal iv_extra_b (create 1 q));
assert (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE iv_extra_b) == be_quad32_to_bytes q);
calc ( == ) {
  slice (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)) 0 12;
  ( == ) { () }
  slice (pad_to_128_bits iv) 0 12;
};
calc ( == ) {
  be_bytes_to_quad32 (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 num_bytes));
  ( == ) { () }
  be_bytes_to_quad32 (pad_to_128_bits (slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE iv_extra_b
                  ))
            0
            num_bytes));
  ( == ) { () }
  be_bytes_to_quad32 (pad_to_128_bits iv);
};
calc ( == ) {
  j0;
  ( == ) { () }
  set_to_one q;
  ( == ) { be_bytes_to_quad32_to_bytes q }
  set_to_one (be_bytes_to_quad32 (be_quad32_to_bytes q));
  ( == ) { (lemma_be_seq_quad32_to_bytes_prefix_equality q;
    lemma_be_bytes_to_quad32_prefix_equality (be_quad32_to_bytes q)
      (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12))) }
  set_to_one (be_bytes_to_quad32 (pad_to_128_bits (slice (be_quad32_to_bytes q) 0 12)));
  ( == ) { lemma_be_bytes_to_quad32_prefix_equality (pad_to_128_bits (slice (be_quad32_to_bytes q)
            0
            12))
    (pad_to_128_bits iv) }
  set_to_one (be_bytes_to_quad32 (pad_to_128_bits iv));
  ( == ) { compute_iv_BE_reveal () }
  compute_iv_BE h_BE iv;
};
()
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.Types_s.quad32 Vale.AES.GCM_BE_s.supported_iv_BE Vale.Def.Words_s.nat64 Prims.unit FStar.Calc.calc_finish Prims.eq2 Vale.AES.GCM_BE_s.compute_iv_BE Prims.Cons FStar.Preorder.relation Prims.Nil FStar.Calc.calc_step Vale.AES.GCM_BE.set_to_one Vale.Def.Types_s.be_bytes_to_quad32 Vale.AES.GCTR_BE_s.pad_to_128_bits FStar.Seq.Base.slice Vale.Def.Words_s.nat8 Vale.Arch.Types.be_quad32_to_bytes FStar.Calc.calc_init FStar.Calc.calc_pack Prims.squash Vale.Arch.Types.be_bytes_to_quad32_to_bytes Vale.AES.GCM_BE.lemma_be_bytes_to_quad32_prefix_equality Vale.AES.GCM_BE.lemma_be_seq_quad32_to_bytes_prefix_equality Vale.AES.GCM_BE_s.compute_iv_BE_reveal 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 Vale.Def.Types_s.nat8 Prims._assert FStar.Seq.Base.equal FStar.Seq.Base.create Vale.Arch.Types.be_seq_quad32_to_bytes_of_singleton FStar.Seq.Base.index FStar.Seq.Base.append FStar.Seq.Base.append_empty_l FStar.Seq.Base.lemma_empty Prims.int FStar.Seq.Base.length Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.Mul.op_Star Prims.op_Division Prims.op_LessThan Prims.op_Addition Vale.Def.Words_s.four Vale.Def.Words_s.Mkfour Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__hi3 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)
  =
  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));
  ()

let lemma_compute_iv_easy (iv_b iv_extra_b:seq quad32) (iv:supported_iv_BE) (num_bytes:nat64) (h_BE j0:quad32) : Lemma
  (requires
    length iv_extra_b == 1 /\
    length iv_b * (128/8) <= num_bytes /\ num_bytes < length iv_b * (128/8) + 128/8 /\
    num_bytes == 96/8 /\
    (let iv_BE = index iv_extra_b 0 in
     j0 == Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3) /\
    (let raw_quads = append iv_b iv_extra_b in
     let iv_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE raw_quads)) 0 num_bytes in
     iv_bytes == iv))
  (ensures j0 == compute_iv_BE h_BE iv)
val lemma_compute_iv_easy (iv_b iv_extra_b:seq quad32) (iv:supported_iv_BE) (num_bytes:nat64) (h_BE j0:quad32) : Lemma
  (requires
    length iv_extra_b == 1 /\
    length iv_b * (128/8) <= num_bytes /\ num_bytes < length iv_b * (128/8) + 128/8 /\
    num_bytes == 96/8 /\
    (let iv_BE = index iv_extra_b 0 in
     j0 == Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3) /\
    (let raw_quads = append iv_b iv_extra_b in
     let iv_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE raw_quads)) 0 num_bytes in
     iv_bytes == iv))
  (ensures j0 == compute_iv_BE h_BE iv)

    iv_b: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    iv_extra_b: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    iv: Vale.AES.GCM_BE_s.supported_iv_BE ->
    num_bytes: Vale.Def.Words_s.nat64 ->
    h_BE: Vale.Def.Types_s.quad32 ->
    j0: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length iv_extra_b == 1 /\ FStar.Seq.Base.length iv_b * (128 / 8) <= num_bytes /\
        num_bytes < FStar.Seq.Base.length iv_b * (128 / 8) + 128 / 8 /\ num_bytes == 96 / 8 /\
        (let iv_BE = FStar.Seq.Base.index iv_extra_b 0 in
          j0 ==
          Vale.Def.Words_s.Mkfour 1 (Mkfour?.lo1 iv_BE) (Mkfour?.hi2 iv_BE) (Mkfour?.hi3 iv_BE)) /\
        (let raw_quads = FStar.Seq.Base.append iv_b iv_extra_b in
          let iv_bytes =
            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
                      raw_quads))
              0
              num_bytes
          in
          iv_bytes == iv)) (ensures j0 == Vale.AES.GCM_BE_s.compute_iv_BE h_BE iv)