source: src/common/StructuredTraces.ma @ 2222

Last change on this file since 2222 was 2186, checked in by tranquil, 8 years ago

updated joint semantics

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