Currently, the DFT integration test (integration_tests/verify_dft4.py) only validates the integer/real specialisation of MatExpr.dft 4, which happens to reduce to the Walsh-Hadamard Transform (all ±1 coefficients). This covers neither the general complex case ω = e^{-2πi/n} nor other sizes.
What needs to be tested:
- Code generation for
MatExpr.dft n where n > 2 and the twiddle factors are genuinely non-trivial (e.g., n=8 with ω = e^{-2πi/8})
- Verify that generated C code computes the correct DFT output for complex-valued inputs
- Test roundtrip property: applying DFT twice (with conjugate) should return a scaled input
Current state:
evalDFT (AlgebraicSemantics.lean:919) implements the generic formula y[k] = Σ ω^{kj} · x[j] over a parametric field element ω- Code generation (FRI/CodeGen.lean:235-243) emits placeholder
dft_n() function calls
- No concrete
ℂ binding or complex arithmetic in code generation
Testing approach:
- Create a reference DFT implementation (NumPy FFT or similar)
- Generate test vectors from random complex inputs using the reference implementation
- Add differential fuzzing: randomly generate inputs, compute reference output, compare against generated code
- Include both hand-crafted vectors (identity, constant, alternating patterns) and fuzzing-generated ones
- Verify roundtrip property: DFT(DFT*(x)) ≈ n·x within numerical tolerance
Missing pieces:
- Complex number representation in generated C (or using a fixed-point encoding for ℂ)
- Actual twiddle factor computation (
ω^k for ω = e^{-2πi/n})
- Test vectors with complex roots (or appropriate fixed-point approximations)
Note on DFT vs. WHT relationship:
For n=4, the DFT with a primitive 4th root of unity mathematically simplifies to the Walsh-Hadamard Transform (all ±1 coefficients). The current integration test exploits this equivalence by using WHT as a reference. Once complex DFT code generation is implemented, the DFT_4 implementation should be verified to produce WHT_4 outputs, confirming the mathematical identity. This could later enable an optimization rule: when MatExpr.dft n is instantiated over Int or a field where the primitive n-th root reduces to ±1, rewrite to faster integer-only butterfly code.
Currently, the DFT integration test (
integration_tests/verify_dft4.py) only validates the integer/real specialisation ofMatExpr.dft 4, which happens to reduce to the Walsh-Hadamard Transform (all ±1 coefficients). This covers neither the general complex caseω = e^{-2πi/n}nor other sizes.What needs to be tested:
MatExpr.dft nwheren > 2and the twiddle factors are genuinely non-trivial (e.g.,n=8withω = e^{-2πi/8})Current state:
evalDFT(AlgebraicSemantics.lean:919) implements the generic formulay[k] = Σ ω^{kj} · x[j]over a parametric field element ωdft_n()function callsℂbinding or complex arithmetic in code generationTesting approach:
Missing pieces:
ω^kforω = e^{-2πi/n})Note on DFT vs. WHT relationship:
For n=4, the DFT with a primitive 4th root of unity mathematically simplifies to the Walsh-Hadamard Transform (all ±1 coefficients). The current integration test exploits this equivalence by using WHT as a reference. Once complex DFT code generation is implemented, the DFT_4 implementation should be verified to produce WHT_4 outputs, confirming the mathematical identity. This could later enable an optimization rule: when
MatExpr.dft nis instantiated overIntor a field where the primitive n-th root reduces to ±1, rewrite to faster integer-only butterfly code.