let compute_iv_BE_reveal = opaque_revealer (`%compute_iv_BE) compute_iv_BE compute_iv_BE_def
let compute_iv_BE_reveal =
opaque_revealer (`%compute_iv_BE) compute_iv_BE compute_iv_BE_def
Vale.AES.GCM_s.fst.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.AES.GHash_s.fst.checked Vale.AES.GCTR_s.fst.checked Vale.AES.AES_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.GCM_s.fst
Vale.Def.Opaque_s.opaque_revealer Vale.Def.Types_s.quad32 Vale.AES.GCM_s.supported_iv_LE Vale.AES.GCM_s.compute_iv_BE Vale.AES.GCM_s.compute_iv_BE_def
module Vale.AES.GCM_s

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Types_s
open Vale.AES.AES_s
open Vale.AES.GCTR_s
open Vale.AES.GHash_s
open FStar.Seq
open FStar.Mul

unfold type gcm_plain_LE = gctr_plain_LE
unfold type gcm_auth_LE = gctr_plain_LE

#reset-options "--z3rlimit 30"

type supported_iv_LE:eqtype = iv:seq nat8 { 1 <= 8 * (length iv) /\ 8 * (length iv) < pow2_64 }

let compute_iv_BE_def (h_LE:quad32) (iv:supported_iv_LE) : quad32
  =
  if 8 * (length iv) = 96 then (
    let iv_LE = le_bytes_to_quad32 (pad_to_128_bits iv) in
    let iv_BE = reverse_bytes_quad32 iv_LE in
    let j0_BE = Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3 in
    j0_BE
  ) else (
    let padded_iv_quads = le_bytes_to_seq_quad32 (pad_to_128_bits iv) in
    let length_BE = insert_nat64_def (Mkfour 0 0 0 0) (8 * length iv) 0 in
    let length_LE = reverse_bytes_quad32 length_BE in
    let hash_input_LE = append padded_iv_quads (create 1 length_LE) in
    let hash_output_LE = ghash_LE h_LE hash_input_LE in
    reverse_bytes_quad32 hash_output_LE
  )
val compute_iv_BE_reveal : _: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.GCM_s.compute_iv_BE == Vale.AES.GCM_s.compute_iv_BE_def)
_: Prims.unit
  -> FStar.Pervasives.Lemma
    (ensures Vale.AES.GCM_s.compute_iv_BE == Vale.AES.GCM_s.compute_iv_BE_def)