source: src/common/StructuredTraces.ma @ 2428

Last change on this file since 2428 was 2423, checked in by tranquil, 7 years ago

as_classifier predicate → as_classify function
as_call predicate from StructuredTraces_jaap → as_call_ident function

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