source: src/common/StructuredTraces.ma @ 3367

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