Our rough plan is:
- prove flat simulations and cost properties up to RTLabs
- prove structured simulations (whatever that may be) to end
- combine with cost proofs to get nice theorems.
What do we want these to look like? (Especially as we have some coinductive
structures around that aren't good for equality.)
CompCert's overall theorems concern relating behaviours of the source program
(except going wrong) to behaviours of the target; where behaviours consist of
result (finishes, diverges silently, diverges loudly) and event trace. This
doesn't require showing the equality of traces.
CompCertTSO shows trace inclusion, but inclusion is by implication again.
We also want to add costs; for the simulation this is just trace preservation,
but at the top level we want to say something more using the theorem from the
ASM level. This is slightly tricky because we've no way to talk about "the
execution of this function call" without structured traces.