In one sense we've already solved the problem of producing structured RTLabs
traces, but there are some extra considerations:
1. The existing construction uses a coinductive flat_trace, which always runs
to completion without I/O and contains evidence of execution. Our current
notion of measurable isn't suitable here, as we allow statements about
partial executions.
One possible solution is a version of make_label_return that takes a trace
and a proof that it came from an exec_steps. Another would be to define
a partial_flat_trace and repeat the definitions.
2. We still need a larger termination measure because of the mutually recursive
function definition (that is, it should be three times larger, like the
current one).
3. It should be possible to prove that the observables are preserved separately
because the start state uniquely determines the execution so long as the
same number of steps are involved.