val gcm_decrypt_LE_tag
      (alg: algorithm)
      (key: seq nat8)
      (iv: supported_iv_LE)
      (cipher auth: seq nat8)
    : Pure (seq nat8)
      (requires is_aes_key alg key /\ length cipher < pow2_32 /\ length auth < pow2_32)
      (ensures fun t -> True)
let gcm_decrypt_LE_tag (alg:algorithm) (key:seq nat8) (iv:supported_iv_LE) (cipher:seq nat8) (auth:seq nat8) :
  Pure (seq nat8)
    (requires
      is_aes_key alg key /\
      length cipher < pow2_32 /\
      length auth < pow2_32
    )
    (ensures fun t -> True)
  =
  let key_LE = seq_nat8_to_seq_nat32_LE key in
  let h_LE = aes_encrypt_LE alg key_LE (Mkfour 0 0 0 0) in
  let j0_BE = compute_iv_BE h_LE iv in

  let lengths_BE = insert_nat64 (insert_nat64 (Mkfour 0 0 0 0) (8 * length auth) 1) (8 * length cipher) 0 in
  let lengths_LE = reverse_bytes_quad32 lengths_BE in

  let zero_padded_c_LE = le_bytes_to_seq_quad32 (pad_to_128_bits cipher) in
  let zero_padded_a_LE = le_bytes_to_seq_quad32 (pad_to_128_bits auth) in

  let hash_input_LE = append zero_padded_a_LE (append zero_padded_c_LE (create 1 lengths_LE)) in
  let s_LE = ghash_LE h_LE hash_input_LE in
  let t = gctr_encrypt_LE j0_BE (le_quad32_to_bytes s_LE) alg key_LE in
  t
val gcm_decrypt_LE_tag
      (alg: algorithm)
      (key: seq nat8)
      (iv: supported_iv_LE)
      (cipher auth: seq nat8)
    : Pure (seq nat8)
      (requires is_aes_key alg key /\ length cipher < pow2_32 /\ length auth < pow2_32)
      (ensures fun t -> True)
let gcm_decrypt_LE_tag
      (alg: algorithm)
      (key: seq nat8)
      (iv: supported_iv_LE)
      (cipher auth: seq nat8)
    : Pure (seq nat8)
      (requires is_aes_key alg key /\ length cipher < pow2_32 /\ length auth < pow2_32)
      (ensures fun t -> True) =
let key_LE = seq_nat8_to_seq_nat32_LE key in
let h_LE = aes_encrypt_LE alg key_LE (Mkfour 0 0 0 0) in
let j0_BE = compute_iv_BE h_LE iv in
let lengths_BE =
  insert_nat64 (insert_nat64 (Mkfour 0 0 0 0) (8 * length auth) 1) (8 * length cipher) 0
in
let lengths_LE = reverse_bytes_quad32 lengths_BE in
let zero_padded_c_LE = le_bytes_to_seq_quad32 (pad_to_128_bits cipher) in
let zero_padded_a_LE = le_bytes_to_seq_quad32 (pad_to_128_bits auth) in
let hash_input_LE = append zero_padded_a_LE (append zero_padded_c_LE (create 1 lengths_LE)) in
let s_LE = ghash_LE h_LE hash_input_LE in
let t = gctr_encrypt_LE j0_BE (le_quad32_to_bytes s_LE) alg key_LE in
t
Vale.AES.GCM.fsti.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.Types.fsti.checked Vale.AES.GHash_s.fst.checked Vale.AES.GHash.fsti.checked Vale.AES.GCTR_s.fst.checked Vale.AES.GCTR.fsti.checked Vale.AES.GCM_s.fst.checked Vale.AES.GCM_helpers.fsti.checked Vale.AES.AES_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.fsti
Vale.AES.AES_common_s.algorithm FStar.Seq.Base.seq Vale.Def.Words_s.nat8 Vale.AES.GCM_s.supported_iv_LE Vale.AES.GCTR_s.gctr_encrypt_LE Vale.Def.Types_s.le_quad32_to_bytes Vale.Def.Types_s.quad32 Vale.AES.GHash_s.ghash_LE FStar.Seq.Base.append FStar.Seq.Base.create Vale.Def.Types_s.le_bytes_to_seq_quad32 Vale.AES.GCTR_s.pad_to_128_bits Vale.Def.Types_s.reverse_bytes_quad32 Vale.Def.Types_s.insert_nat64 Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 FStar.Mul.op_Star FStar.Seq.Base.length Vale.AES.GCM_s.compute_iv_BE Vale.AES.AES_s.aes_encrypt_LE Vale.Def.Words_s.nat32 Vale.Def.Words.Seq_s.seq_nat8_to_seq_nat32_LE Prims.l_and Vale.AES.AES_common_s.is_aes_key Prims.b2t Prims.op_LessThan Vale.Def.Words_s.pow2_32 Prims.l_True
module Vale.AES.GCM

open Vale.Def.Opaque_s
open Vale.Def.Types_s
open Vale.Arch.Types
open Vale.AES.GCM_s
open Vale.AES.AES_s
open Vale.AES.GCM_helpers
open Vale.AES.GCTR_s
open Vale.AES.GCTR
open Vale.AES.GHash_s
open FStar.Mul
open FStar.Seq
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open FStar.Calc

open Vale.Def.Words.Four_s

let set_to_one_LE (q:quad32) : quad32 = four_insert q 1 0 // Mkfour 1 q.lo1 q.hi2 q.hi3 

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

let lower3_equal (q0 q1:quad32) : bool = 
  q0.lo0 = q1.lo0 &&
  q0.lo1 = q1.lo1 &&
  q0.hi2 = q1.hi2

val lemma_compute_iv_easy (iv_b iv_extra_b:seq quad32) (iv:supported_iv_LE) (num_bytes:nat64) (h_LE 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 = reverse_bytes_quad32 (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 (le_seq_quad32_to_bytes raw_quads) 0 num_bytes in
     iv_bytes == iv))
  (ensures j0 == compute_iv_BE h_LE iv)

open Vale.AES.GHash
val lemma_compute_iv_hard (iv:supported_iv_LE) (quads:seq quad32) (length_quad h_LE j0:quad32) : Lemma
  (requires
    ~(length iv == 96/8) /\
    quads == le_bytes_to_seq_quad32 (pad_to_128_bits iv) /\
    j0 == ghash_incremental h_LE (Mkfour 0 0 0 0) (append quads (create 1 length_quad)) /\
    length_quad == reverse_bytes_quad32 (insert_nat64 
                                          (insert_nat64 
                                            (Mkfour 0 0 0 0) 0 1) 
                                        (8 * (length iv)) 0))
  (ensures reverse_bytes_quad32 j0 == compute_iv_BE h_LE iv)

val lemma_length_simplifier (s bytes t:seq quad32) (num_bytes:nat) : Lemma
  (requires t == (if num_bytes > (length s) * 16 then append s bytes else s) /\
            (num_bytes <= (length s) * 16 ==> num_bytes == (length s * 16)) /\
            length s * 16 <= num_bytes /\
            num_bytes < length s * 16 + 16 /\
            length bytes == 1
            )
  (ensures slice (le_seq_quad32_to_bytes t) 0 num_bytes ==
           slice (le_seq_quad32_to_bytes (append s bytes)) 0 num_bytes)

val gcm_blocks_helper_simplified (alg:algorithm) (key:seq nat32)
                   (a128 a_bytes p128x6 p128 p_bytes c128x6 c128 c_bytes:seq quad32)
                   (p_num_bytes a_num_bytes:nat)
                   (iv:supported_iv_LE) (j0_BE h enc_hash length_quad:quad32) : Lemma
  (requires // Required by gcm_blocks
           length p128x6 * 16 + length p128 * 16 <= p_num_bytes /\
           p_num_bytes < length p128x6 * 16 + length p128 * 16 + 16 /\
           length a128 * 16 <= a_num_bytes /\
           a_num_bytes < length a128 * 16 + 16 /\
           a_num_bytes < pow2_32 /\
           length p128x6 == length c128x6 /\
           length p128 == length c128 /\
           length p_bytes == 1 /\
           length c_bytes == 1 /\
           length a_bytes == 1 /\
           is_aes_key_LE alg key /\
           j0_BE == compute_iv_BE h iv /\
           h = aes_encrypt_LE alg key (Mkfour 0 0 0 0) /\

           // Ensured by gcm_blocks
           p_num_bytes < pow2_32 /\ a_num_bytes < pow2_32 /\
           length_quad == reverse_bytes_quad32
             (insert_nat64 (insert_nat64 (Mkfour 0 0 0 0) (8 * a_num_bytes) 1) (8 * p_num_bytes) 0) /\
          (let ctr_BE_1:quad32 = j0_BE in
           let ctr_BE_2:quad32 = inc32 j0_BE 1 in
           let plain:seq quad32 =
             if p_num_bytes > (length p128x6 + length p128) * 16 then
               append (append p128x6 p128) p_bytes
             else
               append p128x6 p128
           in
           let cipher:seq quad32 =
             if p_num_bytes > (length p128x6 + length p128) * 16 then
               append (append c128x6 c128) c_bytes
             else
               append c128x6 c128
           in
           let cipher_bound:nat = length p128x6 + length p128 +
             (if p_num_bytes > (length p128x6 + length p128) * 16 then 1 else 0)
           in
           gctr_partial alg cipher_bound plain cipher key ctr_BE_2 /\

          (let auth_raw_quads =
             if a_num_bytes > (length a128) * 16 then append a128 a_bytes else a128
           in

           let auth_input_bytes = slice (le_seq_quad32_to_bytes auth_raw_quads) 0 a_num_bytes in
           let auth_padded_bytes = pad_to_128_bits auth_input_bytes in
           let auth_quads = le_bytes_to_seq_quad32 auth_padded_bytes in

           let raw_quads = append (append auth_quads c128x6) c128 in
           let total_bytes = (length auth_quads) * 16 + p_num_bytes in
           let raw_quads =
             if p_num_bytes > (length p128x6 + length p128) * 16 then
               let raw_quads = append raw_quads c_bytes in
               let input_bytes = slice (le_seq_quad32_to_bytes raw_quads) 0 total_bytes in
               let input_padded_bytes = pad_to_128_bits input_bytes in
               le_bytes_to_seq_quad32 input_padded_bytes
             else
               raw_quads
           in
           let final_quads = append raw_quads (create 1 length_quad) in
           enc_hash == gctr_encrypt_block ctr_BE_1 (ghash_LE h final_quads) alg key 0
           )))
  (ensures (let auth_raw_quads = append a128 a_bytes in
           let auth_bytes = slice (le_seq_quad32_to_bytes auth_raw_quads) 0 a_num_bytes in
           let plain_raw_quads = append (append p128x6 p128) p_bytes in
           let plain_bytes = slice (le_seq_quad32_to_bytes plain_raw_quads) 0 p_num_bytes in
           let cipher_raw_quads = append (append c128x6 c128) c_bytes in
           let cipher_bytes = slice (le_seq_quad32_to_bytes cipher_raw_quads) 0 p_num_bytes in

           length auth_bytes < pow2_32 /\
           length plain_bytes < pow2_32 /\

           cipher_bytes == fst (gcm_encrypt_LE alg (seq_nat32_to_seq_nat8_LE key) iv plain_bytes auth_bytes) /\
           le_quad32_to_bytes enc_hash ==
             snd (gcm_encrypt_LE alg (seq_nat32_to_seq_nat8_LE key)
                                 iv plain_bytes auth_bytes))

  )

val lemma_gcm_encrypt_decrypt_equiv (alg:algorithm) (key:seq nat32) (iv:supported_iv_LE) (j0_BE:quad32) (plain cipher auth alleged_tag:seq nat8) : Lemma
  (requires
    is_aes_key_LE alg key /\
   (let h_LE = aes_encrypt_LE alg key (Mkfour 0 0 0 0) in
    j0_BE = compute_iv_BE h_LE iv) /\
    length cipher < pow2_32 /\
    length auth < pow2_32 /\
    plain == fst (gcm_encrypt_LE alg (seq_nat32_to_seq_nat8_LE key) iv cipher auth)
  )
  (ensures plain == fst (gcm_decrypt_LE alg (seq_nat32_to_seq_nat8_LE key) iv cipher auth alleged_tag))

val gcm_blocks_helper_dec_simplified (alg:algorithm) (key:seq nat32)
                   (p128x6 p128 p_bytes c128x6 c128 c_bytes:seq quad32)
                   (auth_bytes alleged_tag:seq nat8)
                   (p_num_bytes:nat)
                   (iv:supported_iv_LE) (j0_BE:quad32) : Lemma
  (requires // Required by gcm_blocks
           length p128x6 * 16 + length p128 * 16 <= p_num_bytes /\
           p_num_bytes < length p128x6 * 16 + length p128 * 16 + 16 /\
           length p128x6 == length c128x6 /\
           length p128 == length c128 /\
           length p_bytes == 1 /\
           length c_bytes == 1 /\
           (length auth_bytes) < pow2_32 /\
           is_aes_key_LE alg key /\
          (let h_LE = aes_encrypt_LE alg key (Mkfour 0 0 0 0) in
           j0_BE = compute_iv_BE h_LE 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 p128x6 + length p128) * 16 then
               append (append p128x6 p128) p_bytes
             else
               append p128x6 p128
           in
           let cipher:seq quad32 =
             if p_num_bytes > (length p128x6 + length p128) * 16 then
               append (append c128x6 c128) c_bytes
             else
               append c128x6 c128
           in
           let cipher_bound:nat = length p128x6 + length p128 +
             (if p_num_bytes > (length p128x6 + length p128) * 16 then 1 else 0)
           in
           gctr_partial alg cipher_bound plain cipher key ctr_BE_2
           ))
  (ensures (let plain_raw_quads = append (append p128x6 p128) p_bytes in
           let plain_bytes = slice (le_seq_quad32_to_bytes plain_raw_quads) 0 p_num_bytes in
           let cipher_raw_quads = append (append c128x6 c128) c_bytes in
           let cipher_bytes = slice (le_seq_quad32_to_bytes cipher_raw_quads) 0 p_num_bytes in

           length auth_bytes < pow2_32 /\
           length plain_bytes < pow2_32 /\

           cipher_bytes == fst (gcm_decrypt_LE alg (seq_nat32_to_seq_nat8_LE key) iv plain_bytes auth_bytes alleged_tag)))
           

let gcm_decrypt_LE_tag (alg:algorithm) (key:seq nat8) (iv:supported_iv_LE) (cipher:seq nat8) (auth:seq nat8) :
  Pure (seq nat8)
    (requires
      is_aes_key alg key /\
      length cipher < pow2_32 /\
      length auth < pow2_32
    )
val gcm_decrypt_LE_tag
      (alg: algorithm)
      (key: seq nat8)
      (iv: supported_iv_LE)
      (cipher auth: seq nat8)
    : Pure (seq nat8)
      (requires is_aes_key alg key /\ length cipher < pow2_32 /\ length auth < pow2_32)
      (ensures fun t -> True)

    alg: Vale.AES.AES_common_s.algorithm ->
    key: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 ->
    iv: Vale.AES.GCM_s.supported_iv_LE ->
    cipher: FStar.Seq.Base.seq Vale.Def.Words_s.nat8 ->
    auth: FStar.Seq.Base.seq Vale.Def.Words_s.nat8
  -> Prims.Pure (FStar.Seq.Base.seq Vale.Def.Words_s.nat8)