def Hex.ZPoly.toWP {m : UInt64} (ctx : _root_.MontCtx m) (x : ZPoly) : DensePoly (WordMod ctx)

Reduce an integer polynomial coefficientwise into WordMod ctx.

Equations

• Hex.ZPoly.toWP ctx x = Hex.DensePoly.ofCoeffs (Array.map (fun (c : Int) => Hex.WordMod.ofNat (Hex.ZPoly.intModNat c m.toNat)) (Hex.DensePoly.toArray x))

def Hex.ZPoly.ofWP {m : UInt64} (ctx : _root_.MontCtx m) (p : DensePoly (WordMod ctx)) : ZPoly

Read the canonical [0, M) residues of a WordMod polynomial back into ZPoly.

Equations

• Hex.ZPoly.ofWP ctx p = Hex.DensePoly.ofCoeffs (Array.map (fun (w : Hex.WordMod ctx) => Int.ofNat w.toNat) p.toArray)

@[simp]

theorem Hex.ZPoly.coeff_toWP {m : UInt64} (ctx : _root_.MontCtx m) (x : ZPoly) (j : Nat) : (toWP ctx x).coeff j = WordMod.ofNat (intModNat (DensePoly.coeff x j) m.toNat)

@[simp]

theorem Hex.ZPoly.coeff_ofWP {m : UInt64} (ctx : _root_.MontCtx m) (p : DensePoly (WordMod ctx)) (j : Nat) : DensePoly.coeff (ofWP ctx p) j = Int.ofNat (p.coeff j).toNat

theorem Hex.ZPoly.toWP_congr {m : UInt64} (ctx : _root_.MontCtx m) {x y : ZPoly} (h : x.congr y m.toNat) : toWP ctx x = toWP ctx y

toWP is well-defined on congruence classes modulo M.

@[simp]

theorem Hex.ZPoly.toWP_zero {m : UInt64} (ctx : _root_.MontCtx m) : toWP ctx 0 = 0

theorem Hex.ZPoly.toWP_add {m : UInt64} (ctx : _root_.MontCtx m) (x y : ZPoly) : toWP ctx (x + y) = toWP ctx x + toWP ctx y

Conversion to Montgomery-word polynomials preserves addition.

theorem Hex.ZPoly.toWP_sub {m : UInt64} (ctx : _root_.MontCtx m) (x y : ZPoly) : toWP ctx (x - y) = toWP ctx x - toWP ctx y

Conversion to Montgomery-word polynomials preserves subtraction.

theorem Hex.ZPoly.intModNat_one {M : Nat} (hM : 0 < M) : intModNat 1 M = 1 % M

Reducing one as an integer agrees with the natural-number remainder.

@[simp]

theorem Hex.ZPoly.toWP_one {m : UInt64} (ctx : _root_.MontCtx m) : toWP ctx 1 = 1

theorem Hex.ZPoly.toWP_reduceModPow {m : UInt64} (ctx : _root_.MontCtx m) {p k : Nat} (hM : m.toNat = p ^ k) (hpk : 0 < p ^ k) (x : ZPoly) : toWP ctx (x.reduceModPow p k) = toWP ctx x

The canonical reduction reduceModPow _ p k vanishes under toWP when the working modulus is exactly p^k.

theorem Hex.ZPoly.size_toWP_le {m : UInt64} (ctx : _root_.MontCtx m) (x : ZPoly) : (toWP ctx x).size ≤ DensePoly.size x

theorem Hex.DensePoly.mulCoeffStep_ge {R : Type u_1} [Lean.Grind.CommRing R] [DecidableEq R] (p q : DensePoly R) (n i : Nat) (acc : R) (j : Nat) (hj : q.size ≤ j) : p.mulCoeffStep q n i acc j = acc

An inner schoolbook step past the divisor's support is the identity.

theorem Hex.DensePoly.mulCoeffStep_inner_extend {R : Type u_1} [Lean.Grind.CommRing R] [DecidableEq R] (p q : DensePoly R) (n i : Nat) (acc : R) (t : Nat) (ht : q.size ≤ t) : List.foldl (p.mulCoeffStep q n i) acc (List.range t) = List.foldl (p.mulCoeffStep q n i) acc (List.range q.size)

Extending the inner fold past q.size changes nothing.

theorem Hex.DensePoly.mulCoeffStep_inner_all_zero {R : Type u_1} [Lean.Grind.CommRing R] [DecidableEq R] (p q : DensePoly R) (n i : Nat) (acc : R) (hi : p.size ≤ i) (L : List Nat) : List.foldl (p.mulCoeffStep q n i) acc L = acc

Past p.size, the whole inner fold is the identity.

theorem Hex.DensePoly.mulCoeffStep_outer_extend {R : Type u_1} [Lean.Grind.CommRing R] [DecidableEq R] (p q : DensePoly R) (n : Nat) (acc : R) (s : Nat) (hs : p.size ≤ s) : List.foldl (fun (acc : R) (i : Nat) => List.foldl (p.mulCoeffStep q n i) acc (List.range q.size)) acc (List.range s) = List.foldl (fun (acc : R) (i : Nat) => List.foldl (p.mulCoeffStep q n i) acc (List.range q.size)) acc (List.range p.size)

Extending the outer fold past p.size changes nothing.

theorem Hex.DensePoly.mulCoeffSum_norm {R : Type u_1} [Lean.Grind.CommRing R] [DecidableEq R] (p q : DensePoly R) (n s t : Nat) (hs : p.size ≤ s) (ht : q.size ≤ t) : p.mulCoeffSum q n = List.foldl (fun (acc : R) (i : Nat) => List.foldl (p.mulCoeffStep q n i) acc (List.range t)) 0 (List.range s)

mulCoeffSum computed over any large enough common range s × t.

theorem Hex.ZPoly.toWP_mul {m : UInt64} (ctx : _root_.MontCtx m) (x y : ZPoly) : toWP ctx (x * y) = toWP ctx x * toWP ctx y

Conversion to Montgomery-word polynomials preserves multiplication.

theorem Hex.ZPoly.ofWP_toWP_of_canonical {m : UInt64} (ctx : _root_.MontCtx m) (z : ZPoly) (hz : ∀ (i : Nat), 0 ≤ DensePoly.coeff z i ∧ DensePoly.coeff z i < ↑m.toNat) : ofWP ctx (toWP ctx z) = z

On a polynomial whose coefficients are already canonical in [0, M), ofWP ∘ toWP is the identity.

theorem Hex.ZPoly.toWP_size_eq_of_monic {m : UInt64} (ctx : _root_.MontCtx m) {z : ZPoly} (hz : DensePoly.Monic z) (hzpos : 0 < DensePoly.size z) (h1 : 1 < m.toNat) : (toWP ctx z).size = DensePoly.size z

theorem Hex.ZPoly.toWP_monic {m : UInt64} (ctx : _root_.MontCtx m) {z : ZPoly} (hz : DensePoly.Monic z) (hzpos : 0 < DensePoly.size z) (h1 : 1 < m.toNat) : (toWP ctx z).Monic

Reduction to a nontrivial Montgomery modulus preserves monicity.

theorem Hex.ZPoly.toWP_degree_eq_of_monic {m : UInt64} (ctx : _root_.MontCtx m) {z : ZPoly} (hz : DensePoly.Monic z) (hzpos : 0 < DensePoly.size z) (h1 : 1 < m.toNat) : (toWP ctx z).natDegree = DensePoly.natDegree z

A monic polynomial keeps its degree after reduction to a nontrivial Montgomery modulus.

theorem Hex.ZPoly.toWP_degree_le {m : UInt64} (ctx : _root_.MontCtx m) (z : ZPoly) : (toWP ctx z).natDegree ≤ DensePoly.natDegree z

Modular conversion cannot increase polynomial degree.