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