source: src/common/StructuredTraces.ma @ 3104

Last change on this file since 3104 was 2869, checked in by tranquil, 7 years ago

some reorganization of definitions, and a new taaf_append_taaf

File size: 49.3 KB
Line 
1include "basics/bool.ma".
2include "basics/jmeq.ma".
3include "common/CostLabel.ma".
4include "utilities/option.ma".
5include "basics/lists/listb.ma".
6include "common/IO.ma".
7include "utilities/hide.ma".
8include "ASM/Util.ma".
9
10inductive status_class: Type[0] ≝
11  | cl_return: status_class
12  | cl_jump: status_class
13  | cl_call: status_class
14  | cl_tailcall: status_class
15  | cl_other: status_class.
16
17record abstract_status : Type[1] ≝
18  { as_status :> Type[0]
19  ; as_execute : relation as_status
20  ; as_pc : DeqSet
21  ; as_pc_of : as_status → as_pc
22  ; as_classify : as_status → status_class
23  ; as_label_of_pc : as_pc → option costlabel
24  ; as_after_return : (Σs:as_status. as_classify s =  cl_call) → as_status → Prop
25  ; as_result: as_status → option int
26  ; as_call_ident : (Σs:as_status.as_classify s = cl_call) → ident
27  ; as_tailcall_ident : (Σs:as_status.as_classify s = cl_tailcall) → ident
28  }.
29
30definition as_classifier ≝ λS,s,cl.as_classify S s = cl.
31definition as_call ≝ λS,s,f.as_call_ident S s = f.
32definition as_final ≝ λS,s.as_result S s ≠ None ?.
33
34definition as_label ≝ λS : abstract_status. λs : S. as_label_of_pc ? (as_pc_of ? s).
35
36(* temporary alias for backward compatibility *)
37(* definition final_abstract_status ≝ abstract_status. *)
38
39definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
40  λa_s,st.as_label ? st ≠ None ?.
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 map generalities *)
55
56definition as_cost_labelled_at ≝
57  λS : abstract_status. λl.λpc.as_label_of_pc S pc = Some ? l.
58
59definition as_cost_labelled ≝
60  λS : abstract_status. λl.∃pc.as_cost_labelled_at S l pc.
61
62definition as_cost_label ≝
63  λS : abstract_status. Σl.as_cost_labelled S l.
64
65unification hint 0 ≔ S ⊢ as_cost_label S ≡ Sig costlabel (λl.as_cost_labelled S l).
66
67definition as_cost_labels ≝
68  λS : abstract_status. list (as_cost_label S).
69
70definition as_cost_get_label ≝
71  λS : abstract_status. λl_sig: as_cost_label S. pi1 … l_sig.
72
73(*
74(* JHM: this no longer is a complete definition! but not used; so commented out for now *)
75definition as_cost_get_labels ≝
76  λS : abstract_status. map … (as_cost_get_label S).
77*)
78
79definition as_cost_map ≝
80  λS : abstract_status. (as_cost_label S) → ℕ.
81 
82definition as_label_safe : ∀a_s : abstract_status.
83  (Σs : a_s.as_costed ? s) → as_cost_label a_s ≝
84  λa_s,st_sig.«opt_safe ?? (pi2 … st_sig), ?».
85@hide_prf
86@opt_safe_elim #c #EQ %{EQ} qed.
87 
88definition lift_sigma_map_id :
89  ∀A,B : Type[0].∀P_in,P_out : A → Prop.B →
90    (∀a.P_out a + ¬ P_out a) →
91  ((Σa.P_out a) → B) → (Σa.P_in a) → B ≝ λA,B,P_in,P_out,dflt,dec,m,a_sig.
92   match dec a_sig with
93   [ inl prf ⇒ m «a_sig, prf»
94   | inr _ ⇒ dflt (* labels not present in out code get 0 *)
95   ].
96
97lemma lift_sigma_map_id_eq :
98  ∀A,B,P_in,P_out,dflt,dec,m,a_in,a_out.
99  pi1 ?? a_in = pi1 ?? a_out →
100  lift_sigma_map_id A B P_in P_out dflt dec m a_in = m a_out.
101#A#B#P_in#P_out#dflt#dec#m#a_in#a_out#EQ
102whd in match lift_sigma_map_id; normalize nodelta
103cases (dec a_in) normalize nodelta >EQ cases a_out
104#a #H #G [ % | @⊥ /2 by absurd/ ]
105qed.
106
107definition lift_cost_map_id :
108  ∀S_in,S_out : abstract_status.? →
109  as_cost_map S_out → as_cost_map S_in
110  ≝
111 λS_in,S_out : abstract_status.
112  lift_sigma_map_id costlabel ℕ
113    (*λl.∃pc.as_label_of_pc S_in pc = Some ? l*) (as_cost_labelled S_in)
114    (*λl.∃pc.as_label_of_pc S_out pc = Some ? l*) (as_cost_labelled S_out)
115    0.
116
117lemma lift_cost_map_same_cost :
118  ∀S_in, S_out, dec, m_out, trace_in, trace_out.
119  map … (pi1 ??) trace_in = map … (pi1 ??) trace_out →
120  (Σ_{ l_sig ∈ trace_in } (lift_cost_map_id S_in S_out dec m_out l_sig)) =
121  (Σ_{ l_sig ∈ trace_out } (m_out l_sig)).
122#S_in #S_out #dec #m_out #trace_in elim trace_in
123[2: #hd_in #tl_in #IH] * [2,4: #hd_out #tl_out]
124normalize in ⊢ (%→?);
125[2,3: #ABS destruct(ABS)
126|4: #_ %
127|1:
128  #EQ destruct
129  whd in ⊢(??%%);
130  whd in match lift_cost_map_id; normalize nodelta
131  >(lift_sigma_map_id_eq ????????? e0)
132  >e0 in e1; normalize in ⊢(%→?); #EQ
133  >(IH … EQ) %
134]
135qed.
136
137
138(* structured traces: down to business *)
139
140inductive trace_ends_with_ret: Type[0] ≝
141  | ends_with_ret: trace_ends_with_ret
142  | doesnt_end_with_ret: trace_ends_with_ret.
143
144inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
145  | tlr_base:
146      ∀status_before: S.
147      ∀status_after: S.
148        trace_label_label S ends_with_ret status_before status_after →
149        trace_label_return S status_before status_after
150  | tlr_step:
151      ∀status_initial: S.
152      ∀status_labelled: S.
153      ∀status_final: S.
154        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
155        trace_label_return S status_labelled status_final →
156          trace_label_return S status_initial status_final
157with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
158  | tll_base:
159      ∀ends_flag: trace_ends_with_ret.
160      ∀start_status: S.
161      ∀end_status: S.
162        trace_any_label S ends_flag start_status end_status →
163        as_costed S start_status →
164          trace_label_label S ends_flag start_status end_status
165with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
166  (* Single steps within a function which reach a label.
167     Note that this is the only case applicable for a jump. *)
168  | tal_base_not_return:
169      ∀start_status: S.
170      ∀final_status: S.
171        as_execute S start_status final_status →
172        (as_classifier S start_status cl_jump ∨
173         as_classifier S start_status cl_other) →
174        as_costed S final_status →
175          trace_any_label S doesnt_end_with_ret start_status final_status
176  | tal_base_return:
177      ∀start_status: S.
178      ∀final_status: S.
179        as_execute S start_status final_status →
180        as_classifier S start_status cl_return →
181          trace_any_label S ends_with_ret start_status final_status
182  (* A call followed by a label on return. *)
183  | tal_base_call:
184      ∀status_pre_fun_call: S.
185      ∀status_start_fun_call: S.
186      ∀status_final: S.
187        as_execute S status_pre_fun_call status_start_fun_call →
188        ∀H:as_classifier S status_pre_fun_call cl_call.
189          as_after_return S «status_pre_fun_call, H» status_final →
190          trace_label_return S status_start_fun_call status_final →
191          as_costed S status_final →
192            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
193  (* A tailcall, which ends the trace like a return. *)
194  | tal_base_tailcall:
195      ∀status_pre_fun_call: S.
196      ∀status_start_fun_call: S.
197      ∀status_final: S.
198        as_execute S status_pre_fun_call status_start_fun_call →
199        as_classifier S status_pre_fun_call cl_tailcall →
200          trace_label_return S status_start_fun_call status_final →
201            trace_any_label S ends_with_ret status_pre_fun_call status_final
202  (* A call followed by a non-empty trace. *)
203  | tal_step_call:
204      ∀end_flag: trace_ends_with_ret.
205      ∀status_pre_fun_call: S.
206      ∀status_start_fun_call: S.
207      ∀status_after_fun_call: S.
208      ∀status_final: S.
209        as_execute S status_pre_fun_call status_start_fun_call →
210        ∀H:as_classifier S status_pre_fun_call cl_call.
211          as_after_return S «status_pre_fun_call, H» status_after_fun_call →
212          trace_label_return S status_start_fun_call status_after_fun_call →
213          ¬ as_costed S status_after_fun_call →
214          trace_any_label S end_flag status_after_fun_call status_final →
215            trace_any_label S end_flag status_pre_fun_call status_final
216  | tal_step_default:
217      ∀end_flag: trace_ends_with_ret.
218      ∀status_pre: S.
219      ∀status_init: S.
220      ∀status_end: S.
221        as_execute S status_pre status_init →
222        trace_any_label S end_flag status_init status_end →
223        as_classifier S status_pre cl_other →
224        ¬ (as_costed S status_init) →
225          trace_any_label S end_flag status_pre status_end.
226
227let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
228  on tal : list (as_pc S) ≝
229 match tal with
230 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
231 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
232 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
233 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
234 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
235 | tal_base_tailcall pre _ _ _ _ _ ⇒ [as_pc_of … pre]
236 ].
237
238definition as_trace_any_label_length':
239    ∀S: abstract_status.
240    ∀trace_ends_flag: trace_ends_with_ret.
241    ∀start_status: S.
242    ∀final_status: S.
243    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
244      nat ≝
245  λS: abstract_status.
246  λtrace_ends_flag: trace_ends_with_ret.
247  λstart_status: S.
248  λfinal_status: S.
249  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
250    |tal_pc_list … the_trace|.
251
252let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
253  match tlr with
254  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
255  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
256  ]
257and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
258  match tll with
259  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
260  ]
261and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
262  match tal with
263  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
264    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
265    tal_unrepeating … tl ∧
266    tlr_unrepeating … tlr
267  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
268    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
269    tal_unrepeating … tl
270  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
271  | tal_base_tailcall pre _ _ _ _ trace ⇒ tlr_unrepeating … trace
272  | _ ⇒ True
273  ].
274
275definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
276  trace_label_label S fl st1 st2 → costlabel ≝
277  λS,fl,st1,st2,tr.match tr with
278  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
279
280definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
281  trace_label_return S st1 st2 → costlabel ≝
282  λS,st1,st2,tr.match tr with
283  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
284  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
285  ].
286
287let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
288  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
289cases tal //
290#fl' #st1' [#st_fun] #st2' #st3' #H
291[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
292#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
293qed.
294
295lemma tal_pc_list_start : ∀S,fl,s1,s2. ∀tal: trace_any_label S fl s1 s2.
296  ∃tl. tal_pc_list … tal = (as_pc_of S s1)::tl.
297#S #fl0 #s10 #s20 *
298[ #s1 #s2 #EX #CL #CS
299| #s1 #s2 #EX #CL
300| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
301| #s1 #s2 #s3 #EX #CL #tlr
302| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
303| #fl #s1 #s2 #s3 #EX #tal #CL #CS
304] whd in ⊢ (??(λ_.??%?)); % [2,4,6,8,10,12: % | *: skip ]
305qed.
306
307let rec tal_tail_not_costed S fl st1 st2 tal
308  (H:Not (as_costed S st1)) on tal :
309  All ? (λpc. as_label_of_pc S pc = None ?) (tal_pc_list S fl st1 st2 tal) ≝ ?.
310cases tal in H ⊢ %;
311[ #start #final #EX #CL #CS #CS' % // @(not_costed_no_label ?? CS')
312| #start #final #EX #CL #CS % // @(not_costed_no_label ?? CS)
313| #pre #start #final #EX #CL #AF #tlr #CS #CS' % // @(not_costed_no_label ?? CS')
314| #pre #start #final #EX #CL #tlr #CS' % // @(not_costed_no_label ?? CS')
315| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal' #CS'
316  cases (tal_pc_list_start … tal')
317  #hd #E >E
318  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
319| #fl' #pre #init #end #EX #tal' #CL #CS #CS'
320  cases (tal_pc_list_start … tal')
321  #hd #E >E
322  % [ @(not_costed_no_label ?? CS') | @tal_tail_not_costed assumption ]
323] qed.
324
325
326inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
327  | tac_base:
328      ∀status: S.
329        as_classifier S status cl_call ∨ as_classifier S status cl_tailcall →
330          trace_any_call S status status
331  | tac_step_call:
332      ∀status_pre_fun_call: S.
333      ∀status_after_fun_call: S.
334      ∀status_final: S.
335      ∀status_start_fun_call: S.
336        as_execute S status_pre_fun_call status_start_fun_call →
337        ∀H:as_classifier S status_pre_fun_call cl_call.
338          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
339          trace_label_return S status_start_fun_call status_after_fun_call →
340          ¬ as_costed S status_after_fun_call →
341          trace_any_call S status_after_fun_call status_final →
342            trace_any_call S status_pre_fun_call status_final
343  | tac_step_default:
344      ∀status_pre: S.
345      ∀status_end: S.
346      ∀status_init: S.
347        as_execute S status_pre status_init →
348        trace_any_call S status_init status_end →
349        as_classifier S status_pre cl_other →
350        ¬ (as_costed S status_init) →
351          trace_any_call S status_pre status_end.
352
353             
354inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
355  | tlc_base:
356      ∀start_status: S.
357      ∀end_status: S.
358        trace_any_call S start_status end_status →
359        as_costed S start_status →
360        trace_label_call S start_status end_status
361.
362
363definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
364  trace_label_call S st1 st2 → costlabel ≝
365  λS,st1,st2,tr.match tr with
366  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
367  ].
368   
369coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
370  | tld_step:
371      ∀status_initial: S.
372      ∀status_labelled: S.
373          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
374          trace_label_diverges S status_labelled →
375            trace_label_diverges S status_initial
376  | tld_base:
377      ∀status_initial: S.
378      ∀status_pre_fun_call: S.
379      ∀status_start_fun_call: S.
380        trace_label_call S status_initial status_pre_fun_call →
381        as_execute S status_pre_fun_call status_start_fun_call →
382        ∀H:as_classifier S status_pre_fun_call cl_call.
383          trace_label_diverges S status_start_fun_call →
384            trace_label_diverges S status_initial.
385
386definition tld_hd_label : ∀S : abstract_status.∀st.
387  trace_label_diverges S st → costlabel ≝
388  λS,st,tr.match tr with
389  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
390  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
391  ].       
392
393(* Version in Prop for showing existence. *)
394coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
395  | tld_step':
396      ∀status_initial: S.
397      ∀status_labelled: S.
398          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
399          trace_label_diverges_exists S status_labelled →
400            trace_label_diverges_exists S status_initial
401  | tld_base':
402      ∀status_initial: S.
403      ∀status_pre_fun_call: S.
404      ∀status_start_fun_call: S.
405        trace_label_call S status_initial status_pre_fun_call →
406        as_execute S status_pre_fun_call status_start_fun_call →
407        ∀H:as_classifier S status_pre_fun_call cl_call.
408          trace_label_diverges_exists S status_start_fun_call →
409            trace_label_diverges_exists S status_initial.
410
411inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
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 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 S status_start_fun →
427        trace_whole_program S status_initial.
428
429(* Again, an identical version in Prop for existence proofs. *)
430inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
431  | twp_terminating:
432      ∀status_initial: S.
433      ∀status_start_fun: S.
434      ∀status_final: S.
435        as_classifier S status_initial cl_call →
436        as_execute S status_initial status_start_fun →
437        trace_label_return S status_start_fun status_final →
438        as_final S status_final →
439        trace_whole_program_exists S status_initial
440  | twp_diverges:
441      ∀status_initial: S.
442      ∀status_start_fun: S.
443        as_classifier S status_initial cl_call →
444        as_execute S status_initial status_start_fun →
445        trace_label_diverges_exists S status_start_fun →
446        trace_whole_program_exists S status_initial.
447
448
449let rec trace_any_label_label S s s' f
450  (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 ] ≝
451match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
452[ tal_base_not_return start final _ _ C ⇒ C
453| tal_base_return _ _  _ _ ⇒ I
454| tal_base_call _ _ _ _ _ _ _ C ⇒ C
455| tal_base_tailcall _ _ _ _ _ _ ⇒ I
456| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
457| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
458].
459
460definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
461  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
462  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
463
464lemma trace_label_label_label : ∀S,s,s',f.
465  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
466#S #s #s' #f #tr
467cases tr
468#f #start #end #tr' #C @(trace_any_label_label … tr')
469qed.
470
471definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
472  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
473  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
474
475lemma trace_any_call_call : ∀S,s,s'.
476  trace_any_call S s s' → as_classifier S s' cl_call ∨ as_classifier S s' cl_tailcall.
477#S #s #s' #T elim T [1,3: //]
478#H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 //
479qed.
480
481(*
482(* an trace of unlabeled and cl_other states, possibly empty *)
483inductive trace_no_label_any (S:abstract_status) : S → S → Type[0] ≝
484  | tna_base :
485      ∀start_status: S.
486      ¬as_costed … start_status →
487      trace_no_label_any S start_status start_status
488  | tna_step :
489      ∀status_pre: S.
490      ∀status_init: S.
491      ∀status_end: S.
492        as_execute S status_pre status_init →
493        as_classifier S status_pre cl_other →
494        ¬as_costed … status_pre →
495        trace_no_label_any S status_init status_end →
496          trace_no_label_any S status_pre status_end.
497
498let rec tna_append_tna S st1 st2 st3 (taa1 : trace_no_label_any S st1 st2)
499  on taa1 :
500    trace_no_label_any S st2 st3 →
501    trace_no_label_any S st1 st3 ≝
502  match taa1 with
503  [ tna_base st1' H ⇒ λtaa2.taa2
504  | tna_step st1' st2' st3' H G K tl ⇒
505    λtaa2.tna_step ???? H G K (tna_append_tna … tl taa2)
506  ].
507
508definition tna_non_empty ≝ λS,st1,st2.λtna : trace_no_label_any S st1 st2.
509  match tna with
510  [ tna_base _ _ ⇒ false
511  | tna_step _ _ _ _ _ _ _ ⇒ true
512  ].
513
514coercion tna_to_bool : ∀S,st1,st2.∀tna:trace_no_label_any S st1 st2.bool ≝
515 tna_non_empty on _tna : trace_no_label_any ??? to bool.
516
517lemma tna_unlabelled : ∀S,st1,st2.trace_no_label_any S st1 st2 → ¬as_costed … st1.
518#S #st1 #st2 * [#st #H @H | #st #st' #st'' #_ #_ #H #_ @H] qed.
519
520let rec tna_append_tal S st1 fl st2 st3 (tna : trace_no_label_any S st1 st2)
521  on tna :
522  trace_any_label S fl st2 st3 →
523  if tna then Not (as_costed … st2) else True →
524  trace_any_label S fl st1 st3 ≝
525  match tna return λst1,st2.λx : trace_no_label_any S st1 st2.
526    ∀fl,st3.
527    trace_any_label S fl st2 st3 →
528    if x then Not (as_costed … st2) else True →
529    trace_any_label S fl st1 st3
530  with
531  [ tna_base st1' H ⇒ λfl,st3,taa2,prf.taa2
532  | tna_step st1' st2' st3' H G K tl ⇒ λfl,st3,taa2,prf.
533    tal_step_default ????? H (tna_append_tal ????? tl taa2 ?) G (tna_unlabelled … tl)
534  ] fl st3.
535  cases (tna_non_empty … tl) [@prf|%]
536  qed.
537*)
538
539inductive trace_any_any (S : abstract_status) : S → S → Type[0] ≝
540  | taa_base : ∀st.trace_any_any S st st
541  | taa_step : ∀st1,st2,st3.
542    as_execute S st1 st2 →
543    as_classifier S st1 cl_other →
544    ¬as_costed S st2 →
545    trace_any_any S st2 st3 →
546    trace_any_any S st1 st3.
547
548definition taa_non_empty ≝ λS,st1,st2.λtaa : trace_any_any S st1 st2.
549  match taa with
550  [ taa_base _ ⇒ false
551  | taa_step _ _ _ _ _ _ _ ⇒ true
552  ].
553
554coercion taa_to_bool : ∀S,st1,st2.∀taa:trace_any_any S st1 st2.bool ≝
555 taa_non_empty on _taa : trace_any_any ??? to bool.
556
557let rec taa_append_tal S st1 fl st2 st3
558  (taa : trace_any_any S st1 st2) on taa :
559  trace_any_label S fl st2 st3 →
560  trace_any_label S fl st1 st3 ≝
561  match taa return λst1,st2.λx : trace_any_any S st1 st2.
562    ∀fl,st3.
563    trace_any_label S fl st2 st3 →
564    trace_any_label S fl st1 st3
565  with
566  [ taa_base st1' ⇒ λfl,st3,tal2.tal2
567  | taa_step st1' st2' st3' H G K tl ⇒ λfl,st3,tal2.
568    tal_step_default ????? H (taa_append_tal ????? tl tal2) G K
569  ] fl st3.
570
571interpretation "trace any any label append" 'append taa tal = (taa_append_tal ????? taa tal).
572
573let rec tal_collapsable S fl s1 s2 (tal : trace_any_label S fl s1 s2) on tal : Prop ≝
574match tal with
575[ tal_base_not_return _ _ _ _ _ ⇒ True
576| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable … tl1
577| _ ⇒ False
578].
579
580let rec tlr_rel S1 st1 st1' S2 st2 st2'
581  (tlr1 : trace_label_return S1 st1 st1')
582  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
583match tlr1 with
584  [ tlr_base st1 st1' tll1 ⇒
585    match tlr2 with
586    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
587    | _ ⇒ False
588    ]
589  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
590    match tlr2 with
591    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
592      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
593    | _ ⇒ False
594    ]
595  ]
596and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
597 (tll1 : trace_label_label S1 fl1 st1 st1')
598 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
599  match tll1 with
600  [ tll_base fl1 st1 st1' tal1 H ⇒
601    match tll2 with
602    [ tll_base fl2 st2 st2 tal2 G ⇒
603      pi1 … (as_label_safe … («?, H»)) = pi1 … (as_label_safe … («?, G»)) ∧
604      tal_rel … tal1 tal2
605    ]
606  ]
607and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
608 (tal1 : trace_any_label S1 fl1 st1 st1')
609 (tal2 : trace_any_label S2 fl2 st2 st2')
610   on tal1 : Prop ≝
611  match tal1 with
612  [ tal_base_not_return st1 st1' _ _ _ ⇒
613    fl2 = doesnt_end_with_ret ∧
614    ∃st2mid,taa,H,G,K.
615    tal2 ≃ taa_append_tal ? st2 ??? taa
616      (tal_base_not_return ? st2mid st2' H G K)
617  | tal_base_return st1 st1' _ _ ⇒
618    fl2 = ends_with_ret ∧
619    ∃st2mid,taa,H,G.
620    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
621      (tal_base_return ? st2mid st2' H G)
622  | tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒
623    fl2 = doesnt_end_with_ret ∧
624    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
625    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
626    (* we must allow a tal_base_call to be similar to a call followed
627      by a collapsable trace (trace_any_any followed by a base_not_return;
628      we cannot use trace_any_any as it disallows labels in the end as soon
629      as it is non-empty) *)
630    (∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
631      tal2 ≃ taa @ (tal_base_call … H G K tlr2 L) ∧ tlr_rel … tlr1 tlr2) ∨
632    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
633    ∃tl2 : trace_any_label … doesnt_end_with_ret st2mid'' st2'.
634      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
635      tlr_rel … tlr1 tlr2 ∧ tal_collapsable … tl2
636  | tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒
637    fl2 = ends_with_ret ∧
638    ∃st2mid,G.as_tailcall_ident S2 («st2mid, G») = as_tailcall_ident ? «st1, prf» ∧
639    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
640    ∃tlr2 : trace_label_return ? st2mid' st2'.
641      tal2 ≃ taa @ (tal_base_tailcall … H G tlr2) ∧ tlr_rel … tlr1 tlr2
642  | tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒
643    ∃st2mid,G.as_call_ident S2 («st2mid, G») = as_call_ident ? «st1, prf» ∧
644    ∃taa : trace_any_any ? st2 st2mid.∃st2mid',H.
645    (fl2 = doesnt_end_with_ret ∧ ∃K.∃tlr2 : trace_label_return ? st2mid' st2'.∃L.
646      tal2 ≃ taa @ tal_base_call … H G K tlr2 L ∧
647      tal_collapsable … tl1 ∧ tlr_rel … tlr1 tlr2) ∨
648    ∃st2mid'',K.∃tlr2 : trace_label_return ? st2mid' st2mid''.∃L.
649    ∃tl2 : trace_any_label ? fl2 st2mid'' st2'.
650      tal2 ≃ taa @ (tal_step_call … H G K tlr2 L tl2) ∧
651      tal_rel … tl1 tl2 ∧ tlr_rel … tlr1 tlr2
652  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
653    tal_rel … tl1 tal2 (* <- this makes it many to many *)
654  ].
655
656interpretation "trace any label rel" 'napart t1 t2 = (tal_rel ???????? t1 t2).
657interpretation "trace label label rel" 'napart t1 t2 = (tll_rel ???????? t1 t2).
658interpretation "trace label return rel" 'napart t1 t2 = (tlr_rel ?????? t1 t2).
659
660let rec tal_collapsable_eq_fl S1 fl1 s1 s1'
661  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
662  tal_collapsable … tal1 → fl1 = doesnt_end_with_ret ≝
663match tal1 return λfl1,s1,s1',tal1.
664  tal_collapsable S1 fl1 s1 s1' tal1 → fl1 = doesnt_end_with_ret with
665[ tal_base_not_return _ _ _ _ _ ⇒ λ_.refl …
666| tal_step_default fl1 _ st1' st1'' _ tl1 _ _ ⇒ tal_collapsable_eq_fl … tl1
667| _ ⇒ Ⓧ
668].
669
670let rec tal_rel_eq_fl S1 fl1 s1 s1' S2 fl2 s2 s2'
671  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
672  ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_rel … tal1 tal2 → fl1 = fl2 ≝
673  match tal1 return λfl1,s1,s1',tal1.? with
674  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
675  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
676  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
677  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
678  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
679  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
680  ].
681-fl1 -s1 -s1'
682[1,2,3,4: -tal_rel_eq_fl #tal2 * //
683| #tal2 * #s2_mid * #G2 * #call * #taa2 * #s2' *#H2 *
684  [ * #EQ1 *#K2 *#tlr2 *#L2 ** #_ #coll #_ >(tal_collapsable_eq_fl … coll) //
685  | * #s2_mid' *#K2 *#tlr2 *#L2 *#tl2 ** #_ #step #_
686     @(tal_rel_eq_fl … step)
687  ]
688| #tal2 whd in ⊢ (%→?); #step @(tal_rel_eq_fl … step)
689]
690qed.
691
692let rec taa_rel_inv S1 fl1 st1 st1mid st1' S2 fl2 st2 st2'
693  (taa1 : trace_any_any S1 st1 st1mid) on taa1 :
694  ∀tal1 : trace_any_label S1 fl1 st1mid st1'.
695  ∀tal2 : trace_any_label S2 fl2 st2 st2'.
696  tal_rel … (taa1 @ tal1) tal2 →
697  tal_rel … tal1 tal2 ≝ ?.
698cases taa1 -taa1
699[ -taa_rel_inv //
700| #st #st' #st'' #H #G #K #tl #tal1 #tal2 whd in ⊢ (%→?);
701  @(taa_rel_inv … tl)
702]
703qed.
704
705lemma taa_append_collapsable : ∀S,s1,fl,s2,s3.
706  ∀taa,tal.tal_collapsable S fl s2 s3 tal → tal_collapsable S fl s1 s3 (taa@tal).
707  #S #s1 #fl #s2 #s3 #taa elim taa -s1 -s2 /2/
708qed.
709
710let rec tal_rel_collapsable S1 fl1 s1 s1' S2 fl2 s2 s2'
711  (tal1 : trace_any_label S1 fl1 s1 s1') on tal1 :
712  ∀tal2 : trace_any_label S2 fl2 s2 s2'.tal_collapsable … tal1 → tal_rel … tal1 tal2 →
713  tal_collapsable … tal2 ≝
714  match tal1 return λfl1,s1,s1',tal1.? with
715  [ tal_base_not_return st1 st1' _ _ _ ⇒ let BASE_NR ≝ 0 in ?
716  | tal_base_return st1 st1' _ _ ⇒ let BASE_R ≝ 0 in ?
717  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒ let BASE_C ≝ 0 in ?
718  | tal_base_tailcall st1 st1' st1'' _ _ tlr1 ⇒ let BASE_TC ≝ 0 in ?
719  | tal_step_call flg1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒ let STEP_C ≝ 0 in ?
720  | tal_step_default flg1 st1 st1' st1'' _ tl1 _ _ ⇒ let STEP ≝ 0 in ?
721  ].
722-fl1 -s1 -s1'
723[1,2,3,4: -tal_rel_collapsable #tal2 * *
724  #EQ * #s2 * #taa2 *#H *#G *#K #EQ' destruct @taa_append_collapsable %
725| #tal2 *
726| #tal2 #tal2 whd in ⊢ (%→?); #step @(tal_rel_collapsable … step) assumption
727]
728qed.
729
730inductive intensional_event : Type[0] ≝
731| IEVcost : costlabel → intensional_event
732| IEVcall : ident → intensional_event
733| IEVtailcall : ident → ident → intensional_event
734| IEVret : ident → intensional_event.
735
736(* NB: we don't restrict call idents, because it would need some more tinkering
737   with abstract_status *)
738definition as_emittable : abstract_status → intensional_event → Prop ≝
739λS,ev.
740match ev with
741[ IEVcost c ⇒ as_cost_labelled S c
742| _ ⇒ True
743].
744 
745definition as_trace ≝
746λS : abstract_status.
747Σl : list intensional_event.All … (as_emittable S) l.
748
749unification hint 0 ≔ S ⊢ as_trace S ≡ Sig (list intensional_event) (λl.All … (as_emittable S) l).
750
751definition cons_safe : ∀A,P.(Σx.P x) → (Σl.All A P l) → Σl.All A P l ≝
752λA,P,x,l.«x::l, conj … (pi2 … x) (pi2 … l)».
753
754definition append_safe : ∀A,P.(Σl.All A P l) → (Σl.All A P l) → Σl.All A P l ≝
755λA,P,l1,l2.«l1@l2,
756  cic:/matita/cerco/utilities/lists/All_append.def(2) … (pi2 … l1) (pi2 … l2)».
757
758definition nil_safe : ∀A,P.(Σl.All A P l) ≝ λA,P.«[ ], I».
759
760interpretation "safe consing" 'vcons hd tl = (cons_safe ?? hd tl).
761interpretation "safe appending" 'vappend l1 l2 = (append_safe ?? l1 l2).
762interpretation "safe nil" 'vnil = (nil_safe ??).
763
764definition emittable_cost : ∀S.as_cost_label S → Σev.as_emittable S ev ≝
765λS,l.«IEVcost l, pi2 … l».
766
767let rec observables_trace_label_label
768  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
769    (start_status: S) (final_status: S)
770      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
771      (curr : ident)
772        on the_trace: as_trace S ≝
773  match the_trace with
774  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
775      let label ≝ as_label_safe … «?, labelled_proof» in
776      emittable_cost … label ::: observables_trace_any_label S ends_flag initial final given_trace curr
777  ]
778and observables_trace_any_label
779  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
780    (start_status: S) (final_status: S)
781      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
782      (curr : ident)
783        on the_trace: as_trace S ≝
784  match the_trace with
785  [ tal_base_not_return the_status _ _ _ _ ⇒ [[ ]]
786  | tal_base_call pre_fun_call start_fun_call final _ cl _ call_trace _ ⇒
787      let id ≝ as_call_ident ? «?, cl» in
788      IEVcall id ::: observables_trace_label_return ??? call_trace id
789  | tal_base_tailcall pre_fun_call start_fun_call final _ cl call_trace ⇒
790      let id ≝ as_tailcall_ident ? «?, cl» in
791      IEVtailcall curr id ::: observables_trace_label_return … call_trace id
792  | tal_base_return the_status _ _ _ ⇒ [[ IEVret curr]]
793  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
794    _ cl _ call_trace _ final_trace ⇒
795    let id ≝ as_call_ident ? «?, cl» in
796    let call_cost_trace ≝ observables_trace_label_return … call_trace id in
797    let final_cost_trace ≝ observables_trace_any_label … end_flag … final_trace curr in
798    IEVcall id ::: call_cost_trace @@ final_cost_trace
799  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
800    observables_trace_any_label … tail_trace curr
801  ]
802and observables_trace_label_return
803  (S: abstract_status)
804    (start_status: S) (final_status: S)
805      (the_trace: trace_label_return S start_status final_status)
806      (curr : ident)
807        on the_trace: as_trace S ≝
808  match the_trace with
809  [ tlr_base before after trace_to_lift ⇒
810      observables_trace_label_label … trace_to_lift curr
811  | tlr_step initial labelled final labelled_trace ret_trace ⇒
812    let labelled_cost ≝ observables_trace_label_label … doesnt_end_with_ret … labelled_trace curr in
813    let return_cost ≝ observables_trace_label_return … ret_trace curr in
814        labelled_cost @@ return_cost
815  ]. % qed.
816 
817let rec filter_map X Y (f : X → option Y) (l : list X) on l : list Y ≝
818match l with
819[ nil ⇒ [ ]
820| cons hd tl ⇒
821  match f hd with
822  [ Some y ⇒ [ y ]
823  | None ⇒ [ ]
824  ] @ filter_map … f tl
825].
826
827lemma filter_map_append:
828 ∀X,Y,f,l1,l2. filter_map X Y f (l1@l2) = filter_map … f l1 @ filter_map … f l2.
829 #X #Y #f #l1 elim l1 // #hd #tl #IH #l2 normalize >IH //
830qed.
831
832lemma map_to_filter_map : ∀X,Y,f,l.map X Y f l = filter_map X Y (λx.Some ? (f x)) l.
833#X #Y #f #l elim l normalize // qed.
834
835lemma filter_map_compose : ∀X,Y,Z,f,g,l.
836filter_map Y Z f (filter_map X Y g l) =
837  filter_map X Z (λx.! y ← g x ; f y) l.
838#X #Y #Z #f #g #l elim l [%]
839#hd #tl #IH
840whd in ⊢ (??(????%)%);
841 cases (g ?) normalize nodelta
842 [2: #y >m_return_bind whd in ⊢ (??%?); @eq_f2 [ % ]]
843@IH
844qed.
845
846lemma filter_map_ext_eq : ∀X,Y,f,g,l.
847  (∀x.f x = g x) → filter_map X Y f l = filter_map X Y g l.
848#X #Y #f #g #l #H elim l normalize [%] #hd #tl #IH >H @eq_f @IH qed.
849
850let rec list_distribute_sig_aux X P (l : list X) on l : All X P l → list (Σx.P x) ≝
851match l return λl.All X P l → list (Σx.P x) with
852[ nil ⇒ λ_.[ ]
853| cons hd tl ⇒ λprf.«hd, proj1 … prf» :: list_distribute_sig_aux X P tl (proj2 … prf)
854].
855
856definition list_distribute_sig : ∀A,P.(Σl.All A P l) → list (Σx.P x) ≝
857λA,P,l.list_distribute_sig_aux … l (pi2 … l).
858
859lemma list_distribute_sig_append:
860 ∀A,P,l1,l2,prf1,prf2,prf3.
861  list_distribute_sig A P «l1@l2,prf3» =
862   list_distribute_sig … «l1,prf1» @ list_distribute_sig … «l2,prf2».
863 #A #P #l1 whd in match list_distribute_sig; normalize nodelta elim l1 //
864 #hd #tl #IH normalize #l2 #prf1 #prf2 #prf3 <IH //
865qed.
866
867let rec list_factor_sig X P (l : list (Σx.P x)) on l : Σl.All X P l ≝
868match l with
869[ nil ⇒ [[ ]]
870| cons hd tl ⇒ hd ::: list_factor_sig … tl
871].
872
873definition costlabels_of_observables : ∀S.as_trace S → list (as_cost_label S) ≝
874λS,l.filter_map (Σev.as_emittable S ev) ?
875  (λev.match ev return λev.as_emittable S ev → option ? with
876    [ IEVcost c ⇒ λprf.Some ? «c, prf»
877    | _ ⇒ λ_.None ?
878    ] (pi2 … ev)) (list_distribute_sig … l).
879
880axiom costlabels_of_observables_trace_label_return_id_irrelevant:
881 ∀S,s1,s2,tr,id1,id2.
882  costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id1) =
883  costlabels_of_observables S (observables_trace_label_return S s1 s2 tr id2).
884
885lemma costlabels_of_observables_append:
886 ∀S:abstract_status. ∀tr1,tr2: as_trace S.
887  costlabels_of_observables S (tr1 @ tr2) =
888   costlabels_of_observables … tr1 @ costlabels_of_observables … tr2.
889[ #S #tr1 #tr2 whd in match costlabels_of_observables; normalize nodelta
890  <filter_map_append <list_distribute_sig_append //
891| @All_append [ @(pi2 … tr1) | @(pi2 … tr2) ]]
892qed.
893
894(* JHM: base case now passes the termination checker *)
895let rec taa_append_tal_same_observables
896  S st1 fl st2 st3 (taa : trace_any_any S st1 st2) on taa :
897  ∀tal : trace_any_label S fl st2 st3.∀curr.
898    observables_trace_any_label ???? (taa @ tal) curr =
899      observables_trace_any_label ???? tal curr ≝ ?.
900cases taa -st1 -st2
901[ #st #tal #curr normalize in ⊢ (??%?); //
902| #st_pre #st_init #st2 #H #G #K #taa' #tal #curr
903  whd in match (? @ ?);
904  whd in ⊢ (??%?); //
905]
906qed.
907
908let rec tal_collapsable_observables S fl st1 st2 tal
909  on tal :
910  ∀curr.
911  tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ] ≝
912λcurr.
913match tal
914return λfl,st1,st2,tal.tal_collapsable S fl st1 st2 tal → observables_trace_any_label … tal curr = [ ]
915with
916[ tal_base_not_return the_status _ _ _ _ ⇒ λ_.refl ??
917| tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
918  tal_collapsable_observables ???? tail_trace curr
919| _ ⇒ Ⓧ
920].
921
922let rec tll_rel_to_traces_same_observables
923  (S: abstract_status) (S': abstract_status)
924    (trace_ends_flag_l: trace_ends_with_ret) (trace_ends_flag_r: trace_ends_with_ret)
925    (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
926      (the_trace_l: trace_label_label S trace_ends_flag_l start_status_l final_status_l)
927        (the_trace_r: trace_label_label S' trace_ends_flag_r start_status_r final_status_r)
928        (curr : ident)
929          on the_trace_l:
930            tll_rel … the_trace_l the_trace_r →
931              pi1 … (observables_trace_label_label … the_trace_l curr) =
932                pi1 … (observables_trace_label_label … the_trace_r curr) ≝
933  match the_trace_l with
934  [ tll_base fl1 st1 st1' tal1 H ⇒
935    match the_trace_r with
936    [ tll_base fl2 st2 st2 tal2 G ⇒ ?
937    ]
938  ]
939and tal_rel_to_traces_same_observables
940  (S: abstract_status) (S': abstract_status) (trace_ends_flag_l: trace_ends_with_ret)
941    (trace_ends_flag_r: trace_ends_with_ret)
942      (start_status_l: S) (final_status_l: S) (start_status_r: S') (final_status_r: S')
943        (the_trace_l: trace_any_label S trace_ends_flag_l start_status_l final_status_l)
944          (the_trace_r: trace_any_label S' trace_ends_flag_r start_status_r final_status_r)
945          (curr : ident)
946          on the_trace_l:
947            tal_rel … the_trace_l the_trace_r →
948              pi1 … (observables_trace_any_label … the_trace_l curr) =
949                pi1 … (observables_trace_any_label … the_trace_r curr) ≝
950  match the_trace_l with
951  [ tal_base_not_return st1 st1' H G K ⇒ ?
952  | tal_base_return st1 st1' H G ⇒ ?
953  | tal_base_call st1 st1' st1'' H G K tlr1 L ⇒ ?
954  | tal_base_tailcall st1 st1' st1'' H G tlr1 ⇒ ?
955  | tal_step_call fl1 st1 st1' st1'' st1''' H G K tlr1 L tl1 ⇒ ?
956  | tal_step_default fl1 st1 st1' st1'' H tl1 G K ⇒ ?
957  ]
958and tlr_rel_to_traces_same_observables
959  (S: abstract_status) (S': abstract_status) (start_status_l: S) (final_status_l: S)
960    (start_status_r: S') (final_status_r: S')
961      (the_trace_l: trace_label_return S start_status_l final_status_l)
962        (the_trace_r: trace_label_return S' start_status_r final_status_r)
963        (curr : ident)
964        on the_trace_l:
965          tlr_rel … the_trace_l the_trace_r →
966            pi1 … (observables_trace_label_return … the_trace_l curr) =
967              pi1 … (observables_trace_label_return … the_trace_r curr) ≝
968  match the_trace_l with
969  [ tlr_base before after tll_l ⇒ ?
970  | tlr_step initial labelled final tll_l tlr_l ⇒ ?
971  ]. 
972[ * #EQ #H_tal
973  whd in ⊢ (??%%); @eq_f2 [2: @(tal_rel_to_traces_same_observables … H_tal)]
974  cases (as_label_safe ??) in EQ; #c1 #H1
975  cases (as_label_safe ??) #c2 #H2 #EQ destruct %
976|2,3,4,5,6,7:
977  [1,2,3,4: * #EQ destruct(EQ)]
978  [1,2,3,4,5: * #st_mid [1,2:|*: * #G' * #call ] * #taa
979    [ *#H' *#G' *#K' #EQ
980    | *#H' *#G' #EQ
981    | *#st_mid' *#H' * [|*#st2_mid''] *#K' *#tlr2 *#L'
982      [|*#tl2 *] * #EQ #H_tlr [| #H_tl]
983    | *#st_mid' *#H' *#tlr2 * #EQ #H_tlr
984    | *#st_fun *#H' *
985      [*#fl_EQ destruct(fl_EQ) |* #st2_mid ] *#K' *#tlr2 *#L'
986      [| *#tl2] ** #EQ #H_tl #H_tlr
987    ] >EQ >taa_append_tal_same_observables
988  | whd in ⊢ (%→??(???%)?); @tal_rel_to_traces_same_observables
989  ]
990  whd in ⊢ (??%%);
991  [1,2: %
992  |3,5: >call >(tlr_rel_to_traces_same_observables … H_tlr) %
993  |4,6: >call >(tal_collapsable_observables … H_tl) >append_nil
994    >(tlr_rel_to_traces_same_observables … H_tlr) %
995  |7: >call
996    >(tlr_rel_to_traces_same_observables … H_tlr)
997    >(tal_rel_to_traces_same_observables … H_tl)
998    %
999  ]
1000|*: cases the_trace_r
1001  [1,3: #st_before_r #st_after_r #tll_r
1002    [ @tll_rel_to_traces_same_observables | * ]
1003  |*: #st_init_r #st_labld_r #st_fin_r #tll_r #tlr_r *
1004    #H_tll #H_tlr
1005    whd in ⊢ (??%%);
1006    >(tll_rel_to_traces_same_observables … H_tll)
1007    >(tlr_rel_to_traces_same_observables … H_tlr)
1008    %
1009  ]
1010]
1011qed.
1012
1013(* cost maps specifics: summing over flattened traces *)
1014
1015(* lemma lift_cost_map_same_cost_tal :
1016  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
1017  ∀the_trace_in : trace_any_label S_in f_in start_in end_in.
1018  ∀the_trace_out : trace_any_label S_out f_out start_out end_out.
1019  tal_rel … the_trace_in the_trace_out →
1020  (Σ_{l ∈ flatten_trace_any_label … the_trace_in}
1021    (lift_cost_map_id … dec m_out l)) =
1022  (Σ_{l ∈ flatten_trace_any_label … the_trace_out} (m_out l)).
1023#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
1024#tal_in #tal_out #H_tal
1025@(lift_cost_map_same_cost … (tal_rel_to_traces_same_flatten … H_tal))
1026qed.
1027
1028lemma lift_cost_map_same_cost_tll :
1029  ∀S_in, S_out, dec, m_out, f_in, f_out, start_in, start_out, end_in, end_out.
1030  ∀the_trace_in : trace_label_label S_in f_in start_in end_in.
1031  ∀the_trace_out : trace_label_label S_out f_out start_out end_out.
1032  tll_rel … the_trace_in the_trace_out →
1033  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
1034    (lift_cost_map_id … dec m_out l)) =
1035  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
1036#S_in #S_out #dec #m_out #f_in #f_out #start_in #start_out #end_in #end_out
1037#tll_in #tll_out #H_tll
1038@(lift_cost_map_same_cost … (tll_rel_to_traces_same_flatten … H_tll))
1039qed.
1040*)
1041
1042lemma map_pi1_distribute_sig : ∀A,P,l.
1043  map ?? (pi1 ??) (list_distribute_sig A P l) = pi1 ?? l.
1044#A #P * #l elim l -l normalize // qed.
1045
1046definition flatten_trace_label_return ≝
1047  λS,st1,st2.λtlr : trace_label_return S st1 st2.
1048  (* as cost events do not depend on current function identifier, we
1049     can use a dummy one *)
1050  let dummy ≝ an_identifier ? one in
1051  costlabels_of_observables … (observables_trace_label_return … tlr dummy).
1052
1053definition flatten_trace_label_label ≝
1054  λS,flag,st1,st2.λtll : trace_label_label S flag st1 st2.
1055  (* as cost events do not depend on current function identifier, we
1056     can use a dummy one *)
1057  let dummy ≝ an_identifier ? one in
1058  costlabels_of_observables … (observables_trace_label_label … tll dummy).
1059
1060definition flatten_trace_any_label ≝
1061  λS,flag,st1,st2.λtll : trace_any_label S flag st1 st2.
1062  (* as cost events do not depend on current function identifier, we
1063     can use a dummy one *)
1064  let dummy ≝ an_identifier ? one in
1065  costlabels_of_observables … (observables_trace_any_label … tll dummy).
1066
1067lemma lift_cost_map_same_cost_tlr :
1068  ∀S_in, S_out, dec, m_out, start_in, start_out, end_in, end_out.
1069  ∀the_trace_in : trace_label_return S_in start_in end_in.
1070  ∀the_trace_out : trace_label_return S_out start_out end_out.
1071  tlr_rel … the_trace_in the_trace_out →
1072  (Σ_{l ∈ flatten_trace_label_return … the_trace_in}
1073    (lift_cost_map_id … dec m_out l)) =
1074  (Σ_{l ∈ flatten_trace_label_return … the_trace_out} (m_out l)).
1075#S_in #S_out #dec #m_out #start_in #start_out #end_in #end_out
1076#tlr_in #tlr_out #H_tlr
1077@lift_cost_map_same_cost
1078whd in match flatten_trace_label_return; normalize nodelta
1079>map_to_filter_map >map_to_filter_map >filter_map_compose
1080>filter_map_compose
1081cut (∀S.∀x: (Σev.as_emittable S ev).
1082  ! y ←
1083    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
1084    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
1085  Some ? (pi1 ?? y) =
1086  ! ev ← Some ? (pi1 ?? x) ;
1087  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
1088[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
1089#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
1090<filter_map_compose <filter_map_compose @eq_f
1091<map_to_filter_map <map_to_filter_map
1092>map_pi1_distribute_sig >map_pi1_distribute_sig
1093@(tlr_rel_to_traces_same_observables … H_tlr) %
1094qed.
1095
1096lemma lift_cost_map_same_cost_tll :
1097  ∀S_in, S_out, dec, m_out, fl_in, fl_out, start_in, start_out, end_in, end_out.
1098  ∀the_trace_in : trace_label_label S_in fl_in start_in end_in.
1099  ∀the_trace_out : trace_label_label S_out fl_out start_out end_out.
1100  tll_rel … the_trace_in the_trace_out →
1101  (Σ_{l ∈ flatten_trace_label_label … the_trace_in}
1102    (lift_cost_map_id … dec m_out l)) =
1103  (Σ_{l ∈ flatten_trace_label_label … the_trace_out} (m_out l)).
1104#S_in #S_out #dec #m_out #fl_in #fl_out #start_in #start_out #end_in #end_out
1105#tlr_in #tlr_out #H_tlr
1106@lift_cost_map_same_cost
1107whd in match flatten_trace_label_label; normalize nodelta
1108>map_to_filter_map >map_to_filter_map >filter_map_compose
1109>filter_map_compose
1110cut (∀S.∀x: (Σev.as_emittable S ev).
1111  ! y ←
1112    match pi1 ?? x return λx.as_emittable S x → option (Σc.as_cost_labelled S c) with
1113    [ IEVcost c ⇒ λprf.Some ? «c, prf» | _ ⇒ λ_.None ? ] (pi2 ?? x) ;
1114  Some ? (pi1 ?? y) =
1115  ! ev ← Some ? (pi1 ?? x) ;
1116  match ev with [ IEVcost c ⇒ Some ? c | _ ⇒ None ?])
1117[ #S ** [ #c #em | #i * | #i #j * | #i * ] %]
1118#EQext >(filter_map_ext_eq … (EQext S_in)) >(filter_map_ext_eq … (EQext S_out))
1119<filter_map_compose <filter_map_compose @eq_f
1120<map_to_filter_map <map_to_filter_map
1121>map_pi1_distribute_sig >map_pi1_distribute_sig
1122@(tll_rel_to_traces_same_observables … H_tlr) %
1123qed.
1124
1125(* the equivalent of a collapsable trace_any_label where we do not force
1126   costedness of the lookahead status *)
1127inductive trace_any_any_free (S : abstract_status) : S → S → Type[0] ≝
1128| taaf_base : ∀s.trace_any_any_free S s s
1129| taaf_step : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
1130  as_classifier S s2 cl_other →
1131  trace_any_any_free S s1 s3
1132| taaf_step_jump : ∀s1,s2,s3.trace_any_any S s1 s2 → as_execute S s2 s3 →
1133  as_classifier S s2 cl_jump →
1134  as_costed S s3 →
1135  trace_any_any_free S s1 s3.
1136
1137definition taaf_non_empty ≝ λS,s1,s2.λtaaf : trace_any_any_free S s1 s2.
1138match taaf with
1139[ taaf_base _ ⇒ false
1140| _ ⇒ true
1141].
1142
1143(* utilities on taa and taaf *)
1144
1145let rec taa_append_taa S st1 st2 st3
1146  (taa : trace_any_any S st1 st2) on taa :
1147  trace_any_any S st2 st3 →
1148  trace_any_any S st1 st3 ≝
1149  match taa
1150  with
1151  [ taa_base st1' ⇒ λst3,taa2.taa2
1152  | taa_step st1' st2' st3' H I J tl ⇒ λst3,taa2.
1153    taa_step ???? H I J (taa_append_taa … tl taa2)
1154  ] st3.
1155
1156definition taaf_to_taa : ∀S : abstract_status.∀s1,s2,taaf.
1157if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
1158trace_any_any S s1 s2 ≝
1159λS,s1,s2,taaf.
1160match taaf return λs1,s2,taaf.if taaf_non_empty S s1 s2 taaf then ¬as_costed … s2 else True →
1161  trace_any_any S s1 s2 with
1162[ taaf_base s ⇒ λ_.taa_base …
1163| taaf_step s1 s2 s3 taa ex cl ⇒ λncost.
1164  taa_append_taa … taa (taa_step … ex cl ncost (taa_base …))
1165| taaf_step_jump s1 s2 s3 taa ex cl cost ⇒ λncost.Ⓧ(absurd … cost ncost)
1166].
1167
1168lemma associative_taa_append_tal : ∀S,s1,s2,fl,s3,s4.
1169  ∀taa1 : trace_any_any S s1 s2.
1170  ∀taa2 : trace_any_any S s2 s3.
1171  ∀tal : trace_any_label S fl s3 s4.
1172  (taa_append_taa … taa1 taa2) @ tal = taa1 @ taa2 @ tal.
1173#S #s1 #s2 #fl #s3 #s4 #taa1 elim taa1 -s1 -s2
1174[ #s1 #taa2 #tal %
1175| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
1176  normalize >IH %
1177]
1178qed.
1179
1180lemma associative_taa_append_taa : ∀S,s1,s2,s3,s4.
1181  ∀taa1 : trace_any_any S s1 s2.
1182  ∀taa2 : trace_any_any S s2 s3.
1183  ∀taa3 : trace_any_any S s3 s4.
1184  taa_append_taa … (taa_append_taa … taa1 taa2) taa3 =
1185  taa_append_taa … taa1 (taa_append_taa … taa2 taa3).
1186#S #s1 #s2 #s3 #s4 #taa1 elim taa1 -s1 -s2
1187[ #s1 #taa2 #tal %
1188| #s1 #s1_mid #s2 #H #I #J #tl #IH #taa2 #tal
1189  normalize >IH %
1190]
1191qed.
1192
1193definition taaf_append_tal : ∀S,st1,fl,st2,st3.
1194  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_label S fl st2 st3 →
1195  trace_any_label S fl st1 st3 ≝ λS,st1,fl,st2,st3,taaf,prf.
1196  taa_append_tal … (taaf_to_taa … prf).
1197
1198definition taaf_append_taa : ∀S,st1,st2,st3.
1199  ∀taaf.if taaf_non_empty S st1 st2 taaf then ¬as_costed S st2 else True → trace_any_any S st2 st3 →
1200  trace_any_any S st1 st3 ≝ λS,st1,st2,st3,taaf,prf.
1201  taa_append_taa … (taaf_to_taa … prf).
1202
1203definition taaf_cons : ∀S : abstract_status.∀s1,s2,s3.
1204  as_execute S s1 s2 →
1205  as_classifier … s1 cl_other →
1206  ∀taaf : trace_any_any_free S s2 s3.
1207  (if taaf_non_empty … taaf then ¬as_costed … s2 else True) →
1208  trace_any_any_free S s1 s3 ≝
1209λS,s1,s2,s3,H,I,tl.
1210match tl return λs2,s3,tl.
1211  as_execute … s1 s2 →
1212  if taaf_non_empty … tl then ¬as_costed … s2 else True →
1213  trace_any_any_free S s1 s3
1214with
1215[ taaf_base s2 ⇒ λH.λ_.taaf_step … (taa_base …) H I
1216| taaf_step s2 s3 s4 taa H' I' ⇒
1217  λH,J.taaf_step … (taa_step … H I J taa) H' I'
1218| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒
1219  λH,J.taaf_step_jump … (taa_step ???? H I J taa) H' I' K'
1220] H.
1221
1222lemma taaf_cons_non_empty : ∀S,s1,s2,s3,H,I,tl,J.
1223bool_to_Prop (taaf_non_empty … (taaf_cons S s1 s2 s3 H I tl J)).
1224#S #s1 #s2 #s3 #H #I #tl lapply H -H cases tl
1225[ #s #H * % |*: #s2 #s3 #s4 #taa #H' #I' [2: #K'] #H #J % ]
1226qed.
1227
1228definition taaf_append_taaf :
1229  ∀S,st1,st2,st3.
1230  ∀taaf1 : trace_any_any_free S st1 st2.
1231  ∀taaf2 : trace_any_any_free S st2 st3.
1232  if taaf_non_empty … taaf2 ∧ taaf_non_empty … taaf1 then ¬as_costed … st2 else True →
1233  trace_any_any_free S st1 st3 ≝
1234λS,st1,st2,st3,taaf1,taaf2.
1235match taaf2 return λst2,st3,taaf2.
1236  ∀taaf1 : trace_any_any_free S st1 st2.
1237  if taaf_non_empty … taaf2 ∧ taaf_non_empty … taaf1 then ¬as_costed … st2 else True →
1238  trace_any_any_free S st1 st3 with
1239[ taaf_base s1 ⇒ λtaaf1.λ_.taaf1
1240| taaf_step s1 s2 s3 taa H' I' ⇒ λtaaf1,prf.
1241  taaf_step … (taaf_append_taa … taaf1 ? taa) H' I'
1242| taaf_step_jump s2 s3 s4 taa H' I' K' ⇒ λtaaf1,prf.
1243  taaf_step_jump … (taaf_append_taa … taaf1 ? taa) H' I' K'
1244] taaf1. @prf qed.
Note: See TracBrowser for help on using the repository browser.