source: src/common/StructuredTraces_jaap.ma @ 2420

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