Skip to content

feat(poly-fast): add certified multipoint evaluation - #9610

Open
kim-em wants to merge 14 commits into
mainfrom
poly-fast-eval
Open

feat(poly-fast): add certified multipoint evaluation#9610
kim-em wants to merge 14 commits into
mainfrom
poly-fast-eval

Conversation

@kim-em

@kim-em kim-em commented Aug 25, 2026

Copy link
Copy Markdown
Owner

Summary

  • add an opaque reusable EvalPlan with the original points, balanced ProductTree, and cached reciprocal division plans
  • evaluate bounded inputs through a certified remainder tree without rebuilding the plan; retain a total direct path for oversized inputs and trivial rings
  • prove the executable result equals direct evaluation at every point, including empty plans
  • add conformance coverage and reused-plan direct/cached multipoint benchmarks

Dependency

This is stacked on #9608. The PR targets upstream main; merge #9608 first, then this branch can be rebased or merged normally.

Specification correction

The merged SPEC claimed a fixed finite EvalPlan could cache the reciprocal precision needed for arbitrarily large input polynomials. That is impossible: cached reciprocal precision is finite. The implementation uses the cached O(M(n) log n) route when f.size <= plan.size and an explicit direct total fallback otherwise; the SPEC was corrected in #9608.

Verification

  • lake build (10,294 jobs)
  • lake build HexPolyFast.Conformance
  • lake build HexPolyFast.Bench
  • .lake/build/bin/hexpolyfast_bench verify --tag multipoint
  • python3 scripts/check_phase4.py --base b4618ab98
  • python3 scripts/bench/check_factor_sweep_freshness.py
  • prohibited-proof scan and git diff --check

Kim Morrison added 11 commits August 25, 2026 04:05
The schoolbook path has quadratic coefficient work. Balanced multiplication and specialized squaring satisfy the three-recursion Karatsuba recurrence; the fixed 64-block skew dispatcher preserves that asymptotic bound.
Cost model: long division is quadratic because each leading-coefficient elimination updates a linear suffix. Cold Newton division costs O(M(n)): reciprocal doubling is a geometric series and the quotient/remainder use a constant number of clipped products.
The cached point/remainder tree evaluates bounded inputs in O(M(n) log n); the explicit Horner comparator performs Θ(n²) coefficient operations.
kim-em added 3 commits August 26, 2026 14:52
# Conflicts:
#	.github/workflows/ci.yml
#	scripts/bench/proof_only_runtime_exemptions.json
# Conflicts:
#	.github/workflows/ci.yml
#	scripts/bench/proof_only_runtime_exemptions.json
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant