1 | Using common/FEMeasurable.ma we expect that we can find a measurable subtrace |
---|

2 | of the RTLabs execution that corresponds to the original Clight one. Now we |
---|

3 | need to link it to a structured RTLabs subtrace, and then the back-end. |
---|

4 | |
---|

5 | This involves showing that the stack space bound is still respected, the |
---|

6 | observables are preserved (although we still don't have an observables |
---|

7 | function for the ASM; maybe CSC will want something different) and the |
---|

8 | clock difference implied by the costs is maintained (although we should be |
---|

9 | able to show this from the observables). |
---|

10 | |
---|

11 | Thus we need a notion of stack space usage for RTLabs structured traces. There |
---|

12 | is one for the "joint" languages, which looks like it could be easily reworked |
---|

13 | for arbitrary structured traces [1]. That said, it isn't used anywhere. |
---|

14 | |
---|

15 | For the observables and clock, we should get tlr_rel between the RTLabs |
---|

16 | structured trace and ASM, so however we extract observables from structured |
---|

17 | traces for ASM [2] ought to match what we can get at RTLabs str trace, then |
---|

18 | we can link that with the observables from the measurable version. We also |
---|

19 | need tlr_unrepeating. There's already a lemma showing that the labels given |
---|

20 | by flatten_trace_label_return is preserved when tlr_rel holds, but we have |
---|

21 | to relate the sum over tech_cost_of_label in ASM/CostsProof.ma with something |
---|

22 | suitable for RTLabs. The final lemma in CostsProof looks like it should |
---|

23 | help with this. Should we use the Σ_{l ∈ trace}(...) notation elsewhere [3]? |
---|

24 | |
---|

25 | Looking at compiler.ma again, that lemma appears to be exactly what we need. |
---|

26 | |
---|

27 | |
---|

28 | To do: |
---|

29 | |
---|

30 | Ask on list about [1] and [2]. |
---|

31 | Investigate [3]. |
---|