val lemma_felem_poly (#f:G.field) (e:G.felem f) : Lemma
  (requires True)
  (ensures to_felem f (to_poly e) == e)
  [SMTPat (to_felem f (to_poly e))]
let lemma_felem_poly #f e =
  let G.GF t irred = f in
  let n = I.bits t in
  let u = I.v #t #I.SEC e in
  let s = U.to_vec #n u in
  let r = of_seq s in
  let p = reverse r (n - 1) in
  let r' = reverse p (n - 1) in
  let s' = to_seq r' n in
  let u' = U.from_vec #n s' in
  let e' = Lib.IntTypes.Compatibility.nat_to_uint #t #I.SEC u' in
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  lemma_equal r r';
  assert (equal s s');
  Lib.IntTypes.Compatibility.uintv_extensionality e e';
  ()
val lemma_felem_poly (#f:G.field) (e:G.felem f) : Lemma
  (requires True)
  (ensures to_felem f (to_poly e) == e)
  [SMTPat (to_felem f (to_poly e))]
let lemma_felem_poly #f e =
let G.GF t irred = f in
let n = I.bits t in
let u = I.v #t #I.SEC e in
let s = U.to_vec #n u in
let r = of_seq s in
let p = reverse r (n - 1) in
let r' = reverse p (n - 1) in
let s' = to_seq r' n in
let u' = U.from_vec #n s' in
let e' = Lib.IntTypes.Compatibility.nat_to_uint #t #I.SEC u' in
PL.lemma_index_all ();
PL.lemma_reverse_define_all ();
lemma_equal r r';
assert (equal s s');
Lib.IntTypes.Compatibility.uintv_extensionality e e';
()
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 Spec.GaloisField.felem Lib.IntTypes.inttype Prims.l_and Prims.b2t Lib.IntTypes.unsigned Prims.op_disEquality Lib.IntTypes.U1 Lib.IntTypes.uint_t Lib.IntTypes.SEC Prims.unit Lib.IntTypes.Compatibility.uintv_extensionality Spec.GaloisField.__proj__GF__item__t Prims._assert FStar.Seq.Base.equal Prims.bool Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.Lemmas.lemma_reverse_define_all Vale.Math.Poly2.Lemmas.lemma_index_all Lib.IntTypes.int_t Prims.eq2 Prims.int Prims.l_or Lib.IntTypes.range Prims.op_GreaterThanOrEqual Prims.op_LessThanOrEqual Lib.IntTypes.maxint Lib.IntTypes.v Lib.IntTypes.Compatibility.nat_to_uint FStar.UInt.uint_t FStar.UInt.from_vec FStar.Seq.Base.seq Vale.Math.Poly2_s.to_seq Vale.Math.Poly2_s.poly Vale.Math.Poly2_s.reverse Prims.op_Subtraction Vale.Math.Poly2_s.of_seq FStar.BitVector.bv_t FStar.UInt.to_vec Lib.IntTypes.bits
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)

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))

let lemma_to_poly_degree #f e =
  reveal_defs ()

let lemma_irred_degree f =
  let G.GF t irred = f in
  let n = I.bits t in
  PL.lemma_index_all ();
  PL.lemma_monomial_define n;
  PL.lemma_add_define_all ();
  PL.lemma_degree_is (irred_poly f) n;
  ()

let lemma_poly_felem f p =
  let G.GF t irred = f in
  let n = I.bits t in
  let r = reverse p (n - 1) in
  let s = to_seq r n in
  let u = U.from_vec #n s in
  let e = Lib.IntTypes.Compatibility.nat_to_uint u in
  let u' = I.v #t #I.SEC e in
  let s' = U.to_vec #n u' in
  let r' = of_seq s' in
  let p' = reverse r' (n - 1) in
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  lemma_equal r r';
  lemma_equal p p';
  ()
val lemma_felem_poly (#f:G.field) (e:G.felem f) : Lemma
  (requires True)
  (ensures to_felem f (to_poly e) == e)
  [SMTPat (to_felem f (to_poly e))]
e: Spec.GaloisField.felem f
  -> FStar.Pervasives.Lemma
      (ensures Vale.Math.Poly2.Galois.to_felem f (Vale.Math.Poly2.Galois.to_poly e) == e)
      [SMTPat (Vale.Math.Poly2.Galois.to_felem f (Vale.Math.Poly2.Galois.to_poly e))]