ROADMAP

[dhsorens]

This PR proposes a roadmap for CompPoly as a repository. Feedback would be very helpful!

[github-actions]

🤖 Gemini PR Summary

This PR introduces the initial development roadmap for CompPoly, establishing a strategic framework to evolve the project into a formally verified, high-performance polynomial library specifically optimized for zero-knowledge (ZK) circuit verification.

Documentation

• Introduced ROADMAP.md: Added a comprehensive planning document that outlines:
  • The long-term project vision.
  • Specific criteria and milestones required for a Version 1.0 release.
  • A multi-phase execution plan focusing on formal verification, performance benchmarking, and integration with ZK proof systems.

---

Note: This PR is a policy and planning update; it does not contain functional code changes or bug fixes.

---

Analysis of Changes

Metric	Count
📝 Files Changed	1
✅ Lines Added	0
❌ Lines Removed	0

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

📄 **Per-File Summaries**

• ROADMAP.md: This PR adds a comprehensive development roadmap for CompPoly, outlining the vision, version 1.0 criteria, and a multi-phase plan to establish it as a formally verified, high-performance polynomial library for zero-knowledge circuit verification.

---

Last updated: 2026-01-08 09:59 UTC.

[github-actions]

🤖 AI Review (with external context)

🤖 AI Review

Overall Summary:
No files were reviewed.

---

[alexanderlhicks]

quick notes:

• Serialization could be useful, just needs to be done in a way that's consistent with other libraries ideally
• FFT, NTT, packed field elements/SIMD... will be worth checking what specific variants we might want to align with other existing libraries
• We should make integrating with ArkLib/hax an explicit item on the roadmap, esp wrt to hax and Rust libraries like plonky3 there may be a requirement to add lemmas to work across data structures.
• Tactics and/or simp/grindsets to streamline proofs.
• Performance improvements: native Lean performance improvements vs integrating with MLIR compilers. In any case it would definitely be nice to see what the bottlenecks are.

[alexanderlhicks]

tagging @Julek @quangvdao @chung-thai-nguyen @mitschabaude (since he worked on the original unipoly stuff in arklib) as reviewers in case there's feedback from anyone.