def Hex.ECPP.CM.evaluate (n x : Nat) (coefficients : List Int) : Nat

Horner evaluation modulo the subject, for ascending coefficients.

Equations

• Hex.ECPP.CM.evaluate n x coefficients = List.foldr (fun (c : Int) (acc : Nat) => (Hex.ECPP.residue n c + x * acc) % n) 0 coefficients

def Hex.ECPP.CM.rootWork (n : Nat) (p : ClassPolynomial) : Nat

Conservative modular-operation reservation for one closed-form root call. For Tonelli–Shanks, at most s iterations each use at most 3*s+3 operations; four initial exponentiations use at most eight subject-bit lengths. The remaining margin covers root construction and two Horner checks.

Equations

• Hex.ECPP.CM.rootWork n p = if p.coefficients.length ≤ 2 then 8 else have s := (Hex.Nat.oddSplit (n - 1)).fst; 12 * (HexArith.bitLength n + 1) + 3 * (s + 1) ^ 2 + 64

def Hex.ECPP.CM.roots? (n z : Nat) (p : ClassPolynomial) : List Nat

Checked canonical roots of a monic polynomial of degree at most two. Other polynomial shapes are rejected. The explicit operation reservation is checked by the caller before executing this bounded algorithm.

Equations

• One or more equations did not get rendered due to their size.

def Hex.ECPP.CM.originalPolynomials : List ClassPolynomial

The original nine invariants as linear polynomials, in the same order.

Equations

• Hex.ECPP.CM.originalPolynomials = List.map (fun (inv : Hex.ECPP.CM.Invariant) => { d := inv.d, coefficients := [-inv.j, 1] }) Hex.ECPP.CM.portfolio