1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "common/StructuredTraces.ma". |
---|
16 | |
---|
17 | (* We work with two relations on states in parallel, as well as two derived ones. |
---|
18 | sem_rel is the classic semantic relation between states, keeping track of |
---|
19 | memory and how program counters are mapped between languages. |
---|
20 | call_rel keeps track of what pcs corresponding calls have and just that: |
---|
21 | this is different than corresponance between program counters in sem_rel when |
---|
22 | CALL f ↦ instr* CALL f instr* *) |
---|
23 | |
---|
24 | record status_rel |
---|
25 | (S1 : abstract_status) |
---|
26 | (S2 : abstract_status) |
---|
27 | : Type[1] ≝ |
---|
28 | { sem_rel :2> S1 → S2 → Prop |
---|
29 | (* this is kept separate, as not necessarily carrier will |
---|
30 | synchronise on calls. It should state the minimal properties |
---|
31 | necessary for as_after_return (typically just the program counter) |
---|
32 | maybe what function is called too? *) |
---|
33 | ; call_rel : (Σs.as_classifier S1 s cl_call) → |
---|
34 | (Σs.as_classifier S2 s cl_call) → Prop |
---|
35 | ; sim_final : |
---|
36 | ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2 |
---|
37 | }. |
---|
38 | |
---|
39 | (* The two derived relations are |
---|
40 | label_rel which tells that the two states are colabelled |
---|
41 | ret_rel which tells that two return states are in relation: the idea is that |
---|
42 | it happens when "going back" through as_after_return on one side we get |
---|
43 | a pair of call_rel related states, then we enjoy as_after_return also on the |
---|
44 | other. Roughly call_rel will store just enough information so that we can |
---|
45 | advance locally on a return step and build structured traces any way *) |
---|
46 | |
---|
47 | (* if we later generalise, we should move this inside status_rel *) |
---|
48 | definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2. |
---|
49 | |
---|
50 | definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2. |
---|
51 | λs1_ret,s2_ret. |
---|
52 | ∀s1_pre,s2_pre.as_after_return S1 s1_pre s1_ret → |
---|
53 | call_rel ?? R s1_pre s2_pre → |
---|
54 | as_after_return S2 s2_pre s2_ret. |
---|
55 | |
---|
56 | (* the base property we ask for simulation to work depends on the status_class |
---|
57 | S will mark semantic relation, C call relation, L label relation, R return relation *) |
---|
58 | |
---|
59 | definition status_simulation ≝ |
---|
60 | λS1 : abstract_status. |
---|
61 | λS2 : abstract_status. |
---|
62 | λsim_status_rel : status_rel S1 S2. |
---|
63 | ∀st1,st1',st2.as_execute S1 st1 st1' → |
---|
64 | sim_status_rel st1 st2 → |
---|
65 | match as_classify … st1 with |
---|
66 | [ cl_call ⇒ ∀prf. |
---|
67 | (* |
---|
68 | st1' ------------S----------\ |
---|
69 | ↑ \ \ |
---|
70 | st1 \--L--\ \ |
---|
71 | | \ \ \ |
---|
72 | S \-C-\ st2_after_call →taa→ st2' |
---|
73 | | \ ↑ |
---|
74 | st2 →taa→ st2_pre_call |
---|
75 | *) |
---|
76 | ∃st2_pre_call. |
---|
77 | as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ |
---|
78 | call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ |
---|
79 | ∃st2_after_call,st2'. |
---|
80 | ∃taa2 : trace_any_any … st2 st2_pre_call. |
---|
81 | ∃taa2' : trace_any_any … st2_after_call st2'. |
---|
82 | as_execute … st2_pre_call st2_after_call ∧ |
---|
83 | sim_status_rel st1' st2' ∧ |
---|
84 | label_rel … st1' st2_after_call |
---|
85 | | cl_tailcall ⇒ ∀prf. |
---|
86 | (* |
---|
87 | st1' ------------S----------\ |
---|
88 | ↑ \ \ |
---|
89 | st1 \--L--\ \ |
---|
90 | | \ \ |
---|
91 | S st2_after_call →taa→ st2' |
---|
92 | | ↑ |
---|
93 | st2 →taa→ st2_pre_call |
---|
94 | *) |
---|
95 | ∃st2_pre_call. |
---|
96 | as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧ |
---|
97 | ∃st2_after_call,st2'. |
---|
98 | ∃taa2 : trace_any_any … st2 st2_pre_call. |
---|
99 | ∃taa2' : trace_any_any … st2_after_call st2'. |
---|
100 | as_execute … st2_pre_call st2_after_call ∧ |
---|
101 | sim_status_rel st1' st2' ∧ |
---|
102 | label_rel … st1' st2_after_call |
---|
103 | | cl_return ⇒ |
---|
104 | (* |
---|
105 | st1 |
---|
106 | / ↓ |
---|
107 | | st1'----------S,L------------\ |
---|
108 | S \ \ |
---|
109 | \ \-----R-------\ | |
---|
110 | \ | | |
---|
111 | st2 →taa→ st2_ret | | |
---|
112 | ↓ / | |
---|
113 | st2_after_ret →taaf→ st2' |
---|
114 | |
---|
115 | we also ask that st2_after_ret be not labelled if the taaf tail is |
---|
116 | not empty |
---|
117 | *) |
---|
118 | ∃st2_ret,st2_after_ret,st2'. |
---|
119 | ∃taa2 : trace_any_any … st2 st2_ret. |
---|
120 | ∃taa2' : trace_any_any_free … st2_after_ret st2'. |
---|
121 | (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ |
---|
122 | as_classifier … st2_ret cl_return ∧ |
---|
123 | as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ |
---|
124 | ret_rel … sim_status_rel st1' st2_after_ret ∧ |
---|
125 | label_rel … st1' st2' |
---|
126 | | cl_other ⇒ |
---|
127 | (* |
---|
128 | st1 → st1' |
---|
129 | | \ |
---|
130 | S S,L |
---|
131 | | \ |
---|
132 | st2 →taaf→ st2' |
---|
133 | |
---|
134 | the taaf can be empty (e.g. tunneling) but we ask it must not be the |
---|
135 | case when both st1 and st1' are labelled (we would be able to collapse |
---|
136 | labels otherwise) |
---|
137 | *) |
---|
138 | ∃st2'. |
---|
139 | ∃taa2 : trace_any_any_free … st2 st2'. |
---|
140 | (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ |
---|
141 | sim_status_rel st1' st2' ∧ |
---|
142 | label_rel … st1' st2' |
---|
143 | | cl_jump ⇒ |
---|
144 | (* just like cl_other, but with a hypothesis more *) |
---|
145 | as_costed … st1' → |
---|
146 | ∃st2'. |
---|
147 | ∃taa2 : trace_any_any_free … st2 st2'. |
---|
148 | (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ |
---|
149 | sim_status_rel st1' st2' ∧ |
---|
150 | label_rel … st1' st2' |
---|
151 | ]. |
---|
152 | |
---|
153 | |
---|
154 | (* some useful lemmas *) |
---|
155 | |
---|
156 | let rec taa_append_tal_rel S1 fl1 st1 st1' |
---|
157 | (tal1 : trace_any_label S1 fl1 st1 st1') |
---|
158 | S2 st2 st2mid fl2 st2' |
---|
159 | (taa2 : trace_any_any S2 st2 st2mid) |
---|
160 | (tal2 : trace_any_label S2 fl2 st2mid st2') |
---|
161 | on tal1 : |
---|
162 | tal_rel … tal1 tal2 → |
---|
163 | tal_rel … tal1 (taa2 @ tal2) ≝ |
---|
164 | match tal1 return λfl1,st1,st1',tal1.? with |
---|
165 | [ tal_base_not_return st1 st1' _ _ _ ⇒ ? |
---|
166 | | tal_base_return st1 st1' _ _ ⇒ ? |
---|
167 | | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ? |
---|
168 | | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ? |
---|
169 | | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ? |
---|
170 | | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ? |
---|
171 | ]. |
---|
172 | [ * #EQfl *#st2mid *#taa2' *#H2 *#G2 *#K2 #EQ |
---|
173 | | * #EQfl *#st2mid *#taa2' *#H2 *#G2 #EQ |
---|
174 | | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 * |
---|
175 | [ *#K2 *#tlr2 *#L2 * #EQ #EQ' |
---|
176 | | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll |
---|
177 | ] |
---|
178 | | * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ' |
---|
179 | | * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 * |
---|
180 | [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ' |
---|
181 | | *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #EQ'' |
---|
182 | ] |
---|
183 | | whd in ⊢ (%→%); @(taa_append_tal_rel … tl1) |
---|
184 | ] |
---|
185 | destruct |
---|
186 | <associative_taa_append_tal |
---|
187 | [1,2,3,4,5:%{(refl …)}] %{st2mid} |
---|
188 | [1,2:|*: %{G2} %{EQcall} ] |
---|
189 | %{(taa_append_taa … taa2 taa2')} |
---|
190 | [1,2: %{H2} %{G2} [%{K2}] % |
---|
191 | |5: %{st2mid'} %{H2} %{tlr2} % // |
---|
192 | |*: %{st2mid'} %{H2} |
---|
193 | [1,3: %1 [|%{(refl …)}] |*: %2 %{st2mid''} ] |
---|
194 | %{K2} %{tlr2} %{L2} [3,4: %{tl2} ] /3 by conj/ |
---|
195 | ] |
---|
196 | qed. |
---|
197 | |
---|
198 | (* |
---|
199 | check trace_any_label_label |
---|
200 | let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2) |
---|
201 | on tal : as_costed … st2 ≝ |
---|
202 | match tal return λfl,st1,st2,tal.fl = doesnt_end_with_ret → as_costed ? st2 with |
---|
203 | [ tal_step_call fl' _ _ st1' st2' _ _ _ _ _ tl ⇒ λprf.tal_end_costed ? st1' st2' (tl⌈trace_any_label ????↦?⌉) |
---|
204 | | tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ λprf.tal_end_costed ? st1'st2' (tl⌈trace_any_label ????↦?⌉) |
---|
205 | | tal_base_not_return _ st2' _ _ K ⇒ λ_.K |
---|
206 | | tal_base_return _ _ _ _ ⇒ λprf.⊥ |
---|
207 | | tal_base_call _ _ st2' _ _ _ _ K ⇒ λ_.K |
---|
208 | ] (refl …). |
---|
209 | [ destruct |
---|
210 | |*: >prf % |
---|
211 | ] |
---|
212 | qed. |
---|
213 | *) |
---|
214 | |
---|
215 | lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2. |
---|
216 | if taa_non_empty … taa then ¬as_costed … s2 else True. |
---|
217 | #S #s1 #s2 #taa elim taa -s1 -s2 normalize nodelta |
---|
218 | [ #s1 % |
---|
219 | | #s1 #s2 #s3 #H #G #K #tl lapply K lapply H cases tl -s2 -s3 |
---|
220 | [ #s2 #H #K #_ assumption |
---|
221 | | #s2 #s3 #s4 #H' #G' #K' #tl' #H #K #I @I |
---|
222 | ] |
---|
223 | ] |
---|
224 | qed. |
---|
225 | |
---|
226 | let rec tal_collapsable_to_rel S fl st1 st2 |
---|
227 | (tal : trace_any_label S fl st1 st2) on tal : |
---|
228 | tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J. |
---|
229 | tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) ≝ |
---|
230 | match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∀S2,st12,st22,H,I,J. |
---|
231 | tal_rel … tal (tal_base_not_return S2 st12 st22 H I J) |
---|
232 | with |
---|
233 | [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_to_rel ???? tl |
---|
234 | | tal_base_not_return _ st2' _ _ K ⇒ ? |
---|
235 | | _ ⇒ Ⓧ |
---|
236 | ]. |
---|
237 | * #S2 #st12 #st22 #H #I #J % %[|%{(taa_base ??)} %[|%[|%[| % |
---|
238 | qed. |
---|
239 | |
---|
240 | let rec tal_collapsable_eq_flag S fl st1 st2 |
---|
241 | (tal : trace_any_label S fl st1 st2) on tal : |
---|
242 | tal_collapsable ???? tal → fl = doesnt_end_with_ret ≝ |
---|
243 | match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → fl = ? |
---|
244 | with |
---|
245 | [ tal_step_default fl' _ st1' st2' _ tl _ _ ⇒ tal_collapsable_eq_flag ???? tl |
---|
246 | | tal_base_not_return _ st2' _ _ K ⇒ λ_.refl … |
---|
247 | | _ ⇒ Ⓧ |
---|
248 | ]. |
---|
249 | |
---|
250 | let rec tal_collapsable_split S fl st1 st2 |
---|
251 | (tal : trace_any_label S fl st1 st2) on tal : |
---|
252 | tal_collapsable ???? tal → ∃st2_mid.∃taa : trace_any_any S st1 st2_mid.∃H,I,J. |
---|
253 | tal ≃ taa @ tal_base_not_return … st2 H I J ≝ |
---|
254 | match tal return λfl,st1,st2,tal.tal_collapsable ???? tal → ∃st2_mid,taa,H,I,J. |
---|
255 | tal ≃ taa @ tal_base_not_return … st2_mid ? H I J |
---|
256 | with |
---|
257 | [ tal_step_default fl' st1' st2' st3' H tl I J ⇒ ? |
---|
258 | | tal_base_not_return st1' st2' H I J ⇒ ? |
---|
259 | | _ ⇒ Ⓧ |
---|
260 | ]. |
---|
261 | [ * %{st1'} %{(taa_base …)} %{H} %{I} %{J} % |
---|
262 | | #coll |
---|
263 | elim (tal_collapsable_split … tl coll) #st2_mid * #taa * #H' * #I' *#J' |
---|
264 | #EQ %{st2_mid} %{(taa_step … taa)} try assumption |
---|
265 | %{H'} %{I'} %{J'} lapply EQ lapply tl >(tal_collapsable_eq_flag … coll) -tl #tl |
---|
266 | #EQ >EQ % |
---|
267 | ] |
---|
268 | qed. |
---|
269 | |
---|
270 | lemma tal_collapsable_to_rel_symm : ∀S,fl,st1,st2,tal. |
---|
271 | tal_collapsable S fl st1 st2 tal → ∀S2,st12,st22,H,I,J. |
---|
272 | tal_rel … (tal_base_not_return S2 st12 st22 H I J) tal. |
---|
273 | #S #fl #st1 #st2 #tal #coll #S2 #st12 #st22 #H #I #J |
---|
274 | elim (tal_collapsable_split … coll) lapply tal |
---|
275 | >(tal_collapsable_eq_flag … coll) -tal #tal |
---|
276 | #st2_mid * #taa *#H' *#I' *#J' #EQ >EQ % [%] |
---|
277 | %[|%[|%[|%[|%[| % ]]]]] |
---|
278 | qed. |
---|
279 | |
---|
280 | lemma taaf_append_tal_rel : ∀S1,fl1,st1,st1',S2,fl2,st2_pre,st2,st2',tal1,taaf2,H,tal2. |
---|
281 | tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' tal1 tal2 → |
---|
282 | tal_rel … tal1 (taaf_append_tal S2 st2_pre … taaf2 H tal2). |
---|
283 | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 * -H7 -H8 normalize |
---|
284 | [ // |3: #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 generalize in match (? : False); * ] |
---|
285 | #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 |
---|
286 | change with (taa_step ???? ??? (taa_base ??) @ H23) in match (tal_step_default ?????????); |
---|
287 | /2 by taa_append_tal_rel/ |
---|
288 | qed. |
---|
289 | |
---|
290 | (* little helpers *) |
---|
291 | lemma if_else_True : ∀b,P.P → if b then P else True. |
---|
292 | * // qed-. |
---|
293 | lemma if_then_True : ∀b,P.P → if b then True else P. |
---|
294 | * // qed-. |
---|
295 | |
---|
296 | include alias "basics/logic.ma". |
---|
297 | |
---|
298 | let rec status_simulation_produce_tlr S1 S2 R |
---|
299 | (* we start from this situation |
---|
300 | st1 →→→→tlr→→→→ st1' |
---|
301 | | \ |
---|
302 | L \---S--\ |
---|
303 | | \ |
---|
304 | st2_lab →taa→ st2 (the taa preamble is in general either empty or given |
---|
305 | by the preceding call) |
---|
306 | |
---|
307 | and we produce |
---|
308 | st1 →→→→tlr→→→→ st1' |
---|
309 | \\ / \ |
---|
310 | // R \-L,S-\ |
---|
311 | \\ | \ |
---|
312 | st2_lab →tlr→ st2_mid →taaf→ st2' |
---|
313 | *) |
---|
314 | st1 st1' st2_lab st2 |
---|
315 | (tlr1 : trace_label_return S1 st1 st1') |
---|
316 | (taa2_pre : trace_any_any S2 st2_lab st2) |
---|
317 | (sim_execute : status_simulation S1 S2 R) |
---|
318 | on tlr1 : R st1 st2 → label_rel … st1 st2_lab → |
---|
319 | ∃st2_mid.∃st2'. |
---|
320 | ∃tlr2 : trace_label_return S2 st2_lab st2_mid. |
---|
321 | ∃taa2 : trace_any_any_free … st2_mid st2'. |
---|
322 | (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧ |
---|
323 | R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧ |
---|
324 | tlr_rel … tlr1 tlr2 ≝ |
---|
325 | match tlr1 with |
---|
326 | [ tlr_base st1 st1' tll1 ⇒ ? |
---|
327 | | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ? |
---|
328 | ] |
---|
329 | and status_simulation_produce_tll S1 S2 R |
---|
330 | (* we start from this situation |
---|
331 | st1 →→→→tll→→→ st1' |
---|
332 | | \ |
---|
333 | L \---S--\ |
---|
334 | | \ |
---|
335 | st2_lab →taa→ st2 |
---|
336 | |
---|
337 | and if the tll is a returning one we produce a diagram like the one for tlr, |
---|
338 | otherwise a simpler: |
---|
339 | st1 →→→→tll→→→→ st1' |
---|
340 | \\ | |
---|
341 | // L,S |
---|
342 | \\ | |
---|
343 | st2_lab →→→tll→→→ st2' |
---|
344 | *) |
---|
345 | fl st1 st1' st2_lab st2 |
---|
346 | (tll1 : trace_label_label S1 fl st1 st1') |
---|
347 | (taa2_pre : trace_any_any S2 st2_lab st2) |
---|
348 | (sim_execute : status_simulation S1 S2 R) |
---|
349 | on tll1 : R st1 st2 → label_rel … st1 st2_lab → |
---|
350 | match fl with |
---|
351 | [ ends_with_ret ⇒ |
---|
352 | ∃st2_mid.∃st2'. |
---|
353 | ∃tll2 : trace_label_label S2 ends_with_ret st2_lab st2_mid. |
---|
354 | ∃taa2 : trace_any_any_free … st2_mid st2'. |
---|
355 | (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧ |
---|
356 | R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧ |
---|
357 | tll_rel … tll1 tll2 |
---|
358 | | doesnt_end_with_ret ⇒ |
---|
359 | ∃st2'.∃tll2 : trace_label_label S2 doesnt_end_with_ret st2_lab st2'. |
---|
360 | R st1' st2' ∧ label_rel … st1' st2' ∧ tll_rel … tll1 tll2 |
---|
361 | ] ≝ |
---|
362 | match tll1 with |
---|
363 | [ tll_base fl1' st1' st1'' tal1 H ⇒ ? |
---|
364 | ] |
---|
365 | and status_simulation_produce_tal S1 S2 R |
---|
366 | (* we start from this situation |
---|
367 | st1 →→tal→→ st1' |
---|
368 | | |
---|
369 | S |
---|
370 | | |
---|
371 | st2 |
---|
372 | |
---|
373 | and if the tal is a returning one we produce a diagram like the one for tlr, |
---|
374 | otherwise we allow for two possibilities: |
---|
375 | either |
---|
376 | |
---|
377 | st1 →→tal→→ st1' |
---|
378 | \\ | |
---|
379 | // L,S |
---|
380 | \\ | |
---|
381 | st2 →→tal→→ st2' |
---|
382 | |
---|
383 | or we do not advance from st2: |
---|
384 | |
---|
385 | st1 →→tal→→ st1' collapsable, and st1 uncosted |
---|
386 | / |
---|
387 | /-L,S-/ |
---|
388 | / |
---|
389 | st2 |
---|
390 | *) |
---|
391 | fl st1 st1' st2 |
---|
392 | (tal1 : trace_any_label S1 fl st1 st1') |
---|
393 | (sim_execute : status_simulation S1 S2 R) |
---|
394 | on tal1 : R st1 st2 → |
---|
395 | match fl with |
---|
396 | [ ends_with_ret ⇒ |
---|
397 | ∃st2_mid.∃st2'. |
---|
398 | ∃tal2 : trace_any_label S2 ends_with_ret st2 st2_mid. |
---|
399 | ∃taa2 : trace_any_any_free … st2_mid st2'. |
---|
400 | (if taaf_non_empty … taa2 then ¬as_costed … st2_mid else True) ∧ |
---|
401 | R st1' st2' ∧ ret_rel … R st1' st2_mid ∧ label_rel … st1' st2' ∧ |
---|
402 | tal_rel … tal1 tal2 |
---|
403 | | doesnt_end_with_ret ⇒ |
---|
404 | (∃st2'.∃tal2 : trace_any_label S2 doesnt_end_with_ret st2 st2'. |
---|
405 | R st1' st2' ∧ label_rel … st1' st2' ∧ tal_rel … tal1 tal2) ∨ |
---|
406 | (* empty *) |
---|
407 | (R st1' st2 ∧ label_rel … st1' st2 ∧ tal_collapsable … tal1 ∧ ¬as_costed … st1) |
---|
408 | ] ≝ |
---|
409 | match tal1 with |
---|
410 | [ tal_base_not_return st1' st1'' H G K ⇒ ? |
---|
411 | | tal_base_return st1' st1'' H G ⇒ ? |
---|
412 | | tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ? |
---|
413 | | tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ? |
---|
414 | | tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ? |
---|
415 | | tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ? |
---|
416 | ]. |
---|
417 | #st1_R_st2 |
---|
418 | [1,2,3: #st1_L_st2_lab ] |
---|
419 | [ (* tlr_base *) |
---|
420 | elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab) |
---|
421 | #st2_mid * #st2' * #tll2 #H |
---|
422 | %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H |
---|
423 | | (* tlr_step *) |
---|
424 | elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab) |
---|
425 | #st2_mid * #tll2 ** #H1 #H2 #H3 |
---|
426 | elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2) |
---|
427 | #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5 |
---|
428 | %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2} |
---|
429 | %{H4} %{H3 H5} |
---|
430 | | (* tll_base *) |
---|
431 | lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2) |
---|
432 | cases fl1' in tal1; normalize nodelta #tal1 * |
---|
433 | [3: * #_ #ABS elim (absurd … H ABS) ] |
---|
434 | [ #st2_mid ] * #st2' * #tal2 [* #taa2 ] * #H1 #H2 |
---|
435 | [%{st2_mid}] %{st2'} %{(tll_base … (taa_append_tal … taa2_pre tal2) ?)} |
---|
436 | [1,3: whd <st1_L_st2_lab assumption |
---|
437 | |*: [%{taa2} ] %{H1} % |
---|
438 | [1,3: change with (opt_safe ??? = opt_safe ???) |
---|
439 | @opt_safe_elim #a #EQ1 |
---|
440 | @opt_safe_elim #b <st1_L_st2_lab >EQ1 #EQ2 destruct % |
---|
441 | |*: @taa_append_tal_rel assumption |
---|
442 | ] |
---|
443 | ] |
---|
444 | | (* tal_base_non_return *) whd |
---|
445 | cases G -G #G |
---|
446 | lapply (sim_execute … H st1_R_st2) |
---|
447 | (* without try it fails... why? *) |
---|
448 | try >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta |
---|
449 | [ #H lapply (H K) -H ] * |
---|
450 | #st2' ** -st2 -st2' |
---|
451 | [1,4: #st2 (* taa2 empty → st1' must be not cost_labelled *) |
---|
452 | ** whd in ⊢ (%→?); * |
---|
453 | [1,3: #ncost #R' #L' %2 /4 by conj/ |
---|
454 | |*: * #ABS elim (ABS K) |
---|
455 | ] |
---|
456 | |*: #st2 #st2_mid #st2' #taa2 #H2 #I2 [2,4: #J2 ] |
---|
457 | *** #st1_R_st2' #st1_L_st2' %1 |
---|
458 | %{st2'} %{(taa_append_tal … taa2 (tal_base_not_return … H2 ??))} |
---|
459 | [1,4: %1{I2} |7,10: %2{I2} |2,5: assumption |8,11: whd <st1_L_st2' assumption ] |
---|
460 | % /2 by conj/ |
---|
461 | % try @refl %{st2_mid} %{taa2} %{H2} %[2,4,6,8: %[2,4,6,8: %]] |
---|
462 | ] |
---|
463 | | (* tal_base_return *) whd |
---|
464 | lapply (sim_execute … H st1_R_st2) |
---|
465 | >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); * |
---|
466 | #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2' |
---|
467 | ***** #ncost #J2 #K2 |
---|
468 | #st1_Rret_st2' #st1_Rret_st2' #st1_L_st2' |
---|
469 | %[2,4:%[2,4: %{(taa_append_tal … taa2 (tal_base_return … K2 J2))} %{taa2'} |
---|
470 | % [ /4 by conj/ ] |
---|
471 | %[ % | %[|%[|%[|%[| % ]]]]]]] |
---|
472 | | (* tal_base_call *) whd |
---|
473 | lapply (sim_execute … H st1_R_st2) |
---|
474 | >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); |
---|
475 | #H elim (H G) -H |
---|
476 | * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 |
---|
477 | #st1_R_st2_mid #st1_L_st2_after_call |
---|
478 | elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) |
---|
479 | #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2' |
---|
480 | [ #st2' #tlr2 ***** |
---|
481 | |*: #st2_after_ret #st2_after_ret' #st2' #taa2'' |
---|
482 | #I2 #J2 [2: #K2 ] #tlr2 **** #ncost |
---|
483 | ] |
---|
484 | #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S %1 |
---|
485 | %{st2'} |
---|
486 | [ %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)} |
---|
487 | [3: % [ % assumption ] |
---|
488 | % [%] %[|%[| %{EQcall} %[|%[|%[| %1 %[|%[|%[| %{S} % ]]]]]]]] |
---|
489 | ] |
---|
490 | |*: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (taa2'' @ tal_base_not_return … I2 ??))} |
---|
491 | [2: %1{J2} |6: %2{J2} |
---|
492 | |4,8: % try (% assumption) |
---|
493 | % [1,3:%] %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4: |
---|
494 | % [1,3: %{S} % ] /2 by taa_append_collapsable, I/ |
---|
495 | ]]]]]]]]]] |
---|
496 | ] |
---|
497 | ] |
---|
498 | [1,3,5: @(st1_Rret_st2' … st1_C_st2) assumption |
---|
499 | |*: whd <st1_L_st2' assumption |
---|
500 | ] |
---|
501 | | (* tal_base_tailcall *) whd |
---|
502 | lapply (sim_execute … H st1_R_st2) |
---|
503 | >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); |
---|
504 | #H elim (H G) -H |
---|
505 | * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 |
---|
506 | #st1_R_st2_mid #st1_L_st2_after_call |
---|
507 | elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) |
---|
508 | #st2_after_ret * #st2' * #tlr2 * #taa2'' |
---|
509 | * #props #S |
---|
510 | %{st2_after_ret} %{st2'} |
---|
511 | %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)} |
---|
512 | %{taa2''} |
---|
513 | %{props} |
---|
514 | % [%] %[|%[| %{EQcall} %[|%[|%[|%[| %{S} % ]]]]]] |
---|
515 | | (* tal_step_call *) |
---|
516 | lapply (sim_execute … H st1_R_st2) |
---|
517 | >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); |
---|
518 | #H elim (H G) -H |
---|
519 | * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 |
---|
520 | #st1_R_st2_mid #st1_L_st2_after_call |
---|
521 | elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) |
---|
522 | #st2_after_ret * #st2' * #tlr2 * #taa2'' |
---|
523 | **** |
---|
524 | #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S |
---|
525 | lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2') |
---|
526 | cases fl1' in tl1; #tl1 * |
---|
527 | [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S' |
---|
528 | %[|%[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))} |
---|
529 | [4: %{taa2'''} % [ /4 by conj/ ] |
---|
530 | %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]] |
---|
531 | ]]] |
---|
532 | | *#st2'' *#tl2 ** #st1_R_st2'' #st1_L_st2'' #S' %1 |
---|
533 | %[| %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ? (taaf_append_tal … taa2'' ? tl2))} |
---|
534 | [4: % [ /2 by conj/ ] |
---|
535 | %[|%[| %{EQcall} %[|%[|%[| %2 %[|%[|%[|%[|%[| %{S} % [ % ] @taaf_append_tal_rel @S' ]]]]]]]]]] |
---|
536 | ]] |
---|
537 | | lapply S lapply tlr2 lapply st1_Rret_st2' lapply st1_L_st2' lapply st1_R_st2' |
---|
538 | lapply taa_ncost cases taa2'' -st2_after_ret -st2' |
---|
539 | [ #st2' * #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S |
---|
540 | *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost %1 |
---|
541 | %[| %{(taa2 @ tal_base_call ???? H2 G2 ? tlr2 ?)} |
---|
542 | [3: % [ /2 by conj/ ] |
---|
543 | %[|%[| %{EQcall} %[|%[|%[| %1 %{(refl …)} %[|%[|%[| %{S} %{tl1_coll} % ]]]]]]]]]] |
---|
544 | |*: #st2_after_ret #st2_after_ret' #st2' #hd #I2' #J2' [2: #K2'] #ncost |
---|
545 | #st1_R_st2'#st1_L_st2' #st1_Rret_st2' #tlr2 #S |
---|
546 | *** #st1_R_st2'' #st1_L_st2'' #tl1_coll #ncost' %1 |
---|
547 | %[2,4: %{(taa2 @ tal_step_call ?????? H2 G2 ? tlr2 ncost (hd @ tal_base_not_return ??? I2' ??))} |
---|
548 | [2: %1{J2'} |6: %2{J2'} |
---|
549 | |4,8: % [1,3: /2 by conj/] |
---|
550 | %[2,4:%[2,4: %{EQcall} %[2,4:%[2,4:%[2,4: %2 %[2,4:%[2,4:%[2,4:%[2,4:%[2,4: |
---|
551 | %{S} % [1,3:%] @taa_append_tal_rel /2 by tal_collapsable_to_rel/ |
---|
552 | ]]]]]]]]]] |
---|
553 | ]] |
---|
554 | ] |
---|
555 | ] |
---|
556 | [1,4,7,9,11: @(st1_Rret_st2' … st1_C_st2) assumption |
---|
557 | |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2' |
---|
558 | [1,4: #st2_after_ret * #L whd in ⊢ (?%); <L assumption |
---|
559 | |*: normalize nodelta // |
---|
560 | ] |
---|
561 | |3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption |
---|
562 | |*: whd <st1_L_st2'' @(trace_any_label_label … tl1) |
---|
563 | ] |
---|
564 | | (* step_default *) |
---|
565 | lapply (sim_execute … H st1_R_st2) |
---|
566 | >G in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); * |
---|
567 | #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid |
---|
568 | lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid) |
---|
569 | cases fl1' in tl1; #tl1 * |
---|
570 | [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G |
---|
571 | %[|%[| %{(taaf_append_tal … taa2 ? tal2)} |
---|
572 | [2: %{taa2'} % [/4 by conj/ ] @taaf_append_tal_rel @G ] |
---|
573 | ]] |
---|
574 | | *#st2' *#tal2 *#H #G %1 |
---|
575 | %[| %{(taaf_append_tal … taa2 ? tal2)} |
---|
576 | [2: % [/2 by conj/] @taaf_append_tal_rel @G ] |
---|
577 | ] |
---|
578 | | (* can't happen *) |
---|
579 | *** #_ #L' elim (absurd ?? K) |
---|
580 | whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1) |
---|
581 | ] |
---|
582 | @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption |
---|
583 | ] |
---|
584 | qed. |
---|
585 | |
---|
586 | (* finite flat traces, with recursive structure right to left. The list of |
---|
587 | identifiers represents the call stack *) |
---|
588 | |
---|
589 | inductive flat_trace (S : abstract_status) (start : S) : S → list ident → Type[0] ≝ |
---|
590 | | ft_start : flat_trace S start start [ ] |
---|
591 | | ft_advance_flat : |
---|
592 | ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 → |
---|
593 | ((as_classifier ? st1 cl_jump ∧ as_costed … st2) ∨ as_classifier ? st1 cl_other) → |
---|
594 | flat_trace S start st2 stack |
---|
595 | | ft_advance_call : |
---|
596 | ∀st1,st2,stack.flat_trace S start st1 stack → as_execute S st1 st2 → |
---|
597 | ∀prf : as_classifier ? st1 cl_call. |
---|
598 | flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack) |
---|
599 | | ft_advance_tailcall : |
---|
600 | ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 → |
---|
601 | ∀prf : as_classifier ? st1 cl_tailcall. |
---|
602 | flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack) |
---|
603 | | ft_advance_ret : |
---|
604 | ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 → |
---|
605 | as_classifier ? st1 cl_return → |
---|
606 | flat_trace S start st2 stack. |
---|
607 | |
---|
608 | let rec ft_extend_taa S st1 st2 stack st3 (ft : flat_trace S st1 st2 stack) |
---|
609 | (taa : trace_any_any S st2 st3) |
---|
610 | on taa : flat_trace S st1 st3 stack ≝ |
---|
611 | match taa return λst2,st3,taa.flat_trace ?? st2 ? → flat_trace ?? st3 ? with |
---|
612 | [ taa_base s ⇒ λacc.acc |
---|
613 | | taa_step st1 st2 st3 H G _ tl ⇒ |
---|
614 | λacc.ft_extend_taa ????? (ft_advance_flat ????? acc H (or_intror … G)) tl |
---|
615 | ] ft. |
---|
616 | |
---|
617 | lemma ft_extend_extend_taa : ∀S,st1,st2,stack,st3,st4,ft,taa1,taa2. |
---|
618 | ft_extend_taa S st1 st3 stack st4 (ft_extend_taa ?? st2 ?? ft taa1) taa2 = |
---|
619 | ft_extend_taa … ft (taa_append_taa … taa1 taa2). |
---|
620 | #S #st1 #st2 #stack #st3 #st4 #ft #taa1 lapply ft elim taa1 -st2 -st3 normalize |
---|
621 | /2/ |
---|
622 | qed. |
---|
623 | |
---|
624 | definition ft_extend_taaf ≝ λS,st1,st2,stack,st3.λft : flat_trace S st1 st2 stack. |
---|
625 | λtaaf : trace_any_any_free S st2 st3. |
---|
626 | match taaf return λst2,st3,taaf.flat_trace ?? st2 ? → flat_trace ?? st3 ? with |
---|
627 | [ taaf_base s ⇒ λft.ft |
---|
628 | | taaf_step s1 s2 s3 pre H G ⇒ |
---|
629 | λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_intror … G) |
---|
630 | | taaf_step_jump s1 s2 s3 pre H G K ⇒ |
---|
631 | λft.ft_advance_flat … (ft_extend_taa … ft pre) H (or_introl … (conj … G K)) |
---|
632 | ] ft. |
---|
633 | |
---|
634 | definition option_to_list : ∀A.option A → list A ≝ λA,x. |
---|
635 | match x with |
---|
636 | [ Some x ⇒ [x] |
---|
637 | | None ⇒ [ ] |
---|
638 | ]. |
---|
639 | |
---|
640 | (* the observables of a flat trace (for the moment, only labels, calls and returns) *) |
---|
641 | let rec ft_observables_aux acc S st st' stack |
---|
642 | (ft : flat_trace S st st' stack) on ft : list intensional_event ≝ |
---|
643 | match ft with |
---|
644 | [ ft_start ⇒ acc |
---|
645 | | ft_advance_flat st1_mid st1' stack pre1 _ _ ⇒ |
---|
646 | let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in |
---|
647 | ft_observables_aux (add @ acc) … pre1 |
---|
648 | | ft_advance_call st1_mid st1' stack pre1 _ prf ⇒ |
---|
649 | let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in |
---|
650 | let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in |
---|
651 | ft_observables_aux (add @ acc) … pre1 |
---|
652 | | ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒ |
---|
653 | let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in |
---|
654 | let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in |
---|
655 | ft_observables_aux (add @ acc) … pre1 |
---|
656 | | ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒ |
---|
657 | let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in |
---|
658 | let add ≝ add @ [IEVret f] in |
---|
659 | ft_observables_aux (add @ acc) … pre1 |
---|
660 | ]. |
---|
661 | |
---|
662 | definition ft_observables ≝ ft_observables_aux [ ]. |
---|
663 | |
---|
664 | lemma ft_observables_aux_def : ∀acc,S,st1,st2,stack,ft. |
---|
665 | ft_observables_aux acc S st1 st2 stack ft = ft_observables … ft @ acc. |
---|
666 | #acc #S #st1 #st2 #stack #ft lapply acc -acc elim ft -st2 -stack |
---|
667 | [ // ] |
---|
668 | #st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc |
---|
669 | whd in ⊢ (??%(??%?)); |
---|
670 | >IH >IH >append_nil // |
---|
671 | qed. |
---|
672 | |
---|
673 | lemma ft_extend_taa_obs : ∀S,st1,st2,stack,st3,ft,taa. |
---|
674 | ft_observables … (ft_extend_taa S st1 st2 stack st3 ft taa) = |
---|
675 | ft_observables … ft @ |
---|
676 | if taa then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]. |
---|
677 | #S #st1 #st2 #stack #st3 #ft #taa lapply ft elim taa -st2 -st3 |
---|
678 | [ #st2 #ft >append_nil % ] |
---|
679 | #st2 #st3 #st4 #H #K #G #taa #IH #ft |
---|
680 | normalize in ⊢ (??(?????%)?); >IH |
---|
681 | -IH lapply G lapply H cases taa -st3 -st4 normalize nodelta |
---|
682 | [ #st3 #H #G |
---|
683 | | #st3 #st4 #st5 #ex #H' #G' #taa #H #G |
---|
684 | >(not_costed_no_label … G) |
---|
685 | ] >append_nil whd in ⊢ (??%?); >ft_observables_aux_def >append_nil % |
---|
686 | qed. |
---|
687 | |
---|
688 | lemma ft_extend_taa_advance_call_obs : ∀S,st1,st2,stack,st3,st4. |
---|
689 | ∀ft : flat_trace S st1 st2 stack. |
---|
690 | ∀taa : trace_any_any S st2 st3. |
---|
691 | ∀H : as_execute S st3 st4.∀G. |
---|
692 | ft_observables … (ft_advance_call … (ft_extend_taa … ft taa) H G) = |
---|
693 | ft_observables … ft @ |
---|
694 | option_to_list … (!l←as_label … st2;return IEVcost l) @ |
---|
695 | [IEVcall (as_call_ident … «st3, G»)]. |
---|
696 | #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G |
---|
697 | whd in ⊢ (??%?); >ft_observables_aux_def >append_nil |
---|
698 | >ft_extend_taa_obs |
---|
699 | lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 |
---|
700 | [ #st2 * #ft #H #G >append_nil % |
---|
701 | | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G |
---|
702 | >(not_costed_no_label … K) |
---|
703 | normalize nodelta // |
---|
704 | ] |
---|
705 | qed. |
---|
706 | |
---|
707 | lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4. |
---|
708 | ∀ft : flat_trace S st1 st2 (f :: stack). |
---|
709 | ∀taa : trace_any_any S st2 st3. |
---|
710 | ∀H : as_execute S st3 st4.∀G. |
---|
711 | ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) = |
---|
712 | ft_observables … ft @ |
---|
713 | option_to_list … (!l←as_label … st2;return IEVcost l) @ |
---|
714 | [IEVtailcall f (as_tailcall_ident … «st3, G»)]. |
---|
715 | #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G |
---|
716 | whd in ⊢ (??%?); >ft_observables_aux_def >append_nil |
---|
717 | >ft_extend_taa_obs |
---|
718 | lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 |
---|
719 | [ #st2 * #ft #H #G >append_nil % |
---|
720 | | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G |
---|
721 | >(not_costed_no_label … K) |
---|
722 | normalize nodelta // |
---|
723 | ] |
---|
724 | qed. |
---|
725 | |
---|
726 | lemma ft_extend_taa_advance_ret_obs : ∀S,st1,st2,stack,f,st3,st4. |
---|
727 | ∀ft : flat_trace S st1 st2 (f :: stack). |
---|
728 | ∀taa : trace_any_any S st2 st3. |
---|
729 | ∀H : as_execute S st3 st4.∀G. |
---|
730 | ft_observables … (ft_advance_ret … (ft_extend_taa … ft taa) H G) = |
---|
731 | ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l) @ [IEVret f]. |
---|
732 | #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G |
---|
733 | whd in ⊢ (??%?); >ft_observables_aux_def >append_nil |
---|
734 | >ft_extend_taa_obs |
---|
735 | lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 |
---|
736 | [ #st2 * #ft #H >append_nil % |
---|
737 | | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H |
---|
738 | >(not_costed_no_label … K) |
---|
739 | normalize nodelta // |
---|
740 | ] |
---|
741 | qed. |
---|
742 | |
---|
743 | lemma ft_extend_taa_advance_flat_obs : ∀S,st1,st2,stack,st3,st4. |
---|
744 | ∀ft : flat_trace S st1 st2 stack. |
---|
745 | ∀taa : trace_any_any S st2 st3. |
---|
746 | ∀H : as_execute S st3 st4.∀G. |
---|
747 | ft_observables … (ft_advance_flat … (ft_extend_taa … ft taa) H G) = |
---|
748 | ft_observables … ft @ option_to_list … (!l←as_label … st2;return IEVcost l). |
---|
749 | #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G |
---|
750 | whd in ⊢ (??%?); >ft_observables_aux_def >append_nil |
---|
751 | >ft_extend_taa_obs |
---|
752 | lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa -st2 -st3 |
---|
753 | [ #st2 * #ft #H >append_nil % |
---|
754 | | #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H |
---|
755 | >(not_costed_no_label … K) |
---|
756 | normalize nodelta >append_nil // |
---|
757 | ] |
---|
758 | qed. |
---|
759 | |
---|
760 | lemma ft_extend_taaf_obs : ∀S,st1,st2,stack,st3,ft,taaf. |
---|
761 | ft_observables … (ft_extend_taaf S st1 st2 stack st3 ft taaf) = |
---|
762 | ft_observables … ft @ |
---|
763 | if taaf_non_empty … taaf then option_to_list … (!l←as_label … st2;return IEVcost l) else [ ]. |
---|
764 | #S #st1 #st2 #stack #st3 #ft #taa lapply ft cases taa -st2 -st3 |
---|
765 | [ #st2 #ft >append_nil % ] |
---|
766 | #st2 #st3 #st4 #taa #H normalize nodelta #G [2: #K ] #ft |
---|
767 | @ft_extend_taa_advance_flat_obs |
---|
768 | qed. |
---|
769 | |
---|
770 | (* little helper to avoid splitting equal cases *) |
---|
771 | lemma if_eq : ∀b,A.∀x : A.if b then x else x = x. * // qed-. |
---|
772 | |
---|
773 | theorem status_simulation_produce_ft : |
---|
774 | (* from |
---|
775 | |
---|
776 | st1 →→→ft→→→ st1' |
---|
777 | | |
---|
778 | R,L |
---|
779 | | |
---|
780 | st2 |
---|
781 | |
---|
782 | we produce |
---|
783 | |
---|
784 | st1 →→→ft→→→ st1'-------\ |
---|
785 | // \ \ |
---|
786 | \\ L S |
---|
787 | // | \ |
---|
788 | st2 →→→ft→→→ st2_lab →taa→ st2' |
---|
789 | |
---|
790 | so that from any tlr or tll following st1' we can produce the corresponding |
---|
791 | structured trace from st2_lab using the previous result |
---|
792 | *) |
---|
793 | ∀S1,S2. |
---|
794 | ∀R. |
---|
795 | ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack. |
---|
796 | status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 → |
---|
797 | ∃st2_lab,st2'. |
---|
798 | ∃ft2 : flat_trace S2 st2 st2_lab stack. |
---|
799 | ∃taa : trace_any_any S2 st2_lab st2'. |
---|
800 | label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2. |
---|
801 | #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack |
---|
802 | [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % |
---|
803 | |*: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1'] |
---|
804 | (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S |
---|
805 | [1,2: (* other/jump *) |
---|
806 | lapply (sim_execute … ex G') |
---|
807 | try >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); normalize nodelta |
---|
808 | [ #H lapply (H ncost_st1') -H ] * |
---|
809 | #st2' *#taaf ** #ncost #G'' #H'' |
---|
810 | %{st2'} %{st2'} |
---|
811 | %[1,3: |
---|
812 | @(ft_extend_taaf … taaf) |
---|
813 | @(ft_extend_taa … taa) |
---|
814 | assumption] |
---|
815 | %{(taa_base …)} |
---|
816 | % [1,3: %{H'' G''} ] |
---|
817 | whd in ⊢ (??%?); >ft_observables_aux_def >append_nil |
---|
818 | lapply ncost lapply taa lapply H'' cases taaf -st2_mid -st2' |
---|
819 | [1,4: #st2' #H'' #taa * #ncost |
---|
820 | >ft_extend_taa_obs <L' |
---|
821 | [1,3: >(not_costed_no_label … ncost) >if_eq >S % |
---|
822 | |*: lapply L' lapply H'' lapply S lapply ft2 cases taa -st2_lab -st2' |
---|
823 | [1,3: #st2' #ft2 #S #H'' #L' >append_nil |
---|
824 | >not_costed_no_label |
---|
825 | [1,3: >append_nil @S ] |
---|
826 | whd in ⊢ (?%); >L' <H'' assumption |
---|
827 | |*: normalize nodelta #st2_mid #st2_mid' #st2' #_ #_ #_ #taa #ft2 #S #_ #_ |
---|
828 | >S % |
---|
829 | ] |
---|
830 | ] |
---|
831 | |*: #st2_mid #st2_mid' #st2' #taa' #ex' #cl' [2,4: #cst ] #_ #taa * |
---|
832 | whd in ⊢ (???(?????%)); |
---|
833 | >ft_extend_extend_taa >ft_extend_taa_advance_flat_obs |
---|
834 | >S >L' % |
---|
835 | ] |
---|
836 | |3: (* tailcall *) |
---|
837 | lapply (sim_execute … ex G') |
---|
838 | >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H |
---|
839 | * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2' |
---|
840 | * #taa2 * #taa2' ** #ex' #G'' #H'' |
---|
841 | lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl)) |
---|
842 | generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%); |
---|
843 | <EQcall in ⊢ (%→???%%→%); |
---|
844 | #ft1' #EQft1' |
---|
845 | %{st2_after_call} %{st2'} |
---|
846 | %[@(ft_advance_tailcall … f … ex' cl') |
---|
847 | @(ft_extend_taa … (taa_append_taa … taa taa2)) |
---|
848 | assumption] |
---|
849 | %{taa2'} |
---|
850 | % [ %{H'' G''} ] |
---|
851 | >ft_extend_taa_advance_tailcall_obs |
---|
852 | lapply EQft1' lapply ft1' -ft1' |
---|
853 | >EQcall in ⊢ (%→???%%→%); |
---|
854 | #ft1' #EQft1' destruct (EQft1') |
---|
855 | whd in ⊢ (??%?); |
---|
856 | >ft_observables_aux_def >append_nil |
---|
857 | >S >L' % |
---|
858 | |4: (* ret *) |
---|
859 | lapply (sim_execute … ex G') |
---|
860 | >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); * |
---|
861 | #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2' |
---|
862 | ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'} |
---|
863 | %[@(ft_extend_taaf … taa2') |
---|
864 | @(ft_advance_ret … f … ex' cl') |
---|
865 | @(ft_extend_taa … (taa_append_taa … taa taa2)) |
---|
866 | assumption] |
---|
867 | %{(taa_base …)} |
---|
868 | % [ %{H'' G''} ] |
---|
869 | >ft_extend_taaf_obs |
---|
870 | >ft_extend_taa_advance_ret_obs |
---|
871 | whd in ⊢ (??%?); |
---|
872 | >ft_observables_aux_def >append_nil |
---|
873 | lapply ncost cases taa2' -st2_after_ret -st2' |
---|
874 | [ #st2' * >append_nil |
---|
875 | |*: #st2_after_ret #st2_after_ret' #st2' #taa2' #ex'' #cl'' [2: #cst ] #ncost |
---|
876 | >(not_costed_no_label … ncost) |
---|
877 | >if_eq >append_nil |
---|
878 | ] |
---|
879 | >S >L' % |
---|
880 | |5: (* call *) |
---|
881 | lapply (sim_execute … ex G') |
---|
882 | >cl in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? |_ ⇒ ? |_ ⇒ ? |_ ⇒ ? ]→?); #H elim (H cl) -H |
---|
883 | * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2' |
---|
884 | * #taa2 * #taa2' ** #ex' #G'' #H'' |
---|
885 | %{st2_after_call} %{st2'} |
---|
886 | lapply (refl_jmeq … (ft_advance_call … ft1 ex cl)) |
---|
887 | generalize in match (ft_advance_call … ft1 ex cl) in ⊢ (????%→%); |
---|
888 | <EQcall in ⊢ (%→???%%→%); |
---|
889 | #ft1' #EQft1' |
---|
890 | %[@(ft_advance_call … ex' cl') |
---|
891 | @(ft_extend_taa … (taa_append_taa … taa taa2)) |
---|
892 | assumption] |
---|
893 | %{taa2'} |
---|
894 | % [ %{H'' G''} ] |
---|
895 | >ft_extend_taa_advance_call_obs |
---|
896 | lapply EQft1' lapply ft1' -ft1' |
---|
897 | >EQcall in ⊢ (%→???%%→%); |
---|
898 | #ft1' #EQft1' destruct (EQft1') |
---|
899 | whd in ⊢ (??%?); |
---|
900 | >ft_observables_aux_def >append_nil |
---|
901 | >S >L' % |
---|
902 | ] |
---|
903 | ] |
---|
904 | qed. |
---|