val ghash_BE_def (h_BE: quad32) (x: ghash_plain_BE) : Tot quad32 (decreases %[length x])
let rec ghash_BE_def (h_BE:quad32) (x:ghash_plain_BE) : Tot quad32 (decreases %[length x]) =
  let y_i_minus_1 =
    (if length x = 1 then
       Mkfour 0 0 0 0
     else
       ghash_BE_def h_BE (all_but_last x)) in
  let x_i = last x in
  let xor_BE = quad32_xor y_i_minus_1 x_i in
  gf128_mul_BE xor_BE h_BE
val ghash_BE_def (h_BE: quad32) (x: ghash_plain_BE) : Tot quad32 (decreases %[length x])
let rec ghash_BE_def (h_BE: quad32) (x: ghash_plain_BE) : Tot quad32 (decreases %[length x]) =
let y_i_minus_1 = (if length x = 1 then Mkfour 0 0 0 0 else ghash_BE_def h_BE (all_but_last x)) in
let x_i = last x in
let xor_BE = quad32_xor y_i_minus_1 x_i in
gf128_mul_BE xor_BE h_BE
Vale.AES.GHash_BE_s.fst.checked
Vale.Lib.Seqs_s.fst.checked Vale.Def.Words_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.AES.GF128_s.fsti.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.GHash_BE_s.fst
Vale.Def.Types_s.quad32 Vale.AES.GHash_BE_s.ghash_plain_BE Vale.AES.GHash_BE_s.gf128_mul_BE Vale.Def.Types_s.quad32_xor FStar.Seq.Properties.last Prims.op_Equality Prims.int FStar.Seq.Base.length Vale.Def.Words_s.Mkfour Vale.Def.Types_s.nat32 Prims.bool Vale.AES.GHash_BE_s.ghash_BE_def Vale.Lib.Seqs_s.all_but_last
module Vale.AES.GHash_BE_s

open Vale.Def.Opaque_s
open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.AES.GF128_s
open Vale.Lib.Seqs_s
open FStar.Mul
open FStar.Seq

type ghash_plain_BE:eqtype = s:seq quad32 { length s > 0 }

let gf128_mul_BE (a b:quad32) : quad32 =
  gf128_to_quad32 (gf128_mul (gf128_of_quad32 a) (gf128_of_quad32 b))
val ghash_BE_def (h_BE: quad32) (x: ghash_plain_BE) : Tot quad32 (decreases %[length x])
h_BE: Vale.Def.Types_s.quad32 -> x: Vale.AES.GHash_BE_s.ghash_plain_BE
  -> Prims.Tot Vale.Def.Types_s.quad32