val gcm_blocks_helper_enc
      (alg: algorithm)
      (key: seq nat32)
      (p128 p_bytes c128 c_bytes: seq quad32)
      (auth_bytes: seq nat8)
      (p_num_bytes: nat)
      (iv: supported_iv_BE)
      (j0_BE: quad32)
    : Lemma
      (requires
        length p128 * 16 <= p_num_bytes /\ p_num_bytes < length p128 * 16 + 16 /\
        length p128 == length c128 /\ length p_bytes == 1 /\ length c_bytes == 1 /\
        (length auth_bytes) < pow2_32 /\ is_aes_key_word alg key /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          j0_BE = compute_iv_BE h_BE iv /\ p_num_bytes < pow2_32 /\
          (let ctr_BE_2:quad32 = inc32 j0_BE 1 in
            let plain:seq quad32 =
              if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
            in
            let cipher:seq quad32 =
              if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
            in
            let cipher_bound:nat =
              length p128 + (if p_num_bytes > length p128 * 16 then 1 else 0)
            in
            gctr_partial alg cipher_bound plain cipher key ctr_BE_2)))
      (ensures
        (let plain:seq quad32 =
            if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
          in
          let cipher:seq quad32 =
            if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
          in
          let ctr_BE_2:quad32 = inc32 j0_BE 1 in
          let plain_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes
          in
          let cipher_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes
          in
          cipher_bytes ==
          fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain_bytes auth_bytes)))
let gcm_blocks_helper_enc (alg:algorithm) (key:seq nat32)
                   (p128 p_bytes c128 c_bytes:seq quad32)
                   (auth_bytes:seq nat8)
                   (p_num_bytes:nat)
                   (iv:supported_iv_BE) (j0_BE:quad32) : Lemma
  (requires // Required by gcm_blocks
           length p128 * 16 <= p_num_bytes /\
           p_num_bytes < length p128 * 16 + 16 /\
           length p128 == length c128 /\
           length p_bytes == 1 /\
           length c_bytes == 1 /\
           (length auth_bytes) < pow2_32 /\
           is_aes_key_word alg key /\
          (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
           j0_BE = compute_iv_BE h_BE iv /\

           // Ensured by gcm_blocks
           p_num_bytes < pow2_32 /\
          (let ctr_BE_2:quad32 = inc32 j0_BE 1 in
           let plain:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append p128 p_bytes
             else
               p128
           in
           let cipher:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append c128 c_bytes
             else
               c128
           in
           let cipher_bound:nat = length p128 +
             (if p_num_bytes > length p128 * 16 then 1 else 0)
           in
           gctr_partial alg cipher_bound plain cipher key ctr_BE_2
           )))
  (ensures (let plain:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append p128 p_bytes
             else
               p128
           in
           let cipher:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append c128 c_bytes
             else
               c128
           in
           let ctr_BE_2:quad32 = inc32 j0_BE 1 in
           let plain_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes in
           let cipher_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes in
           //cipher_bytes == gctr_encrypt ctr_BE_2 plain_bytes alg key))
           cipher_bytes == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain_bytes auth_bytes)))
  =
  let ctr_BE_2:quad32 = inc32 j0_BE 1 in
  let plain:seq quad32 =
    if p_num_bytes > length p128 * 16 then
       append p128 p_bytes
    else
      p128
  in
  let cipher:seq quad32 =
    if p_num_bytes > length p128 * 16 then
       append c128 c_bytes
    else
      c128
  in
  let cipher_bound:nat = length p128 +
    (if p_num_bytes > length p128 * 16 then 1 else 0)
  in
  let plain_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes in
  let cipher_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes in
  gctr_partial_opaque_completed alg plain cipher key ctr_BE_2;
  if p_num_bytes > length p128 * 16 then (
    gctr_partial_reveal ();
    assert (gctr_partial alg (length p128) plain cipher key ctr_BE_2);
    assert (equal (slice plain 0 (length p128))
                  (slice p128 0 (length p128)));
    assert (equal (slice cipher 0 (length p128))
                  (slice c128 0 (length p128)));
    gctr_partial_opaque_ignores_postfix
      alg (length p128)
      plain p128
      cipher c128
      key ctr_BE_2;
    assert (gctr_partial alg (length p128) p128 c128 key ctr_BE_2);
    gctr_partial_opaque_completed alg p128 c128 key ctr_BE_2;
    let num_blocks = p_num_bytes / 16 in
    assert(index cipher num_blocks == quad32_xor (index plain num_blocks) (aes_encrypt_word alg key (inc32 ctr_BE_2 num_blocks)));
    gctr_encrypt_block_offset ctr_BE_2 (index plain num_blocks) alg key num_blocks;
    assert( gctr_encrypt_block ctr_BE_2 (index plain num_blocks) alg key num_blocks ==
            gctr_encrypt_block (inc32 ctr_BE_2 num_blocks) (index plain num_blocks) alg key 0);
    aes_encrypt_word_reveal ();
    gctr_partial_to_full_advanced ctr_BE_2 plain cipher alg key p_num_bytes;
    assert (cipher_bytes == gctr_encrypt ctr_BE_2 plain_bytes alg key)
  ) else (
    gctr_partial_to_full_basic ctr_BE_2 plain alg key cipher;
    assert (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher) == gctr_encrypt ctr_BE_2 (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) alg key);
    let plain_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes in
    let cipher_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes in
    assert (equal plain_bytes (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)));
    assert (equal cipher_bytes (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)));
    assert (cipher_bytes == gctr_encrypt ctr_BE_2 plain_bytes alg key)
  );
  gcm_encrypt_BE_fst_helper iv ctr_BE_2 j0_BE plain_bytes auth_bytes cipher_bytes alg key;
  ()
val gcm_blocks_helper_enc
      (alg: algorithm)
      (key: seq nat32)
      (p128 p_bytes c128 c_bytes: seq quad32)
      (auth_bytes: seq nat8)
      (p_num_bytes: nat)
      (iv: supported_iv_BE)
      (j0_BE: quad32)
    : Lemma
      (requires
        length p128 * 16 <= p_num_bytes /\ p_num_bytes < length p128 * 16 + 16 /\
        length p128 == length c128 /\ length p_bytes == 1 /\ length c_bytes == 1 /\
        (length auth_bytes) < pow2_32 /\ is_aes_key_word alg key /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          j0_BE = compute_iv_BE h_BE iv /\ p_num_bytes < pow2_32 /\
          (let ctr_BE_2:quad32 = inc32 j0_BE 1 in
            let plain:seq quad32 =
              if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
            in
            let cipher:seq quad32 =
              if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
            in
            let cipher_bound:nat =
              length p128 + (if p_num_bytes > length p128 * 16 then 1 else 0)
            in
            gctr_partial alg cipher_bound plain cipher key ctr_BE_2)))
      (ensures
        (let plain:seq quad32 =
            if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
          in
          let cipher:seq quad32 =
            if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
          in
          let ctr_BE_2:quad32 = inc32 j0_BE 1 in
          let plain_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes
          in
          let cipher_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes
          in
          cipher_bytes ==
          fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain_bytes auth_bytes)))
let gcm_blocks_helper_enc
      (alg: algorithm)
      (key: seq nat32)
      (p128 p_bytes c128 c_bytes: seq quad32)
      (auth_bytes: seq nat8)
      (p_num_bytes: nat)
      (iv: supported_iv_BE)
      (j0_BE: quad32)
    : Lemma
      (requires
        length p128 * 16 <= p_num_bytes /\ p_num_bytes < length p128 * 16 + 16 /\
        length p128 == length c128 /\ length p_bytes == 1 /\ length c_bytes == 1 /\
        (length auth_bytes) < pow2_32 /\ is_aes_key_word alg key /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          j0_BE = compute_iv_BE h_BE iv /\ p_num_bytes < pow2_32 /\
          (let ctr_BE_2:quad32 = inc32 j0_BE 1 in
            let plain:seq quad32 =
              if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
            in
            let cipher:seq quad32 =
              if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
            in
            let cipher_bound:nat =
              length p128 + (if p_num_bytes > length p128 * 16 then 1 else 0)
            in
            gctr_partial alg cipher_bound plain cipher key ctr_BE_2)))
      (ensures
        (let plain:seq quad32 =
            if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
          in
          let cipher:seq quad32 =
            if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
          in
          let ctr_BE_2:quad32 = inc32 j0_BE 1 in
          let plain_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes
          in
          let cipher_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes
          in
          cipher_bytes ==
          fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain_bytes auth_bytes))) =
let ctr_BE_2:quad32 = inc32 j0_BE 1 in
let plain:seq quad32 = if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128 in
let cipher:seq quad32 = if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128 in
let cipher_bound:nat = length p128 + (if p_num_bytes > length p128 * 16 then 1 else 0) in
let plain_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes in
let cipher_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes in
gctr_partial_opaque_completed alg plain cipher key ctr_BE_2;
if p_num_bytes > length p128 * 16
then
  (gctr_partial_reveal ();
    assert (gctr_partial alg (length p128) plain cipher key ctr_BE_2);
    assert (equal (slice plain 0 (length p128)) (slice p128 0 (length p128)));
    assert (equal (slice cipher 0 (length p128)) (slice c128 0 (length p128)));
    gctr_partial_opaque_ignores_postfix alg (length p128) plain p128 cipher c128 key ctr_BE_2;
    assert (gctr_partial alg (length p128) p128 c128 key ctr_BE_2);
    gctr_partial_opaque_completed alg p128 c128 key ctr_BE_2;
    let num_blocks = p_num_bytes / 16 in
    assert (index cipher num_blocks ==
        quad32_xor (index plain num_blocks) (aes_encrypt_word alg key (inc32 ctr_BE_2 num_blocks)));
    gctr_encrypt_block_offset ctr_BE_2 (index plain num_blocks) alg key num_blocks;
    assert (gctr_encrypt_block ctr_BE_2 (index plain num_blocks) alg key num_blocks ==
        gctr_encrypt_block (inc32 ctr_BE_2 num_blocks) (index plain num_blocks) alg key 0);
    aes_encrypt_word_reveal ();
    gctr_partial_to_full_advanced ctr_BE_2 plain cipher alg key p_num_bytes;
    assert (cipher_bytes == gctr_encrypt ctr_BE_2 plain_bytes alg key))
else
  (gctr_partial_to_full_basic ctr_BE_2 plain alg key cipher;
    assert (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher) ==
        gctr_encrypt ctr_BE_2 (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) alg key);
    let plain_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes in
    let cipher_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes in
    assert (equal plain_bytes (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)));
    assert (equal cipher_bytes (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)));
    assert (cipher_bytes == gctr_encrypt ctr_BE_2 plain_bytes alg key));
gcm_encrypt_BE_fst_helper iv ctr_BE_2 j0_BE plain_bytes auth_bytes cipher_bytes alg key;
()
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.AES_common_s.algorithm FStar.Seq.Base.seq Vale.Def.Words_s.nat32 Vale.Def.Types_s.quad32 Vale.Def.Words_s.nat8 Prims.nat Vale.AES.GCM_BE_s.supported_iv_BE Prims.unit Vale.AES.GCM_BE.gcm_encrypt_BE_fst_helper Prims.op_GreaterThan FStar.Mul.op_Star FStar.Seq.Base.length Prims._assert Prims.eq2 Vale.AES.GCTR_BE_s.gctr_encrypt Vale.AES.GCTR_BE.gctr_partial_to_full_advanced Vale.AES.AES_BE_s.aes_encrypt_word_reveal Vale.AES.GCTR_BE_s.gctr_encrypt_block FStar.Seq.Base.index Vale.AES.GCTR_BE_s.inc32 Vale.AES.GCTR_BE.gctr_encrypt_block_offset Vale.Def.Types_s.quad32_xor Vale.AES.AES_BE_s.aes_encrypt_word Prims.int Prims.op_Division Vale.AES.GCTR_BE.gctr_partial_opaque_completed Vale.AES.GCTR_BE.gctr_partial Vale.AES.GCTR_BE.gctr_partial_opaque_ignores_postfix FStar.Seq.Base.equal FStar.Seq.Base.slice Vale.AES.GCTR_BE.gctr_partial_reveal Prims.bool Vale.Def.Types_s.nat8 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.AES.GCTR_BE.gctr_partial_to_full_basic Prims.op_Addition FStar.Seq.Base.append Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan Vale.Def.Words_s.pow2_32 Vale.AES.AES_BE_s.is_aes_key_word Prims.op_Equality Vale.AES.GCM_BE_s.compute_iv_BE Vale.Def.Words_s.Mkfour Prims.squash FStar.Pervasives.Native.fst Vale.AES.GCM_BE_s.gcm_encrypt_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))
  =
  gcm_encrypt_BE_reveal ()

let gcm_encrypt_BE_snd_helper (iv:supported_iv_BE) (j0_BE length_quad32 hash mac: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
    j0_BE = compute_iv_BE h_BE iv /\
    cipher == fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth) /\
    length_quad32 == two_two_to_four (Mktwo (nat_to_two 32 (8 * length auth)) (nat_to_two 32 (8 * length plain))) /\
    (let auth_padded_quads = be_bytes_to_seq_quad32 (pad_to_128_bits auth) in
     let cipher_padded_quads = be_bytes_to_seq_quad32 (pad_to_128_bits cipher) in
     hash == ghash_BE h_BE (append auth_padded_quads (append cipher_padded_quads (create 1 length_quad32))) /\
     be_quad32_to_bytes mac == gctr_encrypt j0_BE (be_quad32_to_bytes hash) alg key)
  ))
  (ensures be_quad32_to_bytes mac == snd (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain auth))
  =
  gcm_encrypt_BE_reveal ()

#reset-options "--z3rlimit 10"
let gcm_blocks_helper_enc (alg:algorithm) (key:seq nat32)
                   (p128 p_bytes c128 c_bytes:seq quad32)
                   (auth_bytes:seq nat8)
                   (p_num_bytes:nat)
                   (iv:supported_iv_BE) (j0_BE:quad32) : Lemma
  (requires // Required by gcm_blocks
           length p128 * 16 <= p_num_bytes /\
           p_num_bytes < length p128 * 16 + 16 /\
           length p128 == length c128 /\
           length p_bytes == 1 /\
           length c_bytes == 1 /\
           (length auth_bytes) < pow2_32 /\
           is_aes_key_word alg key /\
          (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
           j0_BE = compute_iv_BE h_BE iv /\

           // Ensured by gcm_blocks
           p_num_bytes < pow2_32 /\
          (let ctr_BE_2:quad32 = inc32 j0_BE 1 in
           let plain:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append p128 p_bytes
             else
               p128
           in
           let cipher:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append c128 c_bytes
             else
               c128
           in
           let cipher_bound:nat = length p128 +
             (if p_num_bytes > length p128 * 16 then 1 else 0)
           in
           gctr_partial alg cipher_bound plain cipher key ctr_BE_2
           )))
  (ensures (let plain:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append p128 p_bytes
             else
               p128
           in
           let cipher:seq quad32 =
             if p_num_bytes > length p128 * 16 then
               append c128 c_bytes
             else
               c128
           in
           let ctr_BE_2:quad32 = inc32 j0_BE 1 in
           let plain_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes in
           let cipher_bytes = slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes in
           //cipher_bytes == gctr_encrypt ctr_BE_2 plain_bytes alg key))
val gcm_blocks_helper_enc
      (alg: algorithm)
      (key: seq nat32)
      (p128 p_bytes c128 c_bytes: seq quad32)
      (auth_bytes: seq nat8)
      (p_num_bytes: nat)
      (iv: supported_iv_BE)
      (j0_BE: quad32)
    : Lemma
      (requires
        length p128 * 16 <= p_num_bytes /\ p_num_bytes < length p128 * 16 + 16 /\
        length p128 == length c128 /\ length p_bytes == 1 /\ length c_bytes == 1 /\
        (length auth_bytes) < pow2_32 /\ is_aes_key_word alg key /\
        (let h_BE = aes_encrypt_word alg key (Mkfour 0 0 0 0) in
          j0_BE = compute_iv_BE h_BE iv /\ p_num_bytes < pow2_32 /\
          (let ctr_BE_2:quad32 = inc32 j0_BE 1 in
            let plain:seq quad32 =
              if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
            in
            let cipher:seq quad32 =
              if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
            in
            let cipher_bound:nat =
              length p128 + (if p_num_bytes > length p128 * 16 then 1 else 0)
            in
            gctr_partial alg cipher_bound plain cipher key ctr_BE_2)))
      (ensures
        (let plain:seq quad32 =
            if p_num_bytes > length p128 * 16 then append p128 p_bytes else p128
          in
          let cipher:seq quad32 =
            if p_num_bytes > length p128 * 16 then append c128 c_bytes else c128
          in
          let ctr_BE_2:quad32 = inc32 j0_BE 1 in
          let plain_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE plain)) 0 p_num_bytes
          in
          let cipher_bytes =
            slice (seq_nat32_to_seq_nat8_BE (seq_four_to_seq_BE cipher)) 0 p_num_bytes
          in
          cipher_bytes ==
          fst (gcm_encrypt_BE alg (seq_nat32_to_seq_nat8_BE key) iv plain_bytes auth_bytes)))

    alg: Vale.AES.AES_common_s.algorithm ->
    key: FStar.Seq.Base.seq Vale.Def.Words_s.nat32 ->
    p128: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    p_bytes: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    c128: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    c_bytes: FStar.Seq.Base.seq Vale.Def.Types_s.quad32 ->
    auth_bytes: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 ->
    p_num_bytes: Prims.nat ->
    iv: Vale.AES.GCM_BE_s.supported_iv_BE ->
    j0_BE: Vale.Def.Types_s.quad32
  -> FStar.Pervasives.Lemma
      (requires
        FStar.Seq.Base.length p128 * 16 <= p_num_bytes /\
        p_num_bytes < FStar.Seq.Base.length p128 * 16 + 16 /\
        FStar.Seq.Base.length p128 == FStar.Seq.Base.length c128 /\
        FStar.Seq.Base.length p_bytes == 1 /\ FStar.Seq.Base.length c_bytes == 1 /\
        FStar.Seq.Base.length auth_bytes < Vale.Def.Words_s.pow2_32 /\
        Vale.AES.AES_BE_s.is_aes_key_word alg key /\
        (let h_BE = Vale.AES.AES_BE_s.aes_encrypt_word alg key (Vale.Def.Words_s.Mkfour 0 0 0 0) in
          j0_BE = Vale.AES.GCM_BE_s.compute_iv_BE h_BE iv /\ p_num_bytes < Vale.Def.Words_s.pow2_32 /\
          (let ctr_BE_2 = Vale.AES.GCTR_BE_s.inc32 j0_BE 1 in
            let plain =
              (match p_num_bytes > FStar.Seq.Base.length p128 * 16 with
                | true -> FStar.Seq.Base.append p128 p_bytes
                | _ -> p128)
              <:
              FStar.Seq.Base.seq Vale.Def.Types_s.quad32
            in
            let cipher =
              (match p_num_bytes > FStar.Seq.Base.length p128 * 16 with
                | true -> FStar.Seq.Base.append c128 c_bytes
                | _ -> c128)
              <:
              FStar.Seq.Base.seq Vale.Def.Types_s.quad32
            in
            let cipher_bound =
              FStar.Seq.Base.length p128 +
              (match p_num_bytes > FStar.Seq.Base.length p128 * 16 with
                | true -> 1
                | _ -> 0)
            in
            Vale.AES.GCTR_BE.gctr_partial alg cipher_bound plain cipher key ctr_BE_2)))
      (ensures
        (let plain =
            (match p_num_bytes > FStar.Seq.Base.length p128 * 16 with
              | true -> FStar.Seq.Base.append p128 p_bytes
              | _ -> p128)
            <:
            FStar.Seq.Base.seq Vale.Def.Types_s.quad32
          in
          let cipher =
            (match p_num_bytes > FStar.Seq.Base.length p128 * 16 with
              | true -> FStar.Seq.Base.append c128 c_bytes
              | _ -> c128)
            <:
            FStar.Seq.Base.seq Vale.Def.Types_s.quad32
          in
          let ctr_BE_2 = Vale.AES.GCTR_BE_s.inc32 j0_BE 1 in
          let plain_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
                      plain))
              0
              p_num_bytes
          in
          let cipher_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
                      cipher))
              0
              p_num_bytes
          in
          cipher_bytes ==
          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_bytes
                auth_bytes)))