Add a test suite

[dhsorens]

Any computable library should have a test suite! Especially with Phase 2 nearly under way. This pull request starts that with some basic tests, including ones recently added to Univariate/Raw.lean. This is a very basic test suite, we'll want to build it out especially as we start making algorithms more efficient. Some clear TODOs include including stronger tests for functions, especially when the formal spec may or may not fully cover it. We should also consider build times and choose tests carefully, but for now this is the basic infrastructure.

[github-actions]

🤖 Gemini PR Summary

Establishes a dedicated testing infrastructure under a new tests/ directory, decoupling regression tests from the source code to improve maintainability and prepare for Phase 2 development.

Testing Infrastructure

• Centralized Entry Point: Created tests/CompPolyTests.lean to aggregate all test modules for unified execution and CI/CD integration.
• Computational Verification: Employs native_decide and example-based proofs to verify the correctness of computable polynomial operations.

Univariate Polynomials

• API & Transport: Added tests in Univariate/Basic.lean and Univariate/ToPoly.lean to verify algebraic identities, coefficient properties, and transport lemmas.
• Algorithm Validation: Consolidated implementation-specific tests for divByMonic and modByMonic to ensure algorithmic correctness.

Multivariate Polynomials

• Monomial Consistency: Verified CMvMonomial additive identities and degree computations, ensuring round-trip consistency with Finsupp.
• Degree Restriction: Validated properties of multivariate degree restriction, including zero-preservation and commutativity.

Refactoring

• Separation of Concerns: Migrated existing tests from CompPoly/Univariate/Raw.lean to the tests/ directory, isolating library logic from verification examples.

Future Outlook

• Expand functional testing for areas where formal specifications are incomplete.
• Integrate performance benchmarks to evaluate upcoming algorithm optimizations.

---

Analysis of Changes

Metric	Count
📝 Files Changed	12
✅ Lines Added	250
❌ Lines Removed	23

---

Lean Declarations

• No declarations were added, removed, or affected.

---

sorry Tracking

• No sorrys were added, removed, or affected.

---

🎨 **Style Guide Adherence**

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

• tests/CompPolyTests.lean:1: Missing standard file header with copyright, license, and authors. "Headers: Use standard file headers including copyright, license (Apache 2.0), and authors."
• tests/CompPolyTests.lean:1: Missing module docstring (/-! ... -/). "Module Docstrings: Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
• tests/CompPolyTests/Multivariate/Restrict.lean:27: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Multivariate/Restrict.lean:31: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Multivariate/Restrict.lean:35: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Multivariate/VarsDegrees.lean:33: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:18: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:19: Indentation of 6 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:19: Infix operator = is placed at the start of a new line. "Operators: ... Place them before a line break rather than at the start of the next line."
• tests/CompPolyTests/Univariate/Raw.lean:24: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:25: Indentation of 6 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:25: Infix operator = is placed at the start of a new line. "Operators: ... Place them before a line break rather than at the start of the next line."
• tests/CompPolyTests/Univariate/Raw.lean:31: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:32: Indentation of 6 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:32: Infix operator = is placed at the start of a new line. "Operators: ... Place them before a line break rather than at the start of the next line."
• tests/CompPolyTests/Univariate/Raw.lean:37: Indentation of 4 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:38: Indentation of 6 spaces for a statement continuation. "Indentation: Use 2 spaces for indentation."
• tests/CompPolyTests/Univariate/Raw.lean:38: Infix operator = is placed at the start of a new line. "Operators: ... Place them before a line break rather than at the start of the next line."

---

📄 **Per-File Summaries**

• CompPoly/Univariate/Raw.lean: This change removes several regression test examples for the divByMonic and modByMonic univariate polynomial operations.
• tests/CompPolyTests.lean: This file establishes a central entry point for the project's test suite by aggregating various univariate and multivariate polynomial test modules.
• tests/CompPolyTests/Multivariate/Restrict.lean: This new test file introduces basic sanity checks for multivariate polynomial degree restriction operations, providing proofs for properties such as zero-preservation, composition via minimum degree, and commutativity.
• tests/CompPolyTests/Multivariate/VarsDegrees.lean: This file introduces new test cases via Lean examples to verify basic properties and identities of variables and degrees for multivariate polynomials.
• tests/CompPolyTests/Univariate/Basic.lean: This new file establishes basic sanity checks for the univariate CPolynomial API by providing example proofs of coefficient properties and fundamental algebraic identities.
• tests/CompPolyTests/Univariate/ToPoly.lean: This new test file introduces several example proofs to verify the correctness of conversion and algebraic transport lemmas for univariate polynomials within the CompPoly library.
• tests/CompPolyTests/Univariate/Raw.lean: This new test file introduces regression tests for the CompPoly.Univariate.Raw implementation, using example proofs to verify the correctness of polynomial division and remainder operations via native_decide.
• tests/CompPolyTests/Multivariate/CMvMonomial.lean: This Lean file introduces initial test proofs and examples to verify the core functionality of CMvMonomial, focusing on round-trip conversions with Finsupp, basic additive identities, and degree computations.

---

Last updated: 2026-03-03 15:16 UTC.

[dhsorens]

@alexanderlhicks @quangvdao I think that it is likely a good idea to have a test suite to complement the formal proofs of correctness since this is a computable library.

Reasons for including a test suite:

• Catch gaps in formal specification
• Pre-proof confidence for refactors, rebases, and dependency updates.
• Preserve fixes for known bugs and prevent accidental reintroduction.
• Complement proofs with checks across Raw/Basic/equivalence layers.

Any objections? (Note the bug found in #115 fixed in #124 )

[erdkocak]

I think it would be great! We will be starting working on the implementation of the ntt this week, and we were thinking we should be able to do basic tests before starting the correctness proof. I believe we can integrate those tests to this test suite.

[dhsorens]

Going to merge for the sake of having it here and getting regression tests out of Raw.lean. The main thing with using it is probably:

1. avoid adding tests that are already formally proven (some of those currently here violate this, will be cleaned up later)
2. when implementing something, use tests to target genuine gaps in formal specification; tests are not a replacement for formal specification/verification!
3. it can be very useful to write tests before formally verifying, but please clean up the tests before a pull request in line with the above two points
4. finally, avoid using native_decide for possible soundness issues (this is a TODO for later on this pull request)

[dhsorens]

This pull request only removes regression tests from Raw.lean and leaves the rest of the extant code in place with no breaking changes introduced. Merging