Decoding Fermat-ring residues back into Gaussian-integer blocks

Let $C$ be a list of $N$ canonical residues modulo $F = 2^{4rP}+1$ on stack XD, $l \le 4rP$, and let the registers hold $N$, $2^{4rP-l}$, $2^{4rP}$, $F$, $2^P$, $r$. For $W\ge 2\cdot 4rP+3$, $W\ge\mathrm{zsz}(N)$, $Q\ge P$, $Q \ge \mathrm{zsz}(r)$, the program dcL consumes $C$ and pushes on KO the (reversed) concatenation of decBlk F P r applied to each scaled residue scl (4rP) l c $= c\cdot 2^{2\cdot4rP-l} \bmod F$, within cost dcCost N r P Q W.

Formalization Note. decBlk (unpacking a residue into $r$ Gaussian integers with signed $P$-bit digits) is from Def_IntMul_HvdH_MachineRef. 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.