val lemma_add (f:G.field) (e1 e2:G.felem f) : Lemma
  (requires True)
  (ensures to_poly (G.fadd e1 e2) == to_poly e1 +. to_poly e2)
  [SMTPat (to_poly (G.fadd e1 e2))]
let lemma_add f e1 e2 =
  let G.GF t irred = f in
  GI.define_logxor t e1 e2;
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  PL.lemma_add_define_all ();
  lemma_equal (to_poly (G.fadd e1 e2)) (to_poly e1 +. to_poly e2)
val lemma_add (f:G.field) (e1 e2:G.felem f) : Lemma
  (requires True)
  (ensures to_poly (G.fadd e1 e2) == to_poly e1 +. to_poly e2)
  [SMTPat (to_poly (G.fadd e1 e2))]
let lemma_add f e1 e2 =
let G.GF t irred = f in
GI.define_logxor t e1 e2;
PL.lemma_index_all ();
PL.lemma_reverse_define_all ();
PL.lemma_add_define_all ();
lemma_equal (to_poly (G.fadd e1 e2)) (to_poly e1 +. to_poly e2)
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 Vale.Math.Poly2.lemma_equal Vale.Math.Poly2.Galois.to_poly Spec.GaloisField.fadd Vale.Math.Poly2.op_Plus_Dot Prims.unit Vale.Math.Poly2.Lemmas.lemma_add_define_all Vale.Math.Poly2.Lemmas.lemma_reverse_define_all Vale.Math.Poly2.Lemmas.lemma_index_all Vale.Math.Poly2.Galois.IntTypes.define_logxor
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';
  ()

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';
  ()

let lemma_zero f =
  let G.GF t irred = f in
  let n = I.bits t in
  let a = zero in
  let b = to_poly #f G.zero in
  let eq_i (i:int) : Lemma (a.[i] == b.[i]) =
    PL.lemma_index_all ();
    PL.lemma_reverse_define_all ();
    PL.lemma_zero_define ();
    (if 0 <= i && i < n then U.zero_to_vec_lemma #n (n - 1 - i));
    ()
    in
  PL.lemma_pointwise_equal a b eq_i

//let lemma_zero' (f:G.field) : Lemma
//  (G.zero == to_felem f zero)
//  =
//  lemma_zero f;
//  lemma_felem_poly #f G.zero

let lemma_one f =
  let G.GF t irred = f in
  let n = I.bits t in
  let a = one in
  let b = to_poly #f G.one in
  let eq_i (i:int) : Lemma (a.[i] == b.[i]) =
    PL.lemma_index_all ();
    PL.lemma_reverse_define_all ();
    PL.lemma_one_define ();
    (if 0 <= i && i < n then U.one_to_vec_lemma #n (n - 1 - i));
    ()
    in
  PL.lemma_pointwise_equal a b eq_i
val lemma_add (f:G.field) (e1 e2:G.felem f) : Lemma
  (requires True)
  (ensures to_poly (G.fadd e1 e2) == to_poly e1 +. to_poly e2)
  [SMTPat (to_poly (G.fadd e1 e2))]
f: Spec.GaloisField.field -> e1: Spec.GaloisField.felem f -> e2: Spec.GaloisField.felem f
  -> FStar.Pervasives.Lemma
      (ensures
        Vale.Math.Poly2.Galois.to_poly (Spec.GaloisField.fadd e1 e2) ==
        Vale.Math.Poly2.Galois.to_poly e1 +. Vale.Math.Poly2.Galois.to_poly e2)
      [SMTPat (Vale.Math.Poly2.Galois.to_poly (Spec.GaloisField.fadd e1 e2))]