Cost bound for decoding one Fermat-ring residue

Let $P \ge 1$, $0 \le z < 2^{4rP}+1$, and let registers KZ, KB, KN, KR hold $z$, $2^P$, $2^{4rP}$, $r$. If $P\le Q$ and $\mathrm{zsz}(r) \le Q$, the cost of the decoding program decP from this state is at most $10^6(r+1)(Q+5) + 2\cdot10^5(rP+1)$.

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.