1 | |
---|
2 | include "Cminor/Cminor_abstract.ma". |
---|
3 | include "RTLabs/RTLabs_abstract.ma". |
---|
4 | include "Cminor/toRTLabs.ma". |
---|
5 | |
---|
6 | record cminor_rtlabs_inv (ge_cm:cm_genv) (ge_ra:RTLabs_genv) : Type[0] ≝ { |
---|
7 | }. |
---|
8 | axiom cminor_rtlabs_rel : ∀gc,gr. cminor_rtlabs_inv gc gr → Cminor_state → RTLabs_state → Prop. |
---|
9 | |
---|
10 | axiom cminor_rtlabs_rel_labelled : ∀gc,gr,INV,s,s'. |
---|
11 | cminor_rtlabs_rel gc gr INV s s' → |
---|
12 | Cminor_labelled s = RTLabs_cost s'. |
---|
13 | |
---|
14 | (* Conjectured simulation results |
---|
15 | |
---|
16 | We split these based on the start state: |
---|
17 | |
---|
18 | 1. from a ‘normal’ state we simulate a step by [n] normal steps in RTLabs |
---|
19 | ([n] can be zero if the Cminor program executed an St_skip); |
---|
20 | 2. call and return state steps are simulated by a call/return state step (we |
---|
21 | don't add anything extra in this stage, it happens in Clight to Cminor); |
---|
22 | and |
---|
23 | 3. lone cost label steps are simulates by a lone cost label step |
---|
24 | |
---|
25 | Most of the work in this stage is splitting the execution of complex Cminor |
---|
26 | statements into individual RTLabs steps. This doesn't contradict 2 above - |
---|
27 | the expansion of function parameters, return expressions, etc is done for |
---|
28 | the function call / return *statement*, whereas the call / return *state* is |
---|
29 | a Callstate / Returnstate that is the second half of the operation. |
---|
30 | |
---|
31 | Note that we'll need something more to show that non-termination is |
---|
32 | preserved (because it isn't obvious that we don't squash a loop to zero |
---|
33 | instructions). Options are a traditional measure, or using the soundness of |
---|
34 | the cost labelling. |
---|
35 | |
---|
36 | These should allow us to maintain enough structure to identify the RTLabs |
---|
37 | subtrace corresponding to a measurable Clight/Cminor subtrace. |
---|
38 | *) |
---|
39 | |
---|
40 | definition cminor_normal : Cminor_state → bool ≝ |
---|
41 | λs. match Cminor_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
42 | |
---|
43 | definition rtlabs_normal : RTLabs_state → bool ≝ |
---|
44 | λs. match RTLabs_classify s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
45 | |
---|
46 | axiom cminor_measure : Cminor_state → nat. |
---|
47 | |
---|
48 | axiom cminor_rtlabs_normal : |
---|
49 | ∀ge_cm,ge_ra. |
---|
50 | ∀INV:cminor_rtlabs_inv ge_cm ge_ra. |
---|
51 | ∀s1,s1',s2,tr. |
---|
52 | cminor_rtlabs_rel … INV s1 s1' → |
---|
53 | cminor_normal s1 → |
---|
54 | ¬ Cminor_labelled s1 → |
---|
55 | step ?? Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 → |
---|
56 | ∃n. after_n_steps n … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'. |
---|
57 | tr = tr' ∧ |
---|
58 | (n = 0 → lt (cminor_measure s2) (cminor_measure s1)) ∧ |
---|
59 | cminor_rtlabs_rel … INV s2 s2' |
---|
60 | ). |
---|
61 | |
---|
62 | axiom cminor_rtlabs_call_return : |
---|
63 | ∀ge_cm,ge_ra. |
---|
64 | ∀INV:cminor_rtlabs_inv ge_cm ge_ra. |
---|
65 | ∀s1,s1',s2,tr. |
---|
66 | cminor_rtlabs_rel … INV s1 s1' → |
---|
67 | match Cminor_classify s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false ] → |
---|
68 | step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 → |
---|
69 | after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.rtlabs_normal s) (λtr',s2'. |
---|
70 | tr = tr' ∧ |
---|
71 | cminor_rtlabs_rel … INV s2 s2' |
---|
72 | ). |
---|
73 | |
---|
74 | axiom cminor_rtlabs_cost : |
---|
75 | ∀ge_cm,ge_ra. |
---|
76 | ∀INV:cminor_rtlabs_inv ge_cm ge_ra. |
---|
77 | ∀s1,s1',s2,tr. |
---|
78 | cminor_rtlabs_rel … INV s1 s1' → |
---|
79 | Cminor_labelled s1 → |
---|
80 | step … Cminor_exec ge_cm s1 = Value … 〈tr,s2〉 → |
---|
81 | after_n_steps 1 … RTLabs_exec ge_ra s1' (λs.true) (λtr',s2'. |
---|
82 | tr = tr' ∧ |
---|
83 | cminor_rtlabs_rel … INV s2 s2' |
---|
84 | ). |
---|
85 | |
---|
86 | axiom cminor_rtlabs_init : |
---|
87 | ∀p,s. |
---|
88 | make_initial_state … Cminor_fullexec p = OK … s → |
---|
89 | let p' ≝ cminor_to_rtlabs p in |
---|
90 | ∃INV:cminor_rtlabs_inv (make_global … Cminor_fullexec p) (make_global … RTLabs_fullexec p'). |
---|
91 | ∃s'. make_initial_state … RTLabs_fullexec p' = OK … s' ∧ |
---|
92 | cminor_rtlabs_rel … INV s s'. |
---|
93 | |
---|
94 | include "common/FEMeasurable.ma". |
---|
95 | include "Cminor/Cminor_classified_system.ma". |
---|
96 | include "RTLabs/RTLabs_classified_system.ma". |
---|
97 | |
---|
98 | include "common/ExtraMonads.ma". |
---|
99 | |
---|
100 | lemma Cminor_return_E0 : ∀ge,s,tr,s'. |
---|
101 | step … Cminor_exec ge s = Value … 〈tr,s'〉 → |
---|
102 | Cminor_classify s = cl_return → |
---|
103 | tr = E0. |
---|
104 | #ge * |
---|
105 | [ #f #s #en #H1 #H2 #m #b #k #K #st #tr #s' #STEP #CL whd in CL:(??%?); destruct |
---|
106 | | #id #fd #args #m #st #tr #s' #STEP #CL whd in CL:(??%?); destruct |
---|
107 | | #v #m * |
---|
108 | [ #tr #s' #STEP #_ |
---|
109 | cases v in STEP; [ #E whd in E:(??%?); destruct ] |
---|
110 | * [1,3,4: normalize #A try #B destruct ] |
---|
111 | * #v #STEP whd in STEP:(??%?); destruct % |
---|
112 | | cases v |
---|
113 | [ * [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct // |
---|
114 | | normalize #A #B #C #D #E #F #G #H #I #J #K #L destruct |
---|
115 | ] |
---|
116 | | #v' * |
---|
117 | [ normalize #A #B #C #D #E #F #G #H #I #J #K destruct |
---|
118 | | #A #B #C #D #E #F #G #H #I #J #K #L whd in L:(??%?); destruct // |
---|
119 | ] |
---|
120 | ] |
---|
121 | ] |
---|
122 | | #r #tr #s' #ST #CL normalize in CL; destruct |
---|
123 | ] qed. |
---|
124 | |
---|
125 | (* Build the simulation record for FEMeasurable. Note that sim_call_label is |
---|
126 | made up of the single step for the call combined with a single step for the |
---|
127 | label. *) |
---|
128 | |
---|
129 | definition cminor_rtlabs_meas_sim : meas_sim ≝ |
---|
130 | mk_meas_sim |
---|
131 | Cminor_pcs |
---|
132 | RTLabs_pcs |
---|
133 | (λcmp,rap. cminor_to_rtlabs cmp = rap) |
---|
134 | cminor_rtlabs_inv |
---|
135 | cminor_rtlabs_rel |
---|
136 | ? (* rel_normal *) |
---|
137 | ? (* rel_labelled *) |
---|
138 | ? (* rel_classify_call *) |
---|
139 | ? (* rel_classify_return *) |
---|
140 | ? (* rel_callee *) |
---|
141 | ? (* labelled_normal_1 *) |
---|
142 | ? (* labelled_normal_2 *) |
---|
143 | ? (* notailcalls *) |
---|
144 | ? (* sim_normal *) |
---|
145 | ? (* sim_call_nolabel *) |
---|
146 | ? (* sim_call_label *) |
---|
147 | ? (* sim_return *) |
---|
148 | ? (* sim_cost *) |
---|
149 | ? (* sim_init *) |
---|
150 | . |
---|
151 | [ (* rel_normal *) |
---|
152 | | (* rel_labelled *) |
---|
153 | @cminor_rtlabs_rel_labelled |
---|
154 | | (* rel_classify_call *) |
---|
155 | | (* rel_classify_return *) |
---|
156 | | (* rel_callee *) |
---|
157 | | (* labelled_normal_1 *) |
---|
158 | #g * // |
---|
159 | | (* labelled_normal_2 *) |
---|
160 | #g * // #f #fs #m whd in ⊢ (?% → ?%); whd in match (pcs_classify ???); |
---|
161 | cases (next_instruction f) // |
---|
162 | | (* notailcalls *) |
---|
163 | #g @Cminor_notailcalls |
---|
164 | | (* sim_normal *) |
---|
165 | #g1 #g2 #INV #s1 #s1' #R1 #N1 #NCS1 #s2 #tr #STEP |
---|
166 | cases (cminor_rtlabs_normal … R1 N1 NCS1 STEP) |
---|
167 | #m #AFTER %{m} @(after_n_covariant … AFTER) |
---|
168 | #tr' #s * * #H1 #H2 #H3 /3/ |
---|
169 | | (* sim_call_nolabel *) |
---|
170 | #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP #NCS2 %{0} |
---|
171 | @(cminor_rtlabs_call_return … R1 … STEP) |
---|
172 | change with (Cminor_classify ?) in CL1:(??%?); >CL1 % |
---|
173 | | (* sim_call_label *) |
---|
174 | #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr2 #s3 #tr3 #STEP1 #CS2 #STEP2 %{1} |
---|
175 | lapply (cminor_rtlabs_call_return … R1 … STEP1) |
---|
176 | [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ] |
---|
177 | #AFTER1 @(after_n_covariant … AFTER1) #tr' #s' * #E #R' destruct |
---|
178 | % [ % |
---|
179 | [ % |
---|
180 | | change with (RTLabs_cost s') in ⊢ (?%); <(cminor_rtlabs_rel_labelled … R') @CS2 |
---|
181 | ]| lapply (cminor_rtlabs_cost … R' … CS2 STEP2) |
---|
182 | #AFTER2 cases (after_1_step … AFTER2) |
---|
183 | #trx * #sx * * #NFx #STEPx * #E #Rx destruct |
---|
184 | whd >NFx whd >STEPx whd /3/ |
---|
185 | ] |
---|
186 | | (* sim_return *) |
---|
187 | #g1 #g2 #INV #s1 #s1' #R1 #CL1 #NCS1 #s2 #tr #STEP %{0} |
---|
188 | lapply (cminor_rtlabs_call_return … R1 … STEP) |
---|
189 | [ change with (Cminor_classify ?) in CL1:(??%?); >CL1 % ] |
---|
190 | >(Cminor_return_E0 … STEP CL1) |
---|
191 | #AFTER %{(refl ??)} @AFTER |
---|
192 | | (* sim_cost *) |
---|
193 | #g1 #g2 #INV #s1 #s1' #s2 #tr #R1 #CS1 #STEP |
---|
194 | @(cminor_rtlabs_cost … R1 … STEP) |
---|
195 | @CS1 |
---|
196 | | (* sim_init *) |
---|
197 | #p #p' #s #COMPILE destruct #INIT |
---|
198 | cases (cminor_rtlabs_init … INIT) #INV * #s' * #INIT' #R |
---|
199 | %{s'} % [ @INIT' | %{INV} @R ] |
---|
200 | ] cases daemon qed. |
---|