The parameter-computation program computes mkParams K N

Let $K, N \ge 1$ and $N < 2^{nb}$, and let $s$ be a machine state whose register rN holds $N$ and rNb holds $nb$ on top. Then the straight-line register program parP K is defined on $s$ and its result is parOut s K N: the state $s$ with the parameters of $q=\mathrm{mkParams}(K,N)$ pushed on their registers — $b$, $L$, $E = \lceil \log_2 4L \rceil$, $e$, $d_h$, $K-d_h$, $2^e$, $\alpha$, $p$, $P$, $f_n$, the list of side lengths $s_1,\dots,s_K$ (as records) and their product $S$.

Formalization Note. RS is straight-line code on the 64 item stacks with run/ok; pushV pushes an integer on a stack. mkParams 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.