source: src/common/StructuredTraces.ma @ 1901

Last change on this file since 1901 was 1901, checked in by mulligan, 9 years ago

Slight changes to StructuredTraces?: should not change too much

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