val to_felem (f:G.field) (p:poly) : G.felem f
let to_felem f p =
  let G.GF t irred = f in
  let n = I.bits t in
  let p = reverse p (n - 1) in
  Lib.IntTypes.Compatibility.nat_to_uint (U.from_vec #n (to_seq p n))
val to_felem (f:G.field) (p:poly) : G.felem f
let to_felem f p =
let G.GF t irred = f in
let n = I.bits t in
let p = reverse p (n - 1) in
Lib.IntTypes.Compatibility.nat_to_uint (U.from_vec #n (to_seq p n))
Vale.Math.Poly2.Galois.fst.checked
Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Lemmas.fsti.checked Vale.Math.Poly2.Galois.IntTypes.fsti.checked Vale.Math.Poly2.Defs_s.fst.checked prims.fst.checked Lib.LoopCombinators.fsti.checked Lib.IntTypes.Compatibility.fst.checked Lib.IntTypes.fsti.checked FStar.UInt.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2.Galois.fst
Spec.GaloisField.field Vale.Math.Poly2_s.poly Lib.IntTypes.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.op_disEquality Lib.IntTypes.U1 Lib.IntTypes.uint_t Lib.IntTypes.SEC Lib.IntTypes.Compatibility.nat_to_uint Spec.GaloisField.__proj__GF__item__t FStar.UInt.from_vec Vale.Math.Poly2_s.to_seq Vale.Math.Poly2_s.reverse Prims.op_Subtraction Prims.int Lib.IntTypes.bits Spec.GaloisField.felem
module Vale.Math.Poly2.Galois
open FStar.Mul

module U = FStar.UInt
module PL = Vale.Math.Poly2.Lemmas
module D = Vale.Math.Poly2.Defs_s
//module PD = Vale.Math.Poly2.Defs
module GI = Vale.Math.Poly2.Galois.IntTypes

// recursive definitions of from_vec/to_vec are prone to matching loops, so use no fuel from here on
#reset-options "--max_fuel 0 --max_ifuel 0"

let to_poly #f e =
  let G.GF t irred = f in
  let n = I.bits t in
  reverse (of_seq (U.to_vec #n (I.v e))) (n - 1)
val to_felem (f:G.field) (p:poly) : G.felem f
f: Spec.GaloisField.field -> p: Vale.Math.Poly2_s.poly -> Spec.GaloisField.felem f