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 | For call and return states we only allow the addition of extra steps *after* |
---|
26 | the corresponding call or return state (i.e., the simulation must always |
---|
27 | start with it). This is true in the front-end: Callstate and Returnstate |
---|
28 | are the second half of calls and returns, the first is the instruction for |
---|
29 | the call or return which is translated as a "normal" step, where any extra |
---|
30 | instructions for before the action are added. |
---|
31 | *) |
---|
32 | |
---|
33 | record meas_sim : Type[2] ≝ { |
---|
34 | ms_C1 : preclassified_system; |
---|
35 | ms_C2 : preclassified_system; |
---|
36 | ms_compiled : program … ms_C1 → program … ms_C2 → Prop; |
---|
37 | ms_inv : ? → ? → Type[0]; |
---|
38 | ms_rel : ∀g1,g2. ∀INV:ms_inv g1 g2. state … ms_C1 g1 → state … ms_C2 g2 → Prop; |
---|
39 | 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; |
---|
40 | 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; |
---|
41 | (* It's tempting to have a general result that states in the relation always |
---|
42 | have the same classification, but this may not be true when the step for |
---|
43 | s1 "disappears" in s2. The best we can do is match calls, returns and |
---|
44 | "normal" steps (above), because while we may switch cl_other and cl_jump, |
---|
45 | nothing ever collapses into a cl_call or cl_return because they are always |
---|
46 | preceeded by the corresponding instruction. *) |
---|
47 | ms_rel_classify_call : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_call → pcs_classify ms_C2 g2 s2 = cl_call; |
---|
48 | ms_rel_classify_return : ∀g1,g2,INV,s1,s2. ms_rel g1 g2 INV s1 s2 → pcs_classify ms_C1 g1 s1 = cl_return → pcs_classify ms_C2 g2 s2 = cl_return; |
---|
49 | 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'; |
---|
50 | |
---|
51 | (* These hold in (at least) the languages of interest for measurable subtraces *) |
---|
52 | ms_labelled_normal_1 : ∀g1,s1. pcs_labelled ms_C1 g1 s1 → pnormal_state ms_C1 g1 s1; |
---|
53 | ms_labelled_normal_2 : ∀g2,s2. pcs_labelled ms_C2 g2 s2 → pnormal_state ms_C2 g2 s2; |
---|
54 | ms_notailcalls : ∀g1,s1. pcs_classify ms_C1 g1 s1 ≠ cl_tailcall; |
---|
55 | |
---|
56 | (* Measure on source states; only needed for showing preservation of |
---|
57 | non-termination. Should not be necessary for showing that the measurable |
---|
58 | traces are preserved. |
---|
59 | |
---|
60 | Commented out because we're not using it for now. |
---|
61 | ms_measure1 : ∀g1. state … ms_C1 g1 → nat; |
---|
62 | *) |
---|
63 | |
---|
64 | sim_normal : |
---|
65 | ∀g1,g2. |
---|
66 | ∀INV:ms_inv g1 g2. |
---|
67 | ∀s1,s1'. |
---|
68 | ms_rel g1 g2 INV s1 s1' → |
---|
69 | pnormal_state ms_C1 g1 s1 → |
---|
70 | ¬ pcs_labelled ms_C1 g1 s1 → |
---|
71 | ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
72 | ∃m. after_n_steps m … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. |
---|
73 | tr = tr' ∧ |
---|
74 | ms_rel g1 g2 INV s2 s2' (*∧ |
---|
75 | (m = 0 → lt (ms_measure1 g1 s2) (ms_measure1 g1 s1))*) |
---|
76 | ); |
---|
77 | (* Naughty code without a cost label will end up being rejected, but we don't |
---|
78 | have local information about that. *) |
---|
79 | sim_call_nolabel : |
---|
80 | ∀g1,g2. |
---|
81 | ∀INV:ms_inv g1 g2. |
---|
82 | ∀s1,s1'. |
---|
83 | ms_rel g1 g2 INV s1 s1' → |
---|
84 | pcs_classify ms_C1 g1 s1 = cl_call → |
---|
85 | ¬ pcs_labelled ms_C1 g1 s1 → |
---|
86 | ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
87 | ¬ pcs_labelled ms_C1 g1 s2 → |
---|
88 | ∃m. |
---|
89 | after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. |
---|
90 | tr = tr' ∧ |
---|
91 | ms_rel g1 g2 INV s2 s2' |
---|
92 | ); |
---|
93 | (* Note that extra steps are introduced in the front-end to perform variable |
---|
94 | saves on entry. If there's a cost label (and there ought to be!) then we |
---|
95 | move it forward, so have to include it in the simulation. Unfortunately |
---|
96 | that's a little messy. *) |
---|
97 | sim_call_label : |
---|
98 | ∀g1,g2. |
---|
99 | ∀INV:ms_inv g1 g2. |
---|
100 | ∀s1,s1'. |
---|
101 | ms_rel g1 g2 INV s1 s1' → |
---|
102 | pcs_classify ms_C1 g1 s1 = cl_call → |
---|
103 | ¬ pcs_labelled ms_C1 g1 s1 → |
---|
104 | ∀s2,tr2,s3,tr3. |
---|
105 | step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr2,s2〉 → |
---|
106 | pcs_labelled ms_C1 g1 s2 → |
---|
107 | step … (pcs_exec ms_C1) g1 s2 = Value … 〈tr3,s3〉 → |
---|
108 | ∃m. |
---|
109 | after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. |
---|
110 | tr2 = tr' ∧ |
---|
111 | bool_to_Prop (pcs_labelled ms_C2 g2 s2') ∧ |
---|
112 | (after_n_steps m … (pcs_exec ms_C2) g2 s2' (λs.pnormal_state ms_C2 g2 s) (λtr'',s3'. |
---|
113 | tr'' = tr3 ∧ |
---|
114 | ms_rel g1 g2 INV s3 s3')) |
---|
115 | ); |
---|
116 | sim_return : |
---|
117 | ∀g1,g2. |
---|
118 | ∀INV:ms_inv g1 g2. |
---|
119 | ∀s1,s1'. |
---|
120 | ms_rel g1 g2 INV s1 s1' → |
---|
121 | pcs_classify ms_C1 g1 s1 = cl_return → |
---|
122 | ¬ pcs_labelled ms_C1 g1 s1 → |
---|
123 | (* NB: calls and returns don't emit timing cost labels; otherwise we would |
---|
124 | have to worry about whether the cost labels seen at the final return of |
---|
125 | the measured trace might appear in the target in subsequent steps that |
---|
126 | are *after* the new measurable subtrace. Also note that extra steps are |
---|
127 | introduced in the front-end: to perform variable saves on entry and to |
---|
128 | write back the result *after* exit. The latter do not get included in |
---|
129 | the measurable subtrace because it stops at the return, and they are the |
---|
130 | caller's responsibility. *) |
---|
131 | ∀s2,tr. step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
132 | ∃m. tr = E0 ∧ |
---|
133 | after_n_steps (S m) … (pcs_exec ms_C2) g2 s1' (λs.pnormal_state ms_C2 g2 s) (λtr',s2'. |
---|
134 | E0 = tr' ∧ |
---|
135 | ms_rel g1 g2 INV s2 s2' |
---|
136 | ); |
---|
137 | sim_cost : |
---|
138 | ∀g1,g2. |
---|
139 | ∀INV:ms_inv g1 g2. |
---|
140 | ∀s1,s1',s2,tr. |
---|
141 | ms_rel g1 g2 INV s1 s1' → |
---|
142 | pcs_labelled ms_C1 g1 s1 → |
---|
143 | step … (pcs_exec ms_C1) g1 s1 = Value … 〈tr,s2〉 → |
---|
144 | after_n_steps 1 … (pcs_exec ms_C2) g2 s1' (λs.true) (λtr',s2'. |
---|
145 | tr = tr' ∧ |
---|
146 | ms_rel g1 g2 INV s2 s2' |
---|
147 | ); |
---|
148 | sim_init : |
---|
149 | ∀p1,p2,s. |
---|
150 | ms_compiled p1 p2 → |
---|
151 | make_initial_state ?? ms_C1 p1 = OK ? s → |
---|
152 | ∃s'. make_initial_state ?? ms_C2 p2 = OK ? s' ∧ |
---|
153 | ∃INV. ms_rel ?? INV s s' |
---|
154 | }. |
---|
155 | |
---|
156 | |
---|
157 | |
---|
158 | lemma exec_steps_1_trace : ∀O,I,fx,g,s,trace,s'. |
---|
159 | exec_steps 1 O I fx g s = OK ? 〈trace,s'〉 → |
---|
160 | ∃tr. trace = [〈s,tr〉]. |
---|
161 | #O #I #fx #g #s #trace #s' #EXEC |
---|
162 | cases (exec_steps_S … EXEC) |
---|
163 | #nf * #tr * #s'' * #tl * * #E1 #STEP #EXEC' whd in EXEC':(??%%); destruct |
---|
164 | %{tr} % |
---|
165 | qed. |
---|
166 | |
---|
167 | lemma all_1 : ∀A.∀P:A → bool.∀x. |
---|
168 | P x = all A P [x]. |
---|
169 | #A #P #x whd in ⊢ (???%); cases (P x) // |
---|
170 | qed. |
---|
171 | |
---|
172 | (* First show that the trace up to the start of the measurable subtrace (i.e., |
---|
173 | the prefix of the execution) is preserved using the simulation results in |
---|
174 | the meas_sim record. Note that this doesn't end cleanly - the first states |
---|
175 | in the measurable subtrace may not be in the simulation relation, see the |
---|
176 | comment below. *) |
---|
177 | |
---|
178 | lemma prefix_preserved : |
---|
179 | ∀MS:meas_sim. |
---|
180 | ∀g,g'. |
---|
181 | ∀INV:ms_inv MS g g'. |
---|
182 | ∀s1,s1'. |
---|
183 | ms_rel MS g g' INV s1 s1' → |
---|
184 | |
---|
185 | ∀m,prefix,sf. |
---|
186 | exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈prefix,sf〉 → |
---|
187 | pcs_labelled (ms_C1 MS) g sf → |
---|
188 | |
---|
189 | (* Needed to ensure we can get back into the relation after a call *) |
---|
190 | (∃ex,sx. exec_steps 1 … (pcs_exec … (ms_C1 MS)) g sf = OK ? 〈ex,sx〉) → |
---|
191 | |
---|
192 | ∃m',prefix',sf'. |
---|
193 | exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈prefix',sf'〉 ∧ |
---|
194 | bool_to_Prop (pcs_labelled (ms_C2 MS) g' sf') ∧ |
---|
195 | intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) [ ] prefix = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') [ ] prefix' ∧ |
---|
196 | |
---|
197 | |
---|
198 | (* We may need to make extra steps to get back into the relation. In |
---|
199 | particular, the Clight to Cminor stage adds stores to the stack after |
---|
200 | the function call, but must preserve the position of the cost label at |
---|
201 | the head of the function, so we may need to move past these stores. *) |
---|
202 | ∃r,r',ex,ex',sr,sr'. |
---|
203 | exec_steps r … (pcs_exec … (ms_C1 MS)) g sf = OK … 〈ex,sr〉 ∧ |
---|
204 | bool_to_Prop (all … (λst.pnormal_state (ms_C1 MS) g (\fst st)) ex) ∧ |
---|
205 | exec_steps r' … (pcs_exec … (ms_C2 MS)) g' sf' = OK … 〈ex',sr'〉 ∧ |
---|
206 | bool_to_Prop (all … (λst.pnormal_state (ms_C2 MS) g' (\fst st)) ex') ∧ |
---|
207 | (∀cs. intensional_trace_of_trace (pcs_to_cs (ms_C1 MS) g) cs ex = intensional_trace_of_trace (pcs_to_cs (ms_C2 MS) g') cs ex') ∧ |
---|
208 | ms_rel MS g g' INV sr sr'. |
---|
209 | |
---|
210 | * #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls (*#measure1*) #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init |
---|
211 | #g #g' #INV #s1 #s1' #REL |
---|
212 | #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1' |
---|
213 | generalize in match [ ]; (* current call stack *) |
---|
214 | @(nat_elim1 m0) * |
---|
215 | [ #_ #current_stack #s1 #s1' #REL #prefix #sf #EXEC whd in EXEC:(??%?); destruct #CSf #_ |
---|
216 | %{0} %{[]} %{s1'} |
---|
217 | % [ % [ % [ // | <(rel_labelled … REL) // ] | // ] | %{0} %{0} %{[ ]} %{[ ]} %{sf} %{s1'} /6/ ] |
---|
218 | | #m #IH #current_stack #s1 #s1' #REL #prefix #sf #EXEC #CSf #EXTRA_STEP |
---|
219 | cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 |
---|
220 | cases (true_or_false_Prop … (pcs_labelled … s1)) |
---|
221 | [ #CS |
---|
222 | lapply (sim_cost … REL CS STEP1) |
---|
223 | #AFTER1' |
---|
224 | cases (after_n_exec_steps … AFTER1') |
---|
225 | #prefix' * #s2' * * #EXEC1' #_ * #Etrace #R2 |
---|
226 | cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 |
---|
227 | cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' |
---|
228 | cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] |
---|
229 | #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' |
---|
230 | %{(1+m'')} %{(prefix'@prefix'')} %{sf''} |
---|
231 | % [ % [ % |
---|
232 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
233 | | @CS'' |
---|
234 | ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // |
---|
235 | cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct |
---|
236 | <all_1 assumption |
---|
237 | ]| assumption |
---|
238 | ] |
---|
239 | |
---|
240 | | #NCS |
---|
241 | cases (true_or_false_Prop (pnormal_state C1 g s1)) |
---|
242 | [ #NORMAL |
---|
243 | (* XXX should set things up so that notb_Prop isn't needed *) |
---|
244 | cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1) |
---|
245 | #n' #AFTER1' |
---|
246 | cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
247 | cases (IH m ? current_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] |
---|
248 | #m'' * #prefix'' * #sf'' * * * #EXEC'' #CS'' #OBS'' #R'' |
---|
249 | %{(n'+m'')} %{(prefix'@prefix'')} %{sf''} |
---|
250 | % [ % [ % |
---|
251 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
252 | | @CS'' |
---|
253 | ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
254 | [ assumption |
---|
255 | | cases prefix' in EXEC1' INV ⊢ %; |
---|
256 | [ // |
---|
257 | | * #sx #trx #tl #EXEC1' #INV |
---|
258 | <(exec_steps_first … EXEC1') |
---|
259 | whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL |
---|
260 | @INV |
---|
261 | ] |
---|
262 | | @OBS'' |
---|
263 | ] |
---|
264 | ]| @R'' |
---|
265 | ] |
---|
266 | |
---|
267 | | #CALLRET |
---|
268 | cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) |
---|
269 | [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; |
---|
270 | lapply (no_tailcalls … s1) |
---|
271 | cases (pcs_classify … s1) in CALLRET ⊢ %; |
---|
272 | [ 1,3: #_ #_ /2/ |
---|
273 | | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) |
---|
274 | ] |
---|
275 | ] * #CL |
---|
276 | [ cases (true_or_false_Prop … (pcs_labelled … s2)) |
---|
277 | [ #CS2 |
---|
278 | (* Can we execute another step now, or shall we wait for later? *) |
---|
279 | cases m in IH EXEC2; |
---|
280 | [ #_ (* Nope, use extra step to get back into relation *) |
---|
281 | #EXEC2 whd in EXEC2:(??%%); destruct |
---|
282 | cases EXTRA_STEP #trx * #sx #EXTRA -EXTRA_STEP |
---|
283 | cases (exec_steps_S … EXTRA) #NFf * #trx' * #sx' * #tlx * * #Ex #EXTRA_STEP #EX' whd in EX':(??%?); destruct |
---|
284 | cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 EXTRA_STEP) |
---|
285 | #m' #AFTER1' |
---|
286 | cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace #CS2' #AFTER2' |
---|
287 | cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2 #R3 |
---|
288 | %{1} %{prefix1'} %{s2'} |
---|
289 | % [ % [ % |
---|
290 | [ @EXEC1' |
---|
291 | | @CS2' |
---|
292 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
293 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
294 | destruct <(append_nil … (?::prefix2)) in ⊢ (???%); |
---|
295 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
296 | [ whd in match (cs_classify ??); >CL % |
---|
297 | | whd in match (cs_classify ??); >(rel_classify_call … REL CL) % |
---|
298 | | @INV1 |
---|
299 | | % |
---|
300 | | @(rel_callee … REL) |
---|
301 | ] |
---|
302 | ]| %{1} %{m'} %{[〈sf,trx'〉]} %{prefix2'} %{sx} %{s3'} |
---|
303 | cut (all ? (λst.pnormal_state C2 g' (\fst st)) prefix2') |
---|
304 | [ cases prefix2' in EXEC2' INV2 ⊢ %; |
---|
305 | [ // |
---|
306 | | * #sp #trp #tlp #EXEC2' #INV2 |
---|
307 | whd in ⊢ (?%); <(exec_steps_first … EXEC2') |
---|
308 | >labelled_normal2 // |
---|
309 | ] |
---|
310 | ] #Np2' |
---|
311 | % [ % [ % [ % [ % |
---|
312 | [ @EXTRA |
---|
313 | | whd in ⊢ (?%); >labelled_normal1 // |
---|
314 | ]| @EXEC2' |
---|
315 | ]| @Np2' |
---|
316 | ]| #cs <(append_nil … prefix2') <Etrace2 |
---|
317 | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
318 | [ <normal_state_p @labelled_normal1 // |
---|
319 | | @Np2' |
---|
320 | | // |
---|
321 | ] |
---|
322 | ]| @R3 |
---|
323 | ] |
---|
324 | ] |
---|
325 | (* We can execute the cost label, too. *) |
---|
326 | | #m1 #IH #EXEC2 |
---|
327 | cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3 |
---|
328 | cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2) |
---|
329 | #m' #AFTER1' |
---|
330 | cases (after_n_exec_steps … AFTER1') #prefix1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2' |
---|
331 | cases (after_n_exec_steps … AFTER2') #prefix2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3 |
---|
332 | letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] |
---|
333 | cases (IH m1 ? next_stack … R3 … EXEC3 CSf EXTRA_STEP) [2: // ] |
---|
334 | #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' |
---|
335 | %{(S m' + m'')} %{(prefix1'@prefix2'@prefix'')} %{sf''} |
---|
336 | % [ % [ % |
---|
337 | [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC'' |
---|
338 | | @CSf'' |
---|
339 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
340 | #NF1' * #tr1' * #s2'' * #prefix2'' * * #E #STEP1' #EXEC2'' |
---|
341 | whd in EXEC2'':(??%%); |
---|
342 | destruct |
---|
343 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
344 | [ whd in match (cs_classify ??); >CL % |
---|
345 | | whd in match (cs_classify ??); >(rel_classify_call … REL CL) % |
---|
346 | | % |
---|
347 | | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
348 | [ <normal_state_p @labelled_normal1 @CS2 |
---|
349 | | cases prefix2' in EXEC2' INV2 ⊢ %; |
---|
350 | [ // |
---|
351 | | * #sy #try #tly #EXEC2' #INV2 |
---|
352 | <(exec_steps_first … EXEC2') |
---|
353 | whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 // |
---|
354 | ] |
---|
355 | | assumption |
---|
356 | ] |
---|
357 | | @(rel_callee … REL) |
---|
358 | ] |
---|
359 | ]| @R'' |
---|
360 | ] |
---|
361 | ] |
---|
362 | |
---|
363 | | #NCS2 |
---|
364 | cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1) |
---|
365 | [2: >CL % | 3: @notb_Prop @NCS2 ] |
---|
366 | #m' #AFTER1' |
---|
367 | cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
368 | letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] |
---|
369 | cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: // ] |
---|
370 | #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' |
---|
371 | %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} |
---|
372 | % [ % [ % |
---|
373 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
374 | | @CSf'' |
---|
375 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
376 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
377 | destruct |
---|
378 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
379 | [ whd in match (cs_classify ??); >CL % |
---|
380 | | whd in match (cs_classify ??); >(rel_classify_call … REL CL) % |
---|
381 | | @INV |
---|
382 | | assumption |
---|
383 | | @(rel_callee … REL) |
---|
384 | ] |
---|
385 | ]| @R'' |
---|
386 | ] |
---|
387 | ] |
---|
388 | |
---|
389 | | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] |
---|
390 | #m' * #Etr #AFTER1' |
---|
391 | cases (after_n_exec_steps … AFTER1') #prefix' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
392 | letin next_stack ≝ (tail … current_stack) |
---|
393 | cases (IH m ? next_stack … R2 … EXEC2 CSf EXTRA_STEP) [2: //] |
---|
394 | #m'' * #prefix'' * #sf'' * * * #EXEC'' #CSf'' #OBS'' #R'' |
---|
395 | %{(S m' + m'')} %{(prefix'@prefix'')} %{sf''} |
---|
396 | % [ % [ % |
---|
397 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
398 | | @CSf'' |
---|
399 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
400 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
401 | destruct >Etrace |
---|
402 | @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
403 | [ whd in match (cs_classify ??); >CL % |
---|
404 | | whd in match (cs_classify ??); @(rel_classify_return … REL CL) |
---|
405 | | @INV |
---|
406 | | assumption |
---|
407 | ] |
---|
408 | ]| @R'' |
---|
409 | ] |
---|
410 | ] |
---|
411 | ] |
---|
412 | ] |
---|
413 | ] qed. |
---|
414 | |
---|
415 | definition ends_at_return : ∀C:preclassified_system. ∀g. list (state … C g × trace) → Prop ≝ |
---|
416 | λC,g,x. ∃x',tr2,s2. x = x'@[〈s2,tr2〉] ∧ pcs_classify C g s2 = cl_return. |
---|
417 | |
---|
418 | lemma ends_at_return_append : ∀C,g,t1,t2. |
---|
419 | ends_at_return C g t2 → |
---|
420 | ends_at_return C g (t1@t2). |
---|
421 | #C #g #t1 #t2 * #x * #tr * #s * #E >E #CL |
---|
422 | %{(t1@x)} %{tr} %{s} % /2/ |
---|
423 | qed. |
---|
424 | |
---|
425 | lemma will_return_aux_normal : ∀C,depth,t1,t2. |
---|
426 | all … (λstr. normal_state C (\fst str)) t1 → |
---|
427 | will_return_aux C depth (t1@t2) = will_return_aux C depth t2. |
---|
428 | #C #depth #t1 #t2 elim t1 |
---|
429 | [ #_ % |
---|
430 | | * #s #tr #tl #IH #N cases (andb_Prop_true … N) #N1 #Ntl |
---|
431 | whd in ⊢ (??%?); |
---|
432 | cases (normal_state_inv … N1) #CL >CL |
---|
433 | @IH @Ntl |
---|
434 | ] qed. |
---|
435 | |
---|
436 | (* Now show the preservation of parts of the measurable subtrace from states in |
---|
437 | simulation to the end. (We'll deal with any extra steps at the start from |
---|
438 | the prefix lemma in the theorem below.) The basic idea here is that having |
---|
439 | broken up the simulation results into normal, call, return and cost lemmas, |
---|
440 | we can match up the structure of the two executions, and in particular |
---|
441 | prove the will_return_aux predicate for the target execution. *) |
---|
442 | |
---|
443 | lemma measurable_subtrace_preserved : |
---|
444 | ∀MS:meas_sim. |
---|
445 | ∀g,g'. |
---|
446 | ∀INV:ms_inv MS g g'. |
---|
447 | ∀s1,s1',depth,callstack. |
---|
448 | ms_rel MS g g' INV s1 s1' → |
---|
449 | |
---|
450 | let C ≝ pcs_to_cs (ms_C1 MS) g in |
---|
451 | let C' ≝ pcs_to_cs (ms_C2 MS) g' in |
---|
452 | |
---|
453 | ∀m,interesting,sf. |
---|
454 | exec_steps m … (pcs_exec … (ms_C1 MS)) g s1 = OK ? 〈interesting,sf〉 → |
---|
455 | ends_at_return (ms_C1 MS) g interesting → |
---|
456 | will_return_aux C depth interesting → |
---|
457 | |
---|
458 | ∃m',interesting',sf'. |
---|
459 | exec_steps m' … (pcs_exec … (ms_C2 MS)) g' s1' = OK ? 〈interesting',sf'〉 ∧ |
---|
460 | (* The obs trace equality almost gives this, but doesn't ensure the |
---|
461 | cost/return are exactly at the ends *) |
---|
462 | ends_at_return (ms_C2 MS) g' interesting' ∧ |
---|
463 | bool_to_Prop (will_return_aux C' depth interesting') ∧ |
---|
464 | |
---|
465 | intensional_trace_of_trace C callstack interesting = intensional_trace_of_trace C' callstack interesting'. |
---|
466 | (* Seems a shame to leave this out "∧ ms_rel MS g g' INV sf sf'", but it |
---|
467 | isn't true if the final return step is expanded into the caller, e.g., |
---|
468 | in Clight → Cminor we added an instruction to callers if they need to |
---|
469 | store the result in memory. This extra step doesn't form part of the |
---|
470 | measurable trace, so the end is no longer in the relation. ☹ *) |
---|
471 | |
---|
472 | * #C1 #C2 #compiled #inv #rel #rel_normal #rel_labelled #rel_classify_call #rel_classify_return #rel_callee #labelled_normal1 #labelled_normal2 #no_tailcalls (*#measure1*) #sim_normal #sim_call_nolabel #sim_call_label #sim_return #sim_cost #sim_init |
---|
473 | #g #g' #INV #s1 #s1' #depth #callstack #REL |
---|
474 | #m0 generalize in match s1' in REL ⊢ %; generalize in match s1; -s1 -s1' |
---|
475 | generalize in match callstack; generalize in match depth; -callstack -depth |
---|
476 | @(nat_elim1 m0) * |
---|
477 | [ #_ (* "fake" base case - we can never have zero steps *) |
---|
478 | #depth #current_stack #s1 #s1' #REL #interesting #sf #EXEC |
---|
479 | whd in EXEC:(??%?); destruct * * [2: #x1 #x2] * #x3 * #x4 * #x5 normalize in x5; destruct |
---|
480 | | #m #IH #depth #current_stack #s1 #s1' #REL #prefix #sf #EXEC #END #RETURNS |
---|
481 | cases (exec_steps_S … EXEC) #NF1 * #tr1 * #s2 * #trace2 * * #E1 #STEP1 #EXEC2 |
---|
482 | cases (true_or_false_Prop … (pcs_labelled … s1)) |
---|
483 | [ #CS |
---|
484 | lapply (sim_cost … REL CS STEP1) |
---|
485 | #AFTER1' |
---|
486 | cases (after_n_exec_steps … AFTER1') |
---|
487 | #interesting' * #s2' * * #EXEC1' #_ * #Etrace #R2 |
---|
488 | cut (pnormal_state C1 g s1) [ @labelled_normal1 assumption ] #N1 |
---|
489 | cut (pnormal_state C2 g' s1') [ @labelled_normal2 <(rel_labelled … REL) assumption ] #N1' |
---|
490 | cases (IH m ? depth current_stack … R2 … EXEC2 ??) |
---|
491 | [ 2: // |
---|
492 | | (* End must be later, and still a return *) |
---|
493 | 3: destruct cases END * |
---|
494 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
495 | #CL cases (pnormal_state_inv … N1) >CL #E destruct |
---|
496 | | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
497 | %{t} %{trE} %{sE} /2/ |
---|
498 | ] |
---|
499 | | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; |
---|
500 | cases (pnormal_state_inv … N1) #CL >CL in RETURNS; #RETURNS @RETURNS |
---|
501 | ] |
---|
502 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
503 | %{(1+m'')} %{(interesting'@interesting'')} %{sf''} |
---|
504 | % [ % [ % |
---|
505 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
506 | | @ends_at_return_append assumption |
---|
507 | ]| cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct |
---|
508 | >will_return_aux_normal |
---|
509 | [ @RETURNS'' |
---|
510 | | whd in ⊢ (?%); <normal_state_p >N1' % |
---|
511 | ] |
---|
512 | ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) // |
---|
513 | cases (exec_steps_1_trace … EXEC1') #tr1' #E destruct |
---|
514 | <all_1 assumption |
---|
515 | ] |
---|
516 | |
---|
517 | | #NCS |
---|
518 | cases (true_or_false_Prop (pnormal_state C1 g s1)) |
---|
519 | [ #NORMAL |
---|
520 | (* XXX should set things up so that notb_Prop isn't needed *) |
---|
521 | cases (sim_normal … REL NORMAL (notb_Prop … NCS) … STEP1) |
---|
522 | #n' #AFTER1' |
---|
523 | cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
524 | cases (IH m ? depth current_stack … R2 … EXEC2 ??) |
---|
525 | [ 2: // |
---|
526 | | (* End must be later, and still a return *) |
---|
527 | 3: destruct cases END * |
---|
528 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
529 | #CL cases (pnormal_state_inv … NORMAL) >CL #E destruct |
---|
530 | | #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
531 | %{t} %{trE} %{sE} /2/ |
---|
532 | ] |
---|
533 | | 4: destruct whd in RETURNS:(?%); whd in match (cs_classify ??) in RETURNS; |
---|
534 | cases (pnormal_state_inv … NORMAL) #CL >CL in RETURNS; #RETURNS @RETURNS |
---|
535 | ] |
---|
536 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
537 | %{(n'+m'')} %{(interesting'@interesting'')} %{sf''} |
---|
538 | % [ % [ % |
---|
539 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
540 | | @ends_at_return_append assumption |
---|
541 | ]| >will_return_aux_normal |
---|
542 | [ @RETURNS'' |
---|
543 | | cases n' in EXEC1'; |
---|
544 | [ #EXEC >(lenght_to_nil (*sic*) … interesting') // >(exec_steps_length … EXEC) % |
---|
545 | | #n'' #EXEC cases (exec_steps_S … EXEC) |
---|
546 | #_ * #tr1' * #s2' * #tl * * #E #STEP1' #EXEC2' destruct |
---|
547 | @andb_Prop [ <normal_state_p <(rel_normal … REL) @NORMAL | @INV ] |
---|
548 | ] |
---|
549 | ] |
---|
550 | ]| destruct @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
551 | [ assumption |
---|
552 | | cases interesting' in EXEC1' INV ⊢ %; |
---|
553 | [ // |
---|
554 | | * #sx #trx #tl #EXEC1' #INV |
---|
555 | <(exec_steps_first … EXEC1') |
---|
556 | whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >NORMAL |
---|
557 | @INV |
---|
558 | ] |
---|
559 | | @OBS'' |
---|
560 | ] |
---|
561 | ] |
---|
562 | |
---|
563 | | #CALLRET |
---|
564 | cases trace2 in E1 EXEC2; |
---|
565 | (* For a return we might hit the end - this is the real base case. *) |
---|
566 | [ #E1 #EXEC2 destruct cases END #tl * #tr * #s1x * #E1 #CL |
---|
567 | cases tl in E1; [2: #h * [2: #h2 #t] #E normalize in E; destruct ] |
---|
568 | #E1 normalize in E1; destruct |
---|
569 | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] |
---|
570 | #m' * #Etr #AFTER1' destruct |
---|
571 | cases (after_1_of_n_steps … AFTER1') #tr1' * #s2' * * * #NF1' #STEP1' #_ #AFTER2' |
---|
572 | cut (tr1' = E0) [ |
---|
573 | cases (after_n_exec_steps … AFTER2') #trace * #sf' * * #_ #_ * #H #_ |
---|
574 | cases (Eapp_E0_inv … (sym_eq … H)) // |
---|
575 | ] #E1 destruct |
---|
576 | %{1} %{[〈s1',E0〉]} %{s2'} |
---|
577 | % [ % [ % |
---|
578 | [ whd in ⊢ (??%?); >NF1' >STEP1' whd in ⊢ (??%?); % |
---|
579 | | %{[ ]} %{E0} %{s1'} %{(refl ??)} @(rel_classify_return … REL) assumption |
---|
580 | ]| whd in RETURNS:(?%) ⊢ (?%); |
---|
581 | whd in match (cs_classify ??) in RETURNS; |
---|
582 | whd in match (cs_classify ??); >(rel_classify_return … REL CL) |
---|
583 | >CL in RETURNS ⊢ %; whd in ⊢ (?% → ?%); |
---|
584 | cases depth [ // | #d * ] |
---|
585 | ]| <(append_nil … [〈s1',E0〉]) |
---|
586 | change with (gather_trace … [〈s1',E0〉]) in match E0 in ⊢ (??%?); |
---|
587 | @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
588 | [ @CL |
---|
589 | | whd in ⊢ (??%?); @(rel_classify_return … REL CL) |
---|
590 | | % |
---|
591 | | % |
---|
592 | ] |
---|
593 | ] |
---|
594 | ] |
---|
595 | (* Not at the end *) |
---|
596 | * #s2x #tr2 #trace3 #E1 #EXEC2 |
---|
597 | cut (pcs_classify C1 g s1 = cl_call ∨ pcs_classify C1 g s1 = cl_return) |
---|
598 | [ whd in CALLRET:(?%); whd in match (pnormal_state ???) in CALLRET; |
---|
599 | lapply (no_tailcalls … s1) |
---|
600 | cases (pcs_classify … s1) in CALLRET ⊢ %; |
---|
601 | [ 1,3: #_ #_ /2/ |
---|
602 | | *: normalize * #H #H' try cases (H I) cases H' #H'' cases (H'' (refl ??)) |
---|
603 | ] |
---|
604 | ] * #CL |
---|
605 | |
---|
606 | [ cases (true_or_false_Prop … (pcs_labelled … s2)) |
---|
607 | [ #CS2 |
---|
608 | (* We can't stop here *) |
---|
609 | cases m in IH EXEC2; |
---|
610 | [ #_ #EXEC2 whd in EXEC2:(??%%); destruct ] |
---|
611 | #m1 #IH #EXEC2 |
---|
612 | cases (exec_steps_S … EXEC2) #NF2 * #tr3 * #s3 * #tl3 * * #Etrace2 #STEP2 #EXEC3 |
---|
613 | cases (sim_call_label … REL … CL (notb_Prop … NCS) … STEP1 CS2 STEP2) |
---|
614 | #m' #AFTER1' |
---|
615 | cases (after_n_exec_steps … AFTER1') #interesting1' * #s2' * * #EXEC1' #INV1 * * #Etrace' #CS2' #AFTER2' |
---|
616 | cases (after_n_exec_steps … AFTER2') #interesting2' * #s3' * * #EXEC2' #INV2 * #Etrace2' #R3 |
---|
617 | letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] |
---|
618 | letin next_depth ≝ (S depth) |
---|
619 | cut (pnormal_state C1 g s2) [ @labelled_normal1 assumption ] #N2 |
---|
620 | cases (IH m1 ? next_depth next_stack … R3 … EXEC3 ??) |
---|
621 | [ 2: // |
---|
622 | | (* End must be later, and still a return *) |
---|
623 | 3: destruct cases END * |
---|
624 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
625 | | *: #h1 * |
---|
626 | [ * #trE * #sE * #E normalize in E:(???%); destruct |
---|
627 | #CL cases (pnormal_state_inv … N2) >CL #E destruct |
---|
628 | | #h2 #t * #trE * #sE * #E normalize in E:(???%); destruct #CL |
---|
629 | %{t} %{trE} %{sE} /2/ |
---|
630 | ] |
---|
631 | ] |
---|
632 | | 4: destruct whd in RETURNS:(?%); |
---|
633 | whd in match (cs_classify ??) in RETURNS; |
---|
634 | >CL in RETURNS; whd in ⊢ (?% → ?); |
---|
635 | cases (pnormal_state_inv … N2) #CL2 |
---|
636 | whd in match (cs_classify ??); >CL2 // |
---|
637 | ] |
---|
638 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
639 | %{(S m' + m'')} %{(interesting1'@interesting2'@interesting'')} %{sf''} |
---|
640 | % [ % [ % |
---|
641 | [ @(exec_steps_join … EXEC1') @(exec_steps_join … EXEC2') @EXEC'' |
---|
642 | | @ends_at_return_append @ends_at_return_append assumption |
---|
643 | ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2'' |
---|
644 | destruct whd in ⊢ (?%); whd in match (cs_classify ??); |
---|
645 | >(rel_classify_call … REL CL) whd in ⊢ (?%); whd in INV1:(?(???%)); |
---|
646 | >will_return_aux_normal [2: @INV1 ] |
---|
647 | >will_return_aux_normal |
---|
648 | [ // |
---|
649 | | cases interesting2' in EXEC2' INV2 ⊢ %; |
---|
650 | [ // |
---|
651 | | * #s2'' #tr2'' #tl2'' #E2'' <(exec_steps_first … E2'') #TL |
---|
652 | whd in ⊢ (?%); <normal_state_p >(labelled_normal2 … CS2') @TL |
---|
653 | ] |
---|
654 | ] |
---|
655 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
656 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2'' |
---|
657 | destruct |
---|
658 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
659 | [ whd in match (cs_classify ??); >CL % |
---|
660 | | whd in match (cs_classify ??); >(rel_classify_call … REL CL) % |
---|
661 | | @INV1 |
---|
662 | | @(build_eq_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
663 | (* Repeats bits of proof above, could compress *) |
---|
664 | [ <normal_state_p @labelled_normal1 @CS2 |
---|
665 | | cases interesting2' in EXEC2' INV2 ⊢ %; |
---|
666 | [ // |
---|
667 | | * #sy #try #tly #EXEC2' #INV2 |
---|
668 | <(exec_steps_first … EXEC2') |
---|
669 | whd in ⊢ (?%); <normal_state_p <(rel_normal … REL) >labelled_normal2 // |
---|
670 | ] |
---|
671 | | assumption |
---|
672 | ] |
---|
673 | | @(rel_callee … REL) |
---|
674 | ] |
---|
675 | ] |
---|
676 | |
---|
677 | | #NCS2 |
---|
678 | cases (sim_call_nolabel … REL … (notb_Prop … NCS) … STEP1) |
---|
679 | [2: >CL % | 3: @notb_Prop @NCS2 ] |
---|
680 | #m' #AFTER1' |
---|
681 | cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
682 | letin next_stack ≝ ((pcs_callee C1 g s1 ?)::current_stack) [2: >CL %] |
---|
683 | letin next_depth ≝ (S depth) |
---|
684 | cases (IH m ? next_depth next_stack … R2 … EXEC2 ??) |
---|
685 | [ 2: // |
---|
686 | | (* End must be later, and still a return *) |
---|
687 | 3: destruct cases END * |
---|
688 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
689 | | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
690 | %{t} %{trE} %{sE} /2/ |
---|
691 | ] |
---|
692 | | 4: destruct whd in RETURNS:(?%); |
---|
693 | whd in match (cs_classify ??) in RETURNS; |
---|
694 | >CL in RETURNS; // |
---|
695 | ] |
---|
696 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
697 | %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} |
---|
698 | % [ % [ % |
---|
699 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
700 | | @ends_at_return_append assumption |
---|
701 | ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' |
---|
702 | destruct whd in ⊢ (?%); whd in match (cs_classify ??); |
---|
703 | >(rel_classify_call … REL CL) whd in ⊢ (?%); |
---|
704 | >will_return_aux_normal // |
---|
705 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
706 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
707 | destruct |
---|
708 | @(build_call_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
709 | [ whd in match (cs_classify ??); >CL % |
---|
710 | | whd in match (cs_classify ??); >(rel_classify_call … REL CL) % |
---|
711 | | @INV |
---|
712 | | assumption |
---|
713 | | @(rel_callee … REL) |
---|
714 | ] |
---|
715 | ] |
---|
716 | ] |
---|
717 | | |
---|
718 | |
---|
719 | cases (sim_return … REL … (notb_Prop … NCS) … STEP1) [2: >CL %] |
---|
720 | #m' * #Etr #AFTER1' |
---|
721 | cases (after_n_exec_steps … AFTER1') #interesting' * #s2' * * #EXEC1' #INV * #Etrace #R2 |
---|
722 | letin next_stack ≝ (tail … current_stack) |
---|
723 | letin next_depth ≝ (pred depth) |
---|
724 | cases (IH m ? next_depth next_stack … R2 … EXEC2 ??) |
---|
725 | [ 2: // |
---|
726 | | (* End must be later, and still a return *) |
---|
727 | 3: destruct cases END * |
---|
728 | [ * #trE * #sE * #E whd in E:(???%); destruct |
---|
729 | | *: #h #t * #trE * #sE * #E whd in E:(???%); destruct #CL |
---|
730 | %{t} %{trE} %{sE} /2/ |
---|
731 | ] |
---|
732 | | 4: destruct whd in RETURNS:(?%); |
---|
733 | whd in match (cs_classify ??) in RETURNS; |
---|
734 | >CL in RETURNS; whd in ⊢ (?% → ?); |
---|
735 | whd in match next_depth; cases depth |
---|
736 | [ * | #d' // ] |
---|
737 | ] |
---|
738 | #m'' * #interesting'' * #sf'' * * * #EXEC'' #ENDS'' #RETURNS'' #OBS'' |
---|
739 | %{(S m' + m'')} %{(interesting'@interesting'')} %{sf''} |
---|
740 | % [ % [ % |
---|
741 | [ @(exec_steps_join … EXEC1') @EXEC'' |
---|
742 | | @ends_at_return_append assumption |
---|
743 | ]| cases (exec_steps_S … EXEC1') #NF1' * #tr1' * #s2' * #trace2' * * #E2 #STEP1' #EXEC2' |
---|
744 | destruct whd in RETURNS:(?%) ⊢ (?%); whd in match (cs_classify ??) in RETURNS ⊢ %; |
---|
745 | >(rel_classify_return … REL CL) in RETURNS ⊢ %; >CL whd in ⊢ (?% → ?%); |
---|
746 | whd in match next_depth in RETURNS''; |
---|
747 | cases depth in RETURNS'' ⊢ %; [ #_ * ] #depth' #RETURNS'' #_ |
---|
748 | whd in ⊢ (?%); |
---|
749 | >will_return_aux_normal [ @RETURNS'' | @INV ] |
---|
750 | ]| destruct cases (exec_steps_S … EXEC1') |
---|
751 | #NF1' * #tr1' * #s2' * #prefix2 * * #E #STEP1' #EXEC2' |
---|
752 | destruct >Etrace |
---|
753 | @(build_return_trace (pcs_to_cs C1 g) (pcs_to_cs C2 g')) |
---|
754 | [ whd in match (cs_classify ??); >CL % |
---|
755 | | whd in match (cs_classify ??); @(rel_classify_return … REL CL) |
---|
756 | | @INV |
---|
757 | | assumption |
---|
758 | ] |
---|
759 | ] |
---|
760 | ] |
---|
761 | ] qed. |
---|
762 | |
---|
763 | lemma label_to_ret_inv : ∀C,m,g,s,trace,s'. |
---|
764 | exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → |
---|
765 | trace_is_label_to_return (pcs_to_cs … C g) trace → |
---|
766 | bool_to_Prop (pcs_labelled C g s) ∧ ends_at_return C g trace. |
---|
767 | #C #m #g #s #trace #s' #EXEC |
---|
768 | * #tr * #s1 * #tl * #tr2 * #s2 * * #E #CS #CL destruct |
---|
769 | >(exec_steps_first … EXEC) |
---|
770 | % |
---|
771 | [ @CS |
---|
772 | | %{(〈s1,tr〉::tl)} %{tr2} %{s2} %{(refl ??)} @CL |
---|
773 | ] qed. |
---|
774 | |
---|
775 | lemma build_label_to_ret : ∀C,m,g,s,trace,s'. |
---|
776 | (∀s. pcs_labelled C g s → pnormal_state C g s) → |
---|
777 | exec_steps m … (pcs_exec … C) g s = OK ? 〈trace,s'〉 → |
---|
778 | pcs_labelled C g s → |
---|
779 | ends_at_return C g trace → |
---|
780 | trace_is_label_to_return (pcs_to_cs … C g) trace. |
---|
781 | #C #m #g #s #trace #s' #LABELLED_NORMAL #EXEC #CS * #trace' * #tr2 * #s2 * #E #CL |
---|
782 | destruct |
---|
783 | cases trace' in EXEC ⊢ %; |
---|
784 | [ #EXEC >(exec_steps_first … EXEC) in CS; #CS |
---|
785 | cases (pnormal_state_inv … (LABELLED_NORMAL … CS)) >CL #E destruct |
---|
786 | | * #s1 #tr1 #trace1 #EXEC |
---|
787 | %{tr1} %{s1} %{trace1} %{tr2} %{s2} % [ % [ % | <(exec_steps_first … EXEC) @CS ] | @CL ] |
---|
788 | ] qed. |
---|
789 | |
---|
790 | |
---|
791 | lemma ends_at_return_normal : ∀C,g,t1,t2. |
---|
792 | ends_at_return C g (t1@t2) → |
---|
793 | all … (λst. pnormal_state C g (\fst st)) t1 → |
---|
794 | ends_at_return C g t2. |
---|
795 | #C #g #t1 elim t1 |
---|
796 | [ // |
---|
797 | | * #s #tr #tl #IH #t2 * #tr1 * #tr2 * #s2 * cases tr1 |
---|
798 | [ #E normalize in E; destruct #CL whd in ⊢ (?% → ?); |
---|
799 | lapply (pnormal_state_inv … s2) |
---|
800 | cases (pnormal_state … s2) |
---|
801 | [ #H cases (H I) >CL #E' destruct |
---|
802 | | #_ * |
---|
803 | ] |
---|
804 | | * #s' #tr' #tl' #E whd in E:(??%%); destruct #CL #ALL |
---|
805 | @IH |
---|
806 | [ %{tl'} %{tr2} %{s2} >e0 % // |
---|
807 | | whd in ALL:(?%); cases (pnormal_state … s') in ALL; |
---|
808 | [ // | * ] |
---|
809 | ] |
---|
810 | ] |
---|
811 | ] qed. |
---|
812 | |
---|
813 | |
---|
814 | (* Now put the two main lemmas above together to show that the target has a |
---|
815 | [measurable] subtrace, and that the observables are the same. |
---|
816 | |
---|
817 | To deal with the extra steps from the prefix lemma, note that they are |
---|
818 | "normal" steps, and so cannot interfere with the structure. *) |
---|
819 | |
---|
820 | theorem measured_subtrace_preserved : |
---|
821 | ∀MS:meas_sim. |
---|
822 | ∀p1,p2,m,n,stack_cost,max. |
---|
823 | ms_compiled MS p1 p2 → |
---|
824 | measurable (ms_C1 MS) p1 m n stack_cost max → |
---|
825 | ∃m',n'. |
---|
826 | measurable (ms_C2 MS) p2 m' n' stack_cost max ∧ |
---|
827 | observables (ms_C1 MS) p1 m n = observables (ms_C2 MS) p2 m' n'. |
---|
828 | #MS #p1 #p2 #m #n #stack_cost #max #compiled |
---|
829 | * #s0 * #prefix * #s1 * #interesting * #s2 |
---|
830 | whd in ⊢ (? → ??(λ_.??(λ_.(?%(??%%))))); |
---|
831 | letin g ≝ (make_global … (pcs_exec … ) p1) |
---|
832 | letin g' ≝ (make_global … (pcs_exec … ) p2) |
---|
833 | letin C ≝ (pcs_to_cs ? g) |
---|
834 | letin C' ≝ (pcs_to_cs ? g') |
---|
835 | * * * * * #INIT #EXEC0 #EXEC1 #TLR #RETURNS #MAX |
---|
836 | |
---|
837 | cases (sim_init … compiled INIT) #s0' * #INIT' * #INV #R0 |
---|
838 | cases (label_to_ret_inv … EXEC1 TLR) |
---|
839 | #CS1 #ENDS |
---|
840 | |
---|
841 | cases (prefix_preserved MS g g' INV … R0 … EXEC0 CS1) |
---|
842 | (* Need an extra step from the source in case we end up at a label after a |
---|
843 | function call. *) |
---|
844 | [2: cases n in EXEC1; |
---|
845 | [ #E whd in E:(??%?); destruct cases RETURNS |
---|
846 | | #n1 #EXEC1 cases (exec_steps_split 1 … EXEC1) #ex * #ex2 * #sx * * #EX1 #_ #_ |
---|
847 | %{ex} %{sx} @EX1 |
---|
848 | ] |
---|
849 | ] |
---|
850 | #m' * #prefix' * #s1' * * * #EXEC0' #CS1' #OBS0 |
---|
851 | * #r * #r' * #interesting1 * #interesting1' * #sr * #sr' * * * * * #EXECr #Nr #EXECr' #Nr' #OBS1 #R1 |
---|
852 | |
---|
853 | (* Show that the extra r steps we need to get back into the relation are a |
---|
854 | prefix of the measurable subtrace. *) |
---|
855 | cut (∃nr,interesting2. n = r + nr ∧ |
---|
856 | exec_steps nr … C g sr = OK … 〈interesting2,s2〉 ∧ |
---|
857 | interesting = interesting1 @ interesting2) |
---|
858 | [ cases (plus_split n r) #nr * |
---|
859 | [ #En %{nr} >En in EXEC1; #EXEC1 |
---|
860 | cases (exec_steps_split … EXEC1) |
---|
861 | #interesting1x * #interesting2 * #srx * * #EXEC1x #EXECrx #E |
---|
862 | >EXECr in EXEC1x; #E1x destruct |
---|
863 | %{interesting2} % [ % [ % | assumption ] | % ] |
---|
864 | | #En @⊥ |
---|
865 | >En in EXECr; #EXECr cases (exec_steps_split … EXECr) |
---|
866 | #ex1 * #ex2 * #sx * * #EX1 #EXx #E >E in Nr; >EXEC1 in EX1; #E' destruct |
---|
867 | #Nr cases (andb_Prop_true … (all_append … Nr)) #N1 #N2 |
---|
868 | cases ENDS #le * #tre * #se * #Ee #CLe destruct |
---|
869 | cases (andb_Prop_true … (all_append … N1)) #_ whd in ⊢ (?% → ?); |
---|
870 | lapply (pnormal_state_inv … se) cases (pnormal_state … se) |
---|
871 | [ #H cases (H I) >CLe #E destruct |
---|
872 | | #_ * |
---|
873 | ] |
---|
874 | ] |
---|
875 | ] |
---|
876 | * #nr * #interesting2 * * #En #EXECr2 #Ei destruct |
---|
877 | |
---|
878 | whd in RETURNS:(?%); |
---|
879 | >will_return_aux_normal in RETURNS; |
---|
880 | [2: @Nr] #RETURNS |
---|
881 | |
---|
882 | lapply (ends_at_return_normal … ENDS Nr) |
---|
883 | #ENDS2 |
---|
884 | |
---|
885 | cases (measurable_subtrace_preserved MS … INV … (\fst (intensional_trace_of_trace C [ ] (prefix@interesting1))) R1 … EXECr2 ENDS2 RETURNS) |
---|
886 | #n' * #interesting' * #s2' * * * #EXEC1' #ENDS' #RETURNS' #OBS' |
---|
887 | |
---|
888 | cut (intensional_trace_of_trace C [ ] (prefix@interesting1) = |
---|
889 | intensional_trace_of_trace C' [ ] (prefix'@interesting1')) |
---|
890 | [ >int_trace_append' >(int_trace_append' C') |
---|
891 | <OBS0 @breakup_pair @breakup_pair @breakup_pair @breakup_pair |
---|
892 | <OBS1 % |
---|
893 | ] #OBS01 |
---|
894 | |
---|
895 | cut (intensional_trace_of_trace C [ ] (prefix@interesting1@interesting2) = |
---|
896 | intensional_trace_of_trace C' [ ] (prefix'@interesting1'@interesting')) |
---|
897 | [ <associative_append <associative_append |
---|
898 | >int_trace_append' >(int_trace_append' C') |
---|
899 | <OBS01 |
---|
900 | @breakup_pair @breakup_pair @breakup_pair @breakup_pair |
---|
901 | <OBS' % |
---|
902 | ] #Eobs |
---|
903 | |
---|
904 | lapply (exec_steps_join … EXECr' EXEC1') |
---|
905 | #EXECr'' |
---|
906 | |
---|
907 | %{m'} %{(r' + n')} % |
---|
908 | [ %{s0'} %{prefix'} %{s1'} %{(interesting1'@interesting')} %{s2'} |
---|
909 | % [ % [ % [ % [ % |
---|
910 | [ assumption |
---|
911 | | assumption |
---|
912 | ]| assumption |
---|
913 | ]| @(build_label_to_ret … EXECr'' ? (ends_at_return_append … ENDS')) |
---|
914 | [ #s #CS @(ms_labelled_normal_2 … CS) |
---|
915 | | <(ms_rel_labelled … R1) @CS1' |
---|
916 | ] |
---|
917 | ]| whd in ⊢ (?%); >will_return_aux_normal [2: @Nr'] @RETURNS' |
---|
918 | ]| <Eobs @MAX |
---|
919 | ] |
---|
920 | | >INIT >INIT' |
---|
921 | whd in ⊢ (??%%); >EXEC0 >EXEC0' |
---|
922 | whd in ⊢ (??%%); >EXEC1 >EXECr'' |
---|
923 | whd in ⊢ (??%%); >int_trace_append' in OBS'; <OBS0 |
---|
924 | cases (intensional_trace_of_trace C [ ] prefix) |
---|
925 | #cs #prefixtr whd in ⊢ (??(??(???%)?)(??(???%)?) → ??%%); |
---|
926 | >int_trace_append' >int_trace_append' <OBS1 |
---|
927 | @breakup_pair @breakup_pair @breakup_pair @breakup_pair @breakup_pair |
---|
928 | #OBS' <OBS' % |
---|
929 | ] qed. |
---|