source: src/common/StructuredTraces.ma @ 1910

Last change on this file since 1910 was 1902, checked in by mulligan, 8 years ago

Reverted needless changes to StructuredTraces?

File size: 9.4 KB
Line 
1include "basics/types.ma".
2include "basics/bool.ma".
3include "basics/jmeq.ma".
4
5inductive status_class : Type[0] ≝
6| cl_return : status_class
7| cl_jump   : status_class
8| cl_call   : status_class
9| cl_other : status_class.
10
11record abstract_status : Type[1] ≝
12{
13  as_status :> Type[0];
14  as_execute : as_status → as_status → Prop;
15  as_classifier : as_status → status_class → Prop;
16  as_costed : as_status → Prop;
17  as_after_return : (Σs:as_status. as_classifier s cl_call) → as_status → Prop
18}.
19
20inductive trace_ends_with_ret: Type[0] ≝
21  | ends_with_ret: trace_ends_with_ret
22  | doesnt_end_with_ret: trace_ends_with_ret.
23
24inductive trace_label_return (S:abstract_status) : S → S → Type[0] ≝
25  | tlr_base:
26      ∀status_before: S.
27      ∀status_after: S.
28        trace_label_label S ends_with_ret status_before status_after →
29        trace_label_return S status_before status_after
30  | tlr_step:
31      ∀status_initial: S.
32      ∀status_labelled: S.
33      ∀status_final: S.
34        trace_label_label S doesnt_end_with_ret status_initial status_labelled →
35        trace_label_return S status_labelled status_final →
36          trace_label_return S status_initial status_final
37with trace_label_label: trace_ends_with_ret → S → S → Type[0] ≝
38  | tll_base:
39      ∀ends_flag: trace_ends_with_ret.
40      ∀start_status: S.
41      ∀end_status: S.
42        trace_any_label S ends_flag start_status end_status →
43        as_costed S start_status →
44          trace_label_label S ends_flag start_status end_status
45with trace_any_label: trace_ends_with_ret → S → S → Type[0] ≝
46  (* Single steps within a function which reach a label.
47     Note that this is the only case applicable for a jump. *)
48  | tal_base_not_return:
49      ∀start_status: S.
50      ∀final_status: S.
51        as_execute S start_status final_status →
52        (as_classifier S start_status cl_jump ∨
53         as_classifier S start_status cl_other) →
54        as_costed S final_status →
55          trace_any_label S doesnt_end_with_ret start_status final_status
56  | tal_base_return:
57      ∀start_status: S.
58      ∀final_status: S.
59        as_execute S start_status final_status →
60        as_classifier S start_status cl_return →
61          trace_any_label S ends_with_ret start_status final_status
62  (* A call followed by a label on return. *)
63  | tal_base_call:
64      ∀status_pre_fun_call: S.
65      ∀status_start_fun_call: S.
66      ∀status_final: S.
67        as_execute S status_pre_fun_call status_start_fun_call →
68        ∀H:as_classifier S status_pre_fun_call cl_call.
69          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_final →
70          trace_label_return S status_start_fun_call status_final →
71          as_costed S status_final →
72            trace_any_label S doesnt_end_with_ret status_pre_fun_call status_final
73  (* A call followed by a non-empty trace. *)
74  | tal_step_call:
75      ∀end_flag: trace_ends_with_ret.
76      ∀status_pre_fun_call: S.
77      ∀status_start_fun_call: S.
78      ∀status_after_fun_call: S.
79      ∀status_final: S.
80        as_execute S status_pre_fun_call status_start_fun_call →
81        ∀H:as_classifier S status_pre_fun_call cl_call.
82          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
83          trace_label_return S status_start_fun_call status_after_fun_call →
84          ¬ as_costed S status_after_fun_call →
85          trace_any_label S end_flag status_after_fun_call status_final →
86            trace_any_label S end_flag status_pre_fun_call status_final
87  | tal_step_default:
88      ∀end_flag: trace_ends_with_ret.
89      ∀status_pre: S.
90      ∀status_init: S.
91      ∀status_end: S.
92        as_execute S status_pre status_init →
93        trace_any_label S end_flag status_init status_end →
94        as_classifier S status_pre cl_other →
95        ¬ (as_costed S status_init) →
96          trace_any_label S end_flag status_pre status_end.
97
98inductive trace_any_call (S:abstract_status) : S → S → Type[0] ≝
99  | tac_base:
100      ∀status: S.
101        as_classifier S status cl_call →
102          trace_any_call S status status
103  | tac_step_call:
104      ∀status_pre_fun_call: S.
105      ∀status_after_fun_call: S.
106      ∀status_final: S.
107      ∀status_start_fun_call: S.
108        as_execute S status_pre_fun_call status_start_fun_call →
109        ∀H:as_classifier S status_pre_fun_call cl_call.
110          as_after_return S (mk_Sig ?? status_pre_fun_call H) status_after_fun_call →
111          trace_label_return S status_start_fun_call status_after_fun_call →
112          ¬ as_costed S status_after_fun_call →
113          trace_any_call S status_after_fun_call status_final →
114            trace_any_call S status_pre_fun_call status_final
115  | tac_step_default:
116      ∀status_pre: S.
117      ∀status_end: S.
118      ∀status_init: S.
119        as_execute S status_pre status_init →
120        trace_any_call S status_init status_end →
121        as_classifier S status_pre cl_other →
122        ¬ (as_costed S status_init) →
123          trace_any_call S status_pre status_end.
124             
125inductive trace_label_call (S:abstract_status) : S → S → Type[0] ≝
126  | tlc_base:
127      ∀start_status: S.
128      ∀end_status: S.
129        trace_any_call S start_status end_status →
130        as_costed S start_status →
131        trace_label_call S start_status end_status
132.       
133
134coinductive trace_label_diverges (S:abstract_status) : S → Type[0] ≝
135  | tld_step:
136      ∀status_initial: S.
137      ∀status_labelled: S.
138          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
139          trace_label_diverges S status_labelled →
140            trace_label_diverges S status_initial
141  | tld_base:
142      ∀status_initial: S.
143      ∀status_pre_fun_call: S.
144      ∀status_start_fun_call: S.
145        trace_label_call S status_initial status_pre_fun_call →
146        as_execute S status_pre_fun_call status_start_fun_call →
147        ∀H:as_classifier S status_pre_fun_call cl_call.
148          trace_label_diverges S status_start_fun_call →
149            trace_label_diverges S status_initial.
150
151(* Version in Prop for showing existence. *)
152coinductive trace_label_diverges_exists (S:abstract_status) : S → Prop ≝
153  | tld_step:
154      ∀status_initial: S.
155      ∀status_labelled: S.
156          trace_label_label S doesnt_end_with_ret status_initial status_labelled →
157          trace_label_diverges_exists S status_labelled →
158            trace_label_diverges_exists S status_initial
159  | tld_base:
160      ∀status_initial: S.
161      ∀status_pre_fun_call: S.
162      ∀status_start_fun_call: S.
163        trace_label_call S status_initial status_pre_fun_call →
164        as_execute S status_pre_fun_call status_start_fun_call →
165        ∀H:as_classifier S status_pre_fun_call cl_call.
166          trace_label_diverges_exists S status_start_fun_call →
167            trace_label_diverges_exists S status_initial.
168
169record final_abstract_status : Type[1] ≝ {
170  as_as :> abstract_status;
171  as_final:as_status as_as → Prop
172}.
173
174
175inductive trace_whole_program (S:final_abstract_status) : S → Type[0] ≝
176  | twp_terminating:
177      ∀status_initial: S.
178      ∀status_start_fun: S.
179      ∀status_final: S.
180        as_classifier S status_initial cl_call →
181        as_execute S status_initial status_start_fun →
182        trace_label_return S status_start_fun status_final →
183        as_final S status_final →
184        trace_whole_program S status_initial
185  | twp_diverges:
186      ∀status_initial: S.
187      ∀status_start_fun: S.
188        as_classifier S status_initial cl_call →
189        as_execute S status_initial status_start_fun →
190        trace_label_diverges S status_start_fun →
191        trace_whole_program S status_initial.
192
193(* Again, an identical version in Prop for existence proofs. *)
194inductive trace_whole_program_exists (S:final_abstract_status) : S → Prop ≝
195  | twp_terminating:
196      ∀status_initial: S.
197      ∀status_start_fun: S.
198      ∀status_final: S.
199        as_classifier S status_initial cl_call →
200        as_execute S status_initial status_start_fun →
201        trace_label_return S status_start_fun status_final →
202        as_final S status_final →
203        trace_whole_program_exists S status_initial
204  | twp_diverges:
205      ∀status_initial: S.
206      ∀status_start_fun: S.
207        as_classifier S status_initial cl_call →
208        as_execute S status_initial status_start_fun →
209        trace_label_diverges_exists S status_start_fun →
210        trace_whole_program_exists S status_initial.
211
212
213let rec trace_any_label_label S s s' f
214  (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 ] ≝
215match tr return λf,s,s',tr. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ] with
216[ tal_base_not_return start final _ _ C ⇒ C
217| tal_base_return _ _  _ _ ⇒ I
218| tal_base_call _ _ _ _ _ _ _ C ⇒ C
219| tal_step_call f pre start after final X C RET LR C' tr' ⇒ trace_any_label_label … tr'
220| tal_step_default f pre init end X tr' C C' ⇒ trace_any_label_label … tr'
221].
222
223lemma trace_label_label_label : ∀S,s,s',f.
224  ∀tr:trace_label_label S f s s'. match f with [ doesnt_end_with_ret ⇒ as_costed S s' | ends_with_ret ⇒ True ].
225#S #s #s' #f #tr
226cases tr
227#f #start #end #tr' #C @(trace_any_label_label … tr')
228qed.
229
230lemma trace_any_call_call : ∀S,s,s'.
231  trace_any_call S s s' → as_classifier S s' cl_call.
232#S #s #s' #T elim T //
233qed.
Note: See TracBrowser for help on using the repository browser.