Compiled arithmetic expressions evaluate correctly

For every arithmetic expression $e$ over the 64 registers (built from register tops, literals, $+$, negation, selection on sign, multiplication, shifts, floor division, …) that does not mention the eight scratch stacks $56,\dots,63$ (e.Clean) and is defined in state $s$ (e.ok s), the compiled code e.code zX runs from $s$ to the state obtained by pushing the value e.eval s on stack $56$, within cost e.cost s.

Formalization Note. IRuns I iprog p s s' c is the item-language big-step semantics with cost bound $c$; zX is the record of scratch stacks used by the expression compiler. 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.