val gf128_mul_BE (a b: quad32) : quad32
let gf128_mul_BE (a b:quad32) : quad32 =
  gf128_to_quad32 (gf128_mul (gf128_of_quad32 a) (gf128_of_quad32 b))
val gf128_mul_BE (a b: quad32) : quad32
let gf128_mul_BE (a b: quad32) : quad32 =
gf128_to_quad32 (gf128_mul (gf128_of_quad32 a) (gf128_of_quad32 b))
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.GF128_s.gf128_to_quad32 Vale.AES.GF128_s.gf128_mul Vale.AES.GF128_s.gf128_of_quad32
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 }
val gf128_mul_BE (a b: quad32) : quad32
a: Vale.Def.Types_s.quad32 -> b: Vale.Def.Types_s.quad32 -> Vale.Def.Types_s.quad32