source: src/common/StructuredTraces.ma @ 1544

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

StructuredTraces? inhabited for object code.

File size: 5.1 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3
4inductive status_class : Type[0] ≝
5| cl_return : status_class
6| cl_jump   : status_class
7| cl_call   : status_class
8| cl_other : status_class
9.
10
11record abstract_status : Type[1] ≝ {
12  as_status :> Type[0];
13  as_execute : as_status → as_status → Prop;
14  as_classifier : as_status → status_class → Prop;
15  as_costed : as_status → Prop;
16  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
17}.
18
19inductive trace_ends_with_ret: Type[0] ≝
20  | ends_with_ret: trace_ends_with_ret
21  | doesnt_end_with_ret: trace_ends_with_ret.
22
23inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
24  | tlr_base:
25      ∀status_before: S.
26      ∀status_after: S.
27        trace_label_label S ends_with_ret status_before status_after →
28        trace_label_return S status_before status_after
29  | tlr_step:
30      ∀status_initial: S.
31      ∀status_labelled: S.
32      ∀status_final: S.
33        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
34        trace_label_return S status_labelled status_final →
35          trace_label_return S status_initial status_final
36with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
37  | tll_base:
38      ∀ends_flag: trace_ends_with_ret.
39      ∀start_status: S.
40      ∀end_status: S.
41        trace_any_label S ends_flag start_status end_status →
42        as_costed S start_status →
43          trace_label_label S ends_flag start_status end_status
44with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
45  | tal_base_not_return:
46      ∀start_status: S.
47      ∀final_status: S.
48        as_execute S start_status final_status →
49        ¬ as_classifier S start_status cl_return →
50        as_costed S final_status →
51          trace_any_label S doesnt_end_with_ret start_status final_status
52  | tal_base_return:
53      ∀start_status: S.
54      ∀final_status: S.
55        as_execute S start_status final_status →
56        as_classifier S start_status cl_return →
57          trace_any_label S ends_with_ret start_status final_status
58  | tal_step_call:
59      ∀end_flag: trace_ends_with_ret.
60      ∀status_pre_fun_call: S.
61      ∀status_start_fun_call: S.
62      ∀status_after_fun_call: S.
63      ∀status_final: S.
64        as_execute S status_pre_fun_call status_start_fun_call →
65        ∀H:as_classifier S status_pre_fun_call cl_call.
66          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call →
67          trace_label_return S status_start_fun_call status_after_fun_call →
68          trace_any_label S end_flag status_after_fun_call status_final →
69            trace_any_label S end_flag status_pre_fun_call status_final
70  | tal_step_default:
71      ∀end_flag: trace_ends_with_ret.
72      ∀status_pre: S.
73      ∀status_init: S.
74      ∀status_end: S.
75        as_execute S status_pre status_init →
76        trace_any_label S end_flag status_init status_end →
77        as_classifier S status_pre cl_other →
78        ¬ (as_costed S status_pre) →
79          trace_any_label S end_flag status_pre status_end.
80
81
82coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
83  | tld_step:
84      ∀status_initial: S.
85      ∀status_labelled: S.
86          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
87          trace_label_diverges S status_labelled →
88            trace_label_diverges S status_initial
89  | tld_base:
90      ∀status_initial: S.
91      ∀status_pre_fun_call: S.
92      ∀status_after_fun_call: S.
93      ∀status_start_fun_call: S.
94        trace_label_call S status_initial status_pre_fun_call →
95        as_execute S status_pre_fun_call status_start_fun_call →
96        ∀H:as_classifier S status_pre_fun_call cl_call.
97          trace_label_diverges S status_start_fun_call →
98            trace_label_diverges S status_initial
99             
100with trace_label_call: S → S → Type[0] ≝
101  | tlc_base:
102      ∀start_status: S.
103      ∀end_status: S.
104        trace_any_call S start_status end_status →
105        as_costed S start_status →
106        trace_label_call S start_status end_status
107       
108with trace_any_call: S → S → Type[0] ≝
109  | tac_base:
110      ∀status: S.
111        as_classifier S status cl_call →
112          trace_any_call S status status
113  | tac_step_call:
114      ∀status_pre_fun_call: S.
115      ∀status_after_fun_call: S.
116      ∀status_final: S.
117      ∀status_start_fun_call: S.
118        as_execute S status_pre_fun_call status_start_fun_call →
119        ∀H:as_classifier S status_pre_fun_call cl_call.
120          as_after_return S (dp ?? status_pre_fun_call H) status_after_fun_call →
121          trace_label_return S status_start_fun_call status_after_fun_call →
122          trace_any_call S status_after_fun_call status_final →
123            trace_any_call S status_pre_fun_call status_final
124  | tac_step_default:
125      ∀status_pre: S.
126      ∀status_end: S.
127      ∀status_init: S.
128        as_execute S status_pre status_init →
129        trace_any_call S status_init status_end →
130        as_classifier S status_pre cl_other →
131        ¬ (as_costed S status_pre) →
132          trace_any_call S status_pre status_end.
Note: See TracBrowser for help on using the repository browser.