1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "arithmetics/nat.ma". |
---|
16 | include "basics/types.ma". |
---|
17 | include "basics/deqsets.ma". |
---|
18 | include "../src/ASM/Util.ma". |
---|
19 | |
---|
20 | inductive FunctionName : Type[0] ≝ |
---|
21 | | a_function_id : ℕ → FunctionName. |
---|
22 | |
---|
23 | inductive CallCostLabel : Type[0] ≝ |
---|
24 | | a_call_label : ℕ → CallCostLabel. |
---|
25 | |
---|
26 | inductive ReturnPostCostLabel : Type[0] ≝ |
---|
27 | | a_return_cost_label : ℕ → ReturnPostCostLabel. |
---|
28 | |
---|
29 | inductive NonFunctionalLabel : Type[0] ≝ |
---|
30 | | a_non_functional_label : ℕ → NonFunctionalLabel. |
---|
31 | |
---|
32 | inductive CostLabel : Type[0] ≝ |
---|
33 | | a_call : CallCostLabel → CostLabel |
---|
34 | | a_return_post : ReturnPostCostLabel → CostLabel |
---|
35 | | a_non_functional_label : NonFunctionalLabel → CostLabel. |
---|
36 | |
---|
37 | coercion a_call. |
---|
38 | coercion a_return_post. |
---|
39 | coercion a_non_functional_label. |
---|
40 | |
---|
41 | definition ret_act_label_to_cost_label : |
---|
42 | (ReturnPostCostLabel + NonFunctionalLabel) → CostLabel ≝ |
---|
43 | λx.match x with [inl a ⇒ a_return_post a | inr b ⇒ a_non_functional_label b]. |
---|
44 | |
---|
45 | coercion ret_act_label_to_cost_label. |
---|
46 | |
---|
47 | definition call_act_label_to_cost_label : |
---|
48 | (CallCostLabel + NonFunctionalLabel) → CostLabel ≝ |
---|
49 | λx.match x with [inl a ⇒ a_call a | inr b ⇒ a_non_functional_label b]. |
---|
50 | |
---|
51 | coercion call_act_label_to_cost_label. |
---|
52 | |
---|
53 | inductive ActionLabel : Type[0] ≝ |
---|
54 | | call_act : FunctionName → (CallCostLabel + NonFunctionalLabel) → ActionLabel |
---|
55 | | ret_act : option(ReturnPostCostLabel + NonFunctionalLabel) → ActionLabel |
---|
56 | | cost_act : option NonFunctionalLabel → ActionLabel |
---|
57 | | init_act : ActionLabel. |
---|
58 | |
---|
59 | definition is_cost_label : ActionLabel → Prop ≝ |
---|
60 | λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ]. |
---|
61 | |
---|
62 | inductive status_class : Type[0] ≝ |
---|
63 | | cl_jump : status_class |
---|
64 | | cl_io : status_class |
---|
65 | | cl_other : status_class. |
---|
66 | |
---|
67 | record abstract_status : Type[2] ≝ |
---|
68 | { as_status :> Type[0] |
---|
69 | ; as_execute : ActionLabel → relation as_status |
---|
70 | ; as_syntactical_succ : relation as_status |
---|
71 | ; as_classify : as_status → status_class |
---|
72 | ; is_call_post_label : as_status → bool |
---|
73 | ; as_initial : as_status → bool |
---|
74 | ; as_final : as_status → bool |
---|
75 | ; is_io_entering : NonFunctionalLabel → bool |
---|
76 | ; is_io_exiting : NonFunctionalLabel → bool |
---|
77 | }. |
---|
78 | |
---|
79 | definition is_act_io_entering : abstract_status → ActionLabel → bool ≝ |
---|
80 | λS,l.match l with |
---|
81 | [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_entering S c' ] |
---|
82 | | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false |
---|
83 | | inr c' ⇒ is_io_entering S c'] |
---|
84 | | None ⇒ false |
---|
85 | ] |
---|
86 | | cost_act x ⇒ match x with [ Some c ⇒ is_io_entering S c | None ⇒ false ] |
---|
87 | | init_act ⇒ false |
---|
88 | ]. |
---|
89 | |
---|
90 | definition is_act_io_exiting : abstract_status → ActionLabel → bool ≝ |
---|
91 | λS,l.match l with |
---|
92 | [ call_act f c ⇒ match c with [ inl _ ⇒ false | inr c' ⇒ is_io_exiting S c' ] |
---|
93 | | ret_act x ⇒ match x with [ Some c ⇒ match c with [inl _ ⇒ false |
---|
94 | | inr c' ⇒ is_io_exiting S c'] |
---|
95 | | None ⇒ false |
---|
96 | ] |
---|
97 | | cost_act x ⇒ match x with [ Some c ⇒ is_io_exiting S c | None ⇒ false ] |
---|
98 | | init_act ⇒ false |
---|
99 | ]. |
---|
100 | |
---|
101 | |
---|
102 | inductive raw_trace (S : abstract_status) : S → S → Type[0] ≝ |
---|
103 | | t_base : ∀st : S.raw_trace S st st |
---|
104 | | t_ind : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
105 | as_execute S l st1 st2 → raw_trace S st2 st3 → |
---|
106 | raw_trace S st1 st3. |
---|
107 | |
---|
108 | definition is_cost_act : ActionLabel → Prop ≝ |
---|
109 | λact.∃l.act = cost_act l. |
---|
110 | |
---|
111 | definition is_call_act : ActionLabel → Prop ≝ |
---|
112 | λact.∃f,l.act = call_act f l. |
---|
113 | |
---|
114 | definition is_labelled_ret_act : ActionLabel → Prop ≝ |
---|
115 | λact.∃l.act = ret_act (Some ? l). |
---|
116 | |
---|
117 | definition is_unlabelled_ret_act : ActionLabel → Prop ≝ |
---|
118 | λact.act = ret_act (None ?). |
---|
119 | |
---|
120 | definition is_non_silent_cost_act : ActionLabel → Prop ≝ |
---|
121 | λact. ∃l. act = cost_act (Some ? l). |
---|
122 | |
---|
123 | definition is_costlabelled_act : ActionLabel → Prop ≝ |
---|
124 | λact.match act with [ call_act _ _ ⇒ True |
---|
125 | | ret_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] |
---|
126 | | cost_act x ⇒ match x with [ Some _ ⇒ True | None ⇒ False ] |
---|
127 | | init_act ⇒ False |
---|
128 | ]. |
---|
129 | |
---|
130 | inductive well_formed_trace (S : abstract_status) : |
---|
131 | ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ |
---|
132 | | wf_empty : ∀st: S.well_formed_trace … (t_base S st) |
---|
133 | | wf_cons_no_jump : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
134 | ∀prf: as_execute S l st1 st2.∀ tl: raw_trace S st2 st3. |
---|
135 | well_formed_trace … tl → as_classify … st1 ≠ cl_jump → |
---|
136 | well_formed_trace … (t_ind … prf … tl) |
---|
137 | | wf_cons_jump : ∀st1,st2,st3 : S.∀ l : ActionLabel. |
---|
138 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
---|
139 | well_formed_trace … tl → is_non_silent_cost_act l → |
---|
140 | well_formed_trace … (t_ind … prf … tl). |
---|
141 | (* | wf_cons_io : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
142 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
---|
143 | well_formed_trace … tl → as_classify … st1 = cl_io → |
---|
144 | is_non_silent_cost_act l → well_formed_trace … (t_ind … prf … tl).*) |
---|
145 | |
---|
146 | lemma well_formed_trace_inv : |
---|
147 | ∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2. |
---|
148 | well_formed_trace … t → |
---|
149 | (st1 = st2 ∧ t ≃ t_base S st1) ∨ |
---|
150 | (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2. |
---|
151 | well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧ |
---|
152 | t ≃ t_ind … prf … tl) ∨ |
---|
153 | (∃st1'.∃l.∃ prf : as_execute S l st1 st1'.∃ tl : raw_trace S st1' st2. |
---|
154 | well_formed_trace … tl ∧ is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl). (* ∨ |
---|
155 | (∃st1'.∃l.∃prf : as_execute S l st1 st1'.∃tl : raw_trace S st1' st2. |
---|
156 | well_formed_trace … tl ∧ as_classify … st1 = cl_io ∧ |
---|
157 | is_non_silent_cost_act l ∧ t ≃ t_ind … prf … tl).*) |
---|
158 | #S #st1 #st2 #t #H inversion H |
---|
159 | [ #st #EQ1 #EQ2 destruct(EQ1 EQ2) #EQ destruct(EQ) #_ /5 by refl_jmeq, or_introl, conj/ |
---|
160 | | #st1' #st2' #st3' #l #prf' #tl' #Htl #Hclass #_ #EQ2 #EQ3 #EQ4 destruct #_ |
---|
161 | % %2 %{st2'} %{l} %{prf'} %{tl'} /4 by conj/ |
---|
162 | | #st1' #st2' #st3' #l #prf #tl #Htl #Hl #_ #EQ2 #EQ3 #EQ4 destruct #_ %2 %{st2'} |
---|
163 | %{l} %{prf} %{tl} % // % // |
---|
164 | (*| #st1' #st2' #st3' #l #prf #tl #Htl #Hclass #is_non_silent #_ #EQ1 #EQ2 #EQ3 |
---|
165 | destruct #_ %2 %{st2'} %{l} %{prf} %{tl} /5 by conj/ *) |
---|
166 | ] |
---|
167 | qed. |
---|
168 | |
---|
169 | |
---|
170 | let rec append_on_trace (S : abstract_status) (st1 : S) (st2 : S) (st3 : S) |
---|
171 | (t1 : raw_trace S st1 st2) on t1 : raw_trace S st2 st3 → raw_trace S st1 st3 ≝ |
---|
172 | match t1 |
---|
173 | return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3 |
---|
174 | with |
---|
175 | [ t_base st ⇒ λt2.t2 |
---|
176 | | t_ind st1' st2' st3' l prf tl ⇒ λt2.t_ind … prf … (append_on_trace … tl t2) |
---|
177 | ]. |
---|
178 | |
---|
179 | interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2). |
---|
180 | |
---|
181 | lemma append_associative : ∀S,st1,st2,st3,st4. |
---|
182 | ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. |
---|
183 | ∀t3 : raw_trace S st3 st4.(t1 @ t2) @ t3 = t1 @ (t2 @ t3). |
---|
184 | #S #st1 #st2 #st3 #st4 #t1 elim t1 -t1 |
---|
185 | [ #st #t2 #t3 %] #st1' #st2' #st3' #l #prf #tl #IH #t2 #t3 whd in ⊢ (??%%); >IH % |
---|
186 | qed. |
---|
187 | |
---|
188 | definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 → |
---|
189 | raw_trace … st1 st3 → Prop≝ |
---|
190 | λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3. |
---|
191 | |
---|
192 | definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 → |
---|
193 | raw_trace … st1 st3 → Prop≝ |
---|
194 | λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1. |
---|
195 | |
---|
196 | inductive pre_silent_trace (S : abstract_status) : |
---|
197 | ∀st1,st2 : S.raw_trace S st1 st2 → Prop ≝ |
---|
198 | | silent_empty : ∀st : S.pre_silent_trace … (t_base S st) |
---|
199 | | silent_cons : ∀st1,st2,st3 : S.∀prf : as_execute S (cost_act (None ?)) st1 st2. |
---|
200 | ∀tl : raw_trace S st2 st3. as_classify … st2 ≠ cl_io → pre_silent_trace … tl → |
---|
201 | pre_silent_trace … (t_ind … prf … tl). |
---|
202 | |
---|
203 | lemma silent_io : ∀S : abstract_status. |
---|
204 | ∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io → |
---|
205 | as_classify … s2 ≠ cl_io. |
---|
206 | #S #s1 #s2 #t elim t [ #st #_ #Hclass @Hclass] |
---|
207 | #st1 #st2 #st3 #l #prf #tl #IH #H inversion H |
---|
208 | [ #st' #EQ1 #EQ2 destruct #EQ destruct] |
---|
209 | #st1' #st2' #st3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 destruct |
---|
210 | #EQ destruct #_ #Hclass' @IH [ assumption ] assumption |
---|
211 | qed. |
---|
212 | |
---|
213 | definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2. |
---|
214 | raw_trace S st1 st2 → bool ≝ |
---|
215 | λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ]. |
---|
216 | |
---|
217 | definition silent_trace : ∀S : abstract_status.∀st1,st2 : S. |
---|
218 | raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧ |
---|
219 | (is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧ |
---|
220 | well_formed_trace … t. |
---|
221 | |
---|
222 | lemma silent_is_well_formed : ∀S : abstract_status.∀st1,st2 : S. |
---|
223 | ∀t : raw_trace S st1 st2. silent_trace … t → well_formed_trace … t. |
---|
224 | #S #st1 #st2 #t * // |
---|
225 | qed. |
---|
226 | (* elim t -t |
---|
227 | [ #st #_ %] |
---|
228 | #st1' #st2' #st3' #l #prf #tl #IH * #H #cl %2 |
---|
229 | [2: >cl % #EQ destruct] |
---|
230 | @IH inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct] |
---|
231 | #st1'' #st2'' #st3'' #prf' #tl' #H1 #Htl' #_ #EQ1 #EQ2 #EQ3 destruct #_ |
---|
232 | % [ assumption | #_ assumption] |
---|
233 | qed.*) |
---|
234 | |
---|
235 | inductive pre_measurable_trace (S : abstract_status) : |
---|
236 | ∀st1,st2 : S.raw_trace ? st1 st2 → Prop ≝ |
---|
237 | | pm_empty : ∀st : S. as_classify … st ≠ cl_io → pre_measurable_trace … (t_base ? st) |
---|
238 | | pm_cons_cost_act : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
239 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
---|
240 | as_classify … st1 ≠ cl_io → is_cost_act l → pre_measurable_trace … tl → |
---|
241 | pre_measurable_trace … (t_ind … prf … tl) |
---|
242 | | pm_cons_lab_ret : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
243 | as_classify … st1 ≠ cl_io → |
---|
244 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
---|
245 | is_labelled_ret_act l → pre_measurable_trace … tl → |
---|
246 | pre_measurable_trace … (t_ind … prf … tl) |
---|
247 | | pm_cons_post_call : ∀st1,st2,st3 : S.∀l : ActionLabel. |
---|
248 | ∀prf : as_execute S l st1 st2.∀tl : raw_trace S st2 st3. |
---|
249 | as_classify … st1 ≠ cl_io → is_call_act l → is_call_post_label … st1 → |
---|
250 | pre_measurable_trace … tl → |
---|
251 | pre_measurable_trace … (t_ind … prf … tl) |
---|
252 | | pm_balanced_call : ∀st1,st2,st3,st4,st5.∀l1,l2. |
---|
253 | ∀prf : as_execute S l1 st1 st2.∀t1 : raw_trace S st2 st3. |
---|
254 | ∀t2 : raw_trace S st4 st5.∀prf' : as_execute S l2 st3 st4. |
---|
255 | as_classify … st1 ≠ cl_io → as_classify … st3 ≠ cl_io |
---|
256 | → is_call_act l1 → ¬ is_call_post_label … st1 → |
---|
257 | pre_measurable_trace … t1 → pre_measurable_trace … t2 → |
---|
258 | as_syntactical_succ S st1 st4 → |
---|
259 | is_unlabelled_ret_act l2 → |
---|
260 | pre_measurable_trace … (t_ind … prf … (t1 @ (t_ind … prf' … t2))). |
---|
261 | |
---|
262 | lemma pre_measurable_trace_inv : ∀S : abstract_status. |
---|
263 | ∀st1,st2 : S.∀t : raw_trace … st1 st2. pre_measurable_trace … t → |
---|
264 | (st1 = st2 ∧ as_classify … st1 ≠ cl_io ∧ t ≃ t_base … st1) ∨ |
---|
265 | (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl. |
---|
266 | t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_cost_act l ∧ |
---|
267 | pre_measurable_trace … tl) ∨ |
---|
268 | (∃st1' : S.∃l.∃prf : as_execute S l st1 st1'.∃tl. |
---|
269 | t = t_ind … prf … tl ∧ |
---|
270 | as_classify … st1 ≠ cl_io ∧ is_labelled_ret_act l ∧ pre_measurable_trace … tl) ∨ |
---|
271 | (∃st1' : S .∃l.∃prf : as_execute S l st1 st1'.∃tl. |
---|
272 | t = t_ind … prf … tl ∧ as_classify … st1 ≠ cl_io ∧ is_call_act l ∧ |
---|
273 | (bool_to_Prop (is_call_post_label … st1)) ∧ pre_measurable_trace … tl) ∨ |
---|
274 | (∃st1',st1'',st1''' : S.∃l1,l2.∃prf : as_execute S l1 st1 st1'. |
---|
275 | ∃t1 : raw_trace S st1' st1''.∃t2 : raw_trace S st1''' st2. |
---|
276 | ∃prf' : as_execute S l2 st1'' st1'''. |
---|
277 | t = t_ind … prf … (t1 @ (t_ind … prf' … t2)) ∧ as_classify … st1 ≠cl_io ∧ |
---|
278 | as_classify … st1'' ≠ cl_io ∧ is_call_act l1 ∧ |
---|
279 | bool_to_Prop (¬ is_call_post_label … st1) ∧ |
---|
280 | pre_measurable_trace … t1 ∧ pre_measurable_trace … t2 ∧ |
---|
281 | as_syntactical_succ S st1 st1''' ∧ is_unlabelled_ret_act l2). |
---|
282 | #S #st1 #st2 #t #H inversion H |
---|
283 | [ #st #Hclass #EQ1 #EQ2 destruct #EQ destruct #_ %%%%% // % // |
---|
284 | | #st1' #st2' #st3' #l #prf #tl #Hst1' #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ |
---|
285 | %%%%2 %{st2'} %{l} %{prf} %{tl} % // % // % // |
---|
286 | | #st1' #st2' #st3' #l #Hst1 #prf #tl #Hl #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ |
---|
287 | %%%2 %{st2'} %{l} %{prf} %{tl} % // % // % // |
---|
288 | | #st1' #st2' #st3' #l #prf #tl #Hst1 #Hl #H1st1 #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ |
---|
289 | % %2 %{st2'} %{l} %{prf} %{tl} % // % // % // % // |
---|
290 | | #st1' #st2' #st3' #st4' #st5' #l1 #l2 #prf #t1 #t2 #prf' #Hst1' #Hst3' #Hl1 |
---|
291 | #H1st1' #Ht1 #Ht2 #succ #Hl2 #_ #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 |
---|
292 | %{st2'} %{st3'} %{st4'} %{l1} %{(ret_act (None ?))} %{prf} %{t1} %{t2} |
---|
293 | %{prf'} /12 by conj/ |
---|
294 | ] |
---|
295 | qed. |
---|
296 | |
---|