One inverse (DIT) transform pass over all levels of a Fermat-ring tensor

Let $A$ be a list of $N \le 2^{kb}$ canonical residues modulo $2^n+1$ on stack XD, and let $D$ be a list of level descriptors $(\mathrm{pre}, j, E, \mathrm{post})$ satisfying LvlOK n kb W N J D (each level splits the array into $\mathrm{pre}$ blocks of $2^j$ columns of length $\mathrm{post}$ with $\mathrm{pre}\cdot 2^j\cdot\mathrm{post}=N$, $2^j E = 2n$, $j\le J$), encoded as 8 integers per level (enc8) on the source stack. With $2n+kb+3 \le W$, $J+1\le W$, $\mathrm{zsz}(|D|)\le W$ and the registers holding $kb$, $N$, $2^n$, $2^n+1$, $|D|$, the program passP with the inverse (DIT) butterfly procedure replaces $A$ by lvls (Gt n = ditZ (2^n+1) n) D A (the inverse (DIT) radix-2 Fermat transform of every column of every level, applied level by level), moves the descriptor list to the other descriptor stack (reversed), within cost passCost |D| n kb W N J.

Formalization Note. difZ/ditZ are the decimation-in-frequency / -time transforms with root $2$-power of the published Def_IntMul_HvdH_MachineRef; each column transform is a call of procedure 2 or 3. 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.