Skip to content

ROADMAP.md

Latest commit

 

History

History
308 lines (262 loc) · 19.7 KB

ROADMAP.md

File metadata and controls

308 lines (262 loc) · 19.7 KB
Raw

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). (radix-2 NTT / NTTFast univariate multiplication)
  4. Benchmarks exist for core ops and are reproducible (lake exe CompPolyBench; CI runs benchmarks and uploads reports).
  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

    • ✅ 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)

  2. 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)
    • ✅ partialEvalFirst: Partial evaluation fixing the first variable, with its evaluation and per-variable degree-bound lemmas
    • ✅ isEmptyRingEquiv for CMvPolynomial 0 R
    • ✅ smulZeroClass: Scalar multiplication with zero behavior
    • ✅ sumToIter: Iteration utility with reconstruction/API lemmas
    • ✅ 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 (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
    • ✅ Polynomial-basis GF(2^64) and its degree-3 extension GF(2^192) (Fields/Binary/BF64/), a flat quotient by an irreducible degree-64 pentanomial rather than an iterated quadratic tower
    • ✅ 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

    • ✅ 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
    • ✅ Single-word UInt64 carriers for 64-bit and 31-bit primes outside the Montgomery bounds (Goldilocks/Fast.lean, Mersenne31/Fast.lean), reducing via the modulus identity rather than Montgomery residues
    • ✅ Checked binary-GCD inversion for the eight-limb fields (Montgomery/Native64x8Inv.lean, eprint 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, Lee-O'Sullivan ([LOS06]), approximant-basis (PM-Basis), and hybrid interpolation, plus 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-*
    • ✅ Shoup-style small-characteristic trace splitting ([vzGS92], Roots/Shoup/) and bounded Las Vegas Cantor–Zassenhaus (Roots/LasVegas/, odd-char and char-2 trace branches with probability proofs) for fields without a smooth refinement schedule
    • 🔄 Named high-width binary-tower SmallPrimeTraceContext instances (32/64) and optional GF(2^{48})/GF(2^{72}) carriers for production char-2 benches

  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.
    • ✅ Order-basis (approximant) layer over polynomial matrices (PolynomialMatrix/Approximant/): modular key equations, the divide-and-conquer PM-Basis recursion with X-adic soundness and kernel-leaf completeness, and partial linearization, alongside supporting row selection, minimal weak-Popov forms, and Strassen multiplication used by the recursion.

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: August 2026