Skip to content

Optimize univariate evaluation and power backends #186

@eliasjudin

Description

@eliasjudin

Summary

Univariate evaluation and power backends: replace current naive evaluation with a Horner-style implementation and replace the public raw power backend with exponentiation by squaring.

Keep the public Raw.eval₂, Raw.eval, CPolynomial.eval₂, and CPolynomial.eval entrypoints, and keep the public Raw.pow / Pow surface update the proof layer to the correct lawful theorem surface.

Correctness target

Prove that the Horner evaluator agrees with the existing univariate evaluation semantics and that the fast power backend agrees with canonical repeated multiplication at the lawful layer and on the canonical CPolynomial / QuotientCPolynomial surfaces.

In particular, re-establish the toPoly bridge theorems for evaluation and the lawful power theorems needed to preserve the existing canonical semiring behavior.

Motivation

Advances the phase 2 univariate performance track: improves the asymptotic cost of evaluation and exponentiation without changing the public behavior of the univariate API.

Metadata

Metadata

Assignees

No one assigned

    Labels

    No labels
    No labels

    Type

    No type

    Projects

    No projects

    Milestone

    No milestone

    Relationships

    None yet

    Development

    No branches or pull requests

    Issue actions