val compute_iv_BE_def (h_BE: quad32) (iv: supported_iv_BE) : quad32
let compute_iv_BE_def (h_BE:quad32) (iv:supported_iv_BE) : quad32
  =
  if 8 * (length iv) = 96 then (
    let iv_BE = be_bytes_to_quad32 (pad_to_128_bits iv) in
    let j0_BE = Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3 in
    j0_BE
  ) else (
    let padded_iv_quads = be_bytes_to_seq_quad32 (pad_to_128_bits iv) in
    let length_BE = two_two_to_four (Mktwo (nat_to_two 32 0) (nat_to_two 32 (8 * length iv))) in
    let hash_input_BE = append padded_iv_quads (create 1 length_BE) in
    let hash_output_BE = ghash_BE h_BE hash_input_BE in
    hash_output_BE
  )
val compute_iv_BE_def (h_BE: quad32) (iv: supported_iv_BE) : quad32
let compute_iv_BE_def (h_BE: quad32) (iv: supported_iv_BE) : quad32 =
if 8 * (length iv) = 96
then
  (let iv_BE = be_bytes_to_quad32 (pad_to_128_bits iv) in
    let j0_BE = Mkfour 1 iv_BE.lo1 iv_BE.hi2 iv_BE.hi3 in
    j0_BE)
else
  (let padded_iv_quads = be_bytes_to_seq_quad32 (pad_to_128_bits iv) in
    let length_BE = two_two_to_four (Mktwo (nat_to_two 32 0) (nat_to_two 32 (8 * length iv))) in
    let hash_input_BE = append padded_iv_quads (create 1 length_BE) in
    let hash_output_BE = ghash_BE h_BE hash_input_BE in
    hash_output_BE)
Vale.AES.GCM_BE_s.fst.checked
Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_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_BE_s.fst.checked Vale.AES.GCTR_BE_s.fst.checked Vale.AES.AES_BE_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_BE_s.fst
Vale.Def.Types_s.quad32 Vale.AES.GCM_BE_s.supported_iv_BE Prims.op_Equality Prims.int FStar.Mul.op_Star FStar.Seq.Base.length Vale.Def.Types_s.nat8 Vale.Def.Words_s.four Vale.Def.Words_s.nat32 Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 Vale.Def.Words_s.__proj__Mkfour__item__lo1 Vale.Def.Words_s.__proj__Mkfour__item__hi2 Vale.Def.Words_s.__proj__Mkfour__item__hi3 Vale.Def.Types_s.be_bytes_to_quad32 Vale.AES.GCTR_BE_s.pad_to_128_bits Prims.bool Vale.AES.GHash_BE_s.ghash_BE FStar.Seq.Base.seq FStar.Seq.Base.append FStar.Seq.Base.create Vale.Def.Words_s.natN Prims.pow2 Vale.Def.Words.Four_s.two_two_to_four Vale.Def.Words_s.Mktwo Vale.Def.Words_s.two Vale.Def.Words.Two_s.nat_to_two Vale.Def.Types_s.be_bytes_to_seq_quad32
module Vale.AES.GCM_BE_s

open Vale.Arch.Types
open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.AES.AES_BE_s
open Vale.AES.GCTR_BE_s
open Vale.AES.GHash_BE_s
open FStar.Seq
open FStar.Mul

#reset-options "--z3rlimit 30"

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

let compute_iv_BE_def (h_BE:quad32) (iv:supported_iv_BE) : quad32
val compute_iv_BE_def (h_BE: quad32) (iv: supported_iv_BE) : quad32
h_BE: Vale.Def.Types_s.quad32 -> iv: Vale.AES.GCM_BE_s.supported_iv_BE -> Vale.Def.Types_s.quad32