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...) *) |
---|

16 | |
---|

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

18 | |
---|

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

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

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

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

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

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

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

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

27 | |
---|

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

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

30 | |
---|

31 | (* |
---|

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

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

34 | |
---|

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

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

37 | implict from the observables? |
---|

38 | *) |
---|