val gcm_encrypt_BE_fst_helper
      (iv: supported_iv_BE)
      (iv_enc iv_BE: quad32)
      (plain auth cipher: seq nat8)
      (alg: algorithm)
      (key: seq nat32)
    : Lemma
      (requires
        is_aes_key_word alg key /\ length plain < pow2_32 /\ length auth < pow2_32 /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          iv_enc == inc32 (compute_iv_BE h_BE iv) 1 /\ cipher == gctr_encrypt iv_enc plain alg key))
      (ensures cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth))
let gcm_encrypt_BE_fst_helper (iv:supported_iv_BE) (iv_enc iv_BE:quad32) (plain auth cipher:seq nat8) (alg:algorithm) (key:seq nat32) : Lemma
  (requires
    is_aes_key_word alg key /\
    length plain < pow2_32 /\
    length auth < pow2_32 /\
   (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
    iv_enc == inc32 (compute_iv_BE h_BE iv) 1 /\
    cipher == gctr_encrypt iv_enc plain alg key
  ))
  (ensures cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth))
  =
  gcm_encrypt_BE_reveal ()
val gcm_encrypt_BE_fst_helper
      (iv: supported_iv_BE)
      (iv_enc iv_BE: quad32)
      (plain auth cipher: seq nat8)
      (alg: algorithm)
      (key: seq nat32)
    : Lemma
      (requires
        is_aes_key_word alg key /\ length plain < pow2_32 /\ length auth < pow2_32 /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          iv_enc == inc32 (compute_iv_BE h_BE iv) 1 /\ cipher == gctr_encrypt iv_enc plain alg key))
      (ensures cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth))
let gcm_encrypt_BE_fst_helper
      (iv: supported_iv_BE)
      (iv_enc iv_BE: quad32)
      (plain auth cipher: seq nat8)
      (alg: algorithm)
      (key: seq nat32)
    : Lemma
      (requires
        is_aes_key_word alg key /\ length plain < pow2_32 /\ length auth < pow2_32 /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          iv_enc == inc32 (compute_iv_BE h_BE iv) 1 /\ cipher == gctr_encrypt iv_enc plain alg key))
      (ensures cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth)) =
gcm_encrypt_BE_reveal ()
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.AES.GCM_BE_s.supported_iv_BE Vale.Def.Types_s.quad32 FStar.Seq.Base.seq Vale.Def.Words_s.nat8 Vale.AES.AES_common_s.algorithm Vale.Def.Words_s.nat32 Vale.AES.GCM_BE_s.gcm_encrypt_BE_reveal Prims.unit Prims.l_and Vale.AES.AES_BE_s.is_aes_key_word Prims.b2t Prims.op_LessThan FStar.Seq.Base.length Vale.Def.Words_s.pow2_32 Prims.eq2 Vale.AES.GCTR_BE_s.inc32 Vale.AES.GCM_BE_s.compute_iv_BE Vale.Def.Types_s.nat8 Vale.AES.GCTR_BE_s.gctr_encrypt Vale.AES.AES_BE_s.aes_encrypt_word Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 Prims.squash FStar.Pervasives.Native.fst Vale.AES.GCM_BE_s.gcm_encrypt_BE Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE 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)
  =
  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)
  =
  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;
  };
  ()

let lemma_compute_iv_hard (iv:supported_iv_BE) (quads:seq quad32) (length_quad h_BE j0:quad32) : Lemma
  (requires
    ~(length iv == 96/8) /\
    quads == be_bytes_to_seq_quad32 (pad_to_128_bits iv) /\
    j0 == ghash_incremental h_BE (Mkfour 0 0 0 0) (append quads (create 1 length_quad)) /\
    length_quad == two_two_to_four (Mktwo (nat_to_two 32 0)
                                          (nat_to_two 32 (8 * length iv))))
  (ensures j0 == compute_iv_BE h_BE iv)
  =
  ghash_incremental_to_ghash h_BE (append quads (create 1 length_quad));
  compute_iv_BE_reveal ();
  ()

let gcm_encrypt_BE_fst_helper (iv:supported_iv_BE) (iv_enc iv_BE:quad32) (plain auth cipher:seq nat8) (alg:algorithm) (key:seq nat32) : Lemma
  (requires
    is_aes_key_word alg key /\
    length plain < pow2_32 /\
    length auth < pow2_32 /\
   (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
    iv_enc == inc32 (compute_iv_BE h_BE iv) 1 /\
    cipher == gctr_encrypt iv_enc plain alg key
  ))
  (ensures cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth))
val gcm_encrypt_BE_fst_helper
      (iv: supported_iv_BE)
      (iv_enc iv_BE: quad32)
      (plain auth cipher: seq nat8)
      (alg: algorithm)
      (key: seq nat32)
    : Lemma
      (requires
        is_aes_key_word alg key /\ length plain < pow2_32 /\ length auth < pow2_32 /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          iv_enc == inc32 (compute_iv_BE h_BE iv) 1 /\ cipher == gctr_encrypt iv_enc plain alg key))
      (ensures cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth))

    iv: Vale.AES.GCM_BE_s.supported_iv_BE ->
    iv_enc: Vale.Def.Types_s.quad32 ->
    iv_BE: Vale.Def.Types_s.quad32 ->
    plain: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 ->
    auth: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 ->
    cipher: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 ->
    alg: Vale.AES.AES_common_s.algorithm ->
    key: FStar.Seq.Base.seq Vale.Def.Words_s.nat32
  -> FStar.Pervasives.Lemma
      (requires
        Vale.AES.AES_BE_s.is_aes_key_word alg key /\
        FStar.Seq.Base.length plain < Vale.Def.Words_s.pow2_32 /\
        FStar.Seq.Base.length auth < Vale.Def.Words_s.pow2_32 /\
        (let h_BE = Vale.AES.AES_BE_s.aes_encrypt_word alg key (Vale.Def.Words_s.Mkfour 0 0 0 0) in
          iv_enc == Vale.AES.GCTR_BE_s.inc32 (Vale.AES.GCM_BE_s.compute_iv_BE h_BE iv) 1 /\
          cipher == Vale.AES.GCTR_BE_s.gctr_encrypt iv_enc plain alg key))
      (ensures
        cipher ==
        FStar.Pervasives.Native.fst (Vale.AES.GCM_BE_s.gcm_encrypt_BE alg
              (Vale.Def.Words.Seq_s.seq_nat32_to_seq_nat8_BE key)
              iv
              plain
              auth))