Skip to content

poly-fast: add reusable interpolation plans - #9612

Open
kim-em wants to merge 15 commits into
mainfrom
poly-fast-interpolation
Open

poly-fast: add reusable interpolation plans#9612
kim-em wants to merge 15 commits into
mainfrom
poly-fast-interpolation

Conversation

@kim-em

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

Copy link
Copy Markdown
Owner

Depends on #9610.

Implements the interpolation portion of the hex-poly-fast SPEC:

  • adds reusable distinct-point InterpPlan construction with exact duplicate rejection
  • caches derivative inverses and balanced point products for repeated interpolation
  • handles empty plans and rejects exactly value-count mismatches
  • proves interpolation evaluation soundness, the point-count size bound, and degree-bounded uniqueness
  • adds conformance coverage for duplicates, mismatches, exact recovery, and the empty case
  • benchmarks direct cubic Lagrange construction against planned O(M(n) log n) bottom-up interpolation

Validation:

  • lake build (10,294 jobs)
  • lake build HexPolyFast.Conformance
  • lake exe hexpolyfast_bench verify (11 benchmarks)
  • python3 scripts/check_phase4.py
  • python3 scripts/ci/check_benches_mathlib_free.py
  • copyright, file-line-count, diff, and forbidden-proof scans

Kim Morrison and others added 15 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.
Reusable distinct-point plans cache the derivative weights and balanced point products. Direct Lagrange interpolation is cubic because it rebuilds n growing n-factor numerators; planned bottom-up interpolation costs O(M(n) log n) over the cached balanced tree.
# 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