1 | |
---|
2 | include "Cminor/abstract.ma". |
---|
3 | include "RTLabs/abstract.ma". |
---|
4 | |
---|
5 | record cminor_rtlabs_inv : Type[0] ≝ { |
---|
6 | ge_cm : cm_genv; |
---|
7 | ge_ra : RTLabs_genv |
---|
8 | }. |
---|
9 | axiom cminor_rtlabs_rel : cminor_rtlabs_inv → Cminor_state → RTLabs_state → Prop. |
---|
10 | |
---|
11 | (* Conjectured simulation results |
---|
12 | |
---|
13 | We split these based on the start state: |
---|
14 | |
---|
15 | 1. ‘normal’ states take some [S n] normal steps and simulates them by [m] |
---|
16 | normal steps in RTLabs ([m] can be zero if the Cminor program executed an |
---|
17 | St_skip); |
---|
18 | 2. call and return steps are simulated by a call/return step plus [m] normal |
---|
19 | steps (to copy stack allocated parameters / results); and |
---|
20 | 3. lone cost label steps are simulates by a lone cost label step |
---|
21 | |
---|
22 | Note that we'll need something more to show that non-termination is |
---|
23 | preserved (because it isn't obvious that we don't squash a loop to zero |
---|
24 | instructions). Options are a traditional measure, or using the soundness of |
---|
25 | the cost labelling. |
---|
26 | |
---|
27 | These should allow us to maintain enough structure to identify the RTLabs |
---|
28 | subtrace corresponding to a measurable Clight/Cminor subtrace. |
---|
29 | *) |
---|
30 | |
---|
31 | definition cminor_normal : Cminor_state → bool ≝ |
---|
32 | λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
33 | |
---|
34 | definition rtlabs_normal : RTLabs_state → bool ≝ |
---|
35 | λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
36 | |
---|
37 | axiom cminor_rtlabs_normal : |
---|
38 | ∀INV:cminor_rtlabs_inv. |
---|
39 | ∀s1,s1',s2,tr. |
---|
40 | cminor_rtlabs_rel INV s1 s1' → |
---|
41 | cminor_normal s1 → |
---|
42 | ¬ Cminor_labelled s1 → |
---|
43 | ∃n. after_n_steps (S n) … Cminor_exec (ge_cm INV) s1 (λs.cminor_normal s ∧ ¬ Cminor_labelled s) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
44 | ∃m. after_n_steps m … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'. |
---|
45 | tr = tr' ∧ |
---|
46 | cminor_rtlabs_rel INV s2 s2' |
---|
47 | ). |
---|
48 | |
---|
49 | axiom cminor_rtlabs_call_return : |
---|
50 | ∀INV:cminor_rtlabs_inv. |
---|
51 | ∀s1,s1',s2,tr. |
---|
52 | cminor_rtlabs_rel INV s1 s1' → |
---|
53 | match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] → |
---|
54 | after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
55 | ∃m. after_n_steps (S m) … RTLabs_exec (ge_ra INV) s1' (λs.rtlabs_normal s) (λtr',s2'. |
---|
56 | tr = tr' ∧ |
---|
57 | cminor_rtlabs_rel INV s2 s2' |
---|
58 | ). |
---|
59 | |
---|
60 | axiom cminor_rtlabs_cost : |
---|
61 | ∀INV:cminor_rtlabs_inv. |
---|
62 | ∀s1,s1',s2,tr. |
---|
63 | cminor_rtlabs_rel INV s1 s1' → |
---|
64 | Cminor_labelled s1 → |
---|
65 | after_n_steps 1 … Cminor_exec (ge_cm INV) s1 (λs.true) (λtr',s. 〈tr',s〉 = 〈tr,s2〉) → |
---|
66 | after_n_steps 1 … RTLabs_exec (ge_ra INV) s1' (λs.true) (λtr',s2'. |
---|
67 | tr = tr' ∧ |
---|
68 | cminor_rtlabs_rel INV s2 s2' |
---|
69 | ). |
---|