val to_poly (p: poly{poly == D.poly}) : D.poly
let to_poly (p:poly{poly == D.poly}) : D.poly = coerce D.poly p
val to_poly (p: poly{poly == D.poly}) : D.poly
let to_poly (p: poly{poly == D.poly}) : D.poly =
coerce D.poly p
Vale.Math.Poly2_s.fsti.checked
Vale.Math.Poly2.Defs_s.fst.checked prims.fst.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.Math.Poly2_s.fsti
Vale.Math.Poly2_s.poly Prims.eq2 Vale.Math.Poly2.Defs_s.poly Vale.Math.Poly2_s.coerce
module Vale.Math.Poly2_s
module D = Vale.Math.Poly2.Defs_s
open FStar.Mul
open FStar.Seq

// Polynomials cn * x^n + ... + c0 * x^0
// where coefficients ck are treated mod 2
// Each coefficient is 0 (false) or 1 (true)

val poly : eqtype
val degree (p:poly) : int // note: degree zero == -1
val zero : poly
val one : poly
val monomial (n:nat) : poly // x^n
val shift (p:poly) (n:int) : poly // x^n * p
val reverse (p:poly) (n:nat) : poly // x^n <--> x^0, x^(n-1) <--> x^1, ...

// Index any coefficient, where all coefficients beyond highest-order term are zero
// (and n < 0 returns zero).
// p.[0] is the coefficient of the lowest-order term (x^0).
val poly_index (p:poly) (n:int) : bool
unfold let ( .[] ) = poly_index

val to_seq (p:poly) (n:nat) : Pure (seq bool)
  (requires True)
  (ensures fun s ->
    length s == n /\
    (forall (i:nat).{:pattern (p.[i]) \/ (index s i)} i < length s ==> p.[i] == index s i)
  )

val of_seq (s:seq bool) : Pure poly
  (requires True)
  (ensures fun p ->
    degree p < length s /\
    (forall (i:nat).{:pattern (p.[i]) \/ (index s i)} i < length s ==> p.[i] == index s i)
  )

val of_fun (len:nat) (f:nat -> bool) : Pure poly
  (requires True)
  (ensures fun p ->
    degree p < len /\
    (forall (i:nat).{:pattern p.[i] \/ (f i)} i < len ==> p.[i] == f i) /\
    (forall (i:int).{:pattern p.[i]} p.[i] ==> 0 <= i /\ i < len)
  )

val add (a b:poly) : poly
val mul (a b:poly) : poly
val div (a b:poly) : poly
val mod (a b:poly) : poly
val to_poly (p: poly{poly == D.poly}) : D.poly
p: Vale.Math.Poly2_s.poly{Vale.Math.Poly2_s.poly == Vale.Math.Poly2.Defs_s.poly}
  -> Vale.Math.Poly2.Defs_s.poly