Add a test suite

.github/workflows/lean_action_ci.yml

@@ -12,3 +12,5 @@ jobs:
     steps:
       - uses: actions/checkout@v4
       - uses: leanprover/lean-action@v1
+      - name: Build tests
+        run: lake test

CompPoly/Univariate/Raw.lean

@@ -1615,28 +1615,6 @@ def modByMonic [Field R] (p : CPolynomial.Raw R) (q : CPolynomial.Raw R) :
     CPolynomial.Raw R :=
   (divModByMonicAux p q).2
 
-/-- Regression test for issue #115: `(X^2 - 1) / (X + 1) = X - 1` with zero remainder. -/
-example :
-    divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
-      = #[-(1 : ℚ), 1] := by
-  native_decide
-
-example :
-    modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
-      = #[] := by
-  native_decide
-
-/-- Regression test for review-thread case: `X^3 = (X^2 + 1) * X + (-X)`. -/
-example :
-    divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
-      = #[(0 : ℚ), 1] := by
-  native_decide
-
-example :
-    modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
-      = #[(0 : ℚ), -(1 : ℚ)] := by
-  native_decide
-
 /-- Division of two `CPolynomial.Raw`s. -/
 def div [Field R] (p q : CPolynomial.Raw R) : CPolynomial.Raw R :=
   (C (q.leadingCoeff)⁻¹ • p).divByMonic (C (q.leadingCoeff)⁻¹ * q)

lakefile.lean

@@ -2,11 +2,16 @@ import Lake
 
 open System Lake DSL
 
-package CompPoly where version := v!"0.1.0"
+package CompPoly where
+  version := v!"0.1.0"
+  testDriver := "CompPolyTests"
 
 require "leanprover-community" / mathlib @ git "v4.28.0"
 
 require ExtTreeMapLemmas from git "https://github.com/Verified-zkEVM/ExtTreeMapLemmas"@"v4.28.0"
 
 @[default_target]
 lean_lib CompPoly
+
+lean_lib CompPolyTests where
+  srcDir := "tests"

scripts/style-exceptions.txt

@@ -2,6 +2,8 @@ lake-manifest.json : line 1 : ERR_COP : Malformed or missing copyright header :
 lake-manifest.json : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
 lakefile.lean : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
 lakefile.lean : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
+tests/CompPolyTests.lean : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
+tests/CompPolyTests.lean : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
 lean-toolchain : line 1 : ERR_COP : Malformed or missing copyright header : ERR_COP
 lean-toolchain : line 1 : ERR_MOD : Module docstring missing, or too late : ERR_MOD
 lakefile.lean : line 1 : ERR_TAC2 : In the past, importing 'Lake' has led to dramatic slow-downs of the linter (see e.g. mathlib4#13779). Please consider carefully if this import is useful and make sure to benchmark it. If this is fine, feel free to allow this linter. : ERR_TAC2

tests/CompPolyTests.lean

@@ -0,0 +1,6 @@
+import CompPolyTests.Univariate.Raw
+import CompPolyTests.Univariate.Basic
+import CompPolyTests.Univariate.ToPoly
+import CompPolyTests.Multivariate.CMvMonomial
+import CompPolyTests.Multivariate.Restrict
+import CompPolyTests.Multivariate.VarsDegrees

tests/CompPolyTests/Multivariate/CMvMonomial.lean

@@ -0,0 +1,37 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
+import CompPoly.Multivariate.CMvMonomial
+
+/-!
+  # Multivariate Monomial Tests
+
+  First-pass sanity checks for `CompPoly.Multivariate.CMvMonomial`.
+-/
+
+namespace CPoly
+namespace CMvMonomial
+
+-- TODO: add more arithmetic compatibility checks with `MonoR.evalMonomial`.
+
+example {n : ℕ} (m : CMvMonomial n) : ofFinsupp m.toFinsupp = m := by
+  simp
+
+example {n : ℕ} (m : Fin n →₀ ℕ) : (ofFinsupp m).toFinsupp = m := by
+  simp
+
+example {n : ℕ} (m : CMvMonomial n) : m + 0 = m := by
+  simp [add_zero]
+
+example : CMvMonomial.totalDegree (#m[1, 2] : CMvMonomial 2) = 3 := by
+  -- TODO avoid using native_decide for soundness issues
+  native_decide
+
+example : CMvMonomial.degreeOf (#m[3, 4] : CMvMonomial 2) ⟨1, by decide⟩ = 4 := by
+  -- TODO avoid using native_decide for soundness issues
+  native_decide
+
+end CMvMonomial
+end CPoly

tests/CompPolyTests/Multivariate/Restrict.lean

@@ -0,0 +1,38 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
+import CompPoly.Multivariate.Restrict
+
+/-!
+  # Multivariate Restrict Tests
+
+  Basic sanity checks for `restrictTotalDegree` and `restrictDegree`.
+-/
+
+namespace CPoly
+
+open CMvPolynomial
+
+-- TODO: add concrete finite-support examples exercising mixed degree bounds.
+
+example (d : ℕ) : restrictTotalDegree (n := 2) (R := ℚ) d (0 : CMvPolynomial 2 ℚ) = 0 := by
+  simp [restrictTotalDegree_zero]
+
+example (d : ℕ) : restrictDegree (n := 2) (R := ℚ) d (0 : CMvPolynomial 2 ℚ) = 0 := by
+  simp [restrictDegree_zero]
+
+example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) :
+    restrictTotalDegree d (restrictTotalDegree d' p) = restrictTotalDegree (min d d') p := by
+  simp [restrictTotalDegree_restrictTotalDegree]
+
+example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) :
+    restrictDegree d (restrictDegree d' p) = restrictDegree (min d d') p := by
+  simp [restrictDegree_restrictDegree]
+
+example (d d' : ℕ) (p : CMvPolynomial 2 ℚ) :
+    restrictTotalDegree d (restrictDegree d' p) = restrictDegree d' (restrictTotalDegree d p) := by
+  simp [restrictTotalDegree_restrictDegree_comm]
+
+end CPoly

tests/CompPolyTests/Multivariate/VarsDegrees.lean

@@ -0,0 +1,36 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
+import CompPoly.Multivariate.VarsDegrees
+
+/-!
+  # Multivariate Vars/Degrees Tests
+
+  Basic sanity checks for `vars`, `degrees`, and `degreeOf`.
+-/
+
+namespace CPoly
+
+open CMvPolynomial
+
+-- TODO: add nontrivial examples relating `vars`/`degrees` to explicit monomials.
+
+example (i : Fin 3) : (0 : CMvPolynomial 3 ℚ).degreeOf i = 0 := by
+  simp [degreeOf_zero]
+
+example : (0 : CMvPolynomial 3 ℚ).degrees = 0 := by
+  simp [degrees_zero]
+
+example : (0 : CMvPolynomial 3 ℚ).vars = ∅ := by
+  simp [vars_zero]
+
+example : (1 : CMvPolynomial 3 ℚ).degrees = 0 := by
+  simp [degrees_one]
+
+example (p : CMvPolynomial 3 ℚ) (i : Fin 3) :
+    i ∈ p.vars ↔ 0 < p.degreeOf i := by
+  simp [mem_vars_iff_degreeOf_pos]
+
+end CPoly

tests/CompPolyTests/Univariate/Basic.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
+import CompPoly.Univariate.Basic
+
+/-!
+  # Univariate Basic Tests
+
+  First-pass sanity checks for key API behavior in `CompPoly.Univariate.Basic`.
+-/
+
+namespace CompPoly
+namespace CPolynomial
+
+-- TODO: expand this file with more operation-level regression checks.
+
+example (r : ℚ) : (C r).coeff 0 = r := by
+  simpa using coeff_C (R := ℚ) r 0
+
+example (r : ℚ) : (C r).coeff 3 = 0 := by
+  simpa using coeff_C (R := ℚ) r 3
+
+example : (X : CPolynomial ℚ).coeff 1 = 1 := by
+  native_decide
+
+example (p : CPolynomial ℚ) : (divX p).coeff 2 = p.coeff 3 := by
+  simpa using coeff_divX (R := ℚ) p 2
+
+example (p : CPolynomial ℚ) : p + 0 = p := by
+  simp
+
+example (p : CPolynomial ℚ) : 0 + p = p := by
+  simp
+
+example (p : CPolynomial ℚ) : p * 0 = 0 := by
+  simp
+
+example (p : CPolynomial ℚ) : 1 * p = p := by
+  simp
+
+end CPolynomial
+end CompPoly

tests/CompPolyTests/Univariate/Raw.lean

@@ -0,0 +1,44 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen, Elias Judin
+-/
+import CompPoly.Univariate.Raw
+
+/-!
+  # Univariate Raw Regression Tests
+
+  Lightweight regression checks for `CompPoly.Univariate.Raw`.
+-/
+
+namespace CompPoly
+namespace CPolynomial.Raw
+
+/-- Regression test for issue #115: `(X^2 - 1) / (X + 1) = X - 1` with zero remainder. -/
+example :
+    divByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
+      = #[-(1 : ℚ), 1] := by
+  -- TODO avoid using native_decide for soundness issues
+  native_decide
+
+example :
+    modByMonic ((X : CPolynomial.Raw ℚ) ^ 2 - C 1) ((X : CPolynomial.Raw ℚ) + C 1)
+      = #[] := by
+  -- TODO avoid using native_decide for soundness issues
+  native_decide
+
+/-- Regression test for review-thread case: `X^3 = (X^2 + 1) * X + (-X)`. -/
+example :
+    divByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
+      = #[(0 : ℚ), 1] := by
+  -- TODO avoid using native_decide for soundness issues
+  native_decide
+
+example :
+    modByMonic ((X : CPolynomial.Raw ℚ) ^ 3) ((X : CPolynomial.Raw ℚ) ^ 2 + C 1)
+      = #[(0 : ℚ), -(1 : ℚ)] := by
+  -- TODO avoid using native_decide for soundness issues
+  native_decide
+
+end CPolynomial.Raw
+end CompPoly

tests/CompPolyTests/Univariate/ToPoly.lean

@@ -0,0 +1,39 @@
+/-
+Copyright (c) 2026 CompPoly. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Derek Sorensen
+-/
+import CompPoly.Univariate.ToPoly
+
+/-!
+  # Univariate ToPoly Tests
+
+  First-pass sanity checks for conversion and transport lemmas in
+  `CompPoly.Univariate.ToPoly`.
+-/
+
+namespace CompPoly
+namespace CPolynomial
+
+-- TODO: add focused edge cases for degree/leadingCoeff transport once API settles.
+
+example (p : Polynomial ℚ) : p.toImpl.toPoly = p := by
+  simpa using Raw.toPoly_toImpl (Q := ℚ) (p := p)
+
+example (p : CPolynomial.Raw ℚ) : p.toPoly.toImpl = p.trim := by
+  simp [Raw.toImpl_toPoly]
+
+example (p : CPolynomial ℚ) : p.toPoly.toImpl = p := by
+  simp [toImpl_toPoly_of_canonical]
+
+example (p q : CPolynomial ℚ) : (p + q).toPoly = p.toPoly + q.toPoly := by
+  simp [toPoly_add]
+
+example (p q : CPolynomial ℚ) : (p * q).toPoly = p.toPoly * q.toPoly := by
+  simp [toPoly_mul]
+
+example (r : ℚ) : (C r).toPoly = Polynomial.C r := by
+  simp [C_toPoly]
+
+end CPolynomial
+end CompPoly

tests/README.md

@@ -0,0 +1,25 @@
+# CompPoly tests
+
+This directory contains Lean test modules for regression and behavioral checks.
+
+## Structure
+
+Tests mirror the `CompPoly/` hierarchy under the `CompPolyTests` namespace.
+For example:
+
+- library module: `CompPoly/Univariate/Raw.lean`
+- test module: `tests/CompPolyTests/Univariate/Raw.lean`
+
+## Running tests
+
+Build all tests:
+
+```bash
+lake test
+```
+
+Build a single test module:
+
+```bash
+lake build CompPolyTests.Univariate.Raw
+```