source: LTS/Simulation.ma @ 3418

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

correctness proof in developping

File size: 37.3 KB
RevLine 
[3382]1include "Common.ma".
[3387]2include "Traces.ma".
[3382]3
[3387]4record relations (S : abstract_status) : Type[0] ≝
5 { Srel: S → S → Prop
6 ; Crel: S → S → Prop
[3383]7 }.
[3382]8
[3387]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'.
[3383]11
[3388]12record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝
[3394]13 { initial_is_initial :
14   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) →  bool_to_Prop (as_initial … s2))
15 ; final_is_final :
16   ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2))
17 ; simulate_tau:
[3387]18     ∀s1,s2,s1' : S.
19      as_execute … (cost_act (None ?))  s1 s1'→
[3391]20      Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]21      ∃s2'. ∃t: raw_trace S s2 s2'.
[3388]22        Srel … rel s1' s2' ∧ silent_trace … t
[3383]23 ; simulate_label:
24     ∀s1,s2,l,s1'.
[3387]25      as_execute S (cost_act (Some ? l)) s1 s1' →
[3391]26      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]27      Srel … rel s1 s2 →
[3383]28      ∃s2',s2'',s2'''.
[3387]29       ∃t1: raw_trace S s2 s2'.
[3391]30       as_execute … (cost_act (Some ? l)) s2' s2'' ∧
[3387]31       ∃t3: raw_trace S s2'' s2'''.
[3394]32        Srel … rel  s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3383]33 ; simulate_call_pl:
[3387]34     ∀s1,s2,s1' : S.∀f,l.
35      is_call_post_label … s1 →
36      as_execute … (call_act f l) s1 s1' →
[3391]37      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]38      Srel … rel s1 s2 →
[3383]39      ∃s2',s2'',s2'''.
[3387]40       ∃t1: raw_trace S s2 s2'.
41       as_execute … (call_act f l) s2' s2'' ∧
[3388]42       bool_to_Prop(is_call_post_label … s2') ∧
[3387]43       ∃t3: raw_trace S s2'' s2'''.
[3394]44        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3383]45 ; simulate_ret_l:
[3387]46     ∀s1,s2,s1' : S.∀l.
47      as_execute S (ret_act (Some ? l)) s1 s1' →
[3391]48      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]49      Srel  … rel s1 s2 →
[3383]50      ∃s2',s2'',s2'''.
[3387]51       ∃t1: raw_trace S s2 s2'.
52       as_execute … (ret_act (Some ? l)) s2' s2'' ∧
53       ∃t3: raw_trace S s2'' s2'''.
[3394]54        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3383]55 ; simulate_call_n:
[3387]56     ∀s1,s2,s1' : S.∀f,l.
57      as_execute … (call_act f l) s1 s1' →
58      ¬ is_call_post_label … s1 →
[3391]59      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
[3387]60      Srel … rel s1 s2 →
[3383]61      ∃s2',s2'',s2'''.
[3387]62       ∃t1: raw_trace S s2 s2'.
[3389]63       bool_to_Prop (¬ is_call_post_label … s2') ∧
[3391]64       as_execute … (call_act f l) s2' s2'' ∧
[3387]65       ∃t3: raw_trace S s2'' s2'''.
[3394]66        Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3
[3387]67        ∧ Crel … rel s1 s2'
[3383]68 ; simulate_ret_n:
[3387]69     ∀s1,s2,s1' : S.
70      as_execute … (ret_act (None ?)) s1 s1' →
[3391]71      as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io →
72      Srel … rel s1 s2 →
[3383]73      ∃s2',s2'',s2'''.
[3387]74       ∃t1: raw_trace S s2 s2'.
[3391]75       as_execute … (ret_act (None ?)) s2' s2''  ∧
[3387]76       ∃t3: raw_trace S s2'' s2'''.
[3394]77        Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3
[3389]78        ∧ Rrel … rel s1' s2''
[3394]79 ; simulate_io_in :
80   ∀s1,s2,s1' : S.∀l.
81   as_execute … (cost_act … (Some ? l)) s1 s1' →
82   as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io →
83   Srel … rel s1 s2 →
84   ∃s2',s2'' : S.∃t: raw_trace … s2 s2'.
85   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧
86   as_classify … s2'' = cl_io ∧ Srel … rel s1' s2''
87; simulate_io_out :
88  ∀s1,s2,s1' : S.∀l.
89   as_execute … (cost_act … (Some ? l)) s1 s1' →
90   as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io →
91   Srel … rel s1 s2 →
92   ∃s2',s2'' : S.∃t : raw_trace … s2' s2''.
93   pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧
94   as_classify … s2 = cl_io ∧ Srel … rel s1' s2''
[3383]95 }.
96
[3387]97let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S)
98(t : raw_trace S st1 st2) on t : list CostLabel ≝
99match t with
100[ t_base st ⇒ [ ]
101| t_ind st1' st2' st3' l prf t' ⇒
102    let tl ≝ get_costlabels_of_trace … t' in
103    match l with
[3396]104    [ call_act f c ⇒ [ c ]
[3387]105    | ret_act x ⇒ match x with
[3396]106                  [ Some c ⇒ [ a_return_post c ]
107                  | None ⇒ []
[3387]108                  ]
109    | cost_act x ⇒ match x with
[3396]110                  [ Some c ⇒ [ a_non_functional_label c ]
111                  | None ⇒ []
[3387]112                  ]
[3396]113    | init_act ⇒ []
114    ] @ tl
[3387]115].
116
117
[3388]118lemma append_premeasurable_silent : ∀S : abstract_status.
119∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
[3391]120pre_measurable_trace … t → silent_trace … t' → 
[3388]121pre_measurable_trace … (t' @ t).
122#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
[3391]123[ #st #t #Hpre #_ whd in ⊢ (????%); assumption]
[3394]124#s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?;
[3391]125[ #s #H1 #EQ1 #EQ2 destruct #EQ destruct]
[3388]126#s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3
[3391]127destruct #_ whd in ⊢ (????%); %2
[3388]128[ assumption
129| %{(None ?)} %
[3390]130| @IH try assumption
[3388]131]
[3394]132% assumption
[3388]133qed.
134
[3394]135lemma pre_silent_is_premeasurable : ∀S : abstract_status.
136∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t
[3389]137→ pre_measurable_trace … t.
138#S #st1 #st2 #t elim t
[3391]139[ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ]
140#st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ]
141-t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?;
142[ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl'
[3389]143#_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ]
[3390]144@IH assumption
[3389]145qed.
146
147lemma append_tind_commute : ∀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#S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed.   
151
152lemma append_silent_premeasurable : ∀S : abstract_status.
153∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
[3391]154pre_measurable_trace … t' → silent_trace … t →
[3389]155pre_measurable_trace … (t' @ t).
156#S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht'
[3394]157[ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ]
158  inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11
159  #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_
160  %1 assumption
[3389]161|2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct
[3391]162  [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ]
[3389]163  try ( %{x} %) try @IH try assumption % ]
164#s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1'
165#EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2
[3391]166#r #pre_r normalize
167>append_tind_commute >append_tind_commute >append_associative
168<append_tind_commute in ⊢ (????(??????%)); %5
[3389]169try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption
170qed.
171
[3390]172(*
[3388]173lemma append_well_formed_silent : ∀S : abstract_status.
174∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1.
175well_formed_trace … t → pre_silent_trace … t' →
[3390]176(is_trace_non_empty … t' → as_classify … st) →
[3388]177well_formed_trace … (t' @ t).
178#S #st1' #st1 #st2 #t #t' lapply t -t elim t'
179[ #st #t #H #_ #_ assumption ]
180#s1' #s2' #s3' #l #prf #tl #IH #t #well_formed_t #H
181inversion H in ⊢ ?;
182[ #st #EQ1 #EQ2 #EQ3 destruct]
183#st1'' #st2' #st3' #prf' #tl' #Hclass #silent_tl #_
184#EQ1 destruct #EQ #EQ1 destruct #_ #Hclass1 %2
185[2: >(Hclass1 I) % #EQ destruct]
186@IH try assumption #_ assumption
[3390]187qed.*)
[3388]188
[3391]189(*
[3389]190lemma well_formed_append : ∀S : abstract_status.
191∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
192well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2.
193#S #st1 #st2 #st3 #t1 #t2 #H %
194[ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r
195#H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ]
196#st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_
197#EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_
198[ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ]
199]
200lapply H lapply t2 -t2 elim t1 [ #st #r normalize //]
201#s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?;
202[ #st #EQ1 #EQ2 normalize #EQ3 destruct ]
203#s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct
204#_ @IH assumption
205qed.
206
207
208lemma append_well_formed : ∀S : abstract_status.
209∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
210well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2).
211#S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H
212[ #st #r #H1 @H1 ]
213#s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3]
214try @IH assumption
215qed.
[3390]216(*
[3389]217lemma silent_is_well_formed : ∀S : abstract_status.
218∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t.
219#S #st1 #st2 #t elim t [ #st #_ %]
220#s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct]
221#s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2
222[ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct]
223qed.
[3390]224*)
[3391]225*)
[3388]226lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status.
227∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
[3391]228silent_trace … t1 →
[3388]229get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2.
230#S #st1 #st2 #st3 #t1 elim t1
[3394]231[#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 *
232[2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %]
233#H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct]
[3388]234#st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct
[3394]235#_ whd in ⊢ (??%?); >IH [%] %1 assumption
236qed.
[3388]237
[3389]238lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S.
239∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3.
240get_costlabels_of_trace … (t1 @ t2) =
241 append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2).
242#S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' *
243[#f * #l | * [| * #l] | *  [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH
244qed.
245 
[3388]246(*
247lemma raw_trace_ind_r : ∀S : abstract_status.
248∀P : (∀st1,st2.raw_trace S st1 st2 → Prop).
249(∀st : S.P … (t_base … st)) →
250(∀st1,st2,st3,l.
251 ∀prf : as_execute S l st2 st3.
252 ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) →
253∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t.
254#S #P #base #ind #st1 #st2 #t elim t [ assumption]
255#st1 #st2 #st3 #l #prf #raw #IH
256*)
257
[3391]258lemma head_of_premeasurable_is_not_io : ∀S : abstract_status.
259∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
260as_classify … st1 ≠ cl_io.
261#S #st1 #st2 #t #H inversion H //
262qed.
[3388]263
[3391]264
[3386]265theorem simulates_pre_mesurable:
[3387]266 ∀S : abstract_status.∀rel : relations S.
267 ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'.
[3388]268  simulation_conditions S rel →
[3382]269  pre_measurable_trace … t1 →
[3391]270  ∀s2 : S.
271 as_classify … s2 ≠ cl_io →   Srel … rel s1 s2 →
[3388]272  ∃s2'. ∃t2: raw_trace … s2 s2'.
[3387]273    pre_measurable_trace … t2 ∧
274    get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧
[3388]275    Srel … rel s1' s2'.
276#S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable
[3391]277[ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)}
[3394]278  /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/
[3388]279| #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct
[3391]280  #pre_measurable_tl #IH #s2 #classify_s2 #REL
281  [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2''
[3394]282    #silent_ts2'' cases(IH … RELst2s2'')
283    [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2''
284        [ #x #EQ1 #EQ2 #EQ3 destruct // ]
285        #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ]
[3391]286    #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3
287    %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/
288    whd in ⊢ (??%?); /2/
[3388]289  | cases(simulate_label … good … execute … REL)
[3391]290    [2,3: /2/]
291    #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2''''
[3394]292    #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''')  /2 by pre_silent_io/
[3391]293    #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3}
[3388]294    %{(t_s2'' @ (t_ind … exe_s2''' …))}  [ @(t_s2'''' @ t_s3) ] % [2: assumption]
295    %
[3394]296    [ @append_premeasurable_silent // %2 /2 by ex_intro/
297       [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2''
298         [ #H31 #H32 #H33 #H34 #H35 destruct assumption ]
299         #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
300         cases H47 #ABS @⊥ @ABS % ]
301       @append_premeasurable_silent // % //
[3388]302    | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l
[3391]303      [2: assumption] whd in ⊢ (???%);
304      >get_cost_label_invariant_for_append_silent_trace_l //
[3388]305    ]
306  ]
[3394]307  % assumption
[3388]308| #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ)
[3391]309  #pre_meas_tl #IH #s2 #class_s2 #RELst1s2
310  cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ]
311  #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2'''
312  #sil_t1 #sil_t2 cases(IH … rel_s2_s2''')
[3394]313  [2: @(pre_silent_io … sil_t2) assumption]
[3391]314  #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL
[3388]315  %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption]
316  % [2: whd in ⊢ (??%?);
[3391]317        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
[3388]318        whd in ⊢ (???%);
[3394]319        >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2))
[3388]320        @eq_f assumption ]
[3394]321  @append_premeasurable_silent [2: //] %3
322  [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ]
323  cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1
324  [ #H49 #H50 #H51 #H52 #H53 destruct //]
325  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65
326  #ABS @⊥ @ABS %
[3391]327| #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct
328  #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2'
329   cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2')
330   [2,3: /2 by head_of_premeasurable_is_not_io/ ]
331   #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2
332   cases(IH  … REL)
[3394]333   [2: /2 by pre_silent_io/ ]
[3391]334   #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin}
[3388]335   %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] %
336   [2: whd in ⊢ (??%?);
[3391]337        >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1)
[3388]338        whd in ⊢ (???%);
[3394]339        >(get_cost_label_invariant_for_append_silent_trace_l …  (or_introl … sil_t2))
[3388]340        @eq_f assumption ]
[3391]341   @append_premeasurable_silent try assumption
[3388]342     %4 try assumption
[3394]343     [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //]
344       #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83
345       #ABS @⊥ @ABS %
[3388]346     | whd %{f} %{lab} %
[3394]347     | @append_premeasurable_silent // % assumption
[3388]348     ]
[3389]349| #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 *
350  #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct
[3391]351  #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ]
352  #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1
[3389]353  #sil_tr2 #call_rel cases(IH1 … REL1)
[3394]354  [2: /2 by pre_silent_io/ ]
[3391]355  #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2
356  cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ]
357  #st3'' * #st4' * #st4'' *
[3394]358  #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ]
[3391]359  #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'}
[3389]360  %{(tr1 @ (t_ind … exe_12' …  ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))}
361  % [2: assumption] %
[3391]362  [ @append_premeasurable_silent try assumption %5
[3394]363       [1,2: /2 by pre_silent_io/
364             cases sil_tr1 /2 by pre_silent_io/ inversion tr1
365             [ #H85 #H86 #H87 #H88 #H89 destruct // ]
366             #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct
367             cases H107 #ABS @⊥ @ABS %
[3389]368       | whd %{f} %{l} %
369       | assumption
[3394]370       | @append_premeasurable_silent try assumption [2: % //]
371         @append_silent_premeasurable // % //
[3391]372       | @append_premeasurable_silent try assumption
[3389]373       | @(RET_REL … call_rel) assumption
374       | %
375       ]
[3391]376  | >get_cost_label_invariant_for_append_silent_trace_l [2: // ]
[3389]377    whd in ⊢ (??%%); @eq_f >append_associative
378    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
[3394]379    [2: % // ] >append_associative
[3389]380    >get_cost_label_append in ⊢ (???%);
381    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
[3394]382    [2: % //] normalize
[3389]383    >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%);
[3394]384    [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2
[3389]385    assumption
386  ]
[3394]387  % //
[3388]388]
[3389]389qed.
[3383]390
[3388]391
[3386]392(* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio
393   sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O;
394   cambiare la definizione di traccia tornando a una sola etichetta sugli archi *)
395
396(* measurable fattorizzata sotto come measurable'
397definition measurable ≝
398 λL,s1,s2.λt: raw_trace … s1 s2.
399  ∃L',s0,so. as_execute … s0 s1 L ∧
400  pre_measurable_trace … t ∧
401  well_formed_trace … t ∧
402  as_execute … s2 so L'. *)
403
[3394]404record measurable_trace (S : abstract_status) : Type[0] ≝
[3387]405 { L_label: ActionLabel
[3394]406 ; R_label : option ActionLabel
407 ; L_pre_state : option S
408 ; L_s1 : S
409 ; R_s2: S
410 ; R_post_state : option S
411 ; trace : raw_trace S L_s1 R_s2
412 ; pre_meas : pre_measurable_trace … trace
413 ; L_init_ok : match L_pre_state with
414               [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = init_act
415               | Some s ⇒ is_costlabelled_act L_label ∧
416                          as_execute … L_label s L_s1
417               ]
418 ; R_fin_ok : match R_label with
419               [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ?
420               | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧
421                          (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧
422                          ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s'
423               ]
424}.
425
426lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s.
427#P #H1 #H2 * // @H2 % #EQ destruct qed.
428
429lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io).
430* [2: %%] %2 % #EQ destruct qed.
431
432lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status.
433∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t →
434as_classify … st2 ≠ cl_io.
435#S #st1 #st2 #t #H elim H //
436qed.
437
438lemma get_cost_label_silent_is_empty : ∀S : abstract_status.
439∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ].
440#S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ]
441#H inversion H
442[#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3
443destruct #_ @IH % assumption
444qed.
445
446lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status.
447∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3.
448silent_trace … t2 →
449get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1.
450#S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append
451>(get_cost_label_silent_is_empty … H) //
452qed.
453
454lemma instr_execute_commute : ∀S :abstract_status.
455∀rel : relations S.
456simulation_conditions … rel →
457∀s1,s1': S.∀l.l ≠ init_act → l ≠ cost_act (None ?) →  as_execute S l s1 s1' →
458(as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) →
459∀s2.
460Srel … rel s1 s2 →
461∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧
462∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S.
463∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧
464(is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧
465(as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io).
466#S #rel #good #s1 #s1' #l #l_noinit #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1))
467[ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ)
468  cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1'
469  cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL)
470  #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL'
471  %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % 
472  [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable
473     assumption ] % [  %//  % // ] * #f * #l #EQ destruct
474| #Hclass_s1 cases(case_cl_io … (as_classify … s1'))
475  [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ)
476    cases(simulate_io_in … good … prf … Hclass_s1 EQs1' …  REL) #s2' * #s2'' * #t
477    *** #sil_t #exe #Hclass_s2'' #REL'  %{s2'} %{t} %{(or_introl … sil_t)} %{s2''}
478    %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] %
479     [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct
480  | #Hclass_s1' cases l in prf l_noinit l_notau;
481    [ #f #l #prf #_ #_ inversion(is_call_post_label … s1)
482      [ #Hpost cases(simulate_call_pl … good … prf … REL)
483        [2: >Hpost % |3,4: assumption]
484        #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3
485        %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
486        [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
487        % [ /4 by or_introl, conj/ ] /3 by /
488     | #Hpost cases(simulate_call_n … good … prf … REL)
489       [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3
490       *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''}
491       %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
492       % [2: #_ *] % //
493     ]
494   | *
495     [ #prf #_ #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2''
496       * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'}
497       %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} %
498       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
499       % [ % // % // ] * #f * #l #EQ destruct
500     | #l #prf #_ #_ cases(simulate_ret_l … good … prf … REL) [2,3: //]
501       #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3
502       %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} %
503       [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
504       % [ % // % //] * #f * #l #EQ destruct
505    ]
506  | * [ #_ #_ * #H @⊥ @H % ] #lab #prf #_ #_
507    cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1
508    * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe}
509    %{s2'''} %{t3} %
510    [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ]
511    % [% // % //] * #f * #l #EQ destruct
512  | #_ * #H @⊥ @H %
513  ]
514  % //
515]
516qed.
517
518
519theorem simulate_LR_trace :
520∀S : abstract_status.
521∀t : measurable_trace S.
522∀rel : relations S.
523simulation_conditions … rel →
524∀s2 : S.
525match L_pre_state … t with
526[ None ⇒
527   as_classify … s2 ≠ cl_io ∧
528   Srel … rel (L_s1 … t) s2 
529| Some s1 ⇒ Srel … rel s1 s2 ] →
530∃t' : measurable_trace S.
531 L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
532 get_costlabels_of_trace … (trace … t) =
533  get_costlabels_of_trace … (trace … t') ∧
534match L_pre_state … t with
535[ None ⇒ L_s1 … t' = s2
536| Some s1 ⇒
537         ∃ pre_state : S.
538         L_pre_state … t' = Some ? pre_state ∧
539         ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i
540] ∧
541match R_post_state … t with         
542[ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
543| Some s1' ⇒
544          ∃s2' : S. Srel … rel s1' s2' ∧
545          ∃ post_state : S.
546          R_post_state … t' = Some ? post_state ∧
547          ∃tr : raw_trace S post_state s2'. silent_trace … tr
548].
549#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ]
550[2: #REL_pre
551    cut
552     (∃pre_state: S.
553      ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧
554      ∃middle_state: S.
555       as_execute … (L_label … t) pre_state middle_state ∧
556      ∃final_state: S.
557      ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧
558       as_classify … final_state ≠ cl_io ∧
559       Srel … rel (L_s1 … t) final_state)
560    [ lapply(L_init_ok … t) >EQpre normalize nodelta * #Hcost #exe   
561      cases(instr_execute_commute … good … (L_label … t) … exe … REL_pre)
562      [2,3: % #EQ >EQ in Hcost; * |4: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
563      #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall
564      #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % // % //
565      cases sil_t3 [/2 by pre_silent_io/ ] inversion t3
566      [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ]
567      #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125
568      #H @⊥ @H %]
569    * #pre_state * #tr_i * #silent_i * #middle_state * #step_pre_middle
570    * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL
571| #REL
572  cut(bool_to_Prop (as_initial S s2)∧L_label S t=init_act)
573      [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //]
574        @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label
575]
576cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) //
577#fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t)
578[2,4: #post_s2] #EQpost normalize nodelta
579[3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with 
580 [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S
581 |Some (l:ActionLabel)⇒
582  (is_costlabelled_act l∨is_unlabelled_ret_act l)
583  ∧(is_call_act l→is_call_post_label S fin_s2)
584  ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')])
585  [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta
586      [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption
587      |*: #a ** #_ #_ * #x * >EQpost #EQ destruct
588      ]
589  ] #R_label_fin
590|*: cut(∃l.(R_label … t) = Some ? l)
591    [1,3:  lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct]
592          #a #_ %{a} % ] * #final_label #EQfinal_label
593     cut
594      (∃middle_state: S.
595       ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧
596       ∃post_state : S.
597       as_execute … final_label middle_state post_state ∧
598       (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧
599       ∃final_state: S.
600       ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧
601       Srel … rel post_s2 final_state)
602     [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin
603         * >EQpost #EQ destruct #exe
604          cases(instr_execute_commute … good … final_label … exe … REL')
605          [2,3,6,7: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct]
606          |4,8: %1 @tail_of_premeasurable_is_not_io //
607          ]
608          #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL'
609          #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //]
610          % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe'
611     #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel
612]
613[2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)}
614     normalize nodelta /5 by conj/
615|3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)}
616    normalize nodelta [2: % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
617    |3: /3 by append_silent_premeasurable, append_premeasurable_silent/
618    |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/]
619        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //]
620        >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%)));
621        /2 by refl, pair_destruct_1/
622    | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
623      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
624    ]
625| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)}
626  normalize nodelta
627  [ assumption
628  | % // lapply(L_init_ok … t) >EQpre normalize nodelta * //
629  | /4 by append_premeasurable_silent/
630  | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append
631    >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/
632  ]
633| %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)}
634  normalize nodelta
635 [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_
636      % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] //
637 | /2/
638 | /3 by append_silent_premeasurable/
639 | % [2: %{final_state'} /5 by ex_intro, conj/
640 | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%));
641   // ]
642 ]   
643]
644qed.   
645(*
646xxxxxxxxxxxxxxxxxxxx
[3387]647 
[3394]648theorem simulate_LR_trace :
649∀S : abstract_status.
650∀t : measurable_trace S.
651∀rel : relations S.
652simulation_conditions … rel →
653∀s2 : S.
654match L_pre_state … t with
655[ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → 
656         ∃t' : measurable_trace S.L_s1 … t' = s2 ∧
657         L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
658         get_costlabels_of_trace … (trace … t) =
659                      get_costlabels_of_trace … (trace … t') ∧
660         match R_post_state … t with
661         [ None ⇒  Srel … rel (R_s2 … t) (R_s2 … t')
662         | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
663                      ∃post_state : S.
664                      ∃tr : raw_trace S (opt_safe … prf) post_state.
665                      silent_trace … tr ∧ Srel … rel s2' post_state
666         ]
667| Some s1 ⇒ Srel … rel s1 s2 →
668            ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state.
669            silent_trace … tr_i ∧
670            ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧
671            L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧
672            get_costlabels_of_trace … (trace … t) =
673                      get_costlabels_of_trace … (trace … t') ∧
674            match R_post_state … t with         
675            [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t')
676            | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?).
677                         ∃post_state : S.
678                         ∃tr : raw_trace S (opt_safe … prf) post_state.
679                         silent_trace … tr ∧ Srel … rel s2' post_state
680            ]
681].
682#S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ]
683#REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta
684[1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption]
685     #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL
686     [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)}
687         [ inversion(R_label … t) normalize nodelta
688           [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t)
689             >EQnone normalize nodelta * //
690           | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x *
691             >EQpost #EQ destruct
692           ]
693         | normalize nodelta %
694           [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t)
695           >EQpre normalize nodelta * //
696         | /6 by conj/
697         ]
698     | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct]
699       #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 *
700       #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post))
701       [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ]
702         * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) //
703         [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 *
704         ** #sil_t1 #exe' #Hx2 #REL1
705         %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)}
706         [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %]
707           @notb_Prop % #ABS @(as_final_ok … ABS exe')
708         | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ]
709           -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption
710         | /3 by append_silent_premeasurable/
711         | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] %
712           [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption
713         ]
714       | (*go by cases on the instruction executed TODO *) cases daemon
715       ]
716    ]
717|*: cases daemon (*TODO*)
718]
719qed.
[3386]720
721
[3394]722
723
724#L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t
725normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ]
726* [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*:
727
728
729whd in ⊢ (% → ?);
730
731
732
733
[3386]734(*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se
735  non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio
736  il teorema sotto sembra suggerire il merge *)
737
738definition unmovable_entry_label ≝
[3387]739λS : abstract_status.λl.
740match l with
741[ call_act _ _ ⇒ false
742| ret_act _ ⇒ false
743| cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c
744                            | None ⇒ false
745                            ]
746| init_act ⇒ true
747].
[3386]748 
[3387]749definition unmovable_exit_label ≝
750λS : abstract_status.λl.
751match l with
752[ call_act _ _ ⇒ false
753| ret_act _ ⇒ false
754| cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c
755                            | None ⇒ false
756                            ]
757| init_act ⇒ false
758].
[3386]759
[3387]760theorem simulates_LR_raw_trace :
761∀S : abstract_status.
762∀t : LR_raw_trace S.
763∀rel : relations S.
[3389]764simulation_conditions … rel →
[3387]765measurable S t →
[3389]766∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' →
[3387]767∃ t' : LR_raw_trace S.
768measurable S t' ∧
769if as_initial … (LR_s1 … t) ∨ unmovable_entry_label  S (L_label … t) then
770   LR_s1 … t' = s1'
771else
772   ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t')
773∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧
774if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then
775   LR_s2 … t' = s1''
776else
777  ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t')
778
779get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t').
[3389]780#S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL
781cases(simulates_pre_mesurable … (LR_t … t) … REL)
782[2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ]
783#s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1
784inversion(as_initial … (LR_s1 … t)) #Has_initial
785inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry
786inversion(as_final … (LR_s2 … t)) #Has_final
787inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit
788normalize nodelta
789[ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2:
790
791
792
[3387]793qed.
794
795xxxx
796
[3386]797theorem simulates_L_raw_trace:
798 ∀t: L_raw_trace.
799  pre_measurable_trace … (L_t t1) →
800  well_formed_trace … (L_t t1) →
801 ∀s1'.
802   S (L_s1 t) s1' →
803   s1' -flat-→ (L_s1 t2) →
804   ∃s2',t2: L_raw_trace.
805    pre_mesurable_trace … (L_t t2) ∧
806    well_formed_trace … (L_t t2) ∧
807    |t1| = |t2| ∧
808    S (L_s2 t1) s2' ∧
809    (L_s2 t2) -flat-→ s2'.
810 (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e
811       nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *)
812
813
[3383]814(*********************************************************************)
815
[3386]816(* quello che segue tentava di permettere di evitare l'emissione di label
817   associate a codice morto *)
818
[3383]819replace_last x : weak_trace → weak_trace
820   [] ⇒ [], Some x
821 | l::t ⇒
822     let 〈t',x'〉 ≝ replace_last x t in
823     match x' with
824     [ None ⇒ l::t', None
825     | Some x'' ⇒ [], Some x''
826
827theorem simulates:
828 ∀s1,s2. ∀τ1: raw_trace … s1 s2.
829  pre_measurable_trace … t1 →
830  well_formed_trace … t1.
[3382]831 ∀l1: option NonFunctionalLabel.
832 ∀s1'.
833   S s1 s1' →
[3383]834   ∃dead_labels.
[3382]835   ∃s2'. ∃t2: raw_trace … s1' s2'.
836    pre_mesurable_trace … t2 ∧
837    well_formed_trace … t2.
838   ∃l2: option NonFunctionalLabel.
839    match l1 with
840    [ None ⇒
841       match l2 with
842       [ None ⇒ |t1| = |t2|
843       | Some l2' ⇒ |t1| = l2'::|t2| ]
844    | Some l1' ⇒
[3383]845       match l2 with
846       [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1
847       | Some l2' ⇒
848          if |t2| = [] then |t1| = [l1'] ∧ l2' = l1'
849          else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1
850       ]
[3394]851    ]
852    *)
Note: See TracBrowser for help on using the repository browser.