Skip to content

Home

Jump to bottom
erdkocak edited this page Mar 28, 2026 · 3 revisions

Verified NTT for CompPoly

This project develops an efficient iterative radix-2 Number-Theoretic Transform (NTT) for the CompPoly library in Lean 4, with the long-term goal of full formal verification.

Project Summary

The Number-Theoretic Transform is a finite-field analogue of the Fast Fourier Transform. It is a core building block for fast polynomial multiplication, which is important in cryptography and other algebraic computations.

Our project focuses on:

  • defining NTT domains with primitive roots of unity
  • implementing forward and inverse iterative radix-2 NTTs
  • building an NTT-based fast polynomial multiplication pipeline
  • structuring the code for later formal correctness proofs in Lean 4

Current Status

The current implementation includes:

  • Domain.lean for radix-2 NTT domain parameters
  • Forward.lean for forward NTT specification and iterative implementation
  • Inverse.lean for inverse NTT specification and iterative implementation
  • FastMul.lean for NTT-based polynomial multiplication
  • test and benchmark files for validation over the KoalaBear field

The project is executable and benchmarked. Full correctness proofs are still in progress.

Pages

Team

  • Salih Erdem Koçak
  • Doran Pamukçu

Advisor

  • Doğan Ulus

Clone this wiki locally