1 | include "common/Measurable.ma". |
---|

2 | include "RTLabs/Traces.ma". |
---|

3 | |
---|

4 | definition RTLabs_system : preclassified_system ≝ |
---|

5 | mk_preclassified_system |
---|

6 | RTLabs_fullexec |
---|

7 | (λ_.RTLabs_cost) |
---|

8 | (λ_. RTLabs_classify). |
---|

9 | |
---|

10 | notation "hbox(‘ ident i ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in ?) }. |
---|

11 | notation "hbox(‘ ident i : t ’)" non associative with precedence 90 for @{ (let (${ident i} : unit) ≝ it in (? : $t)) }. |
---|

12 | |
---|

13 | (* The start and end states are existentially quantified because the states |
---|

14 | need to be extended with the shadow stack of functions. (I'm not sure that |
---|

15 | was such a great idea now...) In principle the quantified away part of the |
---|

16 | stack would be important for stack-space correctness, except that the |
---|

17 | structured trace will never touch it, only the suffix of the trace will. |
---|

18 | We could extract the true value from the execution of the prefix anyway. *) |
---|

19 | |
---|

20 | (* XXX: split of observables seem arbitrary *) |
---|

21 | |
---|

22 | theorem measurable_structured_trace : ∀p,m,n,stack_cost,max_stack,obs_pre,obs. |
---|

23 | measurable RTLabs_system p m n stack_cost max_stack → |
---|

24 | observables RTLabs_fullexec p m n = Some ? 〈obs_pre,obs〉 → |
---|

25 | ∃start,end:RTLabs_ext_state (make_global … p). |
---|

26 | state_at … RTLabs_system p m = Some state start → |
---|

27 | state_at … RTLabs_system p n = Some state end → |
---|

28 | ∃tlr:trace_label_return (RTLabs_status (make_global … p)) start end. |
---|

29 | obs = ‘obs’ tlr. |
---|

30 | |
---|

31 | (* XXX: need some assumption on start to kick off further simulations, presumably |
---|

32 | from the execution of the prefix? *) |
---|

33 | |
---|

34 | (* |
---|

35 | There is no clock in the states of rtlabs, instead it's extracted from the |
---|

36 | whole trace. Might not match up well with asm? |
---|

37 | |
---|

38 | i.e., do we build the clock into the semantics so that it appears in the |
---|

39 | structured trace (or equiv, use an instrumented semantics), or use the time |
---|

40 | implict from the observables? |
---|

41 | *) |
---|