val gmul (f: G.field) (a b: G.felem f) : G.felem f
let gmul (f:G.field) (a b:G.felem f) : G.felem f =
  let (p, _, _) = gmul_rec f a b (I.bits f.G.t) in
  p
val gmul (f: G.field) (a b: G.felem f) : G.felem f
let gmul (f: G.field) (a b: G.felem f) : G.felem f =
let p, _, _ = gmul_rec f a b (I.bits f.G.t) in
p
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 Vale.Math.Poly2.Galois.fmul_t Vale.Math.Poly2.Galois.gmul_rec Lib.IntTypes.bits Spec.GaloisField.__proj__GF__item__t
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

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)

let lemma_and f e1 e2 =
  let G.GF t irred = f in
  GI.define_logand t e1 e2;
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  PL.lemma_and_define_all ();
  lemma_equal (to_poly (I.logand e1 e2)) (to_poly e1 &. to_poly e2)

let lemma_or f e1 e2 =
  let G.GF t irred = f in
  GI.define_logor t e1 e2;
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  PL.lemma_or_define_all ();
  lemma_equal (to_poly (I.logor e1 e2)) (to_poly e1 |. to_poly e2)

let lemma_shift_left f e n =
  let G.GF t irred = f in
  let nf = I.bits t in
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  PL.lemma_shift_define_all ();
  PL.lemma_mod_monomial (shift (to_poly e) (I.uint_v n)) nf;
  assert (I.uint_v (I.shift_left e n) == U.shift_left #nf (I.uint_v e) (I.uint_v n));
  lemma_equal (to_poly (I.shift_left e n)) (shift (to_poly e) (I.uint_v n) %. monomial (I.bits f.G.t))

let lemma_shift_right f e n =
  let G.GF t irred = f in
  let nf = I.bits t in
  PL.lemma_index_all ();
  PL.lemma_reverse_define_all ();
  PL.lemma_shift_define_all ();
  assert (I.uint_v (I.shift_right e n) == U.shift_right #nf (I.uint_v e) (I.uint_v n));
  lemma_equal (to_poly (I.shift_right e n)) (shift (to_poly e) (-(I.uint_v n)))

#reset-options

(*
Various definitions of multiply, ranging from Poly2 definition to GaloisField definition:
- Vale.Math.Poly2.Defs_s.mul
- mul_def: same as Defs_s.mul, but using abstract definition of poly
- pmul: equivalent to mul_def, but defined recursively based on adds and shifts by n
- mmul: same as pmul, but also do a "mod m" in the add
- smul: same as mmul, but incrementally shift by 1 rather than shifting by n and implement "mod m" using add
- gmul: same as fmul, but defined using recursion instead of repeati
- fmul: same as Spec.GaloisField.fmul, but use named function instead of lambda
- Spec.GaloisField.fmul
*)

let poly_length (p:poly) : nat =
  (if degree p < 0 then PL.lemma_degree_negative p);
  1 + degree p

unfold let sum_of_bools = D.sum_of_bools
let mul_element_fun (a b:poly) (k i:int) : bool = a.[i] && b.[k - i]

let mul_element (a b:poly) (k:int) : bool =
  sum_of_bools 0 (k + 1) (mul_element_fun a b k)

[@"opaque_to_smt"]
let mul_def (a b:poly) : Pure poly
  (requires True)
  (ensures fun p ->
    let len = poly_length a + poly_length b in
    poly_length p <= len /\
    (forall (i:nat).{:pattern p.[i]} i < len ==> p.[i] == mul_element a b i)
  )
  =
  let len = poly_length a + poly_length b in
  of_fun len (fun (i:nat) -> mul_element a b i)

let rec pmul_rec (a b:poly) (n:nat) : Tot poly (decreases n) =
  if n = 0 then zero
  else
    let n' = n - 1 in
    let p = pmul_rec a b n' in
    if b.[n'] then p +. shift a n' else p

let pmul (a b:poly) : poly =
  pmul_rec a b (poly_length b)

let rec mmul (a b m:poly) (n:nat) : Tot poly (decreases n) =
  if n = 0 then zero
  else
    let n' = n - 1 in
    let p = mmul a b m n' in
    if b.[n'] then p +. (shift a n' %. m) else p

let mod_bit1 (a m:poly) : poly =
  if a.[degree m] then a +. m else a

let rec smul_rec (a b m:poly) (n:nat) : Tot (poly & poly & poly) (decreases n) =
  if n = 0 then (zero, a, b)
  else
    let (p, a, b) = smul_rec a b m (n - 1) in
    let p = p +. (if b.[0] then a else zero) in
    let a = mod_bit1 (shift a 1) m in // mod_bit1 is equivalent to mod in this case
    let b = shift b (-1) in
    (p, a, b)

let smul (a b m:poly) (n:nat) : poly =
  let (p, _, _) = smul_rec a b m n in
  p

let mod_shift1 (a irred:poly) (k:nat) : poly =
  let s = shift a 1 %. monomial k in
  s +. (if a.[k - 1] then irred else zero)

let fmul_t (f:G.field) = G.felem f & G.felem f & G.felem f

let fmul_iter (f:G.field) : i:nat{i < I.bits f.G.t - 1} -> fmul_t f -> fmul_t f =
  fun i (p, a, b) ->
    let b0 = I.eq_mask #f.G.t (I.logand b (G.one #f)) (G.one #f) in
    let p = I.logxor p (I.logand b0 a) in
    let carry_mask = I.eq_mask #f.G.t (I.shift_right a (I.size (I.bits f.G.t - 1))) (G.one #f) in
    let a = I.shift_left a (I.size 1) in
    let a = I.logxor a (I.logand carry_mask f.G.irred) in
    let b = I.shift_right b (I.size 1) in
    (p, a, b)

let rec gmul_rec (f:G.field) (a b:G.felem f) (n:nat) : fmul_t f =
  if n = 0 then (G.zero #f, a, b)
  else
    let (p, a, b) = gmul_rec f a b (n - 1) in
    fmul_iter f 0 (p, a, b)
val gmul (f: G.field) (a b: G.felem f) : G.felem f
f: Spec.GaloisField.field -> a: Spec.GaloisField.felem f -> b: Spec.GaloisField.felem f
  -> Spec.GaloisField.felem f