Pointwise products of two residue lists in the Fermat ring

Let $A, B$ be lists of $N$ canonical residues modulo $2^n+1$, $B$ on stack XD and $A$ on YC, with registers holding $N$, $2^n$, $2^n+1$, and let the multiplication spec $M$ multiply $(n+1)$-bit integers at cost $\le Φ_m$. For $W\ge 2n+2$, $W \ge \mathrm{zsz}(N)$, the program pmL replaces $B$ by the list of products pmulZ (2^n+1) A B $= (a_i b_i \bmod 2^n+1)_i$ and consumes $A$, within cost pmCost N W Φm $= N(Φ_m + 110000(W+2)) + N(14000(W+2)+30) + 8000(W+2)+64$.

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.