source: src/common/StructuredTraces.ma @ 2755

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