source: LTS/Traces.ma @ 3390

Last change on this file since 3390 was 3390, checked in by piccolo, 6 years ago

Patched simulation proof, changed definition of silent trace

File size: 14.0 KB
Line 
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
15include "arithmetics/nat.ma".
16include "basics/types.ma".
17include "basics/deqsets.ma".
18include "../src/ASM/Util.ma".
19
20inductive FunctionName : Type[0] ≝
21 | a_function_id : ℕ → FunctionName.
22 
23inductive CallCostLabel : Type[0] ≝
24 | a_call_label : ℕ → CallCostLabel.
25 
26inductive ReturnPostCostLabel : Type[0] ≝
27 | a_return_cost_label : ℕ → ReturnPostCostLabel.
28 
29inductive NonFunctionalLabel : Type[0] ≝
30 | a_non_functional_label : ℕ → NonFunctionalLabel.
31 
32inductive CostLabel : Type[0] ≝
33 | a_call : CallCostLabel → CostLabel
34 | a_return_post : ReturnPostCostLabel → CostLabel
35 | a_non_functional_label : NonFunctionalLabel → CostLabel.
36
37coercion a_call.
38coercion a_return_post.
39coercion a_non_functional_label.
40
41definition 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
45coercion ret_act_label_to_cost_label.
46
47definition 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
51coercion call_act_label_to_cost_label.
52
53inductive 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 
59definition is_cost_label : ActionLabel → Prop ≝
60λact.match act with [ cost_act nf ⇒ True | _ ⇒ False ].
61
62inductive status_class : Type[0] ≝
63 | cl_jump : status_class
64 | cl_io : status_class
65 | cl_other : status_class.
66
67record 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 
79definition 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
90definition 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
102inductive 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
108definition is_cost_act : ActionLabel → Prop ≝
109λact.∃l.act = cost_act l.
110
111definition is_call_act : ActionLabel → Prop ≝
112λact.∃f,l.act = call_act f l.
113
114definition is_labelled_ret_act : ActionLabel → Prop ≝
115λact.∃l.act = ret_act (Some ? l).
116
117definition is_unlabelled_ret_act : ActionLabel → Prop ≝
118λact.act = ret_act (None ?).
119
120definition is_non_silent_cost_act : ActionLabel → Prop ≝
121λact. ∃l. act = cost_act (Some ? l).
122
123definition 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
130inductive 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
146lemma well_formed_trace_inv :
147∀S : abstract_status.∀st1,st2 : S.∀t : raw_trace S st1 st2.
148well_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.
151well_formed_trace … tl ∧ as_classify … st1 ≠ cl_jump ∧
152t ≃ 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]
167qed.
168
169
170let 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 ≝
172match t1
173return λst1,st2,tr.raw_trace S st2 st3 → raw_trace S st1 st3
174with
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
179interpretation "trace_append" 'append t1 t2 = (append_on_trace ???? t1 t2).
180
181lemma 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 %
186qed.
187
188definition trace_prefix: ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st1 st2 →
189raw_trace … st1 st3 → Prop≝
190λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st2 st3.t2 = t1 @ t3.
191
192definition trace_suffix : ∀S : abstract_status.∀st1,st2,st3 : S.raw_trace … st2 st3 →
193raw_trace … st1 st3 → Prop≝
194λS,st1,st2,st3,t1,t2.∃t3 : raw_trace … st1 st2.t2 = t3 @ t1.
195
196inductive 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
203lemma silent_io : ∀S : abstract_status.
204∀s1,s2 : S. ∀t : raw_trace … s1 s2. pre_silent_trace … t → as_classify … s1 ≠ cl_io →
205as_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
211qed.
212
213definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
214raw_trace S st1 st2 → bool ≝
215λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
216
217definition silent_trace : ∀S : abstract_status.∀st1,st2 : S.
218raw_trace S st1 st2 → Prop ≝ λS,st1,st2,t.pre_silent_trace … t ∧
219(is_trace_non_empty … t → as_classify … st1 ≠ cl_io) ∧
220well_formed_trace … t.
221
222lemma 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 * //
225qed.
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]
233qed.*)
234
235inductive 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                     
262lemma 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]
295qed.
296                     
Note: See TracBrowser for help on using the repository browser.