1 | (* Show that measurable subtraces are preserved in the front-end. *) |
---|
2 | |
---|
3 | include "common/Measurable.ma". |
---|
4 | |
---|
5 | definition pnormal_state : ∀C:preclassified_system. ∀g. state … C g → bool ≝ |
---|
6 | λC,g,s. match pcs_classify C g s with [ cl_other ⇒ true | cl_jump ⇒ true | _ ⇒ false ]. |
---|
7 | |
---|
8 | lemma pnormal_state_inv : ∀C,g,s. |
---|
9 | pnormal_state C g s → |
---|
10 | pcs_classify C g s = cl_other ∨ pcs_classify C g s = cl_jump. |
---|
11 | #C #g #s whd in ⊢ (?% → ?); cases (pcs_classify C g s) /2/ * |
---|
12 | qed. |
---|
13 | |
---|
14 | lemma normal_state_p : ∀C,g,s. |
---|
15 | pnormal_state C g s = normal_state (pcs_to_cs C g) s. |
---|
16 | // |
---|
17 | qed. |
---|
18 | |
---|
19 | (* A record giving the languages and simulation results necessary to show that |
---|
20 | measurability is preserved. |
---|
21 | |
---|
22 | Note: as we're interested in measurable subtraces, we don't have to worry |
---|
23 | about the execution "going wrong." |
---|
24 | *) |
---|
25 | |
---|
26 | record meas_sim : Type[2] ≝ { |
---|
27 | ms_C1 : preclassified_system; |
---|
28 | ms_C2 : preclassified_system; |
---|
29 | ms_compiled : program … ms_C1 → program … ms_C2 → Prop; |
---|
30 | ms_inv : ? → ? → Type[0]; |
---|
31 | ms_stack : ∀g1,g2. ms_inv g1 g2 → (ident → nat); |
---|
32 | ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop; |
---|
33 | ms_rel_normal : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pnormal_state ms_C1 g1 s1 = pnormal_state ms_C2 g2 s2; |
---|
34 | ms_rel_labelled : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_labelled ms_C1 g1 s1 = pcs_labelled ms_C2 g2 s2; |
---|
35 | (* FIXME: this is almost certainly too strong if the step from s1 "disappears" in s2. *) |
---|
36 | ms_rel_classify : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = pcs_classify ms_C2 g2 s2; |
---|
37 | ms_rel_callee : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → ∀H,H'. pcs_callee ms_C1 g1 s1 H = pcs_callee ms_C2 g2 s2 H'; |
---|
38 | |
---|
39 | (* These hold in (at least) the languages of interest for measurable subtraces *) |
---|
40 | ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1; |
---|
41 | ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2; |
---|
42 | ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall; |
---|
43 | |
---|
44 | (* Measure on source states; only needed for showing preservation of |
---|
45 | non-termination. Should not be necessary for showing that the measurable |
---|
46 | traces are preserved. *) |
---|
47 | ms_measure1 : ∀g1. state … ms_C1 g1 → nat; |
---|
48 | |
---|
49 | sim_normal : |
---|
50 | ∀g1,g2. |
---|
51 | ∀INV:ms_inv g1 g2. |
---|
52 | ∀s1,s1'. |
---|
53 | ms_rel g1 g2 INV s1 s1' → |
---|
54 | pnormal_state ms_C1 g1 s1 → |
---|
55 | ¬ pcs_labelled ms_C1 g1 s1 → |
---|
56 | ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
57 | ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. |
---|
58 | tr = tr' ∧ |
---|
59 | ms_rel g1 g2 INV s2 s2' ∧ |
---|
60 | (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1)) |
---|
61 | ); |
---|
62 | sim_call_return : |
---|
63 | ∀g1,g2. |
---|
64 | ∀INV:ms_inv g1 g2. |
---|
65 | ∀s1,s1'. |
---|
66 | ms_rel g1 g2 INV s1 s1' → |
---|
67 | match pcs_classify ms_C1 g1 s1 with [ cl_call ⇒ true | cl_return ⇒ true | _ ⇒ false] → |
---|
68 | ¬ pcs_labelled ms_C1 g1 s1 → |
---|
69 | (* NB: calls and returns don't emit timing cost labels; otherwise we would |
---|
70 | have to worry about whether the cost labels seen at the final return of |
---|
71 | the measured trace might appear in the target in subsequent steps that |
---|
72 | are *after* the new measurable subtrace. Also note that extra steps are |
---|
73 | introduced in the front-end: to perform variable saves on entry and to |
---|
74 | write back the result *after* exit. The latter do not get included in |
---|
75 | the measurable subtrace because it stops at the return, and they are the |
---|
76 | caller's responsibility. *) |
---|
77 | ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
78 | ∃m. tr = E0 ∧ |
---|
79 | after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. |
---|
80 | E0 = tr' ∧ |
---|
81 | ms_rel g1 g2 INV s2 s2' |
---|
82 | ); |
---|
83 | sim_cost : |
---|
84 | ∀g1,g2. |
---|
85 | ∀INV:ms_inv g1 g2. |
---|
86 | ∀s1,s1',s2,tr. |
---|
87 | ms_rel g1 g2 INV s1 s1' → |
---|
88 | pcs_labelled ms_C1 g1 s1 → |
---|
89 | step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
90 | after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'. |
---|
91 | tr = tr' ∧ |
---|
92 | ms_rel g1 g2 INV s2 s2' |
---|
93 | ); |
---|
94 | sim_init : |
---|
95 | ∀p1,p2,s. |
---|
96 | ms_compiled p1 p2 → |
---|
97 | make_initial_state ?? ms_C1 p1 = OK ? s → |
---|
98 | ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧ |
---|
99 | ∃INV. ms_rel ?? INV s s' |
---|
100 | }. |
---|
101 | |
---|
102 | |
---|
103 | (* |
---|
104 | lemma stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. |
---|
105 | exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → |
---|
106 | pnormal_state C g s1 → |
---|
107 | stack_after (pcs_to_cs C g stack) current trace = current. |
---|
108 | #C #g #s1 #trace #s2 #stack #current #EXEC |
---|
109 | cases (exec_steps_S … EXEC) |
---|
110 | #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct |
---|
111 | #N |
---|
112 | whd in ⊢ (??%?); generalize in match (cs_stack ??); |
---|
113 | whd in match (cs_classify ??); |
---|
114 | cases (pnormal_state_inv … N) |
---|
115 | #CL >CL #f % |
---|
116 | qed. |
---|
117 | |
---|
118 | lemma max_stack_normal_step : ∀C:preclassified_system. ∀g,s1,trace,s2,stack,current. |
---|
119 | exec_steps 1 io_out io_in C g s1 = OK ? 〈trace,s2〉 → |
---|
120 | pnormal_state C g s1 → |
---|
121 | max_stack (pcs_to_cs C g stack) current trace = current. |
---|
122 | #C #g #s1 #trace #s2 #stack #current #EXEC |
---|
123 | cases (exec_steps_S … EXEC) |
---|
124 | #NF * #tr * #s' * #tl * * #Etr #STEP #EXEC' whd in EXEC':(??%?); destruct |
---|
125 | #N |
---|
126 | whd in ⊢ (??%?); generalize in match (cs_stack ??); |
---|
127 | whd in match (cs_classify ??); |
---|
128 | cases (pnormal_state_inv … N) |
---|
129 | #CL >CL #f % |
---|
130 | qed. |
---|
131 | |
---|
132 | lemma exec_split : ∀C:preclassified_system.∀g,m,s1,trace,sf. |
---|
133 | exec_steps m io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 → |
---|
134 | ¬pcs_labelled C g s1 → |
---|
135 | pcs_labelled C g sf → |
---|
136 | ∀inv. (∀s. bool_to_Prop (inv s) → ¬pcs_labelled C g s) → |
---|
137 | ∀n,P. after_n_steps n io_out io_in (pcs_exec … C) g s1 inv P → |
---|
138 | ∃p,trace1,s2,trace2. |
---|
139 | exec_steps n io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧ |
---|
140 | P (gather_trace … trace1) s2 ∧ |
---|
141 | exec_steps p io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉 ∧ |
---|
142 | m = n + p. |
---|
143 | #C #g #m elim m -m |
---|
144 | [ #s1 #trace #sf #EXEC whd in EXEC:(??%?); destruct |
---|
145 | #NCS #CS @⊥ @(absurd … CS) @Prop_notb @NCS |
---|
146 | | #m #IH #s1 #trace #sf #EXEC1 #NCS1 #CS2 #inv #H * |
---|
147 | [ #P #AFTER %{(S m)} %{[ ]} %{s1} %{trace} % [ % [ % [ % | @AFTER ] | @EXEC1 ]| % ] |
---|
148 | | #n #P #AFTER |
---|
149 | cases (exec_steps_S … EXEC1) |
---|
150 | #NF1 * #tr1 * #s2 * #tl * * #Etrace #STEP #EXEC2 |
---|
151 | cases (after_1_of_n_steps … AFTER) |
---|
152 | #tr1' * #s2' * * * #NF1' #STEP' #INV2 #AFTER2 |
---|
153 | >STEP in STEP'; #E destruct |
---|
154 | cases (IH … EXEC2 … AFTER2) |
---|
155 | [ #p * #trace1 * #s2 * #trace2 * * * #EXEC2' #P2 #EXEC2 #E |
---|
156 | %{p} % [2: %{s2} %{trace2} % [ % [ % |
---|
157 | [ @(exec_steps_join 1 … EXEC2') [2: whd in ⊢ (??%?); >NF1 in ⊢ (??%?); >STEP in ⊢ (??%?); % | skip ] |
---|
158 | | @P2 ]| @EXEC2 ]| >E % ] | skip ] |
---|
159 | | @H assumption |
---|
160 | | assumption |
---|
161 | | assumption |
---|
162 | ] |
---|
163 | ] |
---|
164 | ] qed. |
---|
165 | |
---|
166 | lemma exec_split1 : ∀C:preclassified_system.∀g,m,s1,trace,sf. |
---|
167 | exec_steps (S m) io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace,sf〉 → |
---|
168 | ∀P,inv. after_n_steps 1 io_out io_in (pcs_exec … C) g s1 inv P → |
---|
169 | ∃trace1,s2,trace2. |
---|
170 | exec_steps 1 io_out io_in (pcs_exec … C) g s1 = OK ? 〈trace1,s2〉 ∧ |
---|
171 | P (gather_trace … trace1) s2 ∧ |
---|
172 | exec_steps m io_out io_in (pcs_exec … C) g s2 = OK ? 〈trace2,sf〉. |
---|
173 | #C #g #m #s1 #trace #sf #EXEC1 #P #inv #AFTER1 |
---|
174 | cases (exec_steps_S … EXEC1) |
---|
175 | #NF1 * #tr * #s2 * #tl * * #E1 destruct #STEP #EXEC2 |
---|
176 | %{[〈s1,tr〉]} %{s2} %{tl} % [ % |
---|
177 | [ whd in ⊢ (??%?); >NF1 >STEP % | whd in AFTER1; >NF1 in AFTER1; >STEP normalize |
---|
178 | cases (inv s2) // * ]| // ] |
---|
179 | qed. |
---|
180 | *) |
---|
181 | (* XXX do I need to do the max_stack reasoning here? perhaps just by preserving |
---|
182 | observables? *) |
---|
183 | |
---|
184 | lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'. |
---|
185 | exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 → |
---|
186 | ∃tr. trace = [〈s,tr〉]. |
---|
187 | #O #I #fx #g #s #trace #s' #EXEC |
---|
188 | cases (exec_steps_S … EXEC) |
---|
189 | #nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct |
---|
190 | %{tr} % |
---|
191 | qed. |
---|
192 | |
---|
193 | lemma all_1 : ∀A.∀P:A → bool.∀x. |
---|
194 | P x = all A P [x]. |
---|
195 | #A #P #x whd in ⊢ (???%); cases (P x) // |
---|
196 | qed. |
---|
197 | |
---|
198 | |
---|
199 | lemma prefix_preserved : |
---|
200 | ∀MS:meas_sim. |
---|
201 | ∀g,g'. |
---|
202 | ∀INV:ms_inv MS g g'. |
---|
203 | ∀s1,s1'. |
---|
204 | ms_rel MS g g' INV s1 s1' → |
---|
205 | |
---|
206 | ∀m,prefix,sf. |
---|
207 | exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → |
---|
208 | pcs_labelled (ms_C1 MS) g sf → |
---|
209 | |
---|
210 | ∃m',prefix',sf'. |
---|
211 | exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧ |
---|
212 | |
---|
213 | intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧ |
---|
214 | ms_rel MS g g' INV sf sf'. |
---|
215 | * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init |
---|
216 | #g #g' #INV #s1 #s1' #REL |
---|
217 | #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1' |
---|
218 | generalize in match [ ]; (* current call stack *) |
---|
219 | elim m0 |
---|
220 | [ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf |
---|
221 | %{0} %{[]} %{s1'} |
---|
222 | % [ % // | // ] |
---|
223 | | #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf |
---|
224 | cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 |
---|
225 | cases (true_or_false_Prop … (pcs_labelled … s1)) |
---|
226 | [ #CS |
---|
227 | lapply (sim_cost … REL CS STEP1) |
---|
228 | #AFTER1' |
---|
229 | cases (after_n_exec_steps … AFTER1') |
---|
230 | #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2 |
---|
231 | cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 |
---|
232 | cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' |
---|
233 | cases (IH current_stack … R2 … EXEC2 CSf) |
---|
234 | #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' |
---|
235 | %{(1+m'')} %{(prefix'@prefix'')} %{sf''} |
---|
236 | % [ % [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
237 | | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // |
---|
238 | cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct |
---|
239 | <all_1 assumption |
---|
240 | ]| assumption |
---|
241 | ] |
---|
242 | |
---|
243 | | #NCS |
---|
244 | cases (true_or_false_Prop (pnormal_state C1 g s1)) |
---|
245 | [ #NORMAL |
---|
246 | (* XXX should set things up so that notb_Prop isn't needed *) |
---|
247 | cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1) |
---|
248 | #n' #AFTER1' |
---|
249 | cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *) |
---|
250 | cases (IH current_stack … R2 … EXEC2 CSf) |
---|
251 | #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' |
---|
252 | %{(n'+m'')} %{(prefix'@prefix'')} %{sf''} |
---|
253 | % [ % [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
254 | | destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
255 | [ assumption |
---|
256 | | cases prefix' in EXEC1' INV ⊢ %; |
---|
257 | [ // |
---|
258 | | * #sx #trx #tl #EXEC1' #INV |
---|
259 | <(exec_steps_first … EXEC1') |
---|
260 | whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL |
---|
261 | @INV |
---|
262 | ] |
---|
263 | | @OBS'' ] ] |
---|
264 | | @R'' |
---|
265 | ] |
---|
266 | | #CALLRET |
---|
267 | cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) |
---|
268 | [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; |
---|
269 | lapply (no_tailcalls … s1) |
---|
270 | cases (pcs_classify … s1) in CALLRET ⊢ %; |
---|
271 | [ 1,3: #_ #_ /2/ |
---|
272 | | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) |
---|
273 | ] |
---|
274 | ] * #CL |
---|
275 | cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) |
---|
276 | [2,4: >CL %] |
---|
277 | #m' * #Etr #AFTER1' |
---|
278 | cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
279 | [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] |
---|
280 | | letin next_stack ≝ (tail … current_stack) |
---|
281 | ] |
---|
282 | cases (IH next_stack … R2 … EXEC2 CSf) |
---|
283 | #m'' * #prefix'' * #sf'' * * #EXEC'' #OBS'' #R'' |
---|
284 | %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} |
---|
285 | % [1,3: % [1,3: @(exec_steps_join … EXEC1') @EXEC'' |
---|
286 | | destruct cases (exec_steps_S … EXEC1') |
---|
287 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
288 | destruct >Etrace |
---|
289 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
290 | [ whd in match (cs_classify ??); >CL % |
---|
291 | | whd in match (cs_classify ??); <(rel_classify … REL) >CL % |
---|
292 | | @INV |
---|
293 | | assumption |
---|
294 | | @(rel_callee … REL) |
---|
295 | ] |
---|
296 | | destruct cases (exec_steps_S … EXEC1') |
---|
297 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
298 | destruct >Etrace |
---|
299 | @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
300 | [ whd in match (cs_classify ??); >CL % |
---|
301 | | whd in match (cs_classify ??); <(rel_classify … REL) >CL % |
---|
302 | | @INV |
---|
303 | | assumption |
---|
304 | ] |
---|
305 | ] |
---|
306 | | 2,4: @R'' |
---|
307 | ] |
---|
308 | ] |
---|
309 | ] |
---|
310 | ] qed. |
---|
311 | |
---|
312 | definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝ |
---|
313 | λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return. |
---|
314 | |
---|
315 | lemma ends_at_return_append : ∀C,g,t1,t2. |
---|
316 | ends_at_return C g t2 → |
---|
317 | ends_at_return C g (t1@t2). |
---|
318 | #C #g #t1 #t2 * #x * #tr * #s * #E >E #CL |
---|
319 | %{(t1@x)} %{tr} %{s} % /2/ |
---|
320 | qed. |
---|
321 | |
---|
322 | lemma will_return_aux_normal : ∀C,depth,t1,t2. |
---|
323 | all … (λstr. normal_state C (\fst str)) t1 → |
---|
324 | will_return_aux C depth (t1@t2) = will_return_aux C depth t2. |
---|
325 | #C #depth #t1 #t2 elim t1 |
---|
326 | [ #_ % |
---|
327 | | * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
328 | whd in ⊢ (??%?); |
---|
329 | cases (normal_state_inv … N1) #CL >CL |
---|
330 | @IH @Ntl |
---|
331 | ] qed. |
---|
332 | |
---|
333 | lemma measurable_subtrace_preserved : |
---|
334 | ∀MS:meas_sim. |
---|
335 | ∀g,g'. |
---|
336 | ∀INV:ms_inv MS g g'. |
---|
337 | ∀s1,s1',depth,callstack. |
---|
338 | ms_rel MS g g' INV s1 s1' → |
---|
339 | |
---|
340 | let C ≝ pcs_to_cs (ms_C1 MS) g in |
---|
341 | let C' ≝ pcs_to_cs (ms_C2 MS) g' in |
---|
342 | |
---|
343 | ∀m,interesting,sf. |
---|
344 | exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 → |
---|
345 | ends_at_return (ms_C1 MS) g interesting → |
---|
346 | will_return_aux C depth interesting → |
---|
347 | |
---|
348 | ∃m',interesting',sf'. |
---|
349 | exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧ |
---|
350 | (* The obs trace equality almost gives this, but doesn't ensure the |
---|
351 | cost/return are exactly at the ends *) |
---|
352 | ends_at_return (ms_C2 MS) g' interesting' ∧ |
---|
353 | bool_to_Prop (will_return_aux C' depth interesting') ∧ |
---|
354 | |
---|
355 | intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'. |
---|
356 | (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it |
---|
357 | isn't true if the final return step is expanded into the caller, e.g., |
---|
358 | in Clight → Cminor we added an instruction to callers if they need to |
---|
359 | store the result in memory. This extra step doesn't form part of the |
---|
360 | measurable trace, so the end is no longer in the relation. ☹ *) |
---|
361 | |
---|
362 | * #C1 #C2 #compiled #inv #stack #rel #rel_normal #rel_labelled #rel_classify #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls #measure1 #sim_normal #sim_call_return #sim_cost #sim_init |
---|
363 | #g #g' #INV #s1 #s1' #depth #callstack #REL |
---|
364 | #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1' |
---|
365 | generalize in match callstack; generalize in match depth; -callstack -depth |
---|
366 | elim m0 |
---|
367 | [ (* "fake" base case - we can never have zero steps *) |
---|
368 | #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC |
---|
369 | whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct |
---|
370 | | #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS |
---|
371 | cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 |
---|
372 | cases (true_or_false_Prop … (pcs_labelled … s1)) |
---|
373 | [ #CS |
---|
374 | lapply (sim_cost … REL CS STEP1) |
---|
375 | #AFTER1' |
---|
376 | cases (after_n_exec_steps … AFTER1') |
---|
377 | #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2 |
---|
378 | cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 |
---|
379 | cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' |
---|
380 | cases (IH depth current_stack … R2 … EXEC2 ??) |
---|
381 | [ (* End must be later, and still a return *) |
---|
382 | 2: destruct cases END * |
---|
383 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
384 | #CL cases (pnormal_state_inv … N1) >CL #E destruct |
---|
385 | | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
386 | %{t} %{trE} %{sE} /2/ |
---|
387 | ] |
---|
388 | | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; |
---|
389 | cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS |
---|
390 | ] |
---|
391 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
392 | %{(1+m'')} %{(interesting'@interesting'')} %{sf''} |
---|
393 | % [ % [ % |
---|
394 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
395 | | @ends_at_return_append assumption |
---|
396 | ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct |
---|
397 | whd in ⊢ (?%); whd in match (cs_classify ??); <(rel_classify … REL) |
---|
398 | cases (pnormal_state_inv … N1) #CL >CL @RETURNS'' |
---|
399 | ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // |
---|
400 | cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct |
---|
401 | <all_1 assumption |
---|
402 | ] |
---|
403 | |
---|
404 | | #NCS |
---|
405 | cases (true_or_false_Prop (pnormal_state C1 g s1)) |
---|
406 | [ #NORMAL |
---|
407 | (* XXX should set things up so that notb_Prop isn't needed *) |
---|
408 | cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1) |
---|
409 | #n' #AFTER1' |
---|
410 | cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * * #Etrace #R2 #_ (* measure *) |
---|
411 | cases (IH depth current_stack … R2 … EXEC2 ??) |
---|
412 | [ (* End must be later, and still a return *) |
---|
413 | 2: destruct cases END * |
---|
414 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
415 | #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct |
---|
416 | | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
417 | %{t} %{trE} %{sE} /2/ |
---|
418 | ] |
---|
419 | | 3: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; |
---|
420 | cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS |
---|
421 | ] |
---|
422 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
423 | %{(n'+m'')} %{(interesting'@interesting'')} %{sf''} |
---|
424 | % [ % [ % |
---|
425 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
426 | | @ends_at_return_append assumption |
---|
427 | ]| >will_return_aux_normal |
---|
428 | [ @RETURNS'' |
---|
429 | | cases n' in EXEC1'; |
---|
430 | [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) % |
---|
431 | | #n'' #EXEC cases (exec_steps_S … EXEC) |
---|
432 | #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct |
---|
433 | @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL | @INV ] |
---|
434 | ] |
---|
435 | ] |
---|
436 | ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
437 | [ assumption |
---|
438 | | cases interesting' in EXEC1' INV ⊢ %; |
---|
439 | [ // |
---|
440 | | * #sx #trx #tl #EXEC1' #INV |
---|
441 | <(exec_steps_first … EXEC1') |
---|
442 | whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL |
---|
443 | @INV |
---|
444 | ] |
---|
445 | | @OBS'' |
---|
446 | ] |
---|
447 | ] |
---|
448 | |
---|
449 | | #CALLRET |
---|
450 | cases trace2 in E1 EXEC2; |
---|
451 | (* For a return we might hit the end - this is the real base case. *) |
---|
452 | [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL |
---|
453 | cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ] |
---|
454 | #E1 normalize in E1; destruct |
---|
455 | cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) |
---|
456 | [2: >CL %] |
---|
457 | #m' * #Etr #AFTER1' destruct |
---|
458 | cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2' |
---|
459 | cut (tr1' = E0) [ |
---|
460 | cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_ |
---|
461 | cases (Eapp_E0_inv … (sym_eq … H)) // |
---|
462 | ] #E1 destruct |
---|
463 | %{1} %{[〈s1',E0〉]} %{s2'} |
---|
464 | % [ % [ % |
---|
465 | [ whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); % |
---|
466 | | %{[ ]} %{E0} %{s1'} %{(refl ??)} <(rel_classify … REL) assumption |
---|
467 | ]| whd in RETURNS:(?%) ⊢ (?%); |
---|
468 | whd in match (cs_classify ??) in RETURNS; |
---|
469 | whd in match (cs_classify ??); <(rel_classify … REL) |
---|
470 | >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%); |
---|
471 | cases depth [ // | #d * ] |
---|
472 | ]| <(append_nil … [〈s1',E0〉]) |
---|
473 | change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?); |
---|
474 | @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
475 | [ @CL |
---|
476 | | whd in ⊢ (??%?); <(rel_classify … REL) @CL |
---|
477 | | % |
---|
478 | | % |
---|
479 | ] |
---|
480 | ] |
---|
481 | ] * #s2x #tr2 #trace3 #E1 #EXEC2 |
---|
482 | cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) |
---|
483 | [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; |
---|
484 | lapply (no_tailcalls … s1) |
---|
485 | cases (pcs_classify … s1) in CALLRET ⊢ %; |
---|
486 | [ 1,3: #_ #_ /2/ |
---|
487 | | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) |
---|
488 | ] |
---|
489 | ] * #CL |
---|
490 | cases (sim_call_return … REL … (notb_Prop … NCS) … STEP1) |
---|
491 | [2,4: >CL %] |
---|
492 | #m' * #Etr #AFTER1' |
---|
493 | cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
494 | [ letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] |
---|
495 | letin next_depth ≝ (S depth) |
---|
496 | | letin next_stack ≝ (tail … current_stack) |
---|
497 | letin next_depth ≝ (pred depth) |
---|
498 | ] |
---|
499 | cases (IH next_depth next_stack … R2 … EXEC2 ??) |
---|
500 | [(* End must be later, and still a return *) |
---|
501 | 2,5: destruct cases END * |
---|
502 | [1,3: * #trE * #sE * #E whd in E:(???%); destruct |
---|
503 | |*: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
504 | %{t} %{trE} %{sE} /2/ |
---|
505 | ] |
---|
506 | | 3: destruct whd in RETURNS:(?%); |
---|
507 | whd in match (cs_classify ??) in RETURNS; |
---|
508 | >CL in RETURNS; // |
---|
509 | | 6: destruct whd in RETURNS:(?%); |
---|
510 | whd in match (cs_classify ??) in RETURNS; |
---|
511 | >CL in RETURNS; whd in ⊢ (?% → ?); |
---|
512 | whd in match next_depth; cases depth |
---|
513 | [ * | #d' // ] |
---|
514 | ] |
---|
515 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
516 | %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} |
---|
517 | % [1,3: % [1,3: % |
---|
518 | [1,3: @(exec_steps_join … EXEC1') @EXEC'' |
---|
519 | |2,4: @ends_at_return_append assumption |
---|
520 | ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' |
---|
521 | destruct whd in ⊢ (?%); whd in match (cs_classify ??); |
---|
522 | <(rel_classify … REL) >CL whd in ⊢ (?%); |
---|
523 | >will_return_aux_normal // |
---|
524 | | cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' |
---|
525 | destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; |
---|
526 | <(rel_classify … REL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); |
---|
527 | whd in match next_depth in RETURNS''; |
---|
528 | cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ |
---|
529 | whd in ⊢ (?%); |
---|
530 | >will_return_aux_normal [ @RETURNS'' | @INV ] |
---|
531 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
532 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
533 | destruct >Etrace |
---|
534 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
535 | [ whd in match (cs_classify ??); >CL % |
---|
536 | | whd in match (cs_classify ??); <(rel_classify … REL) >CL % |
---|
537 | | @INV |
---|
538 | | assumption |
---|
539 | | @(rel_callee … REL) |
---|
540 | ] |
---|
541 | | destruct cases (exec_steps_S … EXEC1') |
---|
542 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
543 | destruct >Etrace |
---|
544 | @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
545 | [ whd in match (cs_classify ??); >CL % |
---|
546 | | whd in match (cs_classify ??); <(rel_classify … REL) >CL % |
---|
547 | | @INV |
---|
548 | | assumption |
---|
549 | ] |
---|
550 | ] |
---|
551 | ] |
---|
552 | ] |
---|
553 | ] qed. |
---|
554 | |
---|
555 | lemma label_to_ret_inv : ∀C,m,g,s,trace,s'. |
---|
556 | exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → |
---|
557 | trace_is_label_to_return (pcs_to_cs … C g) trace → |
---|
558 | bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace. |
---|
559 | #C #m #g #s #trace #s' #EXEC |
---|
560 | * #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct |
---|
561 | >(exec_steps_first … EXEC) |
---|
562 | % |
---|
563 | [ @CS |
---|
564 | | %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL |
---|
565 | ] qed. |
---|
566 | |
---|
567 | lemma build_label_to_ret : ∀C,m,g,s,trace,s'. |
---|
568 | (∀s. pcs_labelled C g s → pnormal_state C g s) → |
---|
569 | exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → |
---|
570 | pcs_labelled C g s → |
---|
571 | ends_at_return C g trace → |
---|
572 | trace_is_label_to_return (pcs_to_cs … C g) trace. |
---|
573 | #C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL |
---|
574 | destruct |
---|
575 | cases trace' in EXEC ⊢ %; |
---|
576 | [ #EXEC >(exec_steps_first … EXEC) in CS; #CS |
---|
577 | cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct |
---|
578 | | * #s1 #tr1 #trace1 #EXEC |
---|
579 | %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ] |
---|
580 | ] qed. |
---|
581 | |
---|
582 | |
---|
583 | theorem measured_subtrace_preserved : |
---|
584 | ∀MS:meas_sim. |
---|
585 | ∀p1,p2,m,n,stack_cost,max. |
---|
586 | ms_compiled MS p1 p2 → |
---|
587 | measurable (ms_C1 MS) p1 m n stack_cost max → |
---|
588 | ∃m',n'. |
---|
589 | measurable (ms_C2 MS) p2 m' n' stack_cost max ∧ |
---|
590 | observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. |
---|
591 | #MS #p1 #p2 #m #n #stack_cost #max #compiled |
---|
592 | * #s0 * #prefix * #s1 * #interesting * #s2 |
---|
593 | whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%))))); |
---|
594 | letin g ≝ (make_global … (pcs_exec … ) p1) |
---|
595 | letin g' ≝ (make_global … (pcs_exec … ) p2) |
---|
596 | letin C ≝ (pcs_to_cs ? g) |
---|
597 | letin C' ≝ (pcs_to_cs ? g') |
---|
598 | * * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX |
---|
599 | |
---|
600 | cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0 |
---|
601 | cases (label_to_ret_inv … EXEC1 TLR) |
---|
602 | #CS1 #ENDS |
---|
603 | |
---|
604 | cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1) |
---|
605 | #m' * #prefix' * #s1' * * #EXEC0' #OBS0 #R1 |
---|
606 | |
---|
607 | cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] prefix)) R1 … EXEC1 ENDS RETURNS) |
---|
608 | #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS' |
---|
609 | |
---|
610 | cut (intensional_trace_of_trace C [ ] (prefix@interesting) = |
---|
611 | intensional_trace_of_trace C' [ ] (prefix'@interesting')) |
---|
612 | [ >int_trace_append' >int_trace_append' |
---|
613 | <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair |
---|
614 | <OBS' % |
---|
615 | ] #Eobs |
---|
616 | |
---|
617 | %{m'} %{n'} % |
---|
618 | [ %{s0'} %{prefix'} %{s1'} %{interesting'} %{s2'} |
---|
619 | % [ % [ % [ % [ % |
---|
620 | [ assumption |
---|
621 | | assumption |
---|
622 | ]| assumption |
---|
623 | ]| @(build_label_to_ret … EXEC1' ? ENDS') |
---|
624 | [ #s #CS @(ms_labelled_normal_2 … CS) |
---|
625 | | <(ms_rel_labelled … R1) @CS1 |
---|
626 | ] |
---|
627 | ]| @RETURNS' |
---|
628 | ]| <Eobs @MAX |
---|
629 | ] |
---|
630 | | >INIT >INIT' |
---|
631 | whd in ⊢ (??%%); >EXEC0 >EXEC0' |
---|
632 | whd in ⊢ (??%%); >EXEC1 >EXEC1' |
---|
633 | whd in ⊢ (??%%); <OBS0 cases (intensional_trace_of_trace C [ ] prefix) in OBS' ⊢ %; |
---|
634 | #cs #prefixtr #OBS' whd in ⊢ (??%%); >OBS' % |
---|
635 | ] qed. |
---|