val gf128_to_quad32 (a: poly) : quad32
let gf128_to_quad32 (a:poly) : quad32 = to_quad32 (reverse a 127)
val gf128_to_quad32 (a: poly) : quad32
let gf128_to_quad32 (a: poly) : quad32 =
to_quad32 (reverse a 127)
Vale.AES.GF128_s.fsti.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Def.Types_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.AES.GF128_s.fsti
Vale.Math.Poly2_s.poly Vale.Math.Poly2.Bits_s.to_quad32 Vale.Math.Poly2_s.reverse Vale.Def.Types_s.quad32
module Vale.AES.GF128_s
open FStar.Mul
open Vale.Math.Poly2_s
open Vale.Math.Poly2.Bits_s
open FStar.Seq
open Vale.Def.Types_s

// x^7 + x^2 + x + 1
let gf128_modulus_low_terms : poly = of_fun 8 (fun (i:nat) -> i = 0 || i = 1 || i = 2 || i = 7)

// x^128 + x^7 + x^2 + x + 1
let gf128_modulus : poly = add (monomial 128) gf128_modulus_low_terms

let gf128_add (a b:poly) : poly = add a b
let gf128_mul (a b:poly) : poly = mod (mul a b) gf128_modulus
val gf128_to_quad32 (a: poly) : quad32
a: Vale.Math.Poly2_s.poly -> Vale.Def.Types_s.quad32