1 | include "basics/types.ma". |
---|
2 | include "basics/bool.ma". |
---|
3 | include "basics/jmeq.ma". |
---|
4 | include "common/CostLabel.ma". |
---|
5 | include "utilities/option.ma". |
---|
6 | include "basics/lists/listb.ma". |
---|
7 | include "ASM/Util.ma". |
---|
8 | |
---|
9 | inductive status_class: Type[0] ≝ |
---|
10 | | cl_return: status_class |
---|
11 | | cl_jump: status_class |
---|
12 | | cl_call: status_class |
---|
13 | | cl_other: status_class. |
---|
14 | |
---|
15 | record abstract_status : Type[1] ≝ |
---|
16 | { as_status :> Type[0] |
---|
17 | ; as_execute : as_status → as_status → Prop |
---|
18 | ; as_pc : DeqSet |
---|
19 | ; as_pc_of : as_status → as_pc |
---|
20 | ; as_classify : as_status → status_class |
---|
21 | ; as_label_of_pc : as_pc → option costlabel |
---|
22 | ; as_after_return : (Σs:as_status. as_classify s = cl_call) → as_status → Prop |
---|
23 | ; as_final: as_status → Prop |
---|
24 | ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident |
---|
25 | }. |
---|
26 | |
---|
27 | definition as_classifier ≝ λS,s,cl.as_classify S s = cl. |
---|
28 | definition as_call ≝ λS,s,f.as_call_ident S s = f. |
---|
29 | |
---|
30 | definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s). |
---|
31 | |
---|
32 | (* temporary alias for backward compatibility *) |
---|
33 | (* definition final_abstract_status ≝ abstract_status. *) |
---|
34 | |
---|
35 | definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝ |
---|
36 | λa_s,st.as_label ? st ≠ None ?. |
---|
37 | |
---|
38 | definition as_label_safe : ∀a_s : abstract_status. |
---|
39 | (Σs : a_s.as_costed ? s) → costlabel ≝ |
---|
40 | λa_s,st_sig.opt_safe … (pi2 … st_sig). |
---|
41 | |
---|
42 | lemma as_costed_exc : ∀S:abstract_status. ∀s:S. (as_costed S s) + (¬as_costed S s). |
---|
43 | #S #s whd in match (as_costed S s); |
---|
44 | cases (as_label S s) [ %2 % * /2/ | #c %1 % #E destruct ] |
---|
45 | qed. |
---|
46 | |
---|
47 | lemma not_costed_no_label : ∀S,st. |
---|
48 | ¬as_costed S st → |
---|
49 | as_label S st = None ?. |
---|
50 | #S #st * normalize cases (as_label_of_pc S ?) |
---|
51 | [ // | #l #H cases (H ?) % #E destruct ] |
---|
52 | qed. |
---|
53 | |
---|
54 | (* cost map generalities *) |
---|
55 | |
---|
56 | definition as_cost_labelled ≝ |
---|
57 | λS : abstract_status. λl.∃pc.as_label_of_pc S pc = Some ? l. |
---|
58 | |
---|
59 | definition as_cost_label ≝ |
---|
60 | λS : abstract_status. Σl.as_cost_labelled S l. |
---|
61 | |
---|
62 | definition as_cost_labels ≝ |
---|
63 | λS : abstract_status. list (as_cost_label S). |
---|
64 | |
---|
65 | definition as_cost_get_label ≝ |
---|
66 | λS : abstract_status. λl_sig: as_cost_label S. pi1 … l_sig. |
---|
67 | |
---|
68 | definition as_cost_get_labels ≝ |
---|
69 | λS : abstract_status. map … (as_cost_get_label S). |
---|
70 | |
---|
71 | definition as_cost_map ≝ |
---|
72 | λS : abstract_status. (as_cost_label S) → ℕ. |
---|
73 | |
---|
74 | definition lift_sigma_map_id : |
---|
75 | ∀A,B : Type[0].∀P_in,P_out : A → Prop.B → |
---|
76 | (∀a.P_out a + ¬ P_out a) → |
---|
77 | ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig. |
---|
78 | match dec a_sig with |
---|
79 | [ inl prf ⇒ m «a_sig, prf» |
---|
80 | | inr _ ⇒ dflt (* labels not present in out code get 0 *) |
---|
81 | ]. |
---|
82 | |
---|
83 | lemma lift_sigma_map_id_eq : |
---|
84 | ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out. |
---|
85 | pi1 ?? a_in = pi1 ?? a_out → |
---|
86 | lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out. |
---|
87 | #A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ |
---|
88 | whd in match lift_sigma_map_id; normalize nodelta |
---|
89 | cases (dec a_in) normalize nodelta >EQ cases a_out |
---|
90 | #a #H #G [ % | @⊥ /2 by absurd/ ] |
---|
91 | qed. |
---|
92 | |
---|
93 | notation > "Σ_{ ident i ∈ l } f" |
---|
94 | with precedence 20 |
---|
95 | for @{'fold plus 0 (λ${ident i}.true) (λ${ident i}. $f) $l}. |
---|
96 | notation < "Σ_{ ident i ∈ l } f" |
---|
97 | with precedence 20 |
---|
98 | for @{'fold plus 0 (λ${ident i}:$X.true) (λ${ident i}:$Y. $f) $l}. |
---|
99 | |
---|
100 | definition lift_cost_map_id : |
---|
101 | ∀S_in,S_out : abstract_status.? → |
---|
102 | as_cost_map S_out → as_cost_map S_in |
---|
103 | ≝ |
---|
104 | λS_in,S_out : abstract_status. |
---|
105 | lift_sigma_map_id costlabel ℕ |
---|
106 | (*λl.∃pc.as_label_of_pc S_in pc = Some ? l*) (as_cost_labelled S_in) |
---|
107 | (*λl.∃pc.as_label_of_pc S_out pc = Some ? l*) (as_cost_labelled S_out) |
---|
108 | 0. |
---|
109 | |
---|
110 | lemma lift_cost_map_same_cost : |
---|
111 | ∀S_in, S_out, dec, m_out, trace_in, trace_out. |
---|
112 | map … (pi1 ??) trace_in = map … (pi1 ??) trace_out → |
---|
113 | (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) = |
---|
114 | (Σ_{ l_sig ∈ trace_out } (m_out l_sig)). |
---|
115 | #S_in #S_out #dec #m_out #trace_in elim trace_in |
---|
116 | [2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out] |
---|
117 | normalize in ⊢ (%→?); |
---|
118 | [2,3: #ABS destruct(ABS) |
---|
119 | |4: #_ % |
---|
120 | |1: |
---|
121 | #EQ destruct |
---|
122 | whd in ⊢(??%%); |
---|
123 | whd in match lift_cost_map_id; normalize nodelta |
---|
124 | >(lift_sigma_map_id_eq ????????? e0) |
---|
125 | >e0 in e1; normalize in ⊢(%→?); #EQ |
---|
126 | >(IH … EQ) % |
---|
127 | ] |
---|
128 | qed. |
---|
129 | |
---|
130 | |
---|
131 | (* structured traces: down to business *) |
---|
132 | |
---|
133 | inductive trace_ends_with_ret: Type[0] ≝ |
---|
134 | | ends_with_ret: trace_ends_with_ret |
---|
135 | | doesnt_end_with_ret: trace_ends_with_ret. |
---|
136 | |
---|
137 | inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝ |
---|
138 | | tlr_base: |
---|
139 | ∀status_before: S. |
---|
140 | ∀status_after: S. |
---|
141 | trace_label_label S ends_with_ret status_before status_after → |
---|
142 | trace_label_return S status_before status_after |
---|
143 | | tlr_step: |
---|
144 | ∀status_initial: S. |
---|
145 | ∀status_labelled: S. |
---|
146 | ∀status_final: S. |
---|
147 | trace_label_label S doesnt_end_with_ret status_initial status_labelled → |
---|
148 | trace_label_return S status_labelled status_final → |
---|
149 | trace_label_return S status_initial status_final |
---|
150 | with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝ |
---|
151 | | tll_base: |
---|
152 | ∀ends_flag: trace_ends_with_ret. |
---|
153 | ∀start_status: S. |
---|
154 | ∀end_status: S. |
---|
155 | trace_any_label S ends_flag start_status end_status → |
---|
156 | as_costed S start_status → |
---|
157 | trace_label_label S ends_flag start_status end_status |
---|
158 | with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝ |
---|
159 | (* Single steps within a function which reach a label. |
---|
160 | Note that this is the only case applicable for a jump. *) |
---|
161 | | tal_base_not_return: |
---|
162 | ∀start_status: S. |
---|
163 | ∀final_status: S. |
---|
164 | as_execute S start_status final_status → |
---|
165 | (as_classifier S start_status cl_jump ∨ |
---|
166 | as_classifier S start_status cl_other) → |
---|
167 | as_costed S final_status → |
---|
168 | trace_any_label S doesnt_end_with_ret start_status final_status |
---|
169 | | tal_base_return: |
---|
170 | ∀start_status: S. |
---|
171 | ∀final_status: S. |
---|
172 | as_execute S start_status final_status → |
---|
173 | as_classifier S start_status cl_return → |
---|
174 | trace_any_label S ends_with_ret start_status final_status |
---|
175 | (* A call followed by a label on return. *) |
---|
176 | | tal_base_call: |
---|
177 | ∀status_pre_fun_call: S. |
---|
178 | ∀status_start_fun_call: S. |
---|
179 | ∀status_final: S. |
---|
180 | as_execute S status_pre_fun_call status_start_fun_call → |
---|
181 | ∀H:as_classifier S status_pre_fun_call cl_call. |
---|
182 | as_after_return S «status_pre_fun_call, H» status_final → |
---|
183 | trace_label_return S status_start_fun_call status_final → |
---|
184 | as_costed S status_final → |
---|
185 | trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final |
---|
186 | (* A call followed by a non-empty trace. *) |
---|
187 | | tal_step_call: |
---|
188 | ∀end_flag: trace_ends_with_ret. |
---|
189 | ∀status_pre_fun_call: S. |
---|
190 | ∀status_start_fun_call: S. |
---|
191 | ∀status_after_fun_call: S. |
---|
192 | ∀status_final: S. |
---|
193 | as_execute S status_pre_fun_call status_start_fun_call → |
---|
194 | ∀H:as_classifier S status_pre_fun_call cl_call. |
---|
195 | as_after_return S «status_pre_fun_call, H» status_after_fun_call → |
---|
196 | trace_label_return S status_start_fun_call status_after_fun_call → |
---|
197 | ¬ as_costed S status_after_fun_call → |
---|
198 | trace_any_label S end_flag status_after_fun_call status_final → |
---|
199 | trace_any_label S end_flag status_pre_fun_call status_final |
---|
200 | | tal_step_default: |
---|
201 | ∀end_flag: trace_ends_with_ret. |
---|
202 | ∀status_pre: S. |
---|
203 | ∀status_init: S. |
---|
204 | ∀status_end: S. |
---|
205 | as_execute S status_pre status_init → |
---|
206 | trace_any_label S end_flag status_init status_end → |
---|
207 | as_classifier S status_pre cl_other → |
---|
208 | ¬ (as_costed S status_init) → |
---|
209 | trace_any_label S end_flag status_pre status_end. |
---|
210 | |
---|
211 | let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2) |
---|
212 | on tal : list (as_pc S) ≝ |
---|
213 | match tal with |
---|
214 | [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl |
---|
215 | | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒ as_pc_of … pre :: tal_pc_list … tl |
---|
216 | | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre] |
---|
217 | | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre] |
---|
218 | | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre] |
---|
219 | ]. |
---|
220 | |
---|
221 | definition as_trace_any_label_length': |
---|
222 | ∀S: abstract_status. |
---|
223 | ∀trace_ends_flag: trace_ends_with_ret. |
---|
224 | ∀start_status: S. |
---|
225 | ∀final_status: S. |
---|
226 | ∀the_trace: trace_any_label S trace_ends_flag start_status final_status. |
---|
227 | nat ≝ |
---|
228 | λS: abstract_status. |
---|
229 | λtrace_ends_flag: trace_ends_with_ret. |
---|
230 | λstart_status: S. |
---|
231 | λfinal_status: S. |
---|
232 | λthe_trace: trace_any_label S trace_ends_flag start_status final_status. |
---|
233 | |tal_pc_list … the_trace|. |
---|
234 | |
---|
235 | let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝ |
---|
236 | match tlr with |
---|
237 | [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll |
---|
238 | | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl |
---|
239 | ] |
---|
240 | and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝ |
---|
241 | match tll with |
---|
242 | [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal |
---|
243 | ] |
---|
244 | and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝ |
---|
245 | match tal with |
---|
246 | [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒ |
---|
247 | bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ |
---|
248 | tal_unrepeating … tl ∧ |
---|
249 | tlr_unrepeating … tlr |
---|
250 | | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒ |
---|
251 | bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧ |
---|
252 | tal_unrepeating … tl |
---|
253 | | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace |
---|
254 | | _ ⇒ True |
---|
255 | ]. |
---|
256 | |
---|
257 | definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2. |
---|
258 | trace_label_label S fl st1 st2 → costlabel ≝ |
---|
259 | λS,fl,st1,st2,tr.match tr with |
---|
260 | [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ]. |
---|
261 | |
---|
262 | definition tlr_hd_label : ∀S : abstract_status.∀st1,st2. |
---|
263 | trace_label_return S st1 st2 → costlabel ≝ |
---|
264 | λS,st1,st2,tr.match tr with |
---|
265 | [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll |
---|
266 | | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll |
---|
267 | ]. |
---|
268 | |
---|
269 | let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal : |
---|
270 | tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?. |
---|
271 | cases tal // |
---|
272 | #fl' #st1' [#st_fun] #st2' #st3' #H |
---|
273 | [ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]* |
---|
274 | #A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption |
---|
275 | qed. |
---|
276 | |
---|
277 | lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2. |
---|
278 | ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl. |
---|
279 | #S #fl0 #s10 #s20 * |
---|
280 | [ #s1 #s2 #EX #CL #CS |
---|
281 | | #s1 #s2 #EX #CL |
---|
282 | | #s1 #s2 #s3 #EX #CL #AF #tlr #CS |
---|
283 | | #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal |
---|
284 | | #fl #s1 #s2 #s3 #EX #tal #CL #CS |
---|
285 | ] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ] |
---|
286 | qed. |
---|
287 | |
---|
288 | let rec tal_tail_not_costed S fl st1 st2 tal |
---|
289 | (H:Not (as_costed S st1)) on tal : |
---|
290 | All ? (λpc. as_label_of_pc S pc = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?. |
---|
291 | cases tal in H ⊢ %; |
---|
292 | [ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS') |
---|
293 | | #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS) |
---|
294 | | #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS') |
---|
295 | | #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS' |
---|
296 | cases (tal_pc_list_start … tal') |
---|
297 | #hd #E >E |
---|
298 | % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ] |
---|
299 | | #fl' #pre #init #end #EX #tal' #CL #CS #CS' |
---|
300 | cases (tal_pc_list_start … tal') |
---|
301 | #hd #E >E |
---|
302 | % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ] |
---|
303 | ] qed. |
---|
304 | |
---|
305 | |
---|
306 | inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝ |
---|
307 | | tac_base: |
---|
308 | ∀status: S. |
---|
309 | as_classifier S status cl_call → |
---|
310 | trace_any_call S status status |
---|
311 | | tac_step_call: |
---|
312 | ∀status_pre_fun_call: S. |
---|
313 | ∀status_after_fun_call: S. |
---|
314 | ∀status_final: S. |
---|
315 | ∀status_start_fun_call: S. |
---|
316 | as_execute S status_pre_fun_call status_start_fun_call → |
---|
317 | ∀H:as_classifier S status_pre_fun_call cl_call. |
---|
318 | as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call → |
---|
319 | trace_label_return S status_start_fun_call status_after_fun_call → |
---|
320 | ¬ as_costed S status_after_fun_call → |
---|
321 | trace_any_call S status_after_fun_call status_final → |
---|
322 | trace_any_call S status_pre_fun_call status_final |
---|
323 | | tac_step_default: |
---|
324 | ∀status_pre: S. |
---|
325 | ∀status_end: S. |
---|
326 | ∀status_init: S. |
---|
327 | as_execute S status_pre status_init → |
---|
328 | trace_any_call S status_init status_end → |
---|
329 | as_classifier S status_pre cl_other → |
---|
330 | ¬ (as_costed S status_init) → |
---|
331 | trace_any_call S status_pre status_end. |
---|
332 | |
---|
333 | |
---|
334 | inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝ |
---|
335 | | tlc_base: |
---|
336 | ∀start_status: S. |
---|
337 | ∀end_status: S. |
---|
338 | trace_any_call S start_status end_status → |
---|
339 | as_costed S start_status → |
---|
340 | trace_label_call S start_status end_status |
---|
341 | . |
---|
342 | |
---|
343 | definition tlc_hd_label : ∀S : abstract_status.∀st1,st2. |
---|
344 | trace_label_call S st1 st2 → costlabel ≝ |
---|
345 | λS,st1,st2,tr.match tr with |
---|
346 | [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf» |
---|
347 | ]. |
---|
348 | |
---|
349 | coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝ |
---|
350 | | tld_step: |
---|
351 | ∀status_initial: S. |
---|
352 | ∀status_labelled: S. |
---|
353 | trace_label_label S doesnt_end_with_ret status_initial status_labelled → |
---|
354 | trace_label_diverges S status_labelled → |
---|
355 | trace_label_diverges S status_initial |
---|
356 | | tld_base: |
---|
357 | ∀status_initial: S. |
---|
358 | ∀status_pre_fun_call: S. |
---|
359 | ∀status_start_fun_call: S. |
---|
360 | trace_label_call S status_initial status_pre_fun_call → |
---|
361 | as_execute S status_pre_fun_call status_start_fun_call → |
---|
362 | ∀H:as_classifier S status_pre_fun_call cl_call. |
---|
363 | trace_label_diverges S status_start_fun_call → |
---|
364 | trace_label_diverges S status_initial. |
---|
365 | |
---|
366 | definition tld_hd_label : ∀S : abstract_status.∀st. |
---|
367 | trace_label_diverges S st → costlabel ≝ |
---|
368 | λS,st,tr.match tr with |
---|
369 | [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll |
---|
370 | | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc |
---|
371 | ]. |
---|
372 | |
---|
373 | (* Version in Prop for showing existence. *) |
---|
374 | coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝ |
---|
375 | | tld_step': |
---|
376 | ∀status_initial: S. |
---|
377 | ∀status_labelled: S. |
---|
378 | trace_label_label S doesnt_end_with_ret status_initial status_labelled → |
---|
379 | trace_label_diverges_exists S status_labelled → |
---|
380 | trace_label_diverges_exists S status_initial |
---|
381 | | tld_base': |
---|
382 | ∀status_initial: S. |
---|
383 | ∀status_pre_fun_call: S. |
---|
384 | ∀status_start_fun_call: S. |
---|
385 | trace_label_call S status_initial status_pre_fun_call → |
---|
386 | as_execute S status_pre_fun_call status_start_fun_call → |
---|
387 | ∀H:as_classifier S status_pre_fun_call cl_call. |
---|
388 | trace_label_diverges_exists S status_start_fun_call → |
---|
389 | trace_label_diverges_exists S status_initial. |
---|
390 | |
---|
391 | inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝ |
---|
392 | | twp_terminating: |
---|
393 | ∀status_initial: S. |
---|
394 | ∀status_start_fun: S. |
---|
395 | ∀status_final: S. |
---|
396 | as_classifier S status_initial cl_call → |
---|
397 | as_execute S status_initial status_start_fun → |
---|
398 | trace_label_return S status_start_fun status_final → |
---|
399 | as_final S status_final → |
---|
400 | trace_whole_program S status_initial |
---|
401 | | twp_diverges: |
---|
402 | ∀status_initial: S. |
---|
403 | ∀status_start_fun: S. |
---|
404 | as_classifier S status_initial cl_call → |
---|
405 | as_execute S status_initial status_start_fun → |
---|
406 | trace_label_diverges S status_start_fun → |
---|
407 | trace_whole_program S status_initial. |
---|
408 | |
---|
409 | (* Again, an identical version in Prop for existence proofs. *) |
---|
410 | inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝ |
---|
411 | | twp_terminating: |
---|
412 | ∀status_initial: S. |
---|
413 | ∀status_start_fun: S. |
---|
414 | ∀status_final: S. |
---|
415 | as_classifier S status_initial cl_call → |
---|
416 | as_execute S status_initial status_start_fun → |
---|
417 | trace_label_return S status_start_fun status_final → |
---|
418 | as_final S status_final → |
---|
419 | trace_whole_program_exists S status_initial |
---|
420 | | twp_diverges: |
---|
421 | ∀status_initial: S. |
---|
422 | ∀status_start_fun: S. |
---|
423 | as_classifier S status_initial cl_call → |
---|
424 | as_execute S status_initial status_start_fun → |
---|
425 | trace_label_diverges_exists S status_start_fun → |
---|
426 | trace_whole_program_exists S status_initial. |
---|
427 | |
---|
428 | |
---|
429 | let rec trace_any_label_label S s s' f |
---|
430 | (tr:trace_any_label S f s s') on tr : match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] ≝ |
---|
431 | match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with |
---|
432 | [ tal_base_not_return start final _ _ C ⇒ C |
---|
433 | | tal_base_return _ _ _ _ ⇒ I |
---|
434 | | tal_base_call _ _ _ _ _ _ _ C ⇒ C |
---|
435 | | tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr' |
---|
436 | | tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr' |
---|
437 | ]. |
---|
438 | |
---|
439 | definition tal_tl_label : ∀S : abstract_status.∀st1,st2. |
---|
440 | trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝ |
---|
441 | λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr». |
---|
442 | |
---|
443 | lemma trace_label_label_label : ∀S,s,s',f. |
---|
444 | ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ]. |
---|
445 | #S #s #s' #f #tr |
---|
446 | cases tr |
---|
447 | #f #start #end #tr' #C @(trace_any_label_label … tr') |
---|
448 | qed. |
---|
449 | |
---|
450 | definition tll_tl_label : ∀S : abstract_status.∀st1,st2. |
---|
451 | trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝ |
---|
452 | λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr». |
---|
453 | |
---|
454 | lemma trace_any_call_call : ∀S,s,s'. |
---|
455 | trace_any_call S s s' → as_classifier S s' cl_call. |
---|
456 | #S #s #s' #T elim T [1,3: //] |
---|
457 | #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 // |
---|
458 | qed. |
---|
459 | |
---|
460 | (* |
---|
461 | (* an trace of unlabeled and cl_other states, possibly empty *) |
---|
462 | inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝ |
---|
463 | | tna_base : |
---|
464 | ∀start_status: S. |
---|
465 | ¬as_costed … start_status → |
---|
466 | trace_no_label_any S start_status start_status |
---|
467 | | tna_step : |
---|
468 | ∀status_pre: S. |
---|
469 | ∀status_init: S. |
---|
470 | ∀status_end: S. |
---|
471 | as_execute S status_pre status_init → |
---|
472 | as_classifier S status_pre cl_other → |
---|
473 | ¬as_costed … status_pre → |
---|
474 | trace_no_label_any S status_init status_end → |
---|
475 | trace_no_label_any S status_pre status_end. |
---|
476 | |
---|
477 | let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2) |
---|
478 | on taa1 : |
---|
479 | trace_no_label_any S st2 st3 → |
---|
480 | trace_no_label_any S st1 st3 ≝ |
---|
481 | match taa1 with |
---|
482 | [ tna_base st1' H ⇒ λtaa2.taa2 |
---|
483 | | tna_step st1' st2' st3' H G K tl ⇒ |
---|
484 | λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2) |
---|
485 | ]. |
---|
486 | |
---|
487 | definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2. |
---|
488 | match tna with |
---|
489 | [ tna_base _ _ ⇒ false |
---|
490 | | tna_step _ _ _ _ _ _ _ ⇒ true |
---|
491 | ]. |
---|
492 | |
---|
493 | coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝ |
---|
494 | tna_non_empty on _tna : trace_no_label_any ??? to bool. |
---|
495 | |
---|
496 | lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1. |
---|
497 | #S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed. |
---|
498 | |
---|
499 | let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2) |
---|
500 | on tna : |
---|
501 | trace_any_label S fl st2 st3 → |
---|
502 | if tna then Not (as_costed … st2) else True → |
---|
503 | trace_any_label S fl st1 st3 ≝ |
---|
504 | match tna return λst1,st2.λx : trace_no_label_any S st1 st2. |
---|
505 | ∀fl,st3. |
---|
506 | trace_any_label S fl st2 st3 → |
---|
507 | if x then Not (as_costed … st2) else True → |
---|
508 | trace_any_label S fl st1 st3 |
---|
509 | with |
---|
510 | [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2 |
---|
511 | | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf. |
---|
512 | tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl) |
---|
513 | ] fl st3. |
---|
514 | cases (tna_non_empty … tl) [@prf|%] |
---|
515 | qed. |
---|
516 | *) |
---|
517 | |
---|
518 | inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝ |
---|
519 | | taa_base : ∀st.trace_any_any S st st |
---|
520 | | taa_step : ∀st1,st2,st3. |
---|
521 | as_execute S st1 st2 → |
---|
522 | as_classifier S st1 cl_other → |
---|
523 | ¬as_costed S st2 → |
---|
524 | trace_any_any S st2 st3 → |
---|
525 | trace_any_any S st1 st3. |
---|
526 | |
---|
527 | definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2. |
---|
528 | match taa with |
---|
529 | [ taa_base _ ⇒ false |
---|
530 | | taa_step _ _ _ _ _ _ _ ⇒ true |
---|
531 | ]. |
---|
532 | |
---|
533 | coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝ |
---|
534 | taa_non_empty on _taa : trace_any_any ??? to bool. |
---|
535 | |
---|
536 | let rec taa_append_tal S st1 fl st2 st3 |
---|
537 | (taa : trace_any_any S st1 st2) on taa : |
---|
538 | trace_any_label S fl st2 st3 → |
---|
539 | trace_any_label S fl st1 st3 ≝ |
---|
540 | match taa return λst1,st2.λx : trace_any_any S st1 st2. |
---|
541 | ∀fl,st3. |
---|
542 | trace_any_label S fl st2 st3 → |
---|
543 | trace_any_label S fl st1 st3 |
---|
544 | with |
---|
545 | [ taa_base st1' ⇒ λfl,st3,tal2.tal2 |
---|
546 | | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2. |
---|
547 | tal_step_default ????? H (taa_append_tal ????? tl tal2) G K |
---|
548 | ] fl st3. |
---|
549 | |
---|
550 | interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal). |
---|
551 | |
---|
552 | let rec tal_collapsable S fl s1 s2 (tal : trace_any_label S fl s1 s2) on tal : Prop ≝ |
---|
553 | match tal with |
---|
554 | [ tal_base_not_return _ _ _ _ _ ⇒ True |
---|
555 | | tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable … tl1 |
---|
556 | | _ ⇒ False |
---|
557 | ]. |
---|
558 | |
---|
559 | let rec tlr_rel S1 st1 st1' S2 st2 st2' |
---|
560 | (tlr1 : trace_label_return S1 st1 st1') |
---|
561 | (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝ |
---|
562 | match tlr1 with |
---|
563 | [ tlr_base st1 st1' tll1 ⇒ |
---|
564 | match tlr2 with |
---|
565 | [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2 |
---|
566 | | _ ⇒ False |
---|
567 | ] |
---|
568 | | tlr_step st1 st1' st1'' tll1 tl1 ⇒ |
---|
569 | match tlr2 with |
---|
570 | [ tlr_step st2 st2' st2'' tll2 tl2 ⇒ |
---|
571 | tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2 |
---|
572 | | _ ⇒ False |
---|
573 | ] |
---|
574 | ] |
---|
575 | and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2' |
---|
576 | (tll1 : trace_label_label S1 fl1 st1 st1') |
---|
577 | (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝ |
---|
578 | match tll1 with |
---|
579 | [ tll_base fl1 st1 st1' tal1 H ⇒ |
---|
580 | match tll2 with |
---|
581 | [ tll_base fl2 st2 st2 tal2 G ⇒ |
---|
582 | as_label_safe … («?, H») = as_label_safe … («?, G») ∧ |
---|
583 | tal_rel … tal1 tal2 |
---|
584 | ] |
---|
585 | ] |
---|
586 | and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2' |
---|
587 | (tal1 : trace_any_label S1 fl1 st1 st1') |
---|
588 | (tal2 : trace_any_label S2 fl2 st2 st2') |
---|
589 | on tal1 : Prop ≝ |
---|
590 | match tal1 with |
---|
591 | [ tal_base_not_return st1 st1' _ _ _ ⇒ |
---|
592 | fl2 = doesnt_end_with_ret ∧ |
---|
593 | ∃st2mid,taa,H,G,K. |
---|
594 | tal2 ≃ taa_append_tal ? st2 ??? taa |
---|
595 | (tal_base_not_return ? st2mid st2' H G K) |
---|
596 | | tal_base_return st1 st1' _ _ ⇒ |
---|
597 | fl2 = ends_with_ret ∧ |
---|
598 | ∃st2mid,taa,H,G. |
---|
599 | tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa |
---|
600 | (tal_base_return ? st2mid st2' H G) |
---|
601 | | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ |
---|
602 | fl2 = doesnt_end_with_ret ∧ |
---|
603 | ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧ |
---|
604 | ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. |
---|
605 | (* we must allow a tal_base_call to be similar to a call followed |
---|
606 | by a collapsable trace (trace_any_any followed by a base_not_return; |
---|
607 | we cannot use trace_any_any as it disallows labels in the end as soon |
---|
608 | as it is non-empty) *) |
---|
609 | (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. |
---|
610 | tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨ |
---|
611 | ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. |
---|
612 | ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'. |
---|
613 | tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ |
---|
614 | tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2 |
---|
615 | | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ |
---|
616 | ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧ |
---|
617 | ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H. |
---|
618 | (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L. |
---|
619 | tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧ |
---|
620 | tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨ |
---|
621 | ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L. |
---|
622 | ∃tl2 : trace_any_label ? fl2 st2mid'' st2'. |
---|
623 | tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧ |
---|
624 | tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2 |
---|
625 | | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ |
---|
626 | tal_rel … tl1 tal2 (* <- this makes it many to many *) |
---|
627 | ]. |
---|
628 | |
---|
629 | interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2). |
---|
630 | interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2). |
---|
631 | interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2). |
---|
632 | |
---|
633 | let rec tal_collapsable_eq_fl S1 fl1 s1 s1' |
---|
634 | (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 : |
---|
635 | tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝ ?. |
---|
636 | cases tal1 -fl1 -s1 -s1' // |
---|
637 | [ #s1 #s1' #H #I * |
---|
638 | | #s1 #s1' #s1'' #s1''' #s1'''' #H #I #J #tlr #K #tl * |
---|
639 | | #fl1 #s1 #s1' #s1'' #H #tl #I #J @(tal_collapsable_eq_fl … tl) |
---|
640 | ] |
---|
641 | qed. |
---|
642 | |
---|
643 | let rec tal_rel_eq_fl S1 fl1 s1 s1' S2 fl2 s2 s2' |
---|
644 | (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 : |
---|
645 | ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_rel … tal1 tal2 → fl1 = fl2 ≝ |
---|
646 | match tal1 return λfl1,s1,s1',tal1.? with |
---|
647 | [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ? |
---|
648 | | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ? |
---|
649 | | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ? |
---|
650 | | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ? |
---|
651 | | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ? |
---|
652 | ]. |
---|
653 | -fl1 -s1 -s1' |
---|
654 | [1,2,3: -tal_rel_eq_fl #tal2 * // |
---|
655 | | #tal2 * #s2_mid * #G2 * #call * #taa2 * #s2' *#H2 * |
---|
656 | [ * #EQ1 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) // |
---|
657 | | * #s2_mid' *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_ |
---|
658 | @(tal_rel_eq_fl … step) |
---|
659 | ] |
---|
660 | | #tal2 whd in ⊢ (%→?); #step @(tal_rel_eq_fl … step) |
---|
661 | ] |
---|
662 | qed. |
---|
663 | |
---|
664 | let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2' |
---|
665 | (taa1 : trace_any_any S1 st1 st1mid) on taa1 : |
---|
666 | ∀tal1 : trace_any_label S1 fl1 st1mid st1'. |
---|
667 | ∀tal2 : trace_any_label S2 fl2 st2 st2'. |
---|
668 | tal_rel … (taa1 @ tal1) tal2 → |
---|
669 | tal_rel … tal1 tal2 ≝ ?. |
---|
670 | cases taa1 -taa1 |
---|
671 | [ -taa_rel_inv // |
---|
672 | | #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?); |
---|
673 | @(taa_rel_inv … tl) |
---|
674 | ] |
---|
675 | qed. |
---|
676 | |
---|
677 | lemma taa_append_collapsable : ∀S,s1,fl,s2,s3. |
---|
678 | ∀taa,tal.tal_collapsable S fl s2 s3 tal → tal_collapsable S fl s1 s3 (taa@tal). |
---|
679 | #S #s1 #fl #s2 #s3 #taa elim taa -s1 -s2 /2/ |
---|
680 | qed. |
---|
681 | |
---|
682 | let rec tal_rel_collapsable S1 fl1 s1 s1' S2 fl2 s2 s2' |
---|
683 | (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 : |
---|
684 | ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_collapsable … tal1 → tal_rel … tal1 tal2 → |
---|
685 | tal_collapsable … tal2 ≝ |
---|
686 | match tal1 return λfl1,s1,s1',tal1.? with |
---|
687 | [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ? |
---|
688 | | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ? |
---|
689 | | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ? |
---|
690 | | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ? |
---|
691 | | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ? |
---|
692 | ]. |
---|
693 | -fl1 -s1 -s1' |
---|
694 | [1,2,3: -tal_rel_collapsable #tal2 * * |
---|
695 | #EQ * #s2 * #taa2 *#H *#G *#K #EQ' destruct @taa_append_collapsable % |
---|
696 | | #tal2 * |
---|
697 | | #tal2 #tal2 whd in ⊢ (%→?); #step @(tal_rel_collapsable … step) assumption |
---|
698 | ] |
---|
699 | qed. |
---|
700 | |
---|
701 | let rec flatten_trace_label_label |
---|
702 | (S: abstract_status) (trace_ends_flag: trace_ends_with_ret) |
---|
703 | (start_status: S) (final_status: S) |
---|
704 | (the_trace: trace_label_label S trace_ends_flag start_status final_status) |
---|
705 | on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝ |
---|
706 | match the_trace with |
---|
707 | [ tll_base ends_flag initial final given_trace labelled_proof ⇒ |
---|
708 | let label ≝ |
---|
709 | match as_label … initial return λx: option costlabel. x ≠ None ? → ? with |
---|
710 | [ None ⇒ λabs. ⊥ |
---|
711 | | Some l ⇒ λ_. l |
---|
712 | ] labelled_proof |
---|
713 | in |
---|
714 | (mk_Sig … label ?)::flatten_trace_any_label S ends_flag initial final given_trace |
---|
715 | ] |
---|
716 | and flatten_trace_any_label |
---|
717 | (S: abstract_status) (trace_ends_flag: trace_ends_with_ret) |
---|
718 | (start_status: S) (final_status: S) |
---|
719 | (the_trace: trace_any_label S trace_ends_flag start_status final_status) |
---|
720 | on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝ |
---|
721 | match the_trace with |
---|
722 | [ tal_base_not_return the_status _ _ _ _ ⇒ [ ] |
---|
723 | | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒ |
---|
724 | flatten_trace_label_return … call_trace |
---|
725 | | tal_base_return the_status _ _ _ ⇒ [ ] |
---|
726 | | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final |
---|
727 | _ _ _ call_trace _ final_trace ⇒ |
---|
728 | let call_cost_trace ≝ flatten_trace_label_return … call_trace in |
---|
729 | let final_cost_trace ≝ flatten_trace_any_label … end_flag … final_trace in |
---|
730 | call_cost_trace @ final_cost_trace |
---|
731 | | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ |
---|
732 | flatten_trace_any_label … tail_trace |
---|
733 | ] |
---|
734 | and flatten_trace_label_return |
---|
735 | (S: abstract_status) |
---|
736 | (start_status: S) (final_status: S) |
---|
737 | (the_trace: trace_label_return S start_status final_status) |
---|
738 | on the_trace: list (as_cost_label S) (*Σl: costlabel. ∃pc. as_label_of_pc S pc = Some … l*) ≝ |
---|
739 | match the_trace with |
---|
740 | [ tlr_base before after trace_to_lift ⇒ |
---|
741 | flatten_trace_label_label … trace_to_lift |
---|
742 | | tlr_step initial labelled final labelled_trace ret_trace ⇒ |
---|
743 | let labelled_cost ≝ flatten_trace_label_label … doesnt_end_with_ret … labelled_trace in |
---|
744 | let return_cost ≝ flatten_trace_label_return … ret_trace in |
---|
745 | labelled_cost @ return_cost |
---|
746 | ]. |
---|
747 | [2: |
---|
748 | cases abs -abs #abs @abs % |
---|
749 | |1: |
---|
750 | %{(as_pc_of … initial)} whd in match label; |
---|
751 | change with (as_label ?? = ?) |
---|
752 | generalize in match labelled_proof; whd in ⊢ (% → ?); |
---|
753 | cases (as_label S initial) |
---|
754 | [1: |
---|
755 | #absurd @⊥ cases absurd -absurd #absurd @absurd % |
---|
756 | |2: |
---|
757 | #costlabel normalize nodelta #_ % |
---|
758 | ] |
---|
759 | ] |
---|
760 | qed. |
---|
761 | |
---|
762 | (* JHM: base case now passes the termination checker *) |
---|
763 | let rec taa_append_tal_same_flatten |
---|
764 | S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa : |
---|
765 | ∀tal : trace_any_label S fl st2 st3. |
---|
766 | flatten_trace_any_label … (taa @ tal) = |
---|
767 | flatten_trace_any_label … tal ≝ ?. |
---|
768 | cases taa -st1 -st2 |
---|
769 | [ #st #tal normalize in ⊢ (??%?); // |
---|
770 | | #st_pre #st_init #st2 #H #G #K #taa' #tal |
---|
771 | whd in match (? @ ?); |
---|
772 | whd in ⊢ (??%?); // |
---|
773 | ] |
---|
774 | qed. |
---|
775 | |
---|
776 | let rec tal_collapsable_flatten S fl st1 st2 tal |
---|
777 | on tal : |
---|
778 | tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] ≝ |
---|
779 | match tal |
---|
780 | return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → flatten_trace_any_label … tal = [ ] |
---|
781 | with |
---|
782 | [ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ?? |
---|
783 | | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒ |
---|
784 | tal_collapsable_flatten ???? tail_trace |
---|
785 | | _ ⇒ Ⓧ |
---|
786 | ]. |
---|
787 | |
---|
788 | let rec tll_rel_to_traces_same_flatten |
---|
789 | (S: abstract_status) (S': abstract_status) |
---|
790 | (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret) |
---|
791 | (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S') |
---|
792 | (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l) |
---|
793 | (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r) |
---|
794 | on the_trace_l: |
---|
795 | tll_rel … the_trace_l the_trace_r → |
---|
796 | map … (pi1 …) (flatten_trace_label_label … the_trace_l) = |
---|
797 | map … (pi1 …) (flatten_trace_label_label … the_trace_r) ≝ |
---|
798 | match the_trace_l with |
---|
799 | [ tll_base fl1 st1 st1' tal1 H ⇒ |
---|
800 | match the_trace_r with |
---|
801 | [ tll_base fl2 st2 st2 tal2 G ⇒ ? |
---|
802 | ] |
---|
803 | ] |
---|
804 | and tal_rel_to_traces_same_flatten |
---|
805 | (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret) |
---|
806 | (trace_ends_flag_r: trace_ends_with_ret) |
---|
807 | (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S') |
---|
808 | (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l) |
---|
809 | (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r) |
---|
810 | on the_trace_l: |
---|
811 | tal_rel … the_trace_l the_trace_r → |
---|
812 | map … (pi1 …) (flatten_trace_any_label … the_trace_l) = |
---|
813 | map … (pi1 …) (flatten_trace_any_label … the_trace_r) ≝ |
---|
814 | match the_trace_l with |
---|
815 | [ tal_base_not_return st1 st1' H G K ⇒ ? |
---|
816 | | tal_base_return st1 st1' H G ⇒ ? |
---|
817 | | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ? |
---|
818 | | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ? |
---|
819 | | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ? |
---|
820 | ] |
---|
821 | and tlr_rel_to_traces_same_flatten |
---|
822 | (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S) |
---|
823 | (start_status_r: S') (final_status_r: S') |
---|
824 | (the_trace_l: trace_label_return S start_status_l final_status_l) |
---|
825 | (the_trace_r: trace_label_return S' start_status_r final_status_r) |
---|
826 | on the_trace_l: |
---|
827 | tlr_rel … the_trace_l the_trace_r → |
---|
828 | map … (pi1 …) (flatten_trace_label_return … the_trace_l) = |
---|
829 | map … (pi1 …) (flatten_trace_label_return … the_trace_r) ≝ |
---|
830 | match the_trace_l with |
---|
831 | [ tlr_base before after tll_l ⇒ ? |
---|
832 | | tlr_step initial labelled final tll_l tlr_l ⇒ ? |
---|
833 | ]. |
---|
834 | [ * whd in match as_label_safe; normalize nodelta |
---|
835 | @opt_safe_elim #l1 #EQ1 |
---|
836 | @opt_safe_elim #l2 #EQ2 |
---|
837 | #EQ destruct(EQ) #H_tal |
---|
838 | change with (? :: ? = ? :: ?) lapply H -H lapply G -G |
---|
839 | whd in match as_costed; normalize nodelta |
---|
840 | >EQ1 >EQ2 normalize nodelta #_ #_ |
---|
841 | >(tal_rel_to_traces_same_flatten … H_tal) @refl |
---|
842 | |2,3,4,5,6: |
---|
843 | [1,2,3: * #EQ destruct(EQ)] |
---|
844 | [1,2,3,4: * #st_mid [1,2:|*: * #G' * #call ] * #taa |
---|
845 | [ *#H' *#G' *#K' #EQ |
---|
846 | | *#H' *#G' #EQ |
---|
847 | | *#st_mid' *#H' * [|*#st2_mid''] *#K' *#tlr2 *#L' |
---|
848 | [|*#tl2 *] * #EQ #H_tlr [| #H_tl] |
---|
849 | | *#st_fun *#H' * |
---|
850 | [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L' |
---|
851 | [| *#tl2] ** #EQ #H_tl #H_tlr |
---|
852 | ] >EQ >taa_append_tal_same_flatten |
---|
853 | | whd in ⊢ (%→??(????%)?); |
---|
854 | @tal_rel_to_traces_same_flatten |
---|
855 | ] |
---|
856 | [1,2: % |
---|
857 | |3: @(tlr_rel_to_traces_same_flatten … H_tlr) |
---|
858 | |4,5: <map_append |
---|
859 | >(tal_collapsable_flatten … H_tl) >append_nil |
---|
860 | >(tlr_rel_to_traces_same_flatten … H_tlr) % |
---|
861 | |6: <map_append |
---|
862 | >(tlr_rel_to_traces_same_flatten … H_tlr) |
---|
863 | >(tal_rel_to_traces_same_flatten … H_tl) |
---|
864 | @map_append |
---|
865 | ] |
---|
866 | |*: cases the_trace_r |
---|
867 | [1,3: #st_before_r #st_after_r #tll_r |
---|
868 | [ @tll_rel_to_traces_same_flatten | * ] |
---|
869 | |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r * |
---|
870 | #H_tll #H_tlr |
---|
871 | <map_append |
---|
872 | >(tll_rel_to_traces_same_flatten … H_tll) |
---|
873 | >(tlr_rel_to_traces_same_flatten … H_tlr) |
---|
874 | @map_append |
---|
875 | ] |
---|
876 | ] |
---|
877 | qed. |
---|
878 | |
---|
879 | (* cost maps specifics: summing over flattened traces *) |
---|
880 | |
---|
881 | lemma lift_cost_map_same_cost_tal : |
---|
882 | ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. |
---|
883 | ∀the_trace_in : trace_any_label S_in f_in start_in end_in. |
---|
884 | ∀the_trace_out : trace_any_label S_out f_out start_out end_out. |
---|
885 | tal_rel … the_trace_in the_trace_out → |
---|
886 | (Σ_{l ∈ flatten_trace_any_label … the_trace_in} |
---|
887 | (lift_cost_map_id … dec m_out l)) = |
---|
888 | (Σ_{l ∈ flatten_trace_any_label … the_trace_out} (m_out l)). |
---|
889 | #S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out |
---|
890 | #tal_in #tal_out #H_tal |
---|
891 | @(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal)) |
---|
892 | qed. |
---|
893 | |
---|
894 | lemma lift_cost_map_same_cost_tll : |
---|
895 | ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out. |
---|
896 | ∀the_trace_in : trace_label_label S_in f_in start_in end_in. |
---|
897 | ∀the_trace_out : trace_label_label S_out f_out start_out end_out. |
---|
898 | tll_rel … the_trace_in the_trace_out → |
---|
899 | (Σ_{l ∈ flatten_trace_label_label … the_trace_in} |
---|
900 | (lift_cost_map_id … dec m_out l)) = |
---|
901 | (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)). |
---|
902 | #S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out |
---|
903 | #tll_in #tll_out #H_tll |
---|
904 | @(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll)) |
---|
905 | qed. |
---|
906 | |
---|
907 | lemma lift_cost_map_same_cost_tlr : |
---|
908 | ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out. |
---|
909 | ∀the_trace_in : trace_label_return S_in start_in end_in. |
---|
910 | ∀the_trace_out : trace_label_return S_out start_out end_out. |
---|
911 | tlr_rel … the_trace_in the_trace_out → |
---|
912 | (Σ_{l ∈ flatten_trace_label_return … the_trace_in} |
---|
913 | (lift_cost_map_id … dec m_out l)) = |
---|
914 | (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)). |
---|
915 | #S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out |
---|
916 | #tlr_in #tlr_out #H_tlr |
---|
917 | @(lift_cost_map_same_cost … (tlr_rel_to_traces_same_flatten … H_tlr)) |
---|
918 | qed. |
---|