val gf128_modulus_low_terms:poly
let gf128_modulus_low_terms : poly = of_fun 8 (fun (i:nat) -> i = 0 || i = 1 || i = 2 || i = 7)
val gf128_modulus_low_terms:poly
let gf128_modulus_low_terms:poly =
of_fun 8 (fun (i: nat) -> i = 0 || i = 1 || i = 2 || i = 7)
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.of_fun Prims.nat Prims.op_BarBar Prims.op_Equality Prims.int Prims.bool
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
val gf128_modulus_low_terms:poly
Vale.Math.Poly2_s.poly