Skip to content

Project Plan

Jump to bottom
erdkocak edited this page Mar 28, 2026 · 1 revision

Project Plan

Main Objective

Deliver an efficient iterative radix-2 NTT implementation in Lean 4 and prepare the full correctness proof pipeline for it.

Work Packages

1. Domain Construction

Define the NTT domain and required proof obligations:

  • primitive root of unity
  • valid domain size
  • invertibility of the domain size in the field

2. Forward Transform

Implement:

  • a direct forward NTT specification
  • an iterative radix-2 forward transform

3. Inverse Transform

Implement:

  • a direct inverse NTT specification
  • an iterative inverse transform with normalization

4. Fast Multiplication

Implement fast polynomial multiplication using:

  • forward NTT
  • pointwise multiplication
  • inverse NTT

5. Testing and Benchmarking

Validate the implementation by:

  • comparing against naive multiplication
  • benchmarking over a range of input sizes
  • identifying the practical crossover point

6. Formal Verification

Prove the main correctness bridges:

  • forward implementation equals forward specification
  • inverse implementation equals inverse specification
  • fast multiplication specification equals standard multiplication
  • fast multiplication implementation equals fast multiplication specification

Current Progress

Completed or mostly completed:

  • NTT domain structure
  • forward transform implementation
  • inverse transform implementation
  • fast multiplication pipeline
  • benchmark and test setup

Still in progress:

  • full correctness proofs
  • proof of equivalence between iterative implementations and direct specifications

Risks

Main risks include:

  • proof complexity for summations and root-of-unity identities
  • proof complexity for bit-reversal and butterfly stages
  • balancing execution efficiency with proof-friendly definitions
  • Lean performance when reasoning about finite-field computations

Success Criteria

The project will be considered successful if:

  • the NTT pipeline works correctly on tested examples
  • the implementation is benchmarked and faster than naive multiplication at scale
  • the key correctness theorems are fully proved in Lean
  • the implementation remains kernel-safe and avoids untrusted shortcuts

Clone this wiki locally