The machine program fwP computes the Fermat-ring convolution fermatW

Let $q$ be HvdH parameters with $P\ge 1$, $K \le f_n$, $\mathrm{logOuter} \le f_n$, $\mathrm{logOuter}\le kb$, and let $M$ be a multiplication spec that multiplies $(f_n+1)$-bit integers at cost $\le Φ_m$. Let $U, V$ be lists of $2^{\mathrm{logOuter}}\cdot r$ Gaussian integers ($r = 2^e$) with all coordinates of absolute value $<2^P$, stored as item lists on stacks GU and VI, and let the constant registers hold their prescribed values ($2^P$, $r$, $2^{2rP}$, $2^{f_n}+1$, $2^{f_n}$, $2^{\mathrm{logOuter}}$, $kb$, $K-1$, $2^{f_n-\mathrm{logOuter}}$, and the encoded axis descriptors of the outer axes). Then the program fwP runs from $s$ (calling the multiplication procedure for the pointwise products), consumes $U$ and $V$, and pushes fermatW q U V — the cyclic convolution of the published reference computed by Kronecker packing into the Fermat ring $\mathbb Z/(2^{f_n}+1)$, forward DIF transforms, pointwise products, DIT transform and unpacking — onto OUT, with cost at most fwCost q kb Φm.

Formalization Note. The machine layer: IState HS is a state with $64$ stacks of items (Item = integer or mark), an input position and an output; RM programs (straight-line register code RS, loops rep, conditionals, calls of the multiplication procedure through a MulSpec $M$ giving its domain and cost) have a functional semantics p.run s, a definedness predicate p.ok M s and a cost p.cost M s; Spec M p s s' c abbreviates p.ok M s ∧ p.run s = s' ∧ p.cost M s ≤ c. ints L / gints U push an integer list / a list of pairs as items (head = top); zsz z is the bit length of $|z|$. MulBnd M m Φ says the multiplication procedure accepts all pairs of integers of bit length $\le m$ at cost $\le Φ$. Register names (GU, CR, KB, XN, …) are fixed stack indices.