feat(univariate): efficient evaluation on a batch of points using subproduct-tree algorithm

[olympichek]

This PR is a work in progress

[github-actions]

🤖 PR Summary

Mathematical Foundations

• Defines 2-adicity and primitive roots of unity for BabyBear and KoalaBear fields, including computational proofs of their properties.
• Introduces the Valid predicate for subproduct trees to ensure correct representation of products for recursive modular reduction.
• Establishes the FittingDomain abstraction for radix-2 NTT domain selection based on input length.

Polynomial Algorithms

• Implements the subproduct-tree algorithm for high-performance univariate batch evaluation via recursive modular reduction.
• Adds modByMonicRemainderOnly, an optimized monic polynomial division routine that computes remainders without full multiplication steps.
• Introduces truncated polynomial operations: truncate, takeLow, and mulLowNaive.

Infrastructure & Optimization

• Implements MulContext and ModContext architectures to enable pluggable backends for switching between naive and NTT-optimized polynomial operations.
• Updates the CompPoly module to export univariate utilities and field configurations as a unified API.
• Expands benchmarking to cover batch evaluation and NTT-based operations for BabyBear and KoalaBear fields.

Formal Verification

• Proves functional equivalence between specification-level evaluators (direct and Horner’s method) and the optimized subproduct-tree implementation.
• Verifies the relationship between high-level CPolynomial types and their Raw representations regarding negation, subtraction, and exponentiation.
• Proves that polynomial evaluation is preserved under modular reduction by monic polynomials that vanish at the target evaluation points.

---

Statistics

Metric	Count
📝 Files Changed	20
✅ Lines Added	1405
❌ Lines Removed	94

---

Lean Declarations

✏️ **Added:** 59 declaration(s)

• theorem eval_divModByMonicAux_go_snd_eq_self_of_eval_eq_zero in CompPoly/Univariate/ToPoly/Impl.lean
• theorem eval_mul [CommSemiring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/ToPoly/Impl.lean
• private theorem valid_combine [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem map_eval_modContext_eq_map_eval [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• def buildList [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) in CompPoly/Univariate/BatchEval/SubproductTree.lean
• def ntt [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Context.lean
• def evalBatchHorner [Semiring R] (p : CPolynomial R) (xs : Array R) : Array R in CompPoly/Univariate/BatchEval/Naive.lean
• def evalBatchSubproduct [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/SubproductTree.lean
• def truncate [Zero R] (k : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean
• def mulLowNaive [Semiring R] (k : Nat) (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean
• private theorem valid_combinePairs [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) in CompPoly/Univariate/BatchEval/Correctness.lean
• def domainOfLogN (logN : Nat) (hlogN : logN ≤ _root_.BabyBear.twoAdicity) : in CompPoly/Univariate/NTT/BabyBear.lean
• def leafFor [Field R] [BEq R] [LawfulBEq R] (x : R) : SubproductTree R in CompPoly/Univariate/BatchEval/SubproductTree.lean
• private def pointsList [Zero R] : List (SubproductTree R) → List R in CompPoly/Univariate/BatchEval/Correctness.lean
• theorem evalBatchSubproduct_eq_evalBatch [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem valid_root [Semiring R] {tree : SubproductTree R} (h : Valid tree) in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem pointsList_combinePairs [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem length_combinePairs_pair_le [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• def buildFromTrees [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (level : Nat) : in CompPoly/Univariate/BatchEval/SubproductTree.lean
• theorem twoPowNatCast_ne_zero in CompPoly/Univariate/NTT/KoalaBear.lean
• def poly [Zero R] : SubproductTree R → CPolynomial R in CompPoly/Univariate/BatchEval/SubproductTree.lean
• def domainOfLogN (logN : Nat) (hlogN : logN ≤ _root_.KoalaBear.twoAdicity) : in CompPoly/Univariate/NTT/KoalaBear.lean
• def remainderOnly [Field R] [BEq R] [LawfulBEq R] : ModContext R where in CompPoly/Univariate/BatchEval/Context.lean
• theorem eval_modByMonic_eq_self_of_eval_eq_zero in CompPoly/Univariate/ToPoly/Impl.lean
• theorem eval_sub_C_mul_X_pow_trim_eq_self_of_eval_eq_zero in CompPoly/Univariate/ToPoly/Impl.lean
• private theorem valid_leafFor [Field R] [BEq R] [LawfulBEq R] (x : R) : in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem buildList_exists_of_ne_nil [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• theorem modByMonicRemainderOnly_eq_modByMonic [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean
• private theorem pointsList_map_leafFor [Field R] [BEq R] [LawfulBEq R] : in CompPoly/Univariate/BatchEval/Correctness.lean
• def naive [Field R] [BEq R] [LawfulBEq R] : ModContext R where in CompPoly/Univariate/BatchEval/Context.lean
• def evalBatch [Semiring R] (p : CPolynomial R) (xs : Array R) : Array R in CompPoly/Univariate/BatchEval/Naive.lean
• private theorem length_combinePairs_le [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• def buildArray [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) in CompPoly/Univariate/BatchEval/SubproductTree.lean
• def evalList [Field R] [BEq R] [LawfulBEq R] (D : ModContext R) in CompPoly/Univariate/BatchEval/SubproductTree.lean
• lemma Raw.toPoly_pow [LawfulBEq R] (p : CPolynomial.Raw R) : in CompPoly/Univariate/ToPoly/Equiv.lean
• private theorem valid_leafFor_list [Field R] [BEq R] [LawfulBEq R] : in CompPoly/Univariate/BatchEval/Correctness.lean
• lemma Raw.toPoly_neg {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial.Raw R) : in CompPoly/Univariate/ToPoly/Equiv.lean
• private theorem combinePairs_ne_nil_of_ne_nil [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• def modByMonicRemainderOnly [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/Basic.lean
• def combine [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) in CompPoly/Univariate/BatchEval/SubproductTree.lean
• private theorem eval_linearFactor [Field R] [BEq R] [LawfulBEq R] (x : R) : in CompPoly/Univariate/BatchEval/Correctness.lean
• private def points [Zero R] : SubproductTree R → List R in CompPoly/Univariate/BatchEval/Correctness.lean
• def bitsOfLogN (logN : Nat) (hlogN : logN ≤ _root_.BabyBear.twoAdicity) : in CompPoly/Univariate/NTT/BabyBear.lean
• def subScaledShift [Field R] (p q : CPolynomial.Raw R) (scale : R) (shift : Nat) : in CompPoly/Univariate/Raw/Division.lean
• private theorem buildList_valid_points [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem evalList_eq_map_eval [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• def linearFactor [Field R] [BEq R] [LawfulBEq R] (x : R) : CPolynomial R in CompPoly/Univariate/BatchEval/SubproductTree.lean
• private theorem buildArray_valid_points [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem buildFromTrees_exists_of_length_le [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• private theorem eval_modContext_eq_self_of_eval_eq_zero in CompPoly/Univariate/BatchEval/Correctness.lean
• theorem evalBatchHorner_eq_evalBatch [Semiring R] (p : CPolynomial R) (xs : Array R) : in CompPoly/Univariate/BatchEval/Correctness.lean
• def combinePairs [Field R] [BEq R] [LawfulBEq R] (M : MulContext R) (level : Nat) : in CompPoly/Univariate/BatchEval/SubproductTree.lean
• def bitsOfLogN (logN : Nat) (hlogN : logN ≤ _root_.KoalaBear.twoAdicity) : in CompPoly/Univariate/NTT/KoalaBear.lean
• theorem twoPowNatCast_ne_zero in CompPoly/Univariate/NTT/BabyBear.lean
• private theorem buildFromTrees_valid_points [Field R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/BatchEval/Correctness.lean
• def modByMonicRemainderOnly [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) : in CompPoly/Univariate/Raw/Division.lean
• def takeLow [Zero R] (k : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/Raw/Ops.lean
• lemma Raw.toPoly_sub {R : Type*} [Ring R] [BEq R] [LawfulBEq R] in CompPoly/Univariate/ToPoly/Equiv.lean
• private def Valid [Semiring R] : SubproductTree R → Prop in CompPoly/Univariate/BatchEval/Correctness.lean

✏️ **Affected:** 1 declaration(s) (line number changed)

• lemma toPoly_neg {R : Type*} [Ring R] [BEq R] [LawfulBEq R] (p : CPolynomial R) : in CompPoly/Univariate/ToPoly/Equiv.lean moved from L27 to L35

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

The following violations of the CompPoly style guide were found in the provided diff:

• Grouped Violation: Missing Declaration Docstrings
  • Rule: "Every definition and major theorem should have a docstring."
  • Count: 57 violations.
  • Representative Examples:
    • CompPoly/Fields/BabyBear.lean: pBits (line 32), twoAdicity (line 35), twoAdicGenerators (line 59), and isPrimitiveRoot_twoAdicGenerator (line 181).
    • CompPoly/Univariate/BatchEval/Correctness.lean: points (line 34), Valid (line 42), and valid_combine (line 63).
    • CompPoly/Univariate/Raw/Proofs.lean: coeff_mul_X_pow (line 1021) and coeff_C_mul_X_pow (line 1047).
    • CompPoly/Univariate/ToPoly/Equiv.lean: Raw.toPoly_neg (line 27) and Raw.toPoly_pow (line 116).
    • CompPoly/Univariate/ToPoly/Impl.lean: eval_mul (line 241) and Raw.eval_modByMonic_eq_self_of_eval_eq_zero (line 281).

---

📄 **Per-File Summaries**

• CompPoly.lean: This change updates the CompPoly top-level module to export new functionality for univariate polynomial batch evaluation and specific Number Theoretic Transform (NTT) implementations. It integrates subproduct tree methods, correctness proofs, and the BabyBear and KoalaBear field configurations into the library's main entry point.
• CompPoly/Fields/BabyBear.lean: This update defines the BabyBear field as a Field instance and introduces a precomputed table of $2^n$-th roots of unity for its 2-adicity. It includes several new definitions and theorems that formally verify these elements are primitive roots of unity using repeated squaring and computational proofs.
• CompPoly/Univariate/Basic.lean: This update introduces a new definition, modByMonicRemainderOnly, for calculating polynomial remainders modulo a monic polynomial and includes a theorem proving its equivalence to the existing modByMonic implementation. No sorry or admit placeholders were added.
• CompPoly/Univariate/BatchEval.lean: This file establishes the root module for univariate batch evaluation, importing the necessary submodules for context, naive implementations, subproduct tree algorithms, and correctness proofs. It serves as the primary entry point for executable batch-evaluation APIs for canonical univariate polynomials.
• CompPoly/Univariate/BatchEval/Context.lean: This file introduces the MulContext and ModContext structures to provide pluggable backends for polynomial multiplication and remainder operations within batch evaluation algorithms. It includes several definitions for naive and NTT-optimized implementations, along with proofs ensuring these backends are equivalent to canonical polynomial operations.
• CompPoly/Univariate/BatchEval/Correctness.lean: This file establishes the correctness of univariate batch-evaluation implementations by proving that Horner and subproduct-tree based methods are equivalent to the direct evaluator. It introduces a Valid predicate for subproduct trees and provides theorems for their construction and recursive evaluation, with no sorry or admit placeholders used.
• CompPoly/Univariate/BatchEval/Naive.lean: This file introduces the evalBatch and evalBatchHorner definitions for performing batch evaluation of univariate polynomials over arrays of inputs. These functions provide specification-level evaluators using direct evaluation and Horner's method, respectively, and contain no sorry placeholders.
• CompPoly/Univariate/BatchEval/SubproductTree.lean: This file introduces the SubproductTree inductive data structure and associated functions to implement univariate batch evaluation via tree-based modular reduction. It provides definitions for constructing the subproduct tree from evaluation points and descending the tree to compute remainders efficiently, with no sorry or admit placeholders.
• CompPoly/Univariate/NTT/BabyBear.lean: This file introduces radix-2 NTT domains for the BabyBear field by defining a construction for domains of supported two-adic sizes. It includes a theorem proving that these domain sizes are non-zero in the field and provides the domainOfLogN definition to instantiate the NTT domain structure.
• CompPoly/Univariate/NTT/Domain.lean: This update introduces definitions and proofs for selecting the optimal radix-2 NTT domain for a given length requirement. It adds the bestLogN calculation, the FittingDomain subtype, and the bestDomainForLength? lookup function, complete with correctness proofs and no sorry placeholders.
• CompPoly/Univariate/NTT/KoalaBear.lean: This file introduces definitions and theorems to support radix-2 Number Theoretic Transform (NTT) domains over the KoalaBear field. It provides the domainOfLogN definition and the twoPowNatCast_ne_zero theorem to verify that domain sizes are compatible with the field's two-adic structure.
• CompPoly/Univariate/Raw/Division.lean: This update introduces the subScaledShift and modByMonicRemainderOnly definitions to provide an optimized, executable implementation for monic polynomial division. These additions allow for computing the remainder without relying on general polynomial multiplication during each cancellation step.
• CompPoly/Univariate/Raw/Ops.lean: This change introduces new definitions for truncated polynomial operations, including truncate, takeLow, and mulLowNaive for calculating lower-degree coefficients. It also defines the MulLowContext structure to provide a framework for verified multiplication backends that agree with full polynomial multiplication up to a specified degree.
• CompPoly/Univariate/Raw/Proofs.lean: This update introduces a naive backend for low-degree polynomial multiplication and adds several theorems characterizing polynomial division, such as coefficient formulas for shifted polynomials. It establishes the correctness of the optimized modByMonicRemainderOnly algorithm by proving its equivalence to the canonical monic division implementation, with no sorry placeholders introduced.
• CompPoly/Univariate/ToPoly/Equiv.lean: This PR refactors the relationship between CPolynomial and its underlying Raw representation by introducing several new lemmas for Raw.toPoly (negation, subtraction, and exponentiation). These additions allow for significantly simplified proofs for the corresponding high-level toPoly theorems, and no sorry or admit placeholders were introduced.
• CompPoly/Univariate/ToPoly/Impl.lean: This update introduces several new theorems regarding the relationship between polynomial evaluation and division, notably proving that evaluation is preserved under multiplication and modular reduction by a monic polynomial that vanishes at the evaluation point. No sorry or admit placeholders were added to the file.
• bench/CompPolyBench.lean: This change expands the univariate polynomial benchmarking suite to include performance tests for batch evaluation, NTT-based multiplication, and remainder operations. It introduces various helper functions and configuration constants to support these new benchmarks across the BabyBear and KoalaBear fields; no 'sorry' or 'admit' placeholders were added.
• bench/README.md: The documentation for the benchmark suite has been updated to reflect an expanded scope, now explicitly including performance measurements for direct univariate multiplication and root-of-unity NTT multiplication alongside existing evaluation and additive NTT benchmarks.
• tests/CompPolyTests/Univariate/NTT/Benchmark.lean: Refactored the univariate NTT benchmark to use the library's standardized bestDomainForLength? utility and FittingDomain abstraction, simplifying the code by removing manual domain construction and its associated proofs. The changes also update imports and types to align with reorganized KoalaBear field definitions without introducing any sorry or admit placeholders.
• tests/CompPolyTests/Univariate/NTT/Common.lean: Refactors NTT test helpers by delegating the construction of test domains and bit calculations to the centralized CPolynomial.NTT.KoalaBear module. This change simplifies the file by removing redundant local definitions and proofs, and it introduces no sorry or admit placeholders.

---

Last updated: 2026-05-14 18:02 UTC.