Using common/FEMeasurable.ma we expect that we can find a measurable subtrace
of the RTLabs execution that corresponds to the original Clight one. Now we
need to link it to a structured RTLabs subtrace, and then the back-end.
This involves showing that the stack space bound is still respected, the
observables are preserved (although we still don't have an observables
function for the ASM; maybe CSC will want something different) and the
clock difference implied by the costs is maintained (although we should be
able to show this from the observables).
Thus we need a notion of stack space usage for RTLabs structured traces. There
is one for the "joint" languages, which looks like it could be easily reworked
for arbitrary structured traces [1]. That said, it isn't used anywhere.
For the observables and clock, we should get tlr_rel between the RTLabs
structured trace and ASM, so however we extract observables from structured
traces for ASM [2] ought to match what we can get at RTLabs str trace, then
we can link that with the observables from the measurable version. We also
need tlr_unrepeating. There's already a lemma showing that the labels given
by flatten_trace_label_return is preserved when tlr_rel holds, but we have
to relate the sum over tech_cost_of_label in ASM/CostsProof.ma with something
suitable for RTLabs. The final lemma in CostsProof looks like it should
help with this. Should we use the Σ_{l ∈ trace}(...) notation elsewhere [3]?
Looking at compiler.ma again, that lemma appears to be exactly what we need.
To do:
Ask on list about [1] and [2].
Investigate [3].