Encoding blocks of Gaussian integers into the Fermat ring

Let $U$ be a list of $N\cdot r$ Gaussian integers with coordinates of absolute value $<2^P$ ($P,r\ge1$), stored on stack GU, and let the registers hold $2^P$, $r$, $2^{2rP}$, $2^{4rP}+1$ and $N$. For bounds $Q\ge P$ with $\mathrm{zsz}(r)\le Q$ and $W\ge 4rP+1$, $W \ge \mathrm{zsz}(N)$, the program encL consumes $U$ and pushes on XD the list of residues encRes P r blk (Kronecker packing of each block of $r$ consecutive entries, real parts in the low half and imaginary parts times $2^{2rP}$, reduced modulo $2^{4rP}+1$) for the $N$ blocks of $U$, within cost encCost N r P Q W.

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.