FoldNTT: A Multiplier- and Twiddle-Lean NTT Core with Formally Verified Arithmetic for Proth Primes

1. INTRODUCTION

• FoldNTT preserves the reference forward transform, corrects its inverse, and proves each arithmetic block against the mathematics before validating composition by simulation.The redesign starts from the open-RTL CFNTT accelerator.Source: §1 · p. 1
• For q = 12289 = 3⋅2^12 + 1, shift-add K-RED folds replace two Barrett-reduction multipliers, leaving one multiplier per butterfly.The constant factor from the folds is absorbed into the twiddle ROM, and the same ROM fold helps implement the inverse fix.Source: §1 · p. 1
• For Falcon's ψ = 7, the bit-reversed table relation w[N/2+j] = ψ⋅w[j] derives half the twiddle words without a multiplier.The stored-word count is reduced from 1023 to 512; the folded table retains a scaled w[0] base word.Source: §1 · p. 1
• The verification methodology checks arithmetic and datapath RTL against a mathematical specification, proves control-safety properties inductively, and is mutation-tested.The inverse bug was found by this checking rather than by the shipped testbench.Source: §1 · p. 1
• 3→1 DSP per butterfly, half the stored twiddle bits, and about 4% whole-core Fmax cost are reported for the retrofit.The whole-core measurements use a reconstructed controller because the released radix-2 core's FSM was not published.Source: §1 · p. 1
• A generator extends the K-RED reducer to other Proth NTT primes and is validated on Kyber, while a separate sequential core builds to a timing-gated Basys-3 bitstream.The Kyber reducer is validated; the own-FSM core packages the verified blocks as a self-contained accelerator.Source: §1 · pp. 1–2

2. BACKGROUND

• The NTT turns negacyclic polynomial multiplication from O(N^2) convolution into O(N log N) evaluations, with ψ-weighting handling the x^N = −1 wrap.The ring is R_q = Z_q[x]/(x^N + 1).Source: §2 · p. 2
• Forward DIT-NR and inverse DIF-RN stages share a bit-reversed twiddle table, while the inverse butterfly requires per-stage 1/2 scaling.For Falcon, N = 1024, q = 12289, and ψ = 7; the released radix-2 core omits the inverse scaling operator.Source: §2 · p. 2
• CFNTT uses parity-striped two-bank memory so each radix-2 butterfly's operands can be read and written in the same cycle without bank conflicts.The retrofit leaves its memory system and address generators untouched, changing the butterfly arithmetic and ROM internals.Source: §2 · p. 2
• K-RED uses shifts and adds for Proth-prime reduction; prior hardware examples include Kyber's K2-RED and FHE-sized-modulus variants.Barrett and Montgomery are described as general-purpose reduction choices.Source: §2 · p. 2
• Prior twiddle-ROM reductions use on-the-fly generation with a multiplier per butterfly or a half-memory generator based on negation symmetry.FoldNTT instead uses an address-halving relation that is multiplier-free when ψ is shift-friendly.Source: §2 · p. 2
• Recent machine-checked PQC-hardware work targets masking and side-channel leakage [10] [11], while Casas et al. verify an FHE NTT datapath and micro-sequencer compositionally.FoldNTT's stated focus is functional checking against the mathematical transform.Source: §2 · p. 2

3. A BUG IN THE RELEASED INVERSE TRANSFORM

• The radix-2 butterfly omits the required 1/2 scaling in each inverse stage, although the reference algorithm and Python model apply it.The released radix-2 RTL ships modular_half.v but does not instantiate it in compact_bf.v; the radix-4 processing elements do instantiate it.Source: §3 · p. 2
• After ten inverse stages, the released radix-2 core returns 2^10x instead of x, while its forward transform is unaffected.Each stage is too large by a factor of two, yielding a global constant error.Source: §3 · p. 2
• The authors report the omission as a bug because the radix-2 RTL disagrees with its own paper and model, and no compensating constant appears elsewhere in the released tree.The radix-4 processing elements' use of modular_half also supports the intended scaling.Source: §3 · p. 2
• The shipped testbench asserts nothing about results and includes no reference vector, so a single end-to-end functional assertion would have caught the defect.Source: §3 · p. 2
• SMT and simulation round-trip checks exposed the 2^10 factor, which the authors localized to the uninstantiated modular_half and reproduced at full-core RTL level.The full-core simulation used a reconstructed controller because the released FSM was missing.Source: §3 · p. 3
• Restoring the halving adds two shift-add gates per butterfly but no multiplier, latency, or port change; the verified core round-trips exactly.The K-RED design derives the inverse twiddle scaling within the existing twiddle delay chain and adds the other gate on the add path.Source: §3 · p. 3

4. DESIGN

• The butterfly and ROM changes are applied as a pair: the multiplier returns 9⋅a⋅b mod q and the ROM supplies 9^-1-scaled words, preserving the reference ports, delay fabric, and latencies.Their contracts include operands below q, a mode held constant during a transform, and the corrected inverse.Source: §4 · p. 3
• One multiplier plus two op21 gates replaces the reference's three multipliers, with the gates also implementing the inverse fix.The two gates act on the ROM word and the add path.Source: §4 · p. 3

4.1 K-RED butterfly

• For q = 3⋅2^12 + 1, two K-RED folds reduce the full product to a value below 2q, followed by one conditional subtraction.The shift-add identities produce d ≡ 3z and e ≡ 9z mod q; storing W = 9^-1⋅w cancels the resulting factor in the butterfly product.Source: §4.1 · p. 3
• The butterfly uses shifts, adds, and one conditional subtraction with one hardware multiplier instead of three, while the inverse twiddle scaling fuses the missing halving.Pointwise multiplication would require two passes through the unit per product, halving throughput on one unit; the paper's cores do not implement PWM in RTL.Source: §4.1 · p. 3

4.2 𝜓-fold twiddle ROM

• The bit-reversed relation w[N/2+j] = ψ⋅w[j] lets the ROM store 512 lower words and derive the upper half for Falcon's ψ = 7 without a multiplier.Six parallel constant comparators select a multiple and one subtraction reduces the derived word; the quarter-table relation is algebraic but unbuilt and unmeasured.Source: §4.2 · p. 3

4.3 Generalization: other Proth primes

• The generator computes and checks per-prime K-RED schedules, and the Kyber q = 3329 reducer is checked exhaustively over z < q^2 and by a 60k-vector RTL sweep.That sweep is simulation, not exhaustive; Kyber validates the reducer only because its incomplete NTT does not have the primitive 2N-th root required for the full negacyclic-table relation.Source: §4.3 · p. 4
• K-RED fold count stays at two to three when m is large relative to k's width, while each fold's k⋅x cost depends on k's signed-digit weight.The planner's table uses analytical cost estimates, not a synthesized datapath; total cost also depends on width, fold count, and pipeline placement.Source: §4.3 · p. 4
• Goldilocks needs no ROM scaling when k^F ≡ 1 mod q, and low signed-digit-weight k can make the constant multiply inexpensive, unlike arbitrary RNS primes with large random k.The authors expect the congruence encoding to scale to 30–64-bit RNS moduli but have not run those proofs.Source: §4.3 · p. 4

5. VERIFICATION

• Exact-width SMT proves every arithmetic unit over its full input domain, while domain-faithful abstractions discharge the operand-range seams in composition.The divider-free congruence encoding closes an obligation that had not converged after two hours in 11 seconds.Source: §5 · pp. 4–5
• Vendor-tool timing, physical hardware, and side channels remain outside verification scope; CI reruns the reported checks on every push.A monolithic proof of the roughly 150k-cycle round trip is beyond bounded model checking.Source: §5 · pp. 5–6
• SymbiYosys proves butterfly and ROM pipelines against latency-aligned behavior, assuming operands are < q and mode remains constant during each proof.Time-local assertions and a bounded check through the guard and latency cover every assertion window.Source: §5 · p. 5
• K-induction proves own-FSM control-safety invariants under arbitrary host and start behavior, but the proof does not establish liveness or analyze datapath leakage.The datapath is stubbed for control proofs; simulations cover completion and butterfly issuance.Source: §5 · p. 5
• Eight RTL mutations across five harnesses must trigger counterexamples, while composed transforms and the generated Kyber reducer receive simulation checks.The Kyber reducer is checked on 60k vectors; mutation kills are selected fault-detection evidence, not proof against all vacuity.Source: §5 · p. 5
• Full-core simulation validates exact retrofit round trips; the shipped core instead returns 2^10*x after inverse, with both variants taking 5290 cycles per transform.The full-core schedule uses a reconstructed controller, not the unreleased original FSM.Source: §5 · p. 6

Whole-core comparison

• Against the same-architecture, same-flow base, ENS fell 21% (969→767), driven by DSP reduction from 3 to 1; the forward transform was unchanged, inverse corrected, and Fmax within a few percent.Base area and Fmax use the released radix-2 datapath with our reconstructed controller, not CFNTT’s published vendor-flow figures; the controller schedule is ours, not the CFNTT authors’.Source: §6 · pp. 7–8

Post-route timing

• 137.5 MHz versus 143.1 MHz whole-core post-route Fmax is a 4% reduction, inside the 127–143 versus 130–138 MHz seed ranges.Three seeds do not resolve the difference; these are open-flow timing estimates.Source: Figure 3 · p. 6, §6 · p. 7

Twiddle storage

• The folded twiddle ROM halves stored bits, but at N=1024 both 1023- and 512-word tables fit one RAMB18.On FPGA, the LUT reduction is about 20% (241→192), rather than the larger generic-gate synthesis reduction.Source: §6 · p. 6

Whole-core area

• At the core level, DSP count falls 3→1, FF falls 14%, LUT rises 4%, and RAMB18 is unchanged.The twiddle ROM maps to distributed LUT-ROM, so halving its stored bits does not reduce BRAM count at N=1024.Source: §6 · p. 6, Table 3 · p. 7

Own-FSM core

• The own-FSM single-BFU core takes about 74k cycles per 1024-point transform and builds a timing-gated Basys-3 bitstream, which has not been run on a board.The streaming retrofit is the throughput design point; the own-FSM core is the high-latency, self-contained design point.Source: §6 · p. 7

Comparison with Compact-FALCON

• Compact-FALCON is roughly 8× faster per NTT (4.78 vs 38.5 μs), while using roughly 10× the ENS and 20 DSPs.FoldNTT claims area and DSP cost advantages, not a throughput win, against this throughput-optimized combined FFT+NTT design.Source: §6 · p. 8

NTT accelerators and conflict-free memory

• CFNTT provides parity-based conflict-free memory mapping, while the closest Falcon designs use Barrett reduction and full twiddle ROMs.The K-RED retrofit and ψ-fold are absent from both CFNTT and Compact-FALCON.Source: §7 · p. 8

Modular reduction

• K-RED [5] and hardware variants establish shift-add reduction, while FoldNTT contributes a verified drop-in retrofit with the residual factor folded into the twiddle ROM.The same fold also corrects the inverse transform.Source: §7 · p. 8

Twiddle storage

• Unlike prior half-memory generators based on negation symmetry, the ψ-fold derives entries through w[N/2+j] = ψ·w[j], a relation usable for shift-friendly ψ.The prior on-the-fly generator uses a modular multiplier per butterfly; the ψ-fold is multiplier-free and its half-table RTL is proven against the shipped ROM.Source: §7 · p. 8

Verified PQC hardware

• Unlike recent PQC hardware verification focused on leakage [10] [11], FoldNTT checks functional correctness; Casas et al. compositionally verify a proprietary FHE NTT engine.FoldNTT applies block-plus-control verification to an open published accelerator, down to ROM contents, and uses the check as a design driver.Source: §7 · pp. 8–9

How the techniques were found

• Each of 37 design-loop revisions followed a verify, render, critique, change, and re-verify cycle, with candidates accepted only after verification.K-RED entered as a conventional optimization; the ψ-fold was noticed after the reduced arithmetic left the twiddle ROM visibly largest.Source: §8 · p. 9
• The authors claim no generality for the design loop: it was used for one design, found once, and its components were not ablated.The revision history, renders, and verification verdicts are published for inspection.Source: §8 · p. 9

Limitations and future work

• Whole-core Fmax is 143 vs 138 MHz, measured on a core using a reconstructed controller; the unreleased FSM’s original timing and cycle count remain unknowable.Full-transform correctness is simulation-validated, while formal proofs cover listed blocks and control-safety invariants; physical execution and vendor-flow confirmation remain undone.Source: §8 · p. 9
• The own-FSM core is sequential, and a pipelined two-bank instantiation for about one butterfly per cycle remains future work.Pointwise multiplication is absent from RTL, and timing differences of a few percent are unresolved because only the best of three seeds is kept for per-module Fmax.Source: §8 · p. 9

Conclusion

• FoldNTT uses a third of the multipliers and about half the stored constants while preserving the forward transform and correcting the inverse to specification.The inverse bug surfaced during verification; the K-RED retrofit fixes it with two shift-add gates and no added multiplier or latency.Source: §9 · p. 9
• Every arithmetic block is proven equal to the mathematics, and the composed transform is validated by simulation.The own-FSM core has inductively proven control-safety invariants and builds to a timing-gated Basys-3 bitstream.Source: §9 · p. 9
• A generator extends the construction to other Proth primes, and the proofs, simulations, and area numbers are rerun by the public repository’s CI.The paper demonstrates a drop-in streaming retrofit and a complete own-FSM core.Source: §9 · p. 9

Reproducibility

• The public repository includes the retrofit RTL, reference submodule, proofs, generator, FPGA flow, and design-loop montage; proof, simulation, and area checks rerun in CI.The paper’s numbers are from commit 2571d66, and the source builds both the canonical PDF and a single-column draft.Source: REPRODUCIBILITY · pp. 9–10
• The verification suite includes exact-width arithmetic proofs, compositional SymbiYosys checks, control-safety induction, mutation tests, and streaming and own-core simulations.The own-core checks also perform independent-golden NTT/INTT checks and streaming cross-validation.Source: REPRODUCIBILITY · pp. 9–10
• Area scripts measure per-module and whole-core costs, while the post-route Fmax scripts use openXC7 nextpnr-xilinx on Artix-7 without Vivado.The toolchain is pinned in the flake for the Fmax scripts.Source: REPRODUCIBILITY · p. 10
• The own-FSM core has a separate timing-gated, Vivado-free Basys-3 bitstream flow; the design-loop montage shows five stages from v1 through v37.The montage panels are rendered from RTL-grounded scenes.Source: REPRODUCIBILITY · p. 10, Figure 4 · p. 10

• The proofs are short and kept with the artifact; machine checks serve as their certificates.The proof notes live in docs/lemmas.md.Source: Appendix A · p. 10
• The stated setting assumes q = k·2^m + 1 is a Proth prime, N = 2^n, and 2N divides q − 1.ψ is a primitive 2N-th root of unity modulo q.Source: Appendix A · p. 10

Lemma 1 (K-RED fold)

• K-RED folds reduce Proth-prime inputs to a residue below 2q, after which one conditional subtraction suffices.For q = 12289, two folds suffice when z < 2^28.Source: Appendix A · p. 10

Lemma 2 (INTT-halving fusion)

• A scaled ROM constant lets the forward butterfly multiply exactly and the inverse butterfly incorporate the required per-stage halving.The inverse operation uses op21(W) = (2k^F)^-1·w.Source: Appendix A · p. 10

Lemma 3 (ψ-fold)

• In the bit-reversed twiddle layout, each table half is derived from the preceding half by multiplying by a power of ψ.For shift-friendly ψ = 7, the derived half needs no multiplier because 7x = (x<<3) − x.Source: Appendix A · p. 10

Lemma 4 (composition)

• Constant scalings commute modulo q, allowing the ROM scaling and ψ-fold to coexist while restoring the specified transform.The composition is checked end-to-end with run_stream.py.Source: Appendix A · p. 10

• Every row in the detail behind Figure 2 is rerun by CI on each push.Source: Appendix B · p. 10

Table 5

• Table 5 presents deliverables alongside their certificates.Source: Table 5 · p. 11

Table 6

• Table 6 presents verification obligations with their methods and scopes.Source: Table 6 · p. 11