source: src/common/StructuredTraces.ma @ 1938

Last change on this file since 1938 was 1938, checked in by sacerdot, 8 years ago

Definitions moved to the right places, now everything compiles again.

File size: 19.6 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 : as_status → 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
27(* temporary alias for backward compatibility *)
28definition final_abstract_status ≝ abstract_status.
29
30definition as_costed : ∀a_s : abstract_status.a_s → Prop ≝
31  λa_s,st.as_label ? st ≠ None ?.
32
33definition as_label_safe : ∀a_s : abstract_status.
34  (Σs : a_s.as_costed ? s) → costlabel ≝
35  λa_s,st_sig.opt_safe … (pi2 … st_sig).
36
37inductive trace_ends_with_ret: Type[0] ≝
38  | ends_with_ret: trace_ends_with_ret
39  | doesnt_end_with_ret: trace_ends_with_ret.
40
41inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
42  | tlr_base:
43      ∀status_before: S.
44      ∀status_after: S.
45        trace_label_label S ends_with_ret status_before status_after →
46        trace_label_return S status_before status_after
47  | tlr_step:
48      ∀status_initial: S.
49      ∀status_labelled: S.
50      ∀status_final: S.
51        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
52        trace_label_return S status_labelled status_final →
53          trace_label_return S status_initial status_final
54with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
55  | tll_base:
56      ∀ends_flag: trace_ends_with_ret.
57      ∀start_status: S.
58      ∀end_status: S.
59        trace_any_label S ends_flag start_status end_status →
60        as_costed S start_status →
61          trace_label_label S ends_flag start_status end_status
62with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
63  (* Single steps within a function which reach a label.
64     Note that this is the only case applicable for a jump. *)
65  | tal_base_not_return:
66      ∀start_status: S.
67      ∀final_status: S.
68        as_execute S start_status final_status →
69        (as_classifier S start_status cl_jump ∨
70         as_classifier S start_status cl_other) →
71        as_costed S final_status →
72          trace_any_label S doesnt_end_with_ret start_status final_status
73  | tal_base_return:
74      ∀start_status: S.
75      ∀final_status: S.
76        as_execute S start_status final_status →
77        as_classifier S start_status cl_return →
78          trace_any_label S ends_with_ret start_status final_status
79  (* A call followed by a label on return. *)
80  | tal_base_call:
81      ∀status_pre_fun_call: S.
82      ∀status_start_fun_call: S.
83      ∀status_final: S.
84        as_execute S status_pre_fun_call status_start_fun_call →
85        ∀H:as_classifier S status_pre_fun_call cl_call.
86          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
87          trace_label_return S status_start_fun_call status_final →
88          as_costed S status_final →
89            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
90  (* A call followed by a non-empty trace. *)
91  | tal_step_call:
92      ∀end_flag: trace_ends_with_ret.
93      ∀status_pre_fun_call: S.
94      ∀status_start_fun_call: S.
95      ∀status_after_fun_call: S.
96      ∀status_final: S.
97        as_execute S status_pre_fun_call status_start_fun_call →
98        ∀H:as_classifier S status_pre_fun_call cl_call.
99          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
100          trace_label_return S status_start_fun_call status_after_fun_call →
101          ¬ as_costed S status_after_fun_call →
102          trace_any_label S end_flag status_after_fun_call status_final →
103            trace_any_label S end_flag status_pre_fun_call status_final
104  | tal_step_default:
105      ∀end_flag: trace_ends_with_ret.
106      ∀status_pre: S.
107      ∀status_init: S.
108      ∀status_end: S.
109        as_execute S status_pre status_init →
110        trace_any_label S end_flag status_init status_end →
111        as_classifier S status_pre cl_other →
112        ¬ (as_costed S status_init) →
113          trace_any_label S end_flag status_pre status_end.
114
115let rec tal_pc_list (S : abstract_status) fl st1 st2 (tal : trace_any_label S fl st1 st2)
116  on tal : list (as_pc S) ≝
117 match tal with
118 [ tal_step_call fl' pre _ st1' st2' _ _ _ _ _ tl ⇒ as_pc_of … pre :: tal_pc_list … tl
119 | tal_step_default fl' pre st1' st2' _ tl _ _ ⇒  as_pc_of … pre :: tal_pc_list … tl
120 | tal_base_not_return pre _ _ _ _ ⇒ [as_pc_of … pre]
121 | tal_base_return pre _ _ _ ⇒ [as_pc_of … pre]
122 | tal_base_call pre _ _ _ _ _ _ _ ⇒ [as_pc_of … pre]
123 ].
124
125definition as_trace_any_label_length':
126    ∀S: abstract_status.
127    ∀trace_ends_flag: trace_ends_with_ret.
128    ∀start_status: S.
129    ∀final_status: S.
130    ∀the_trace: trace_any_label S trace_ends_flag start_status final_status.
131      nat ≝
132  λS: abstract_status.
133  λtrace_ends_flag: trace_ends_with_ret.
134  λstart_status: S.
135  λfinal_status: S.
136  λthe_trace: trace_any_label S trace_ends_flag start_status final_status.
137    |tal_pc_list … the_trace|.
138
139let rec tlr_unrepeating S st1 st2 (tlr : trace_label_return S st1 st2) on tlr : Prop ≝
140  match tlr with
141  [ tlr_base st1 st2 tll ⇒ tll_unrepeating … tll
142  | tlr_step st1 st2 st3 tll tl ⇒ tll_unrepeating … tll ∧ tlr_unrepeating … tl
143  ]
144and tll_unrepeating S fl st1 st2 (tll : trace_label_label S fl st1 st2) on tll : Prop ≝
145  match tll with
146  [ tll_base fl st1 st2 tal _ ⇒ tal_unrepeating … tal
147  ]
148and tal_unrepeating S fl st1 st2 (tal : trace_any_label S fl st1 st2) on tal : Prop ≝
149  match tal with
150  [ tal_step_call fl st1 st2 st3 st4 _ _ _ tlr _ tl ⇒
151    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
152    tal_unrepeating … tl ∧
153    tlr_unrepeating … tlr
154  | tal_step_default fl st1 st2 st3 _ tl _ _ ⇒
155    bool_to_Prop (notb (memb ? (as_pc_of … st1) (tal_pc_list … tl))) ∧
156    tal_unrepeating … tl
157  | tal_base_call pre _ _ _ _ _ trace _ ⇒ tlr_unrepeating … trace
158  | _ ⇒ True
159  ].
160
161definition tll_hd_label : ∀S : abstract_status.∀fl,st1,st2.
162  trace_label_label S fl st1 st2 → costlabel ≝
163  λS,fl,st1,st2,tr.match tr with
164  [ tll_base _ st1' _ _ prf ⇒ as_label_safe … «st1', prf» ].
165
166definition tlr_hd_label : ∀S : abstract_status.∀st1,st2.
167  trace_label_return S st1 st2 → costlabel ≝
168  λS,st1,st2,tr.match tr with
169  [ tlr_base st1' st2' tll ⇒ tll_hd_label … tll
170  | tlr_step st1' st2' _ tll _ ⇒ tll_hd_label … tll
171  ].
172
173let rec tal_unrepeating_uniqueb S fl st1 st2 tal on tal :
174  tal_unrepeating S fl st1 st2 tal → bool_to_Prop (uniqueb … (tal_pc_list … tal)) ≝ ?.
175cases tal //
176#fl' #st1' [#st_fun] #st2' #st3' #H
177[ #H0 #H1 #tlr #G #tal | #tal #H0 #G ] whd in ⊢ (% → ?%); [*]*
178#A #B [#_] >A normalize nodelta @tal_unrepeating_uniqueb assumption
179qed.
180
181inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
182  | tac_base:
183      ∀status: S.
184        as_classifier S status cl_call →
185          trace_any_call S status status
186  | tac_step_call:
187      ∀status_pre_fun_call: S.
188      ∀status_after_fun_call: S.
189      ∀status_final: S.
190      ∀status_start_fun_call: S.
191        as_execute S status_pre_fun_call status_start_fun_call →
192        ∀H:as_classifier S status_pre_fun_call cl_call.
193          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
194          trace_label_return S status_start_fun_call status_after_fun_call →
195          ¬ as_costed S status_after_fun_call →
196          trace_any_call S status_after_fun_call status_final →
197            trace_any_call S status_pre_fun_call status_final
198  | tac_step_default:
199      ∀status_pre: S.
200      ∀status_end: S.
201      ∀status_init: S.
202        as_execute S status_pre status_init →
203        trace_any_call S status_init status_end →
204        as_classifier S status_pre cl_other →
205        ¬ (as_costed S status_init) →
206          trace_any_call S status_pre status_end.
207
208             
209inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
210  | tlc_base:
211      ∀start_status: S.
212      ∀end_status: S.
213        trace_any_call S start_status end_status →
214        as_costed S start_status →
215        trace_label_call S start_status end_status
216.
217
218definition tlc_hd_label : ∀S : abstract_status.∀st1,st2.
219  trace_label_call S st1 st2 → costlabel ≝
220  λS,st1,st2,tr.match tr with
221  [ tlc_base st1' _ _ prf ⇒ as_label_safe … «st1', prf»
222  ].
223   
224coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
225  | tld_step:
226      ∀status_initial: S.
227      ∀status_labelled: S.
228          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
229          trace_label_diverges S status_labelled →
230            trace_label_diverges S status_initial
231  | tld_base:
232      ∀status_initial: S.
233      ∀status_pre_fun_call: S.
234      ∀status_start_fun_call: S.
235        trace_label_call S status_initial status_pre_fun_call →
236        as_execute S status_pre_fun_call status_start_fun_call →
237        ∀H:as_classifier S status_pre_fun_call cl_call.
238          trace_label_diverges S status_start_fun_call →
239            trace_label_diverges S status_initial.
240
241definition tld_hd_label : ∀S : abstract_status.∀st.
242  trace_label_diverges S st → costlabel ≝
243  λS,st,tr.match tr with
244  [ tld_step st' st'' tll _ ⇒ tll_hd_label … tll
245  | tld_base st' st'' _ tlc _ _ _ ⇒ tlc_hd_label … tlc
246  ].       
247
248(* Version in Prop for showing existence. *)
249coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
250  | tld_step:
251      ∀status_initial: S.
252      ∀status_labelled: S.
253          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
254          trace_label_diverges_exists S status_labelled →
255            trace_label_diverges_exists S status_initial
256  | tld_base:
257      ∀status_initial: S.
258      ∀status_pre_fun_call: S.
259      ∀status_start_fun_call: S.
260        trace_label_call S status_initial status_pre_fun_call →
261        as_execute S status_pre_fun_call status_start_fun_call →
262        ∀H:as_classifier S status_pre_fun_call cl_call.
263          trace_label_diverges_exists S status_start_fun_call →
264            trace_label_diverges_exists S status_initial.
265
266inductive trace_whole_program (S: abstract_status) : S → Type[0] ≝
267  | twp_terminating:
268      ∀status_initial: S.
269      ∀status_start_fun: S.
270      ∀status_final: S.
271        as_classifier S status_initial cl_call →
272        as_execute S status_initial status_start_fun →
273        trace_label_return S status_start_fun status_final →
274        as_final S status_final →
275        trace_whole_program S status_initial
276  | twp_diverges:
277      ∀status_initial: S.
278      ∀status_start_fun: S.
279        as_classifier S status_initial cl_call →
280        as_execute S status_initial status_start_fun →
281        trace_label_diverges S status_start_fun →
282        trace_whole_program S status_initial.
283
284(* Again, an identical version in Prop for existence proofs. *)
285inductive trace_whole_program_exists (S: abstract_status) : S → Prop ≝
286  | twp_terminating:
287      ∀status_initial: S.
288      ∀status_start_fun: S.
289      ∀status_final: S.
290        as_classifier S status_initial cl_call →
291        as_execute S status_initial status_start_fun →
292        trace_label_return S status_start_fun status_final →
293        as_final S status_final →
294        trace_whole_program_exists S status_initial
295  | twp_diverges:
296      ∀status_initial: S.
297      ∀status_start_fun: S.
298        as_classifier S status_initial cl_call →
299        as_execute S status_initial status_start_fun →
300        trace_label_diverges_exists S status_start_fun →
301        trace_whole_program_exists S status_initial.
302
303
304let rec trace_any_label_label S s s' f
305  (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 ] ≝
306match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
307[ tal_base_not_return start final _ _ C ⇒ C
308| tal_base_return _ _  _ _ ⇒ I
309| tal_base_call _ _ _ _ _ _ _ C ⇒ C
310| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
311| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
312].
313
314definition tal_tl_label : ∀S : abstract_status.∀st1,st2.
315  trace_any_label S doesnt_end_with_ret st1 st2 → costlabel ≝
316  λS,st1,st2,tr.as_label_safe … «st2, trace_any_label_label … tr».
317
318lemma trace_label_label_label : ∀S,s,s',f.
319  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
320#S #s #s' #f #tr
321cases tr
322#f #start #end #tr' #C @(trace_any_label_label … tr')
323qed.
324
325definition tll_tl_label : ∀S : abstract_status.∀st1,st2.
326  trace_label_label S doesnt_end_with_ret st1 st2 → costlabel ≝
327  λS,st1,st2,tr.as_label_safe … «st2, trace_label_label_label … tr».
328
329lemma trace_any_call_call : ∀S,s,s'.
330  trace_any_call S s s' → as_classifier S s' cl_call.
331#S #s #s' #T elim T //
332qed.
333
334(* an uncalling, unreturning and *unjumping*,
335  as well as unlabelled (but possibly for the first and last statuses)
336  possibly empty trace segment *)
337inductive trace_any_any (S:abstract_status) : S → S → Type[0] ≝
338  | taa_base :
339      ∀start_status: S.
340        trace_any_any S start_status start_status
341  | taa_step :
342      ∀status_pre: S.
343      ∀status_init: S.
344      ∀status_end: S.
345        as_execute S status_pre status_init →
346        trace_any_any S status_init status_end →
347        as_classifier S status_pre cl_other →
348        ¬as_costed … status_init →
349          trace_any_any S status_pre status_end.
350
351let rec taa_status_list S st1 st2 (taa : trace_any_any S st1 st2) on taa : list S ≝
352  match taa with
353  [ taa_base st1' ⇒ [st1']
354  | taa_step st1' st2' st3' _ tl _ _ ⇒ st1' :: taa_status_list … tl
355  ].
356
357let rec taa_append_taa S st1 st2 st3 (taa1 : trace_any_any S st1 st2)
358  on taa1 : trace_any_any S st2 st3 → trace_any_any S st1 st3 ≝
359  match taa1
360  return λst1,st2.λx : trace_any_any S st1 st2.
361    trace_any_any S st2 st3 → trace_any_any S st1 st3
362  with
363  [ taa_base _ ⇒ λtaa2.taa2
364  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
365      taa_step … H (taa_append_taa … tl taa2) G K
366  ].
367
368let rec taa_append_tal S st1 fl st2 st3 (taa : trace_any_any S st1 st2)
369  on taa :
370  trace_any_label S fl st2 st3 →
371  trace_any_label S fl st1 st3 ≝
372  match taa
373  return λst1,st2.λx : trace_any_any S st1 st2.
374    trace_any_label S fl st2 st3 → trace_any_label S fl st1 st3
375  with
376  [ taa_base _ ⇒ λtaa2.taa2
377  | taa_step st1' st2' st3' H tl G K ⇒ λtaa2.
378      tal_step_default … H (taa_append_tal … tl taa2) G K
379  ].
380
381let rec tlr_rel S1 st1 st1' S2 st2 st2'
382  (tlr1 : trace_label_return S1 st1 st1')
383  (tlr2 : trace_label_return S2 st2 st2') on tlr1 : Prop ≝
384match tlr1 with
385  [ tlr_base st1 st1' tll1 ⇒
386    match tlr2 with
387    [ tlr_base st2 st2' tll2 ⇒ tll_rel … tll1 tll2
388    | _ ⇒ False
389    ]
390  | tlr_step st1 st1' st1'' tll1 tl1 ⇒
391    match tlr2 with
392    [ tlr_step st2 st2' st2'' tll2 tl2 ⇒
393      tll_rel … tll1 tll2 ∧ tlr_rel … tl1 tl2
394    | _ ⇒ False
395    ]
396  ]
397and tll_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
398 (tll1 : trace_label_label S1 fl1 st1 st1')
399 (tll2 : trace_label_label S2 fl2 st2 st2') on tll1 : Prop ≝
400  match tll1 with
401  [ tll_base fl1 st1 st1' tal1 H ⇒
402    match tll2 with
403    [ tll_base fl2 st2 st2 tal2 G ⇒
404      as_label_safe … («?, H») = as_label_safe … («?, G») ∧
405      tal_rel … tal1 tal2
406    ]
407  ]
408and tal_rel S1 fl1 st1 st1' S2 fl2 st2 st2'
409 (tal1 : trace_any_label S1 fl1 st1 st1')
410 (tal2 : trace_any_label S2 fl2 st2 st2')
411   on tal1 : Prop ≝
412  match tal1 with
413  [ tal_base_not_return st1 st1' _ _ _ ⇒
414    ∃st2mid,taa,H,G,K.
415    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
416      (tal_base_not_return ? st2mid st2' H G K)
417  | tal_base_return st1 st1' _ _ ⇒
418    ∃st2mid,taa,H,G.
419    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
420      (tal_base_return ? st2mid st2' H G)
421  | tal_base_call st1 st1' st1'' _ _ _ tlr1 _ ⇒
422    ∃st2mid,taa,st2mid',H,G,K,tlr2,L.
423    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
424      (tal_base_call ? st2mid st2mid' st2' H G K tlr2 L) ∧
425      tlr_rel … tlr1 tlr2
426  | tal_step_call fl1 st1 st1' st1'' st1''' _ _ _ tlr1 _ tl1 ⇒
427    ∃st2mid,taa,st2_fun,st2_after_fun,H,G,K,tlr2,L,tl2.
428    tal2 ≃ taa_append_tal ? st2 ? st2mid st2' taa
429      (tal_step_call ?? st2mid st2_fun st2_after_fun st2' H G K tlr2 L tl2) ∧
430      tlr_rel … tlr1 tlr2 ∧ tal_rel … tl1 tl2
431  | tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒
432    tal_rel … tl1 tal2 (* <- this makes it many to many *)
433  ].
434
435let rec as_compute_cost_trace_label_label
436  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
437    (start_status: S) (final_status: S)
438      (the_trace: trace_label_label S trace_ends_flag start_status final_status)
439        on the_trace: list (Σl: costlabel. ∃s. as_label S s = Some … l) ≝
440  match the_trace with
441  [ tll_base ends_flag initial final given_trace labelled_proof ⇒
442      let label ≝
443        match as_label … initial return λx: option costlabel. x ≠ None costlabel → ? with
444        [ None ⇒ λabs. ⊥
445        | Some l ⇒ λ_. l
446        ] labelled_proof
447      in
448        (mk_Sig … label ?)::as_compute_cost_trace_any_label S ends_flag initial final given_trace
449  ]
450and as_compute_cost_trace_any_label
451  (S: abstract_status) (trace_ends_flag: trace_ends_with_ret)
452    (start_status: S) (final_status: S)
453      (the_trace: trace_any_label S trace_ends_flag start_status final_status)
454        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
455  match the_trace with
456  [ tal_base_not_return the_status _ _ _ _ ⇒ [ ]
457  | tal_base_call pre_fun_call start_fun_call final _ _ _ call_trace _ ⇒
458      as_compute_cost_trace_label_return … call_trace
459  | tal_base_return the_status _ _ _ ⇒ [ ]
460  | tal_step_call end_flag pre_fun_call start_fun_call after_fun_call final
461    _ _ _ call_trace _ final_trace ⇒
462    let call_cost_trace ≝ as_compute_cost_trace_label_return … call_trace in
463    let final_cost_trace ≝ as_compute_cost_trace_any_label … end_flag … final_trace in
464        call_cost_trace @ final_cost_trace
465  | tal_step_default end_flag status_pre status_init status_end _ tail_trace _ _ ⇒
466      as_compute_cost_trace_any_label … tail_trace
467  ]
468and as_compute_cost_trace_label_return
469  (S: abstract_status)
470    (start_status: S) (final_status: S)
471      (the_trace: trace_label_return S start_status final_status)
472        on the_trace: list (Σl: costlabel. ∃s. as_label … s = Some … l) ≝
473  match the_trace with
474  [ tlr_base before after trace_to_lift ⇒
475      as_compute_cost_trace_label_label … trace_to_lift
476  | tlr_step initial labelled final labelled_trace ret_trace ⇒
477    let labelled_cost ≝ as_compute_cost_trace_label_label … doesnt_end_with_ret … labelled_trace in
478    let return_cost ≝ as_compute_cost_trace_label_return … ret_trace in
479        labelled_cost @ return_cost
480  ].
481  [2:
482    cases abs -abs #abs @abs %
483  |1:
484    %{initial} whd in match label;
485    generalize in match labelled_proof; whd in ⊢ (% → ?);
486    cases (as_label S initial)
487    [1:
488      #absurd @⊥ cases absurd -absurd #absurd @absurd %
489    |2:
490      #costlabel normalize nodelta #_ %
491    ]
492  ]
493qed.
Note: See TracBrowser for help on using the repository browser.