Transposing an n×m integer array stored on a stack

Let $L$ be a list of $n\cdot m$ integers on stack XD ($m \ge 1$, $nm \le 2^{kb}$), and registers $a, b$ (distinct from the scratch stacks 1,2,3) and KBR hold $n$, $m$, $kb$. If all entries and $n,m,kb$ have bit length $\le W$, the program trWith a b replaces $L$ by its transpose transposeL n m L (row-major $n\times m$ to row-major $m\times n$) within cost $10^6(kb+1)(nm+1)\cdot 2(W+kb+5) + 20000(W+2)$.

Formalization Note. The transpose is implemented by tagging every entry with its target index, a radix sort on the tags, and stripping the tags. transposeL 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.