Project Documentation

Project Documentation

Goal

The goal of this project is to build a kernel-safe and efficient NTT-based fast multiplication path for CompPoly in Lean 4.

We want the implementation to be:

• mathematically clean
• executable inside Lean
• suitable for full formal verification

Module Structure

The implementation is currently split into four main modules.

Domain

Domain.lean defines the parameters of a radix-2 NTT domain:

• transform size 2^logN
• primitive root of unity omega
• proof that omega is a primitive root
• proof that the domain size is invertible in the field

Forward Transform

Forward.lean contains:

• a direct mathematical NTT specification
• an iterative radix-2 butterfly implementation
• bit-reversal permutation support

Inverse Transform

Inverse.lean contains:

• a direct mathematical inverse NTT specification
• an iterative inverse transform
• final normalization by n⁻¹

Fast Multiplication

FastMul.lean contains the full multiplication pipeline:

1. forward transform of both inputs
2. pointwise multiplication in evaluation form
3. inverse transform
4. truncation back to the needed coefficient range

Methodology

Our methodology separates the code into two layers:

• Spec functions: direct mathematical definitions
• Impl functions: efficient executable implementations

This lets us:

• test the implementation against the specification
• benchmark the optimized version
• later prove that the implementation is equivalent to the specification

Testing and Validation

Validation currently relies on:

• unit-style test files under the test namespace
• direct comparisons between NTT-based multiplication and naive multiplication
• benchmark runs over the KoalaBear field

The benchmark results show that the NTT-based multiplication becomes significantly faster than naive multiplication for medium and large input sizes.

Importance

This work matters because verified polynomial multiplication is relevant for:

• formal verification of mathematical software
• cryptographic correctness
• reliable low-level algebraic infrastructure