pub fn emit_ntt_butterfly_pipelined_verilog(name: &str, cuts: NttCuts) -> StringExpand description
Emit module name: emit_ntt_butterfly_verilog’s butterfly as a pipeline taking one butterfly a cycle, its
result NttCuts::latency edges after its operands, registered after the steps cuts names. Each value a later
stage reads reaches it through one register a stage, and only those values are carried.
The product zeta·b is an aligned tree of adds over its sixteen partial products (b’s bit 15 weighs −2¹⁵), each
add as wide as the range of its sum needs. m = p[15:0]·q⁻¹ mod 2¹⁶ keeps the product’s low byte and corrects the
high one: q⁻¹ = 1 − 2⁸ − 2¹⁰ − 2¹¹ mod 2¹⁶. The reduction subtracts only high halves: the low halves of p and
m·q agree (Montgomery’s invariant), so t = p[31:16] − (m·q)[31:16], and with q = 13·2⁸ + 1 that high half is
(13·m + (m >>> 8)) >>> 8 — the low byte of m cannot carry into it.