[2502] | 1 | include "common/Measurable.ma". |
---|

[2601] | 2 | include "RTLabs/RTLabs_traces.ma". |
---|

[2502] | 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 |
---|

[2511] | 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. *) |
---|

[2502] | 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? |
---|

[2511] | 41 | *) |
---|