Item-language compiler correctness with cost preservation

Let iprog be an item-language program with $P$ procedures over $S$ item stacks, and let prog be a stack-machine program over $S+4$ stacks whose procedures are the compilations of those of iprog ($\mathrm{prog}\ j = \mathrm{compile}(\mathrm{iprog}\ j)$ for all $j$). Suppose the item statement $p$ executes (big-step semantics IExec, with input word $I$) from item state $s$ to $s'$ with cost $c$. Then

1. the compiled statement runs on the encoded states within the same cost:

2. if moreover $p = \mathrm{loop}\ i\ f\ b$, then $24\le c$ and the inner loop of its compilation runs from $\mathrm{encF}\ i\ f\ s$ (the encoding of $s$ with the loop flag for the test $f$ on stack $i$ pushed on the scratch stack $s_3$) to $\mathrm{encI}\ s'$ with a $0$ flag pushed on $s_3$, within cost $c-24$.

Part 2 is the strengthened induction hypothesis needed for loops. The item-level costs (e.g. $+25$ for a conditional, $+30$ per loop test) are chosen to dominate the compiled code, so all cost bounds proved in the item language transfer verbatim to the stack machine and hence, via multipliesAt_of_exec, to the Turing machine.

Formalization Note. Item states IState S have item stacks G, input pointer ip and output out; encI s writes each item stack $G_i$ as the concatenation of item encodings on stack $i$ and leaves the four extra scratch stacks ($s_q, s_1, s_2, s_3$ = indices $S,\dots,S+3$) empty. Runs asserts an exact final state and an upper bound on the cost; IExec carries the exact item-level cost.