NTT-based univariate multiplication by erdkocak · Pull Request #174 · Verified-zkEVM/CompPoly

erdkocak · 2026-03-21T18:42:00Z

Add an NTT domain carrying the transform size, primitive root, and normalization data
Define direct forward and inverse NTT specs
Implement iterative radix-2 forward and inverse transforms
Compose them into an NTT-based multiplication pipeline
Add executable tests for forward, inverse, and multiplication
Add benchmarks for the fast multiplication path
Prove forwardImpl = forwardSpec
Prove inverseImpl = inverseSpec
Prove fastMulImpl = p * q

n^2 ntt implementation, some basic tests

Refactor NTT butterfly iterations & remove redundant input arrays and padding

Improve NTT benchmark sweep and dynamic domain selection

Split univariate NTT tests by module

Minor cleanup

github-actions · 2026-03-21T18:59:06Z

🤖 Gemini PR Summary

Core Components

Domain structure manages radix-2 NTT parameters: primitive roots of unity, domain size constraints, and normalization factors.
Formal specifications for forward and inverse transforms provided alongside iterative radix-2 implementations.
Formalization of bit-reversal permutations and butterfly operations for Cooley-Tukey and Gentleman-Sande patterns.
Fast multiplication pipeline utilizing pointwise NTT multiplication, including automatic domain size selection and polynomial truncation.
Integration into the CompPoly library for univariate polynomial arithmetic.

Status of Proofs

CRITICAL: This PR adds several sorry placeholders for fundamental correctness theorems.
Proofs relating iterative implementations to high-level specifications (e.g., forwardImpl = forwardSpec and inverseImpl = inverseSpec) are incomplete.
The final correctness proof relating the NTT-based multiplication pipeline (fastMulImpl) to standard polynomial multiplication is marked with sorry.

Testing and Benchmarking

Executable tests using #guard verify NTT implementations against concrete cases in the KoalaBear field.
Benchmarking utilities measure the performance of NTT-based multiplication against standard methods.
Automated script identifies the efficiency crossover point where the NTT-based approach outperforms naive multiplication.

Statistics

Metric	Count
📝 Files Changed	11
✅ Lines Added	680
❌ Lines Removed	0

Lean Declarations

✏️ **Added:** 41 declaration(s)

theorem fastMulSpec_eq_mul (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean
def testBits32 : Fin (KoalaBear.twoAdicity + 1) in tests/CompPolyTests/Univariate/NTT/Common.lean
def testDomain32 : Domain KoalaBear.Field where in tests/CompPolyTests/Univariate/NTT/Common.lean
def bestLogN (requiredLen : Nat) : Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
theorem forwardImpl_correct (D : Domain R) (p : CPolynomial.Raw R) : in CompPoly/Univariate/NTT/Forward.lean
def q : CPolynomial.Raw KoalaBear.Field in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def testLogN32 : Nat in tests/CompPolyTests/Univariate/NTT/Common.lean
def requiredLength (p q : CPolynomial.Raw R) : Nat in CompPoly/Univariate/NTT/Domain.lean
def bitRevPermute (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
def benchSizes : Array Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def bestDomainForLength? (requiredLen : Nat) : Option (Domain KoalaBear.Field) in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def inverseSpec (D : Domain R) (v : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
def testDomain64 : Domain KoalaBear.Field where in tests/CompPolyTests/Univariate/NTT/Common.lean
def avgMsString (totalMs reps : Nat) : String in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def timeRepeated {α : Type} (reps : Nat) (f : Unit → α) : IO (Nat × α) in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def normalize (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
def mkPoly (n seed : Nat) : CPolynomial.Raw KoalaBear.Field in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def testLogN : Nat in tests/CompPolyTests/Univariate/NTT/Common.lean
def testLogN64 : Nat in tests/CompPolyTests/Univariate/NTT/Common.lean
def bitRevPermute (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
def butterflyStage (D : Domain R) (stage : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
def truncate (m : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/NTT/Domain.lean
def p : CPolynomial.Raw KoalaBear.Field in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def bitRevNat : Nat → Nat → Nat in CompPoly/Univariate/NTT/Forward.lean
theorem fastMulSpec_coeff (D : Domain R) (p q : CPolynomial.Raw R) (i : Nat) : in CompPoly/Univariate/NTT/FastMul.lean
def fits (D : Domain R) (p q : CPolynomial.Raw R) : Prop in CompPoly/Univariate/NTT/Domain.lean
def repeatsFor (n : Nat) : Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def runStages (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
theorem inverseImpl_correct (D : Domain R) (v : Array R) : in CompPoly/Univariate/NTT/Inverse.lean
def runStages (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
def checkSize : Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def testBits : Fin (KoalaBear.twoAdicity + 1) in tests/CompPolyTests/Univariate/NTT/Common.lean
def testDomain : Domain KoalaBear.Field where in tests/CompPolyTests/Univariate/NTT/Common.lean
def inttAt (D : Domain R) (v : Array R) (k : D.Idx) : R in CompPoly/Univariate/NTT/Inverse.lean
def testBits64 : Fin (KoalaBear.twoAdicity + 1) in tests/CompPolyTests/Univariate/NTT/Common.lean
theorem fastMulImpl_correct (D : Domain R) (p q : CPolynomial.Raw R) : in CompPoly/Univariate/NTT/FastMul.lean
def inverseImpl (D : Domain R) (v : Array R) : CPolynomial.Raw R in CompPoly/Univariate/NTT/Inverse.lean
abbrev Idx (D : Domain R) in CompPoly/Univariate/NTT/Domain.lean
def butterflyStage (D : Domain R) (stage : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
def speedupString (nttMs rawMs : Nat) : String in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
theorem fastMulImpl_eq_mul (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean

sorry Tracking

❌ **Added:** 5 `sorry`(s)

theorem fastMulSpec_eq_mul (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean (L63)
theorem forwardImpl_correct (D : Domain R) (p : CPolynomial.Raw R) : in CompPoly/Univariate/NTT/Forward.lean (L79)
theorem fastMulSpec_coeff (D : Domain R) (p q : CPolynomial.Raw R) (i : Nat) : in CompPoly/Univariate/NTT/FastMul.lean (L59)
theorem fastMulImpl_eq_mul (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean (L67)
theorem inverseImpl_correct (D : Domain R) (v : Array R) : in CompPoly/Univariate/NTT/Inverse.lean (L81)

🎨 **Style Guide Adherence**

There are more than 20 violations in this diff. They are grouped by rule below:

Documentation Standards
- Rule: "Every definition and major theorem should have a docstring." (39 violations)
  - Domain.lean (line 56): def requiredLength (p q : CPolynomial.Raw R) : Nat :=
  - Forward.lean (line 33): def bitRevNat : Nat → Nat → Nat
  - Benchmark.lean (line 27): def bestLogN (requiredLen : Nat) : Nat :=
- Rule: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references." (8 violations: All new files lack Notation and References sections)
  - Domain.lean (line 10)
  - FastMul.lean (line 11)
  - Forward.lean (line 8)
Syntax and Formatting
- Rule: "Avoid parentheses where possible. Use <| (pipe left) and |> (pipe right) to reduce nesting." (11 violations)
  - Domain.lean (line 27): natCast_ne_zero : (((2 ^ logN : Nat) : R) ≠ 0)
  - Forward.lean (line 27): ... D.omega ^ ((k : Nat) * (j : Nat))
  - Benchmark.lean (line 69): s!"{(Float.ofNat totalMs) / (Float.ofNat reps)}"
- Rule: "Prefer fun x ↦ ... over λ x, ...." (10 violations: The guide specifies the ↦ delimiter)
  - FastMul.lean (line 26): Array.ofFn (fun i : D.Idx => a.getD i.1 0 * b.getD i.1 0)
  - Forward.lean (line 31): Array.ofFn (fun k : D.Idx => nttAt D a k)
  - Benchmark.lean (line 99): (fun _ => FastMul.fastMulImpl benchDomain p q)
- Rule: "Indentation: Use 2 spaces for indentation." (5 violations: Unnecessary indentation of module docstring content)
  - Benchmark.lean (line 9): # Univariate Multiplication Benchmark
  - Common.lean (line 9): # Univariate NTT Test Helpers
  - FastMul.lean (line 9 - tests): # Univariate NTT FastMul Tests

📄 **Per-File Summaries**

CompPoly.lean: This update expands the CompPoly library by importing new modules related to univariate Lagrange interpolation and the Number Theoretic Transform (NTT), including its application for fast multiplication. No new theorems or proofs are implemented directly in this file, and no sorry placeholders are introduced.
CompPoly/Univariate/NTT/Domain.lean: This file introduces the Domain structure and associated definitions to represent radix-2 Number Theoretic Transform (NTT) parameters, including roots of unity and domain size constraints. It also provides helper functions for polynomial truncation and determining the required domain size for convolutions. No sorry or admit placeholders are included.
CompPoly/Univariate/NTT/FastMul.lean: This new file defines the specification and implementation pipelines for fast polynomial multiplication using Number Theoretic Transforms (NTT), including the pointwise multiplication of transformed arrays. It introduces the fastMulSpec and fastMulImpl definitions and proves the implementation's correctness relative to the specification; however, the final proofs relating these functions to standard polynomial multiplication are currently marked with sorry.
CompPoly/Univariate/NTT/Inverse.lean: This file introduces definitions and an implementation for the Inverse Number Theoretic Transform (INTT), including a direct formula specification and an iterative radix-2 butterfly algorithm. It provides several helper functions for bit-reversal and normalization alongside a correctness theorem relating the implementation to the specification, which currently contains a sorry placeholder.
tests/CompPolyTests.lean: This update expands the univariate polynomial test suite by integrating new test modules for Number Theoretic Transform (NTT) operations, specifically covering forward transforms, inverse transforms, and fast multiplication. No new theorems, definitions, or sorry placeholders are introduced in this file.
tests/CompPolyTests/Univariate/NTT/Common.lean: This new file defines shared helper constants and Domain instances for the KoalaBear field to support univariate NTT testing. It introduces concrete definitions and proofs for domain properties across multiple sizes, including primitive root verifications, without any sorry placeholders.
tests/CompPolyTests/Univariate/NTT/FastMul.lean: This file introduces a suite of executable tests for the Number Theoretic Transform (NTT) fast multiplication implementation. It uses #guard statements to verify that FastMul.fastMulImpl correctly matches standard polynomial multiplication across various concrete cases in the KoalaBear field. No sorry or admit placeholders are included.
tests/CompPolyTests/Univariate/NTT/Inverse.lean: This new test file introduces concrete executable checks for the univariate inverse Number Theoretic Transform (NTT). It uses #guard commands to verify that the inverse NTT implementation matches its specification across several test cases, and it contains no sorry or admit placeholders.
tests/CompPolyTests/Univariate/NTT/Forward.lean: This new test file introduces concrete executable checks for the forward Number Theoretic Transform (NTT) implementation. It uses #guard commands to verify consistency between the implementation and its specification across several polynomial examples, containing no sorry placeholders.
CompPoly/Univariate/NTT/Forward.lean: This file defines the forward Number Theoretic Transform (NTT) by providing both a direct mathematical specification and an iterative radix-2 implementation. It introduces necessary components such as bit-reversal permutations and butterfly stages, and includes a placeholder theorem forwardImpl_correct (marked with sorry) for the eventual proof of correctness.
tests/CompPolyTests/Univariate/NTT/Benchmark.lean: This file introduces a benchmarking suite to compare the performance of NTT-based polynomial multiplication against standard "raw" multiplication using the KoalaBear field. It defines several utility functions for performance measurement and NTT domain selection, concluding with an executable script that identifies the efficiency crossover point across various operand sizes.

Last updated: 2026-03-21 19:17 UTC.

Fix NTT test lint violations

dhsorens

at first glance, the code is clean and well-organized and spec looks to be right. Just a few comments for now

dhsorens · 2026-04-03T06:38:17Z

+def bitRevPermute (D : Domain R) (a : Array R) : Array R :=
+  Array.ofFn (fun i : D.Idx => a.getD (bitRevNat D.logN i.1) 0)
+
+/-- One butterfly stage of the iterative radix-2 transform. -/


it looks like bitRevPermute, butterflyStage, and runStages are nearly identical between Forward.lean and Inverse.lean. to avoid code duplication, it's probably a good idea to factor these into a shared definition (parametric over omega/omegaInv) in a shared file. you might want to put all the shared operations in there as well (e.g. including bitRevNat)

dhsorens · 2026-04-03T06:42:35Z

+namespace NTT
+namespace Inverse
+
+variable {R : Type*} [Field R]


it might be worth trying to weaken the field assumption, if possible. we can always generalize results once they're proved though so don't worry too much about this right away

dhsorens · 2026-04-03T06:56:16Z

+/-- Required convolution length for multiplying `p` and `q`. -/
+def requiredLength (p q : CPolynomial.Raw R) : Nat :=
+  p.trim.size + q.trim.size - 1
+


note that in Nat, 0 - 1 = 0 which can lead to undesirable behavior. worth checking that this underflow won't affect the rest

github-actions · 2026-04-29T08:50:20Z

🤖 PR Summary

⚠️ PR title does not follow conventional commit format type[(scope)]: subject. Got: NTT-based univariate multiplication

NTT Framework

Defines a Domain structure for radix-2 Number Theoretic Transforms (NTT), managing transform sizes, primitive roots, and normalization factors. Implements iterative forward and inverse transforms using bit-reversal permutations and butterfly stages.

Verification and Discrepancy

Formalizes the proof forwardImpl = forwardSpec. A discrepancy exists regarding the verification status: while the PR body marks proofs for inverseImpl = inverseSpec and fastMulImpl = p * q as pending, the implementation analysis indicates that the full pipeline, including fastMulImpl_eq_mul, is complete and contains no sorry or admit placeholders.

Testing and Benchmarking

Provides executable tests and benchmarks over the KoalaBear field for domains of 8, 32, and 64 points. These tools facilitate performance comparison between NTT-based and naive multiplication.

Statistics

Metric	Count
📝 Files Changed	12
✅ Lines Added	2129
❌ Lines Removed	0

Lean Declarations

✏️ **Added:** 146 declaration(s)

theorem forwardStageSpec_eq_forwardStagePureSpec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
theorem bitRevNat_even (bits b : Nat) : in CompPoly/Univariate/NTT/Transform.lean
theorem butterflyStageSpec_forwardMathStageSpec_succ in CompPoly/Univariate/NTT/Forward.lean
private theorem natDegree_toPoly_lt_of_trim_size_le in CompPoly/Univariate/NTT/FastMul.lean
private theorem butterflyInnerStep_forwardMathPairsSpec_succ in CompPoly/Univariate/NTT/Forward.lean
theorem inverseImpl_correct (D : Domain R) (v : Array R) : in CompPoly/Univariate/NTT/Inverse.lean
theorem normalize_forwardSpec_inverse_eq_inverseSpec (D : Domain R) (v : Array R) : in CompPoly/Univariate/NTT/Inverse.lean
private def stageTwiddle (D : Domain R) (stage : Nat) : R in CompPoly/Univariate/NTT/Forward.lean
@[inline] def omegaInv (D : Domain R) : R in CompPoly/Univariate/NTT/Domain.lean
def forwardStagePureSpec (D : Domain R) (completed : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
def mkPoly (n seed : Nat) : CPolynomial.Raw KoalaBear.Field in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
private theorem pointwise_forwardSpec_eq_forwardSpec_mul_of_natDegree_lt in CompPoly/Univariate/NTT/FastMul.lean
private theorem pointwise_getD_eq_zero_of_left_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
def timeRepeated {α : Type} (reps : Nat) (f : Unit → α) : IO (Nat × α) in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
private theorem kernel_term_eq (D : Domain R) {i : Nat} (hi : i < D.n) (j k : Nat) : in CompPoly/Univariate/NTT/FastMul.lean
theorem fastMulImpl_correct (D : Domain R) (p q : CPolynomial.Raw R) : in CompPoly/Univariate/NTT/FastMul.lean
@[inline] def node (D : Domain R) (i : D.Idx) : R in CompPoly/Univariate/NTT/Domain.lean
def butterflyBlockStep in CompPoly/Univariate/NTT/Transform.lean
@[simp] theorem forwardStageSpec_succ (D : Domain R) (stage : Nat) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem forwardMathValueAt_succ_lower in CompPoly/Univariate/NTT/Forward.lean
theorem forwardImpl_correct (D : Domain R) (p : CPolynomial.Raw R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem pointwise_getD_eq_zero_of_right_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
private theorem butterflyBlockStep_forwardMathBlocksSpec_succ in CompPoly/Univariate/NTT/Forward.lean
def testBits32 : Fin (KoalaBear.twoAdicity + 1) in tests/CompPolyTests/Univariate/NTT/Common.lean
private theorem fastMulSpec_coeff_eq_zero_of_left_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
@[inline] def nInv (D : Domain R) : R in CompPoly/Univariate/NTT/Domain.lean
theorem forwardMathStageSpec_final_eq_forwardSpec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
@[simp] theorem size_forwardStageSpec (D : Domain R) (completed : Nat) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private def forwardMathBlocksSpec in CompPoly/Univariate/NTT/Forward.lean
def testLogN32 : Nat in tests/CompPolyTests/Univariate/NTT/Common.lean
private theorem forwardMathPairsSpec_get_upper_next in CompPoly/Univariate/NTT/Forward.lean
def avgMsString (totalMs reps : Nat) : String in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def bestDomainForLength? (requiredLen : Nat) : Option (Domain KoalaBear.Field) in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def bitRevPermute (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Transform.lean
private theorem foldl_range_eq_rec {α : Type*} (f : Nat → α → α) (x : α) : in CompPoly/Univariate/NTT/Transform.lean
private theorem butterfly_lower_div_half (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
def inverse (D : Domain R) : Domain R where in CompPoly/Univariate/NTT/Domain.lean
def testDomain : Domain KoalaBear.Field where in tests/CompPolyTests/Univariate/NTT/Common.lean
private theorem natDegree_toPoly_lt_trim_size_of_pos in CompPoly/Univariate/NTT/FastMul.lean
theorem bitRevNat_odd (bits b : Nat) : in CompPoly/Univariate/NTT/Transform.lean
private theorem foldl_range_eq_rec_fst {α β : Type*} in CompPoly/Univariate/NTT/Transform.lean
private theorem mul_coeff_eq_zero_of_requiredLength_le in CompPoly/Univariate/NTT/FastMul.lean
private theorem forwardSpec_get_eq_eval_of_natDegree_lt in CompPoly/Univariate/NTT/FastMul.lean
private theorem forwardMathValueAt_succ_upper in CompPoly/Univariate/NTT/Forward.lean
private theorem omega_pow_add_domain_mul (D : Domain R) (e k : Nat) : in CompPoly/Univariate/NTT/Forward.lean
def truncate (m : Nat) (p : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/NTT/Domain.lean
def normalize (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
private theorem forwardMathBlocksSpec_zero in CompPoly/Univariate/NTT/Forward.lean
private theorem butterfly_upper_lt_of_lower_lt_domain in CompPoly/Univariate/NTT/Forward.lean
def testDomain32 : Domain KoalaBear.Field where in tests/CompPolyTests/Univariate/NTT/Common.lean
private theorem stageTwiddle_eq_stride in CompPoly/Univariate/NTT/Forward.lean
@[simp] theorem size_butterflyInnerStep in CompPoly/Univariate/NTT/Transform.lean
def butterflyInnerStep in CompPoly/Univariate/NTT/Transform.lean
def testLogN64 : Nat in tests/CompPolyTests/Univariate/NTT/Common.lean
private theorem eq_lower_or_upper_of_block_pair in CompPoly/Univariate/NTT/Forward.lean
def repeatsFor (n : Nat) : Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
private theorem omega_pow_domain_half_eq_neg_one in CompPoly/Univariate/NTT/Forward.lean
abbrev Idx (D : Domain R) in CompPoly/Univariate/NTT/Domain.lean
private theorem butterflyBlockStep_aux_forwardMathPairsSpec in CompPoly/Univariate/NTT/Forward.lean
def testLogN : Nat in tests/CompPolyTests/Univariate/NTT/Common.lean
@[simp] theorem forwardStagePureSpec_succ (D : Domain R) (stage : Nat) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
theorem runStages_bitRevPermute_eq_forwardStageSpec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
theorem bitRevNat_lt (bits i : Nat) : bitRevNat bits i < 2 ^ bits in CompPoly/Univariate/NTT/Transform.lean
private theorem forwardMathPairsSpec_get_unchanged in CompPoly/Univariate/NTT/Forward.lean
def testBits : Fin (KoalaBear.twoAdicity + 1) in tests/CompPolyTests/Univariate/NTT/Common.lean
private def forwardMathPairsSpec in CompPoly/Univariate/NTT/Forward.lean
def testDomain64 : Domain KoalaBear.Field where in tests/CompPolyTests/Univariate/NTT/Common.lean
@[inline] def pointwiseMul (D : Domain R) (a b : Array R) : Array R in CompPoly/Univariate/NTT/FastMul.lean
theorem fastMulSpec_eq_mul (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean
private theorem butterflyStageSpec_aux_forwardMathBlocksSpec in CompPoly/Univariate/NTT/Forward.lean
@[inline] def fastMulSpec (D : Domain R) (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/NTT/FastMul.lean
def speedupString (nttMs rawMs : Nat) : String in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
@[simp] def n (D : Domain R) : Nat in CompPoly/Univariate/NTT/Domain.lean
private theorem butterfly_lower_div_block (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
def bestLogN (requiredLen : Nat) : Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
def checkSize : Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
private theorem omegaInv_pow_mul_eq (D : Domain R) {i : Nat} (hi : i < D.n) (k : Nat) : in CompPoly/Univariate/NTT/FastMul.lean
private theorem coeff_truncate (m : Nat) (a : CPolynomial.Raw R) (i : Nat) : in CompPoly/Univariate/NTT/FastMul.lean
theorem fastMulSpec_coeff (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean
private theorem stage_stride_half_eq_domain_half in CompPoly/Univariate/NTT/Forward.lean
private def forwardMathValueAt (D : Domain R) (completed : Nat) (a : Array R) (idx : Nat) : R in CompPoly/Univariate/NTT/Forward.lean
@[simp] theorem forwardStagePureSpec_zero (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem forwardSpec_getD_eq_zero_of_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
def butterflyStage (D : Domain R) (stage : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Transform.lean
private theorem kernel_sum_eq_if (D : Domain R) (i j : D.Idx) : in CompPoly/Univariate/NTT/FastMul.lean
private theorem size_butterflyBlockStep_aux in CompPoly/Univariate/NTT/Transform.lean
@[simp] theorem size_pointwiseMul (D : Domain R) (a b : Array R) : in CompPoly/Univariate/NTT/FastMul.lean
private theorem dvd_add_sub_iff_fin_eq (D : Domain R) (i j : D.Idx) : in CompPoly/Univariate/NTT/FastMul.lean
@[simp] theorem size_forwardStagePureSpec (D : Domain R) (completed : Nat) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem butterfly_upper_div_half (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
private theorem forwardMathPairsSpec_half in CompPoly/Univariate/NTT/Forward.lean
theorem butterflyStage_eq_butterflyStageSpec in CompPoly/Univariate/NTT/Transform.lean
theorem runStages_eq_rec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Transform.lean
private theorem forwardMathPairsSpec_get_lower_next in CompPoly/Univariate/NTT/Forward.lean
theorem bitRevNat_odd_or (bits b : Nat) : in CompPoly/Univariate/NTT/Transform.lean
private theorem omega_sum_pow_mul_eq_if_dvd (D : Domain R) (m : Nat) : in CompPoly/Univariate/NTT/FastMul.lean
private theorem raw_eval_mul (x : R) (p q : CPolynomial.Raw R) : in CompPoly/Univariate/NTT/FastMul.lean
private theorem forwardMathPairsSpec_get_lower_current in CompPoly/Univariate/NTT/Forward.lean
@[simp] lemma n_pos (D : Domain R) : 0 < D.n in CompPoly/Univariate/NTT/Domain.lean
private theorem butterfly_upper_mod_half (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
def butterflyStageSpec (D : Domain R) (stage : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Transform.lean
@[simp] lemma n_ne_zero (D : Domain R) : D.n ≠ 0 in CompPoly/Univariate/NTT/Domain.lean
def q : CPolynomial.Raw KoalaBear.Field in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
theorem forwardMathStageSpec_zero (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem butterfly_upper_div_block (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
private theorem fastMulSpec_coeff_eq_zero_of_right_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
theorem forwardStagePureSpec_eq_forwardMathStageSpec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
def runStages (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Transform.lean
@[simp] theorem size_forwardSpec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem mul_coeff_eq_zero_of_right_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
private theorem butterfly_lower_mod_half (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
theorem size_butterflyStageSpec (D : Domain R) (stage : Nat) (a : Array R) (ha : a.size = D.n) : in CompPoly/Univariate/NTT/Transform.lean
private theorem coeff_zero_of_trim_size_le in CompPoly/Univariate/NTT/FastMul.lean
private theorem mul_coeff_eq_zero_of_left_trim_size_zero in CompPoly/Univariate/NTT/FastMul.lean
private theorem butterfly_j_mod_blockSize (stage j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
def inverseImpl (D : Domain R) (v : Array R) : CPolynomial.Raw R in CompPoly/Univariate/NTT/Inverse.lean
@[simp] theorem forwardStageSpec_zero (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
private theorem butterfly_upper_mod_blockSize (stage block j : Nat) (hj : j < 2 ^ stage) : in CompPoly/Univariate/NTT/Forward.lean
def forwardStageSpec (D : Domain R) (completed : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
@[inline] def fastMulImpl (D : Domain R) (p q : CPolynomial.Raw R) : CPolynomial.Raw R in CompPoly/Univariate/NTT/FastMul.lean
@[simp] theorem size_butterflyBlockStep in CompPoly/Univariate/NTT/Transform.lean
@[simp] theorem size_normalize (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Inverse.lean
def testBits64 : Fin (KoalaBear.twoAdicity + 1) in tests/CompPolyTests/Univariate/NTT/Common.lean
private theorem inverse_forwardSpec_coeff_of_lt (D : Domain R) (a : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean
theorem fastMulImpl_eq_mul (D : Domain R) (p q : CPolynomial.Raw R) in CompPoly/Univariate/NTT/FastMul.lean
private theorem omega_pow_stage_stride_eq_neg_one in CompPoly/Univariate/NTT/Forward.lean
private theorem forwardMathPairsSpec_get_upper_current in CompPoly/Univariate/NTT/Forward.lean
def requiredLength (p q : CPolynomial.Raw R) : Nat in CompPoly/Univariate/NTT/Domain.lean
@[inline] def forwardSpec (D : Domain R) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
private theorem forwardMathBlocksSpec_final in CompPoly/Univariate/NTT/Forward.lean
def inverseSpec (D : Domain R) (v : Array R) : Array R in CompPoly/Univariate/NTT/Inverse.lean
def bitRevNat : Nat → Nat → Nat in CompPoly/Univariate/NTT/Transform.lean
def fits (D : Domain R) (p q : CPolynomial.Raw R) : Prop in CompPoly/Univariate/NTT/Domain.lean
private theorem size_butterflyStageSpec_aux in CompPoly/Univariate/NTT/Transform.lean
def p : CPolynomial.Raw KoalaBear.Field in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
theorem size_butterflyStage (D : Domain R) (stage : Nat) (a : Array R) (ha : a.size = D.n) : in CompPoly/Univariate/NTT/Transform.lean
private theorem inverseSpec_getD_eq_zero_of_getD_zero in CompPoly/Univariate/NTT/FastMul.lean
@[simp] theorem size_inverseSpec (D : Domain R) (v : Array R) : in CompPoly/Univariate/NTT/Inverse.lean
def forwardMathStageSpec (D : Domain R) (completed : Nat) (a : Array R) : Array R in CompPoly/Univariate/NTT/Forward.lean
private theorem forwardMathPairsSpec_zero in CompPoly/Univariate/NTT/Forward.lean
@[inline] def forwardImpl (D : Domain R) (p : CPolynomial.Raw R) : Array R in CompPoly/Univariate/NTT/Forward.lean
def inttAt (D : Domain R) (v : Array R) (k : D.Idx) : R in CompPoly/Univariate/NTT/Inverse.lean
def benchSizes : Array Nat in tests/CompPolyTests/Univariate/NTT/Benchmark.lean
theorem forwardStageSpec_final_eq_forwardSpec (D : Domain R) (a : Array R) : in CompPoly/Univariate/NTT/Forward.lean
@[inline] def nttAt (D : Domain R) (a : Array R) (k : D.Idx) : R in CompPoly/Univariate/NTT/Forward.lean
private theorem omega_pow_domain_mul (D : Domain R) (k : Nat) : in CompPoly/Univariate/NTT/Forward.lean

sorry Tracking

No sorrys were added, removed, or affected.

Lean Quality Signals

⚠️ #eval debug command left in code in tests/CompPolyTests/Univariate/NTT/Benchmark.lean (L92)

🎨 **Style Guide Adherence**

The reviewed code contains a large number of style guide violations (over 20). Below are the violations grouped by rule with representative examples.

Variable Conventions
- Rule: "Variable Conventions: m, n, k, ... : Natural numbers", "i, j, k, ... : Integers"
- Count: 50+
- Examples:
  - CompPoly/Univariate/NTT/Domain.lean:38: Using i for a Fin (Natural) index in node.
  - CompPoly/Univariate/NTT/FastMul.lean:34: Using i : Nat in omegaInv_pow_mul_eq.
  - CompPoly/Univariate/NTT/Transform.lean:40: Using i for a Nat in bitRevNat.
Documentation Standards (Docstrings)
- Rule: "Every definition and major theorem should have a docstring."
- Count: 45+
- Examples:
  - CompPoly/Univariate/NTT/FastMul.lean:244: fastMulImpl_correct (major theorem) lacks a docstring.
  - CompPoly/Univariate/NTT/Forward.lean:866: forwardImpl_correct lacks a docstring.
  - CompPoly/Univariate/NTT/Transform.lean:211: size_butterflyStageSpec lacks a docstring.
Tactic Mode Formatting
- Rule: "Place by at the end of the line preceding the tactic block. Indent the tactic block."
- Count: 60+
- Examples:
  - CompPoly/Univariate/NTT/Domain.lean:55: n_pos ... := by simp [n] (should be on a new line).
  - CompPoly/Univariate/NTT/Forward.lean:104: size_forwardStageSpec ... := by induction ....
  - CompPoly/Univariate/NTT/Transform.lean:107: ha := ha used inside a by block on the same line as the theorem signature.
Syntax and Formatting (Functions)
- Rule: "Functions: Prefer fun x ↦ ... over λ x, ...." (The project adheres to community guidelines preferring ↦ over => for math declarations).
- Count: 25+
- Examples:
  - CompPoly/Univariate/NTT/FastMul.lean:28: Array.ofFn (fun i : D.Idx => ...).
  - CompPoly/Univariate/NTT/Inverse.lean:30: Array.ofFn (fun k : D.Idx => ...).
Module Docstrings
- Rule: "Each file should start with a /-! ... -/ block containing a title, summary, notation, and references."
- Count: 8
- Examples:
  - CompPoly/Univariate/NTT/Domain.lean:8: Missing Notation and References sections.
  - CompPoly/Univariate/NTT/FastMul.lean:12: Missing Notation and References sections.
Delimiters
- Rule: "Delimiters: Avoid parentheses where possible."
- Count: 12
- Examples:
  - CompPoly/Univariate/NTT/Domain.lean:27: (((2 ^ logN : Nat) : R) ≠ 0) contains redundant nesting.
  - CompPoly/Univariate/NTT/FastMul.lean:157: ((D.n : Nat) : R) could be (D.n : Nat : R).
Line Length
- Rule: "Line Length: Keep lines under 100 characters."
- Count: 8
- Examples:
  - CompPoly/Univariate/NTT/Forward.lean:414: Signature of forwardMathPairsSpec_get_unchanged exceeds 100 characters.
  - CompPoly/Univariate/NTT/Transform.lean:140: Line length in butterflyStage_eq_butterflyStageSpec proof.
Tactic Argument Spacing
- Rule: "Operators: Put spaces on both sides of :, :=, and infix operators."
- Count: 4
- Examples:
  - CompPoly/Univariate/NTT/FastMul.lean:270: rw[fastMulImpl_correct] missing space before bracket.
  - CompPoly/Univariate/NTT/FastMul.lean:294: rw[fastMulImpl_correct] missing space.

📄 **Per-File Summaries**

CompPoly.lean: This update expands the CompPoly.lean module by importing several new submodules related to Number Theoretic Transform (NTT) functionality, including forward/inverse transforms and fast multiplication. These changes integrate NTT-based polynomial operations into the main library structure without adding any new theorems, definitions, or 'sorry' placeholders directly to this file.
CompPoly/Univariate/NTT/Domain.lean: Introduces the Domain structure and associated utility functions to define radix-2 Number Theoretic Transform (NTT) parameters, including primitive roots of unity and domain size. The file provides definitions for evaluation nodes and inverse domains, as well as basic lemmas and helpers for polynomial size calculations used in NTT operations.
CompPoly/Univariate/NTT/FastMul.lean: This file implements and proves the correctness of fast polynomial multiplication via the Number Theoretic Transform (NTT). It introduces definitions for pointwise multiplication and the fastMulImpl pipeline, along with new theorems such as fastMulImpl_eq_mul which formally verifies that the NTT-based implementation is equivalent to algebraic polynomial multiplication. No sorry or admit placeholders are included in the proofs.
CompPoly/Univariate/NTT/Forward.lean: This file defines the forward Number Theoretic Transform (NTT) through both a direct formula-based specification and an iterative radix-2 implementation. It introduces several intermediate stagewise definitions and provides a complete formal proof of the iterative algorithm's correctness relative to the NTT formula. No sorry or admit placeholders are used in the development.
CompPoly/Univariate/NTT/Inverse.lean: This new file defines the specification and implementation of the inverse Number Theoretic Transform (NTT), including a normalization step and a fast implementation entry point. It provides several theorems establishing the correctness of the implementation relative to its specification and the forward transform, with no sorry or admit placeholders.
CompPoly/Univariate/NTT/Transform.lean: This file introduces the core radix-2 NTT machinery, providing new definitions for bit-reversal permutations and iterative butterfly transformation stages. It establishes several theorems relating imperative array-based implementations to functional specifications and proves that the transformation stages preserve the size of the underlying evaluation arrays.
tests/CompPolyTests.lean: This change updates the test suite by importing new test modules for univariate Number Theoretic Transform (NTT) operations, including forward and inverse transforms and fast multiplication. No new theorems, definitions, or sorry placeholders are introduced in this file.
tests/CompPolyTests/Univariate/NTT/Benchmark.lean: This new benchmark file evaluates the performance of NTT-based univariate polynomial multiplication against raw multiplication using the KoalaBear field. It introduces utilities for domain selection, polynomial generation, and automated timing across a range of operand sizes to identify performance crossover points.
tests/CompPolyTests/Univariate/NTT/Common.lean: This new file introduces shared test helper definitions and concrete Domain instances for the KoalaBear field to be used in univariate Number Theoretic Transform (NTT) tests. It establishes several test domains of varying sizes (8, 32, and 64 points) and provides accompanying validity proofs without any sorry placeholders.
tests/CompPolyTests/Univariate/NTT/FastMul.lean: This file introduces a suite of concrete executable tests for the univariate Number Theoretic Transform (NTT) fast multiplication implementation. It utilizes #guard statements to verify the correctness of FastMul.fastMulImpl against standard polynomial multiplication across various test domains and input sizes.
tests/CompPolyTests/Univariate/NTT/Forward.lean: This new test file introduces concrete executable checks to verify that the forward Number Theoretic Transform (NTT) implementation matches its specification across various polynomial inputs and domains. It utilizes #guard commands for validation and contains no sorry or admit placeholders.
tests/CompPolyTests/Univariate/NTT/Inverse.lean: This new test file introduces concrete executable checks for the univariate inverse NTT implementation by verifying that the implementation aligns with its specification. It utilizes #guard statements to validate the inverse transform on specific input vectors and contains no sorry or admit placeholders.

Last updated: 2026-05-01 19:04 UTC.

Co-authored-by: Copilot <copilot@github.com>

erdkocak and others added 17 commits March 21, 2026 18:27

draft imp

94c2902

n^2 impl, and unit tests

7426cc0

move to array from eval vec

7bbb5bb

fast mul impl some tests and basic benchmark

fcc44e3

Merge pull request #1 from erdkocak/ntt

04a4665

n^2 ntt implementation, some basic tests

remove redundant inputArray usage from forward.lean

cc742e0

remove redundant padding from domain.lean

ba21fde

optimize the main for loop inside butterfly stages

5136d13

Merge pull request #3 from erdkocak/ntt-basic-fixes

e4885b1

Refactor NTT butterfly iterations & remove redundant input arrays and padding

benchmark updated

d728353

add authors

8a10675

Merge pull request #4 from erdkocak/benchmark-update

eda9f7d

Improve NTT benchmark sweep and dynamic domain selection

tests refactored into 3 files and a helper file

d79e0d0

Merge pull request #5 from erdkocak/ntt-tests-refactoring

b41dcc2

Split univariate NTT tests by module

comment fixes, redundant function removal

65ffb15

Merge pull request #6 from erdkocak/small-fixes

d19099a

Minor cleanup

Merge upstream/master into fork

e43b06a

erdkocak and others added 2 commits March 21, 2026 22:07

fix linter issues

a56b9a6

Merge pull request #7 from erdkocak/linter-fixes

51db7dd

Fix NTT test lint violations

dhsorens reviewed Apr 3, 2026

View reviewed changes

eliasjudin mentioned this pull request Apr 4, 2026

feat(univariate): add fixed-domain barycentric interpolation #184

Open

forwardImpl_correct proof

7c81b54

erdkocak and others added 4 commits May 1, 2026 20:48

refactoring common code of forward and inverse into transform

d35acc4

rest of the changes

9e892e3

inverseImpl_correct proof

d9366bd

completed the working proofs

6f4a280

Co-authored-by: Copilot <copilot@github.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

NTT-based univariate multiplication#174

NTT-based univariate multiplication#174
erdkocak wants to merge 24 commits intoVerified-zkEVM:masterfrom
erdkocak:master

erdkocak commented Mar 21, 2026 •

edited

Loading

Uh oh!

github-actions Bot commented Mar 21, 2026 •

edited

Loading

Uh oh!

dhsorens left a comment

Uh oh!

dhsorens Apr 3, 2026

Uh oh!

dhsorens Apr 3, 2026

Uh oh!

dhsorens Apr 3, 2026

Uh oh!

github-actions Bot commented Apr 29, 2026 •

edited

Loading

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

Conversation

erdkocak commented Mar 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

github-actions Bot commented Mar 21, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 Gemini PR Summary

Core Components

Status of Proofs

Testing and Benchmarking

Uh oh!

dhsorens left a comment

Choose a reason for hiding this comment

Uh oh!

dhsorens Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

dhsorens Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

dhsorens Apr 3, 2026

Choose a reason for hiding this comment

Uh oh!

github-actions Bot commented Apr 29, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

🤖 PR Summary

NTT Framework

Verification and Discrepancy

Testing and Benchmarking

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants

erdkocak commented Mar 21, 2026 •

edited

Loading

github-actions Bot commented Mar 21, 2026 •

edited

Loading

github-actions Bot commented Apr 29, 2026 •

edited

Loading