FoldNTT：面向Proth素数的乘法器与旋转因子精简NTT核心，具备形式化验证的算术单元
FoldNTT: A Multiplier- and Twiddle-Lean NTT Core with Formally Verified Arithmetic for Proth Primes
- Nyx Foundation（Nyx基金会）
机构由 AI 辅助整理，请以论文原文为准。
AI总结：
FoldNTT重新设计NTT硬件，每个蝶形仅用一个乘法器并减半旋转因子存储，通过形式化验证修正逆变换错误，在Artix-7上以约4%频率代价实现3倍DSP节省。
AI中文摘要：
用于格基后量子密码学的硬件在其面积中很大一部分用于数论变换（NTT），其中以模乘器和旋转因子存储为主。FoldNTT是对已发布的基-2 CFNTT加速器（TCHES 2022）的重新设计，针对Falcon / FN-DSA素数q = 12289，每个蝶形单元仅使用一个硬件乘法器（而非三个），并且存储的旋转因子常量减少约一半。Proth形式q = 3*2^12 + 1将模约简转化为移位加K-RED折叠，且位反转旋转因子表满足w[N/2+j] = psi*w[j]，因此表的一半无需乘法器即可推导。将已发布的RTL与数学对照检查还暴露了一个错误：其逆变换省略了每级减半操作，返回2^10*x，此次改造修正了该问题。每个算术模块均通过精确位宽SMT和组合式SymbiYosys证明验证，控制安全不变量通过k-归纳法验证；这些证明经过变异测试，组合变换通过仿真验证，所有步骤均由CI重新运行。在Artix-7上采用完全开放的流程，改造后每个蝶形单元的DSP48从3个降至1个，存储的旋转因子位数减少50%，整个核心的Fmax代价约为4%（三个种子中的最佳值，在种子间差异范围内），这是在由我们重建的控制器（参考FSM从未发布）驱动的已发布数据通路上测量，并通过全核心仿真验证；采用我们自己的控制器的顺序核心可构建为时序门控的Basys-3比特流。
英文摘要：
Hardware for lattice-based post-quantum cryptography spends a large share of its area on the number-theoretic transform (NTT), dominated by modular multipliers and twiddle storage. FoldNTT is a redesign of the released radix-2 CFNTT accelerator (TCHES 2022) for the Falcon / FN-DSA prime q = 12289 with one hardware multiplier per butterfly instead of three and about half the stored twiddle constants. The Proth shape q = 3*2^12 + 1 turns modular reduction into shift-and-add K-RED folds, and the bit-reversed twiddle table obeys w[N/2+j] = psi*w[j], so half the table is derived without a multiplier. Checking the released RTL against the mathematics also exposed a bug: its inverse transform omits a per-stage halving and returns 2^10*x, which the retrofit corrects. Every arithmetic block is proven by exact-width SMT and compositional SymbiYosys proofs, control-safety invariants by k-induction; the proofs are mutation-tested and the composed transform is validated by simulation, all rerun by CI. On Artix-7 in a fully open flow, the retrofit costs 3->1 DSP48 per butterfly and -50% stored twiddle bits at a whole-core Fmax cost of about 4% (best of three seeds; within the seed-to-seed spread), measured on the released datapath driven by a controller we reconstructed (the reference FSM was never released) and validated by full-core simulation; a sequential core with our own controller builds to a timing-gated Basys-3 bitstream.
