feat: bump to 4.30.0-rc2 (#221)

* feat: bump to 4.30.0-rc2

* feat: update roadmap

Author: dhsorens

CompPoly/Data/List/Lemmas.lean

@@ -25,7 +25,7 @@ theorem append_getLast_dropLast {α : Type u} (l : List α) (h : l ≠ []) :
     | nil =>
       simp [dropLast, getLast]
     | cons hd' tl' =>
-      simp only [dropLast_cons₂, getLast]
+      simp only [dropLast_cons_cons, getLast]
       simp only [cons_append, cons.injEq, true_and]
       apply ih
 

CompPoly/Data/Vector/Basic.lean

@@ -8,6 +8,7 @@ import CompPoly.Data.List.Lemmas
 import Mathlib.Algebra.BigOperators.Fin
 import Mathlib.Algebra.Order.Star.Basic
 import Mathlib.Algebra.Order.Sub.Basic
+import Mathlib.Data.List.Fold
 import Mathlib.Data.Matrix.Mul
 import Mathlib.Tactic.Ring
 
@@ -147,8 +148,17 @@ lemma dotProduct_cons [AddCommMonoid R] [Mul R] (a : R) (b : Vector R n) (c : R)
   rw [zipWith_cons]
   simp_rw [foldl_eq_toList_foldl]
   rw [cons_toList_eq_List_cons]
-  rw [List.foldl_eq_of_comm' (hf:=by exact fun a b c ↦ add_right_comm a b c)]
-  rw [@AddCommMonoid.add_comm]
+  have h : ∀ (init : R) (L : List R),
+      List.foldl (fun x1 x2 => x1 + x2) init L = init + List.foldl (fun x1 x2 => x1 + x2) 0 L := by
+    intro init L
+    induction L generalizing init with
+    | nil => simp
+    | cons x xs ih =>
+      show List.foldl _ (init + x) xs = init + List.foldl _ (0 + x) xs
+      rw [ih (init + x), ih (0 + x), _root_.zero_add, _root_.add_assoc]
+  rw [List.foldl_cons]
+  show List.foldl _ (0 + a * c) _ = _
+  rw [_root_.zero_add, h]
 
 /-- A matrix represented as iterated vectors in row-major order.
 `m` is the number of rows, and `n` is the number of columns -/

CompPoly/Fields/Binary/AdditiveNTT/NovelPolynomialBasis.lean

@@ -1331,7 +1331,7 @@ lemma degree_Xⱼ (ℓ : ℕ) (h_ℓ : ℓ ≤ r) (j : Fin (2 ^ ℓ)) :
         Nat.cast_pow, Nat.cast_ofNat, CharP.cast_eq_zero, hF₂.out]
       -- ⊢ ↑(↑j >>> ↑i % 2) * 2 ^ ↑i = if ↑j >>> ↑i % 2 = 1 then 2 ^ ↑i else 0
       by_cases h: (j.val >>> i.val) % 2 = 1
-      · simp only [h, Nat.cast_one, one_mul, ↓reduceIte]; rfl
+      · simp only [h, Nat.cast_one, one_mul, ↓reduceIte]
       · simp only [h, if_false];
         have h_0: (j.val >>> i.val) % 2 = 0 := by
           exact Nat.mod_two_ne_one.mp h

CompPoly/Fields/Binary/BF128Ghash/Basic.lean

@@ -189,7 +189,8 @@ def root : BF128Ghash := AdjoinRoot.root ghashPoly
 theorem root_satisfies_poly : root^128 + root^7 + root^2 + root + 1 = 0 := by
   unfold root ghashPoly
   have h := AdjoinRoot.eval₂_root ghashPoly
-  simp only [ghashPoly, eval₂_add, eval₂_X, eval₂_one] at h
+  unfold ghashPoly at h
+  simp only [eval₂_add, eval₂_X, eval₂_one] at h
   erw [eval₂_pow, eval₂_X, eval₂_pow, eval₂_X, eval₂_pow, eval₂_X] at h
   exact h
 

CompPoly/Fields/Binary/BF128Ghash/Prelude.lean

@@ -214,7 +214,7 @@ lemma toPoly_one_shiftLeft {w : Nat} (n : Nat) (h : n < w) :
 
 -- Main Proof
 lemma ghashPoly_eq_P_val : ghashPoly = toPoly P_val := by
-  rw [ghashPoly, P_val]
+  unfold ghashPoly P_val
   repeat rw [toPoly_xor]
   rw [toPoly_one_shiftLeft (h := by omega), toPoly_one_shiftLeft (h := by omega),
     toPoly_one_shiftLeft (h := by omega), toPoly_one_shiftLeft (h := by omega)]
@@ -443,7 +443,8 @@ private theorem toPoly_mulByP_Nat (x : B128) :
   rw [toPoly_ofNat_shiftLeft_to256 x 2 (by omega)]
   rw [toPoly_ofNat_shiftLeft_to256 x 7 (by omega)]
   rw [toPoly_ofNat_shiftLeft_to256 x 128 (by omega)]
-  rw [← ghashPoly_eq_P_val, ghashPoly]
+  rw [← ghashPoly_eq_P_val]
+  unfold ghashPoly
   ring
 
 /-- Soundness of the kernel-efficient square-step checker. -/

CompPoly/Fields/Binary/Tower/Abstract/Algebra.lean

@@ -168,7 +168,7 @@ theorem towerAlgebraMap_assoc : ∀ r mid l : ℕ, (h_l_le_mid : l ≤ mid) →
 **Formalization of Cross-Level Algebra** : For any `k ≤ τ`, `BTField τ` is an
 algebra over `BTField k`.
 -/
-instance : AlgebraTower (BTField) where
+noncomputable instance : AlgebraTower (BTField) where
   algebraMap := towerAlgebraMap
   commutes' := by
     intro i j h r x

CompPoly/Fields/Binary/Tower/Support/LinearIndependentFin2.lean

@@ -26,7 +26,7 @@ variable {v : ι → V} {s t : Set ι} {x y : V}
 
 theorem linearIndependent_fin2' {f : Fin 2 → V} :
     LinearIndependent K f ↔ f 0 ≠ 0 ∧ ∀ a : K, a • f 0 ≠ f 1 := by
-  rw [linearIndependent_fin_succ', linearIndependent_unique_iff, Set.range_unique,
+  rw [linearIndependent_finSucc', linearIndependent_unique_iff, Set.range_unique,
     Submodule.mem_span_singleton,
     not_exists]
   rw [show Fin.init f default = f 0 by rfl]

CompPoly/Multivariate/MvPolyEquiv/Instances.lean

@@ -123,9 +123,9 @@ lemma map_one : fromCMvPolynomial (1 : CMvPolynomial n R) = 1 := by
   · have finsupp_m_eq_one : CMvMonomial.ofFinsupp m = CMvMonomial.zero := by
       rw [g']
       unfold CMvMonomial.ofFinsupp CMvMonomial.zero
-      ext i h
-      simp only [Nat.zero_eq, Finsupp.coe_mk]
-      grind
+      ext i hi
+      show (Vector.ofFn (⇑(0 : Fin n →₀ ℕ)))[i] = (Vector.replicate n 0)[i]
+      simp only [Finsupp.coe_zero, Pi.zero_apply, Vector.getElem_ofFn, Vector.getElem_replicate]
     rw [finsupp_m_eq_one]
     have one_one_get₁ :
       ({(CMvMonomial.zero, 1)} : Unlawful n R)[(@CMvMonomial.zero n)]?.getD 0 = One.one := by
@@ -387,7 +387,9 @@ lemma fromCMvPolynomial_C (r : R) :
     unfold C Lawful.C coeff Unlawful.C MonoR.C
     simp only [hr, ite_false]
     have ofFinsupp_zero : CMvMonomial.ofFinsupp (0 : Fin n →₀ ℕ) = CMvMonomial.zero := by
-      unfold CMvMonomial.ofFinsupp CMvMonomial.zero; ext i hi; grind
+      unfold CMvMonomial.ofFinsupp CMvMonomial.zero; ext i hi
+      show (Vector.ofFn (⇑(0 : Fin n →₀ ℕ)))[i] = (Vector.replicate n 0)[i]
+      simp only [Finsupp.coe_zero, Pi.zero_apply, Vector.getElem_ofFn, Vector.getElem_replicate]
     by_cases hm : (0 : Fin n →₀ ℕ) = m
     · subst hm; rw [if_pos rfl]
       erw [ExtTreeMap.getElem?_ofList_of_mem

CompPoly/Univariate/Raw/Proofs.lean

@@ -323,7 +323,8 @@ theorem double_sum_eq [LawfulBEq R] (p q r : CPolynomial.Raw R) (n : ℕ) :
                   = ∑ i ∈ Finset.range (n + 1),
                       ∑ j ∈ Finset.Ico i (n + 1),
                           p.coeff i * q.coeff (j - i) * r.coeff (n - j) := by
-            rw [ Finset.range_eq_Ico, Finset.sum_Ico_Ico_comm ]
+            simp_rw [Finset.range_eq_Ico]
+            rw [Finset.sum_Ico_Ico_comm]
           convert h_interchange using 2
           rw [ Finset.sum_Ico_eq_sum_range ]
           simp +decide [ Nat.sub_add_comm ( Finset.mem_range_succ_iff.mp ‹_› ) ]

ROADMAP.md

@@ -8,8 +8,8 @@ CompPoly aims to be the premier formally verified library for computable polynom
 
 1. Zero `sorry`s in all shipped modules.
 1. Complete core API for `CPolynomial`, `CMvPolynomial`, `CMlPolynomial`, including evaluation + interpolation + conversions.
-1. At least one "fast path" implemented + proven correct (FFT/NTT multiplication OR fast multilinear transforms).
-<!-- 1. Benchmarks exist for core ops and are reproducible (CI integration optional for v1.0). -->
+1. ✅ At least one "fast path" implemented + proven correct (FFT/NTT multiplication OR fast multilinear transforms). *(radix-2 NTT / `NTTFast` univariate multiplication)*
+1. Benchmarks exist for core ops and are reproducible (`lake exe CompPolyBench`; CI runs benchmarks and uploads reports).
 <!-- 1. Property tests exist for core ops (eval, mul, interpolation). -->
 1. Proof ergonomics baseline: common operations (add, mul, eval) mostly simp/grind-driven, documented.
 1. At least one real integration example (ArkLib or RT extraction exemplar) demonstrating use as a dependency.
@@ -66,18 +66,21 @@ CompPoly aims to be the premier formally verified library for computable polynom
    - 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](https://github.com/erdkocak) and [doran2728](https://github.com/doran2728) have communicated they will be working on this.
+   - ✅ 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**
-   - Implement batch evaluation at multiple points
+   - ✅ 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
    - Optimize for common ZK evaluation patterns
 
@@ -86,7 +89,12 @@ CompPoly aims to be the premier formally verified library for computable polynom
    - ✅ Prove equivalence between fast and spec implementations
    - 🔄 Add performance guarantees and complexity proofs (done in comments, formal benchmarking still TODO)
 
-6. **Bivariate polynomial operations**
+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)` and evaluate whether a more specialized representation is beneficial
    - Efficient factorization algorithms for bivariate polynomials
    - Integration with existing `CMvPolynomial 2 R` with equivalence proofs