Moving a list of integers between stacks (expression-controlled count)

Let $i,j,c$ be distinct registers below 55 ($c$ different from $i,j$), let stack $i$ start with the integer list $l$, and let $n$ be a clean linear expression, defined in $s$, with value $|l|$ and bit size bounded by $B$, where every entry of $l$ has bit length $\le B$. Then the straight-line program mvList i j c n moves $l$ reversed onto stack $j$ (using $c$ as counter), with cost at most $(\mathrm{size}(n)+1)\cdot2000(B+2) + |l|(14000(B+2)+30) + 32$.

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.