Clight to Cminor
----------------

This looks like it will be an n:m simulation with n,m≥1.  We need to allow n>1
because statements like Sbreak can take several steps to find the appropriate
continuation (unlike, say, Sreturn, which uses call_cont to find the right
one in one step).  However, it won't take zero steps as we always generate an
statement to be consumed for each step of the Clight (even for steps which
process the continuation - we still have something like a goto to match the
skip against).

When compiling loops we're going to need to match states like

  skip, Kfor a2 a3 s k   <--->  skip, kseq (goto entry) k'

Presumably some kind of invariant on goto labels is required, perhaps that
goto labels are unique or equivalently that any label produced is found by the
label lookup function.  This might be enough (as a hyp for the construction of
the simulation relation):

∀EX,INV,KINV.
  find_label_always entry (f_body f) Kend EX f en INV KINV =
    Some ? 〈[loop body],[suitable continuation]〉.

We can then step back through the loop.

Cminor to RTLabs
----------------

Here we have to allow for statements that disappear (skips and goto labels) as
well as large expansions as expressions are broken down.