# CompPoly Development Roadmap

## Vision

CompPoly aims to be the premier formally verified library for computable polynomial operations over finite fields, serving as the mathematical foundation for zero-knowledge circuit verification. We aim to provide efficient, proven-correct implementations of univariate, multivariate, and multilinear polynomial arithmetic that seamlessly integrate with the Lean 4/Mathlib ecosystem.

## V1.0 Criteria

1. Zero `sorry`s in all shipped modules.
1. Complete core API for `CPolynomial`, `CMvPolynomial`, `CMlPolynomial`, including evaluation + interpolation + conversions.
1. ✅ At least one "fast path" implemented + proven correct (FFT/NTT multiplication OR fast multilinear transforms). *(radix-2 NTT / `NTTFast` univariate multiplication)*
1. Benchmarks exist for core ops and are reproducible (`lake exe CompPolyBench`; CI runs benchmarks and uploads reports).
<!-- 1. Property tests exist for core ops (eval, mul, interpolation). -->
1. Proof ergonomics baseline: common operations (add, mul, eval) mostly simp/grind-driven, documented.
1. At least one real integration example (ArkLib or RT extraction exemplar) demonstrating use as a dependency.
1. Minimal docs: README + module docs sufficient for contributors.
1. CI stability: all tests pass consistently.

## Development Phases

### Phase 1: Theoretical Foundation

**Goal**: Establish complete mathematical foundations and close critical gaps.

#### Priorities

1. **Theoretical completeness**
   - ✅ Implement `nodal` and `interpolate` for Lagrange interpolation
   - ✅ Implement `AddCommGroup`/`Semiring`/`CommSemiring`/`Ring`/`CommRing` instances for `CPolynomial` and `QuotientCPolynomial`
   - ✅ Prove isomorphism between `CPolynomial` and Mathlib's `Polynomial` (`ringEquiv` in `Univariate/ToPoly.lean`); prove for `QuotientCPolynomial` as needed
   - ✅ Prove `CommSemiring` for `CMvPolynomial` and `polyRingEquiv` (ring isomorphism with Mathlib's `MvPolynomial (Fin n) R`)
   - ✅ Complete remaining algebraic structures (`CommRing`, `Algebra`, scalar action / `SMulZeroClass`)

1. **API completeness**
   - ✅ Add `monomial` constructors for univariate and multivariate polynomials
   - ✅ Implement monomial-order baseline (`MonomialOrder.degree`, `leadingMonomial`, `leadingCoeff`, `leadingTerm`)
   - ✅ `degreeLT`, `degreeLE`: Bounded-degree submodules for univariate polynomials
   - ✅ `mem_degreeLT`, `mem_degreeLE`: Membership characterizations for bounded-degree polynomials
   - ✅ `degreeLTEquiv`: Linear equivalence for coefficient access
   - ✅ `restrictDegree`: Degree restrictions for multilinear extensions
   - ✅ `vars`: Variable set extraction
   - ✅ `aeval`, `bind₁`: Algebra evaluation and substitution
   - ✅ `algebra`, `module`: Algebra and module structures
   - ✅ `degrees`; ✅ `eval₂Hom`: Degree utilities and evaluation homomorphisms
   - ✅ `finSuccEquiv`: Variable manipulation equivalences (for `CMvPolynomial`)
   - ✅ `isEmptyRingEquiv` for `CMvPolynomial 0 R`
   - ✅ `smulZeroClass`: Scalar multiplication with zero behavior
   - ✅ `sumToIter`: Iteration utility with reconstruction/API lemmas
   - ✅ Implement `rename` / `renameEquiv` for variable renaming

1. **Further data types**
   - ✅ Basic field definitions (currently in Arklib) ported into CompPoly (e.g. BabyBear, Goldilocks, BN254, BLS12_381, binary tower)
      - ✅ computable field extensions with interface (`CompPoly/Fields/Extension/`):
        `F[X]/f` for an **arbitrary monic** `f` with `CommRing`/`Field`, `Algebra F (Ext P)`
        (hence `Module`), a base embedding `ofBase`, the adjoined root `gen` with
        `aeval gen poly = 0`, a ring equivalence to `AdjoinRoot`, and cardinality `q ^ d`.
        Binomials `X^d - W` are the special case via `BinomialParams.toExtensionParams`,
        keeping `gen ^ d = ofBase W`. Irreducibility comes from a general Rabin criterion
        (`CompPoly/Data/Polynomial/Rabin.lean`), collapsed to two base-field exponentiations
        for binomials and discharged by kernel-checked certificates otherwise
        (`CompPoly/Data/Polynomial/RabinCertificate.lean`, generated by
        `scripts/gen_rabin_certificate.py`), at prime **and** composite degree — one
        coprimality certificate per prime factor of `d`. Concrete instances: degree-4 over
        BabyBear, KoalaBear, and Hachi (`2^32 - 99`); non-binomial degree-5
        (`X^5 + X^2 - 1`) and degree-6 (`X^6 + X^3 + 1 = Φ₉`, ~`2^186`) over KoalaBear, the
        latter identified with Mathlib's `GaloisField` in `KoalaBear/Ext6/GaloisField.lean`.
         - Tower support (`AlgebraTower`) is the main interface gap: `F ⊂ Ext F 2 ⊂ Ext F 4`
           does not yet compose. The blocker is not `ExtensionParams` — it is generic over
           `[Field F] [Fintype F]`, and `Ext P` supplies both, so a two-level type is
           well-formed today — but discharging `Fact (Irreducible P'.poly)` over an `Ext`
           base: `reduce_mod_char` needs the base as `ZMod <numeral>` and the certificate
           layer is built on `toPoly : List ℕ → (ZMod p)[X]`. With `native_decide` forbidden
           this needs a certificate layer over a non-prime base
         - 🔄 Performance: after routing compilation through the `Ext.red` reduction table
           (`mul_eq_mulTbl`, `@[csimp]`), `mul` measures ~25us at degree 4 and ~64us at
           degree 6, with `inv` ~3.5ms and ~15ms (`lake exe CompPolyBench --small`) — a
           3-8x gain over the specification, growing with `d` as the `O(d^5)`→`O(d^3)`
           change predicts. Still far off a native implementation. In priority order:
           take `Ext.mul` from `O(d^3)` to **`O(d^2)`** with an allocation-free array loop
           (schoolbook convolution to `2d - 1` folded through `red`, with `red` hoisted so it
           is built once per `P` rather than per multiplication); instantiate over the
           `FastField` Montgomery carrier instead of `ZMod`; replace Fermat inversion with a
           norm-based (Itoh–Tsujii) inverse — neither `Ext.frobenius` nor `Ext.norm` exists
           yet, and `Φ₉` was chosen partly because its Frobenius (`θ ↦ θ^2`) is sparse
         - Rebase the GHASH Rabin specialization
           (`irreducible_of_rabin_128_passed_over_GF2`) onto the general
           `Polynomial.irreducible_of_rabin` so the two soundness proofs do not need
           parallel maintenance
         - 64-bit-radix Montgomery layer, so `Hachi` gets a `FastField` base
   - ✅ Implement a specialized Bivariate polynomial type, e.g. as `CPolynomial (CPolynomial R)` with specialized polynomial operations (that can then be optimized)

**Success Criteria**: Zero `sorry`s in core operations, all ring structures complete, clean build with no warnings, reasonable proof ergonomics.

---

### Phase 2: Performance & Efficiency

**Goal**: Optimize critical operations for production use in ZK verification.

#### Priorities
1. **Fast field arithmetic**
   - ✅ Radix-generic Montgomery reduction shared by every fast prime field
     (`Fields/Montgomery/Basic.lean`)
   - ✅ Single-word `UInt32` Montgomery carrier for 31-bit primes
     (`Montgomery/Native32.lean`, `Montgomery/Native32Field.lean`, `Mont32Field`),
     instantiated by `BabyBear/Fast.lean` and `KoalaBear/Fast.lean`
   - ✅ Eight-limb Montgomery carrier with CIOS multiplication for moduli below
     `2^255` (`Montgomery/Native64x8*.lean`, `Mont64x8Field`), instantiated by
     `BN254/Fast.lean`, `BLS12_381/Fast.lean`, and `BLS12_377/Fast.lean`
   - ✅ Checked binary-GCD inversion for the eight-limb fields
     (`Montgomery/Native64x8Inv.lean`, [eprint 2020/972](https://eprint.iacr.org/2020/972)),
     benchmarked against `ZMod` extended Euclid and Fermat in `fields-mont64x8-*-inv`
   - 🔄 64-bit-radix Montgomery layer, so Goldilocks and Hachi (`2^32 - 99`) gain a
     `FastField` base; `Mont32Field` requires modulus < `2^31`
   - 🔄 Instantiate `Extension.Ext` over a Montgomery carrier rather than `ZMod`
     (see the extension performance notes under Phase 1)

2. **Polynomial multiplication**
   - ✅ Radix-2 NTT domain, forward/inverse transforms, and reference fast multiply (`Univariate/NTT/`)
   - ✅ NTT-based `fastMulImpl` / `safeFastMul` / `withFallback` with full correctness proofs (`NTT/FastMul`)
   - ✅ Concrete NTT domains for BabyBear and KoalaBear (`NTT/BabyBear`, `NTT/KoalaBear`)
   - ✅ Low-product multiplication via NTT (`NTT/FastMulLow`)
   - ✅ Optimized `NTTFast` path: cached twiddle plans, DIF/radix-4 stages, paired forward transforms, refinement proofs vs `NTT` (`Univariate/NTTFast/`)
   - ✅ Pluggable multiply backends for batch algorithms (`BatchEval/Context`: `MulContext.ntt`, `MulContext.nttFast`)
   - 🔄 Additional concrete domains and field-specific tuning beyond BabyBear/KoalaBear

3. **Exponentiation optimization**
   - ✅ Replace repeated multiplication with repeated squaring
   - ✅ Reduce complexity from O(n) to O(log n) multiplications

4. **Evaluation optimizations**
   - ✅ Batch evaluation at multiple points: naive, Horner, and subproduct-tree algorithms (`Univariate/BatchEval/`)
   - ✅ Subproduct-tree batch eval with configurable multiply/remainder backends (naive, NTT, NTTFast)
   - ✅ Add Horner's method where beneficial
   - ✅ Many-polynomial, one-shared-point evaluation — the common commitment-opening
     shape — with correctness proofs (`Univariate/ManyEval/`, `Multilinear/ManyEval/`)
   - 🔄 Optimize for further common ZK evaluation patterns

5. **Complete multilinear transform functions**
   - ✅ Complete documentation of zeta/Möbius transform formulas
   - ✅ Prove equivalence between fast and spec implementations
   - 🔄 Add performance guarantees and complexity proofs (done in comments, formal benchmarking still TODO)

6. **Benchmarking**
   - ✅ Basic, reproducible evaluation benchmark executable (`lake exe CompPolyBench`; see `bench/README.md`)
   - ✅ CI build/run with artifact upload (GitHub Actions `lean_action_ci.yml`)
   - 🔄 Expand regression coverage and published performance baselines

7. **Bivariate polynomial operations**
   - ✅ Optimize the existing bivariate polynomial type `CPolynomial (CPolynomial R)`:
     Kronecker substitution (`Bivariate/Kronecker.lean`) turns a bivariate
     multiplication into a single univariate one (`kroneckerPack_mul`,
     `kroneckerUnpack_mul`), with linear-time `kroneckerPackFast` /
     `kroneckerUnpackFast` proved equal to the spec versions and NTT-backed
     `kroneckerUnpack_withFallback`. Benchmarked as `bivariate-full-*`. The nested
     representation was kept; no more specialized one proved necessary.
   - 🔄 Efficient factorization algorithms for bivariate polynomials. What exists
     is linear-factor deflation rather than general factorization:
     `Bivariate/Factor.lean` defines `divByLinearY` (the computable factor theorem,
     over any `CommRing`) and `Bivariate/FactorMonic.lean` proves
     `divByLinearY_eq_divByMonic`, tying it to general monic Euclidean division.
     Benchmarked as `bivariate-deflate-*`.
   - ✅ Integration with existing `CMvPolynomial 2 R` with equivalence proofs

8. **Error-correcting interpolation algorithms**
   - ✅ Reed-Solomon encoding through the forward NTT
     (`Univariate/ReedSolomon/NTTEncode.lean`): `forwardImpl_eq_encode` and
     `nttCodeword_eq_encode` identify the `O(n log n)` transform with
     `ReedSolomon.encode` exactly, with no padding required
   - ✅ Unique decoding via Gao's key-equation decoder
     (`ReedSolomon/GaoDecoder.lean`, [Gao02]) with `GaoCorrectness.lean`:
     `decode_sound`, `decode_eq_some`, `decode_eq_none_iff`, and
     `decode_none_farness`, which reads decoder refusal as a farness certificate
   - ✅ Implement Guruswami-Sudan list-decoding algorithm
     (`Bivariate/GuruswamiSudan/`), following the interpolation-and-root-finding
     decomposition of [GS99]: a backend-parametric `Core` / `Context` with dense
     and Lee-O'Sullivan ([LOS06]) interpolation and Roth-Ruckenstein ([RR00]) and
     Alekhnovich ([Ale05]) root search, instantiated in `Implementations` and
     `Executable`
   - ✅ Proofs of correctness: `gsCore_sound`, `gsCore_complete_of_interpolate`,
     and `gsCore_complete_of_roots_all_valid_witnesses` in `CoreCorrectness.lean`,
     stated against the context contracts so they hold for every backend
   - Berlekamp-Welch decoding. Gao's decoder already covers the same
     unique-decoding regime, so this is worth adding only as a cross-check, or if a
     downstream specification asks for it by name.
   - Integration with FRI commitments and polynomial commitment schemes

9. **Univariate root finding**
   - ✅ Backend-parametric root pipeline (`Univariate/Roots/`): the `Backend`,
     `Context`, and `Splitter` interfaces, candidate extraction / validation /
     deduplication (`Extraction.lean`), `RootProduct.lean`, and `Correctness.lean`
   - ✅ Smooth multiplicative-subgroup refinement splitting for finite fields whose
     multiplicative group admits a smooth schedule ([MOV92],
     `Roots/SmoothSubgroup/`), benchmarked as `univariate-roots-finite-field-*`
   - 🔄 Splitting strategies for fields with no smooth refinement schedule

10. **Computable linear algebra**
    - ✅ Dense row-major matrices with row operations, RREF shape and semantics, and
      kernel extraction, each with a `*Correctness.lean` companion
      (`LinearAlgebra/Dense/`)
    - ✅ In-place kernel solver (`Dense/KernelInPlace.lean`) with correctness, used
      by the dense Guruswami-Sudan interpolation backend
    - ✅ Polynomial matrices with shifted degrees and row spans, plus
      Mulders-Storjohann shifted row reduction ([MS03],
      `LinearAlgebra/PolynomialMatrix/`). The fast variants are proved extensionally
      equal to the direct ones in `MuldersStorjohannCorrectness/Fast.lean`, so every
      correctness result transfers.

**Success Criteria**: notable speedup for large polynomial operations, verified correctness, benchmarks demonstrating competitive performance with industry-standard implementations.

---

### Phase 3: Further Optimization and Integration

**Goal**: Turn CompPoly into an integration-ready, downstream-friendly library by adding interoperability layers, serialization, proof automation, and extraction compatibility.

#### Priorities

1. **Lowering / interop with LLZK / PrimeIR polynomial dialects**
	- Explore representing CompPoly structures in the MLIR pipeline
	- Evaluate tradeoffs: “fast Lean code” vs “Lean spec + lowering to fast backend”
	- Goal: enable verification of PrimeIR/LLZK polynomial implementations against CompPoly semantics
2.	**Serialization (bytes/JSON/protocol/hashing)**
	- Define serialization format(s) for polynomial types
	- Compatibility with ArkLib protocol serialization needs
	- Consider: to/from bytes, to/from JSON, canonical encoding for hashing
3.	**FFT-based interpolation variants (post-FFT/NTT)**
	- Implement FFT-based Lagrange interpolation when the evaluation domain is an FFT/NTT-friendly subgroup
	- Add fast barycentric interpolation for repeated interpolation queries over a fixed set of nodes
	- Provide `interpolateFFT` / `interpolateNTT` APIs that reuse precomputed twiddle factors and domain metadata
	- Prove equivalence to the spec (naive) `interpolate` implementation and document complexity (O(n log n))
	- Include edge-case handling: non-power-of-two domains, zero-padding strategies, and domain mismatch errors
4.	**Proof ergonomics: simp/grind sets + tactics**
	- Identify rewrite bottlenecks when porting Mathlib poly proofs → CompPoly
	- Build simp sets and grind sets for common operations
	- Goal: “one-liner conversions” (or near) between spec polynomials and computable polynomials

5.	**Integration with ArkLib / Hax + Rust libraries (e.g. plonky3)**
	- Make CompPoly the canonical polynomial backend for ArkLib specs where applicable
	- Add bridging lemmas and conversion utilities across representations (CompPoly ↔ Mathlib ↔ extracted Rust ↔ downstream libs)
	- Document and implement invariants required for robust interop (canonical ordering, normalization, domain metadata)
	- Ensure hax-extracted Rust polynomial structures can be mapped into CompPoly with minimal proof overhead
	- Validate the integration with at least one downstream example (e.g. ArkLib protocol component or plonky3 polynomial routine)

**Success criteria**: CompPoly is integration-ready—it supports canonical serialization, has strong simp/grind-based proof ergonomics, includes a validated interop pathway with LLZK/PrimeIR-style representations, and demonstrates at least one end-to-end Rust extraction → Lean translation → refinement proof against CompPoly.

---

### Phase 4: Integration & Polish

**Goal**: Ensure seamless integration, excellent developer experience, and production readiness.

#### Priorities
1. **Documentation & examples**
   - Comprehensive module-level documentation
   - Usage examples for common ZK verification patterns
   - Performance characteristics guide
   - Best practices documentation

2. **Performance benchmarking suite**
   - Property-based tests/proofs of correctness for all operations
   - Performance benchmarks and regression tests
   - Edge case coverage

3. **Integration with ArkLib and other libraries**
   - Ensure all equivalences are proven and documented
   - Add conversion utilities and compatibility layers
   - Seamless integration with Verified-zkEVM ecosystem

4. **Developer experience & community**
   - Consistent API design patterns
   - Helpful error messages
   - Type aliases for common use cases
   - Advanced optimizations based on usage patterns
   - Community feedback and refinements

**Success Criteria**: Excellent documentation, comprehensive test coverage, smooth integration with Arklib, active community adoption, etc.

---

## Success Metrics

- **Mathematical completeness**: Zero `sorry`s in core operations, all ring structures proven, formal verification of correctness properties
- **Performance**: Competitive with unverified implementations for large polynomials (target: within 2x of optimized C/Rust implementations for degree ≥ 10⁴)
- **API completeness**: Full feature parity with Mathlib's `Polynomial` and `MvPolynomial` APIs, plus ZK-specific extensions
- **Usability**: Complete documentation with examples, clear integration guides, beginner-friendly tutorials
- **Adoption**: Seamless integration with Verified-zkEVM ecosystem, adoption by ZK protocol implementations, community contributions
- **Research impact**: Foundation for formally verified ZK systems, potential for academic publications on verified polynomial arithmetic

---

*Last updated: August 2026*