source: LTS/Simulation.ma @ 3389

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

Ended simulation proof

File size: 24.8 KB
Line 
1include "Common.ma".
2include "Traces.ma".
3
4record relations (S : abstract_status) : Type[0] ≝
5 { Srel: S → S → Prop
6 ; Crel: S → S → Prop
7 }.
8
9definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S.
10 ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'.
11
12record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
13 { simulate_tau:
14     ∀s1,s2,s1' : S.
15      as_execute … (cost_act (None ?))  s1 s1'→
16      Srel … rel s1 s2 →
17      ∃s2'. ∃t: raw_trace S s2 s2'.
18        Srel … rel s1' s2' ∧ silent_trace … t
19 ; simulate_label:
20     ∀s1,s2,l,s1'.
21      as_execute S (cost_act (Some ? l)) s1 s1' →
22      as_classify … s1' ≠ cl_io →
23      Srel … rel s1 s2 →
24      ∃s2',s2'',s2'''.
25       ∃t1: raw_trace S s2 s2'.
26       as_execute … (cost_act (Some ? l)) s2' s2'' ∧ as_classify … s2'' ≠ cl_io ∧
27       ∃t3: raw_trace S s2'' s2'''.
28        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
29 ; simulate_call_pl:
30     ∀s1,s2,s1' : S.∀f,l.
31      is_call_post_label … s1 →
32      as_execute … (call_act f l) s1 s1' →
33      as_classify … s1' ≠ cl_io →
34      Srel … rel s1 s2 →
35      ∃s2',s2'',s2'''.
36       ∃t1: raw_trace S s2 s2'.
37       as_classify … s2' ≠ cl_jump ∧
38       as_execute … (call_act f l) s2' s2'' ∧
39       bool_to_Prop(is_call_post_label … s2') ∧
40       as_classify … s2'' ≠ cl_io ∧
41       ∃t3: raw_trace S s2'' s2'''.
42        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
43 ; simulate_ret_l:
44     ∀s1,s2,s1' : S.∀l.
45      as_execute S (ret_act (Some ? l)) s1 s1' →
46      as_classify … s1' ≠ cl_io →
47      Srel  … rel s1 s2 →
48      ∃s2',s2'',s2'''.
49       ∃t1: raw_trace S s2 s2'.
50       as_classify … s2' ≠ cl_jump ∧
51       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
52       as_classify … s2'' ≠ cl_io ∧
53       ∃t3: raw_trace S s2'' s2'''.
54        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
55 ; simulate_call_n:
56     ∀s1,s2,s1' : S.∀f,l.
57      as_execute … (call_act f l) s1 s1' →
58      ¬ is_call_post_label … s1 →
59      Srel … rel s1 s2 →
60      ∃s2',s2'',s2'''.
61       ∃t1: raw_trace S s2 s2'.
62       bool_to_Prop (¬ is_call_post_label … s2') ∧
63       as_execute … (call_act f l) s2' s2'' ∧ as_classify … s2' ≠ cl_jump ∧
64       as_classify … s2'' ≠ cl_io ∧
65       ∃t3: raw_trace S s2'' s2'''.
66        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
67        ∧ Crel … rel s1 s2'
68 ; simulate_ret_n:
69     ∀s1,s2,s1' : S.
70      as_execute … (ret_act (None ?)) s1 s1' →
71      Srel … rel s1 s2 → as_classify … s2 ≠ cl_io ∧
72      ∃s2',s2'',s2'''.
73       ∃t1: raw_trace S s2 s2'.
74       as_execute … (ret_act (None ?)) s2' s2''  ∧ as_classify … s2' ≠ cl_jump ∧
75       as_classify … s2'' ≠ cl_io ∧
76       ∃t3: raw_trace S s2'' s2'''.
77        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t3
78        ∧ Rrel … rel s1' s2''
79 }.
80
81let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
82(t : raw_trace S st1 st2) on t : list CostLabel ≝
83match t with
84[ t_base st ⇒ [ ]
85| t_ind st1' st2' st3' l prf t' ⇒
86    let tl ≝ get_costlabels_of_trace … t' in
87    match l with
88    [ call_act f c ⇒ c :: tl
89    | ret_act x ⇒ match x with
90                  [ Some c ⇒ ret_act_label_to_cost_label c :: tl
91                  | None ⇒ tl
92                  ]
93    | cost_act x ⇒ match x with
94                  [ Some c ⇒ a_non_functional_label c :: tl
95                  | None ⇒ tl
96                  ]
97    | init_act ⇒ tl
98    ]
99].
100
101
102lemma append_premeasurable_silent : ∀S : abstract_status.
103∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
104pre_measurable_trace … t → pre_silent_trace … t' → as_classify … st1' ≠ cl_io →
105pre_measurable_trace … (t' @ t).
106#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
107[ #st #t #Hpre #_ #_ whd in ⊢ (????%); assumption]
108#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;
109[ #s #EQ1 #EQ2 destruct #EQ destruct]
110#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
111destruct #_ #Hs1' whd in ⊢ (????%); %2
112[ assumption
113| %{(None ?)} %
114| @IH try assumption >Hclass % #EQ destruct
115]
116qed.
117
118lemma pre_silent_is_premeasurable : ∀S : abstract_status.
119∀st1,st2 : S. ∀t : raw_trace S st1 st2.as_classify … st1 ≠cl_io → pre_silent_trace … t
120→ pre_measurable_trace … t.
121#S #st1 #st2 #t elim t
122[ #st #Hst #H inversion H in ⊢ ?; [ #st' #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
123  #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
124-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #Hst1 #H inversion H in ⊢ ?;
125[ #st #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
126#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
127@IH [ >Hst2' % #EQ destruct | assumption]
128qed.
129
130lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
131    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
132    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2.
133#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
134
135lemma append_silent_premeasurable : ∀S : abstract_status.
136∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
137pre_measurable_trace … t' → pre_silent_trace … t → as_classify … st1 ≠ cl_io →
138pre_measurable_trace … (t' @ t).
139#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
140[ normalize #st #Hst #r #H1 #H2 @pre_silent_is_premeasurable assumption
141|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
142  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r #Hs3 [ %2 | %3 | %4 ]
143  try ( %{x} %) try @IH try assumption % ]
144#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
145#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
146#r #pre_r #Hs5 normalize
147cut(∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l.
148    ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3.
149    ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2)
150[ @append_tind_commute ] #H >H >H >append_associative <H in ⊢ (????(??????%)); %5
151try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
152qed.
153
154
155
156definition is_trace_non_empty : ∀S : abstract_status.∀st1,st2.
157raw_trace S st1 st2 → bool ≝
158λS,st1,st2,t.match t with [ t_base _ ⇒ false | _ ⇒ true ].
159
160lemma append_well_formed_silent : ∀S : abstract_status.
161∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
162well_formed_trace … t → pre_silent_trace … t' →
163(is_trace_non_empty … t' → as_classify … st1' = cl_other) →
164well_formed_trace … (t' @ t).
165#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
166[ #st #t #H #_ #_ assumption ]
167#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
168inversion H in ⊢ ?;
169[ #st #EQ1 #EQ2 #EQ3 destruct]
170#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
171#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
172[2: >(Hclass1 I) % #EQ destruct]
173@IH try assumption #_ assumption
174qed.
175
176lemma well_formed_append : ∀S : abstract_status.
177∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
178well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
179#S #st1 #st2 #st3 #t1 #t2 #H %
180[ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
181#H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
182#st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
183#EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
184[ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
185]
186lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
187#s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
188[ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
189#s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
190#_ @IH assumption
191qed.
192
193
194lemma append_well_formed : ∀S : abstract_status.
195∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
196well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
197#S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
198[ #st #r #H1 @H1 ]
199#s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
200try @IH assumption
201qed.
202
203lemma silent_is_well_formed : ∀S : abstract_status.
204∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
205#S #st1 #st2 #t elim t [ #st #_ %]
206#s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
207#s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
208[ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
209qed.
210
211
212lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
213∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
214pre_silent_trace … t1 →
215get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
216#S #st1 #st2 #st3 #t1 elim t1
217[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H
218inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
219#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
220#_ whd in ⊢ (??%?); >IH [%] assumption
221qed.
222
223lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
224∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
225get_costlabels_of_trace … (t1 @ t2) =
226 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
227#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
228[#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH
229qed.
230 
231(*
232lemma raw_trace_ind_r : ∀S : abstract_status.
233∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
234(∀st : S.P … (t_base … st)) →
235(∀st1,st2,st3,l.
236 ∀prf : as_execute S l st2 st3.
237 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
238∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
239#S #P #base #ind #st1 #st2 #t elim t [ assumption]
240#st1 #st2 #st3 #l #prf #raw #IH
241*)
242
243
244theorem simulates_pre_mesurable:
245 ∀S : abstract_status.∀rel : relations S.
246 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
247  simulation_conditions S rel →
248  pre_measurable_trace … t1 →
249  well_formed_trace … t1 → ∀s2 : S.
250  as_classify … s2 ≠ cl_io → Srel … rel s1 s2 →
251  ∃s2'. ∃t2: raw_trace … s2 s2'.
252    pre_measurable_trace … t2 ∧
253    well_formed_trace … t2 ∧
254    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
255    Srel … rel s1' s2'.
256#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
257[ #st #H1 #well_formed #s2 #H2 #REL %{s2} %{(t_base …)}
258  /8 by refl, pm_empty, wf_empty, conj/
259| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
260  #pre_measurable_tl #IH #well_formed #s2 #classify_s2 #REL
261  [ cases(simulate_tau … good … execute … REL) #s2'' * #t_s2'' * #RELst2s2''
262    * #silent_ts2'' #Hclass_s2 cases(IH … RELst2s2'')
263    [2: cases(well_formed_trace_inv … well_formed)
264         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
265             #EQ destruct(EQ) assumption
266         | *
267            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
268                assumption
269            | * #EQ1 #EQ2 destruct
270            ]
271         ]
272    |3: @(silent_io … silent_ts2'')  assumption   
273    ]
274    #s3 * #ts3 *** #pre_meas_ts3 #well_formed_ts3 #EQcost #RELst3s3
275    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] %
276    [ %
277      [ @append_premeasurable_silent assumption
278      | @append_well_formed_silent assumption
279      ]
280    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
281      [% | assumption]
282    ]
283  | cases(simulate_label … good … execute … REL)
284    [2: cases pre_measurable_tl
285        [ #st #H @H
286        | #st1 #st2 #st3 #l #prf #tl #H #_ #_ @H
287        | #st1 #st2 #st3 #l #H #_ #tl #_ #_ @H
288        | #st1 #st2 #st3 #l #_ #tl #H #_ #_ #_ @H
289        | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #_ #t1 #t2 #_ #H #_ #_ #_ #_ #_ #_ #_ @H
290        ]
291    ]
292    #s2'' * #s2''' * #s2'''' * #t_s2'' ** #exe_s2''' #CLASS' * #t_s2'''' ** #RELst2_s2''''
293    * #sil_ts2'' #Hclass_s2 * #sil_t_s2'''' #Hclass_s2''' cases(IH … RELst2_s2'''')
294    [2: cases(well_formed_trace_inv … well_formed)
295         [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_
296             #EQ destruct(EQ) assumption
297         | *
298            [2: * #st2''' * #l''' * #prf''' * #tl''' ** #H #_ #EQ destruct
299                assumption
300            | * #EQ1 #EQ2 destruct
301            ]
302         ]
303    |3: @(silent_io … sil_t_s2'''') assumption
304    ]
305    #s3 * #t_s3 *** #pre_s3 #well_s3 #EQcost #RElst3s3 %{s3}
306    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
307    %
308    [ %
309      [ @append_premeasurable_silent try assumption %2
310        [ @(silent_io … t_s2'') assumption
311        | %{(Some ? c)} %
312        ]
313        @append_premeasurable_silent assumption
314      | @append_well_formed_silent try assumption inversion(as_classify … s2'')
315        #Hclass
316        [ %3 [2: %{c} %]
317        |*: %2 [2,4: >Hclass % #EQ destruct]
318        ]
319        @append_well_formed_silent assumption
320      ]
321    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
322      [2: assumption] whd in ⊢ (???%);
323      >get_cost_label_invariant_for_append_silent_trace_l
324      [ % | assumption]
325    ]
326  ]
327| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
328  #pre_meas_tl #IH #H inversion H
329  [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
330  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
331  [ #class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
332  #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #class_s2 #RELst1s2
333  cases(simulate_ret_l … good … exe_st1_st2 … RELst1s2)
334  [2: inversion pre_meas_tl
335      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
336      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
337      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
338      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
339      destruct assumption ]
340  #s2' * #s2'' * #s2''' * #t1 *** #j_s2' #exe_s2'' #class_s2'' * #t2 ** #rel_s2_s2'''
341  #sil_t1 #sil_t2
342  cases(IH … wf_tl' … rel_s2_s2''')
343  [2: @(silent_io … (proj1 … sil_t2)) assumption]
344  #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL
345  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
346  % [2: whd in ⊢ (??%?);
347        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
348        whd in ⊢ (???%);
349        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
350        @eq_f assumption ]
351  %
352  [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
353    %3
354    [ @(silent_io … (proj1 … sil_t1)) assumption
355    | whd %{ret_lab} %
356    | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
357    ]
358  | @append_well_formed_silent
359    [ %2 try assumption @append_well_formed_silent try assumption
360      [ @(proj1 … sil_t2)
361      | @(proj2 … sil_t2)
362      ]
363    | @(proj1 … sil_t1)
364    | @(proj2 … sil_t1)
365    ]
366  ]
367| #s2 #s2' #s2'' #l #exe_s2_s2' #tl #class_s2 whd in ⊢ (% → ?); * #f * #lab #EQ destruct
368  #post #pre_tl #IH #H inversion H [ #s3 #EQ1 #EQ2 destruct #ABS destruct(ABS) ]
369  #st1 #st2 #st3 #l #exe_st1_st2 #tl' #wf_tl'
370  [#class_no_jump | whd in ⊢ (% → ?); * #nf #EQ destruct(EQ) ]
371   #_ #EQ1 #EQ2 #EQ3 destruct #_ -H #s2 #io_s2 #REL_st1_s2
372   cases(simulate_call_pl … good … post … exe_st1_st2 … REL_st1_s2)
373   [2: inversion pre_tl
374      try #x1 try #x2 try #x3 try #x4 try #x5 try #x6
375      try #x11 try #x12 try #x13 try #x14 try #x15 try #x16
376      try #x17 try #x18 try #x19 try #x20 try #x21 try #x22
377      try #x37 try #x38 try #x39 try #x30 try #x31 try #x32 try #x33
378      destruct assumption ]
379   #s2' * #s2'' * #s2''' * #t1 **** #j_s2' #exe_s2'' #post' #io_s2'' * #t2 ** #REL #sil_t1 #sil_t2
380   cases(IH … wf_tl' … REL)
381   [2: @(silent_io … (proj1 … sil_t2)) assumption ]
382   #s2_fin * #t_fin *** #pre_t_fin #wf_t_fin #EQcost #REL1 %{s2_fin}
383   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
384   [2: whd in ⊢ (??%?);
385        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t1))
386        whd in ⊢ (???%);
387        >(get_cost_label_invariant_for_append_silent_trace_l … (proj1 … sil_t2))
388        @eq_f assumption ]
389   %
390   [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_t1)]
391     %4 try assumption
392     [ @(silent_io … (proj1 … sil_t1)) assumption
393     | whd %{f} %{lab} %
394     | @append_premeasurable_silent try assumption @(proj1 … sil_t2)
395     ]
396   | @append_well_formed_silent
397     [ %2 try assumption @append_well_formed_silent try assumption
398        [ @(proj1 … sil_t2)
399        | @(proj2 … sil_t2)
400        ]
401     | @(proj1 …  sil_t1)
402     | @(proj2 … sil_t1)
403     ]
404   ]
405| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
406  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
407  #IH1 #IH2 #wf_all #st1' #Hst1' #REL
408  cases(simulate_call_n … good … exe_12 … Hst1 … REL)
409  #st1'' * #st1''' * #st2' * #tr1 **** #nps_st1'' #exe_12' #Hst1'' #Hst1''' * #tr2 *** #REL1 #sil_tr1
410  #sil_tr2 #call_rel cases(IH1 … REL1)
411  [2: inversion wf_all [ #st #EQ1 #EQ2 #EQ3 destruct]
412      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ) ] #_
413      #EQ1 #EQ2 #EQ3 destruct #_ @(proj1 … (well_formed_append … wf_tl))
414  |3: @(silent_io … (proj1 … sil_tr2)) assumption
415  ]
416  #st3' * #tr3 *** #pre_tr3 #wf_tr3 #EQcost_tr3 #REL2
417  cases(simulate_ret_n … good … exe_34 … REL2) #Hst3' * #st3'' * #st4' * #st4'' *
418  #tr4 *** #exe_34' #Hst3'' #Hst4' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3)
419  [2: inversion wf_all in ⊢ ?; [#st #EQ1 #EQ2 destruct whd in ⊢ (????% → ?); #EQ destruct]
420      #x1 #x2 #x3 #y #prf #tl #wf_tl [ #Hx1 | * #y1 #EQ destruct(EQ)] #_
421      #EQ1 #EQ2 #EQ3 destruct #_ cases(well_formed_append … wf_tl) -wf_tl -wf_all
422      #_ #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 destruct]
423      #z1 #z2 #z3 #w #prf' #tl' #wf_tl' [ #Hz1 | * #w1 #EQ destruct(EQ)] #_
424      #EQ1 #EQ2 #EQ3 destruct #_ assumption
425  |3: @(silent_io … (proj1 … sil_tr5)) assumption
426  ]
427  #st5' * #tr6 *** #pre_tr6 #wf_tr6 #EQcost_tr6 #REL4 %{st5'}
428  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
429  % [2: assumption] %
430  [ %
431     [ @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr1) ]
432       %5
433       [ @(silent_io … (proj1 … sil_tr1)) assumption
434       | @(silent_io … (proj1 … sil_tr4)) assumption
435       | whd %{f} %{l} %
436       | assumption
437       | @append_premeasurable_silent try assumption [2: @(proj1 … sil_tr2)]
438         @append_silent_premeasurable try assumption @(proj1 … sil_tr4)
439       | @append_premeasurable_silent try assumption @(proj1 … sil_tr5)
440       | @(RET_REL … call_rel) assumption
441       | %
442       ]
443     | @append_well_formed_silent [2: @(proj1 … sil_tr1) |3: @(proj2 … sil_tr1) ]
444       %2 [2: assumption] >append_associative @append_well_formed_silent
445       [2: @(proj1 … sil_tr2) |3: @(proj2 … sil_tr2) ] @append_well_formed
446       [ @append_well_formed try assumption @silent_is_well_formed assumption ]
447       %2 [2: assumption] @append_well_formed try assumption @silent_is_well_formed
448       assumption
449     ]
450  | >get_cost_label_invariant_for_append_silent_trace_l [2: @(proj1 … sil_tr1) ]
451    whd in ⊢ (??%%); @eq_f >append_associative
452    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
453    [2: @(proj1 … sil_tr2) ] >append_associative
454    >get_cost_label_append in ⊢ (???%);
455    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
456    [2: @(proj1 … sil_tr4) ] normalize
457    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
458    [2: @(proj1 …  sil_tr5) ] >get_cost_label_append in ⊢ (??%?); @eq_f2
459    assumption
460  ]
461]
462qed.
463
464xxxxx
465
466
467(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
468   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
469   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
470
471(* measurable fattorizzata sotto come measurable'
472definition measurable ≝
473 λL,s1,s2.λt: raw_trace … s1 s2.
474  ∃L',s0,so. as_execute … s0 s1 L ∧
475  pre_measurable_trace … t ∧
476  well_formed_trace … t ∧
477  as_execute … s2 so L'. *)
478
479record LR_raw_trace (S : abstract_status) : Type[0] ≝
480 { L_label: ActionLabel
481 ; R_label : ActionLabel
482 ; LR_s1: S
483 ; LR_s2: S
484 ; LR_t : raw_trace S LR_s1 LR_s2
485 ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act
486 ; L_noinit_ok :
487      bool_to_Prop (¬ as_initial … LR_s1) →
488        ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label
489        ∧ ¬ bool_to_Prop (is_act_io_entering S L_label)
490 ; R_nonfin_ok :
491    bool_to_Prop (¬ as_final … (LR_s2)) →
492      ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label
493          ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label)
494 }.
495 
496definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S.
497pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t).
498
499
500(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
501  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
502  il teorema sotto sembra suggerire il merge *)
503
504definition unmovable_entry_label ≝
505λS : abstract_status.λl.
506match l with
507[ call_act _ _ ⇒ false
508| ret_act _ ⇒ false
509| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
510                            | None ⇒ false
511                            ]
512| init_act ⇒ true
513].
514 
515definition unmovable_exit_label ≝
516λS : abstract_status.λl.
517match l with
518[ call_act _ _ ⇒ false
519| ret_act _ ⇒ false
520| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
521                            | None ⇒ false
522                            ]
523| init_act ⇒ false
524].
525
526theorem simulates_LR_raw_trace :
527∀S : abstract_status.
528∀t : LR_raw_trace S.
529∀rel : relations S.
530simulation_conditions … rel →
531measurable S t →
532∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
533∃ t' : LR_raw_trace S.
534measurable S t' ∧
535if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
536   LR_s1 … t' = s1'
537else
538   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
539∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
540if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
541   LR_s2 … t' = s1''
542else
543  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
544
545get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
546#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
547cases(simulates_pre_mesurable … (LR_t … t) … REL)
548[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
549#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
550inversion(as_initial … (LR_s1 … t)) #Has_initial
551inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
552inversion(as_final … (LR_s2 … t)) #Has_final
553inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
554normalize nodelta
555[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
556
557
558
559qed.
560
561xxxx
562
563theorem simulates_L_raw_trace:
564 ∀t: L_raw_trace.
565  pre_measurable_trace … (L_t t1) →
566  well_formed_trace … (L_t t1) →
567 ∀s1'.
568   S (L_s1 t) s1' →
569   s1' -flat-→ (L_s1 t2) →
570   ∃s2',t2: L_raw_trace.
571    pre_mesurable_trace … (L_t t2) ∧
572    well_formed_trace … (L_t t2) ∧
573    |t1| = |t2| ∧
574    S (L_s2 t1) s2' ∧
575    (L_s2 t2) -flat-→ s2'.
576 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
577       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
578
579
580(*********************************************************************)
581
582(* quello che segue tentava di permettere di evitare l'emissione di label
583   associate a codice morto *)
584
585replace_last x : weak_trace → weak_trace
586   [] ⇒ [], Some x
587 | l::t ⇒
588     let 〈t',x'〉 ≝ replace_last x t in
589     match x' with
590     [ None ⇒ l::t', None
591     | Some x'' ⇒ [], Some x''
592
593theorem simulates:
594 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
595  pre_measurable_trace … t1 →
596  well_formed_trace … t1.
597 ∀l1: option NonFunctionalLabel.
598 ∀s1'.
599   S s1 s1' →
600   ∃dead_labels.
601   ∃s2'. ∃t2: raw_trace … s1' s2'.
602    pre_mesurable_trace … t2 ∧
603    well_formed_trace … t2.
604   ∃l2: option NonFunctionalLabel.
605    match l1 with
606    [ None ⇒
607       match l2 with
608       [ None ⇒ |t1| = |t2|
609       | Some l2' ⇒ |t1| = l2'::|t2| ]
610    | Some l1' ⇒
611       match l2 with
612       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
613       | Some l2' ⇒
614          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
615          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
616       ]
617    ]
Note: See TracBrowser for help on using the repository browser.