Skip to content

Latest commit

 

History

History
183 lines (139 loc) · 10.3 KB

ROADMAP.md

File metadata and controls

183 lines (139 loc) · 10.3 KB

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 sorrys in all shipped modules.
  2. Complete core API for CPolynomial, CMvPolynomial, CMlPolynomial, including evaluation + interpolation + conversions.
  3. At least one "fast path" implemented + proven correct (FFT/NTT multiplication OR fast multilinear transforms).
  1. Proof ergonomics baseline: common operations (add, mul, eval) mostly simp/grind-driven, documented.
  2. At least one real integration example (ArkLib or RT extraction exemplar) demonstrating use as a dependency.
  3. Minimal docs: README + module docs sufficient for contributors.
  4. 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

    • Prove all remaining sorrys
    • ✅ 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); prove remaining algebraic instances (CommRing, Algebra, Module) without sorry

  2. API completeness

    • ✅ Add monomial constructors for univariate and multivariate polynomials
    • Implement monomial order support (MonomialOrder.degree, leadingCoeff) — stubs exist, proofs pending
    • 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 — stubs exist, proofs pending
    • algebra, module: Algebra and module structures
    • ✅ degrees; eval₂Hom: Degree utilities and evaluation homomorphisms (latter pending)
    • finSuccEquiv, optionEquivLeft: Variable manipulation equivalences (for CMvPolynomial)
    • ✅ CommSemiring for CMvPolynomial; isEmptyAlgEquiv: Additional algebra structures (latter pending)
    • smulZeroClass, sumToIter: Scalar multiplication and iteration utilities — stubs exist, proofs pending
    • ✅ Implement rename / renameEquiv for variable renaming

  3. 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
    • ✅ Implement a specialized Bivariate polynomial type, e.g. as CPolynomial (CPolynomial R) with specialized polynomial operations (that can then be optimized)

Success Criteria: Zero sorrys 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

    • Optimized implementations of off-the-shelf available Field instances to enable performance, including for prime and other finite fields

  2. Polynomial multiplication

    • Implement FFT/NTT-based multiplication (O(n log n) vs current O(n²))
    • Focus on NTT for finite field arithmetic
    • Maintain correctness proofs alongside optimizations

Note: erdkocak and doran2728 have communicated they will be working on this.

  1. Exponentiation optimization

    • Replace repeated multiplication with repeated squaring
    • Reduce complexity from O(n) to O(log n) multiplications

  2. Evaluation optimizations

    • Implement batch evaluation at multiple points
    • Add Horner's method where beneficial
    • Optimize for common ZK evaluation patterns

  3. 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

  4. Bivariate polynomial operations

    • Implement efficient bivariate polynomial type: CPolynomial (CPolynomial R) or specialized representation, with optimized operations
    • Efficient factorization algorithms for bivariate polynomials
    • Integration with existing CMvPolynomial 2 R with equivalence proofs
    • Critical for sum-check protocols, FRI commitments, and zkVM constraint systems

  5. Error-correcting interpolation algorithms

    • Implement Berlekamp-Welch algorithm for Reed-Solomon decoding
    • Implement Guruswami-Sudan list-decoding algorithm
    • Proofs of correctness
    • Integration with FRI commitments and polynomial commitment schemes

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 sorrys 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: February 2026