source: src/common/StructuredTraces.ma @ 2398

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