source: src/common/StructuredTraces.ma @ 2503

Last change on this file since 2503 was 2503, checked in by mckinna, 7 years ago

tidied up, with new auxiliary defns, some refactoring, some code motion, to support a cleaned-up compiler.ma

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