include "Traces.ma". record relations (S : abstract_status) : Type[0] ≝ { Srel: S → S → Prop ; Crel: S → S → Prop }. definition Rrel ≝ λS : abstract_status.λrel : relations S.λs,s' : S. ∀s1,s1'. as_syntactical_succ S s1 s → Crel … rel s1 s1' → as_syntactical_succ S s1' s'. record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝ { initial_is_initial : ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop (as_initial … s1) → bool_to_Prop (as_initial … s2)) ; final_is_final : ∀s1,s2 : S.Srel … rel s1 s2 → (bool_to_Prop(as_final … s1) → bool_to_Prop (as_final … s2)) ; simulate_tau: ∀s1,s2,s1' : S. as_execute … (cost_act (None ?)) s1 s1'→ Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → ∃s2'. ∃t: raw_trace S s2 s2'. Srel … rel s1' s2' ∧ silent_trace … t ; simulate_label: ∀s1,s2,l,s1'. as_execute S (cost_act (Some ? l)) s1 s1' → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → Srel … rel s1 s2 → ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. as_execute … (cost_act (Some ? l)) s2' s2'' ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 ; simulate_call_pl: ∀s1,s2,s1' : S.∀f,l. is_call_post_label … s1 → as_execute … (call_act f l) s1 s1' → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → Srel … rel s1 s2 → ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. as_execute … (call_act f l) s2' s2'' ∧ bool_to_Prop(is_call_post_label … s2') ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 ; simulate_ret_l: ∀s1,s2,s1' : S.∀l. as_execute S (ret_act (Some ? l)) s1 s1' → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → Srel … rel s1 s2 → ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. as_execute … (ret_act (Some ? l)) s2' s2'' ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 ; simulate_call_n: ∀s1,s2,s1' : S.∀f,l. as_execute … (call_act f l) s1 s1' → ¬ is_call_post_label … s1 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → Srel … rel s1 s2 → ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. bool_to_Prop (¬ is_call_post_label … s2') ∧ as_execute … (call_act f l) s2' s2'' ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 ∧ Crel … rel s1 s2' ; simulate_ret_n: ∀s1,s2,s1' : S. as_execute … (ret_act (None ?)) s1 s1' → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → Srel … rel s1 s2 → ∃s2',s2'',s2'''. ∃t1: raw_trace S s2 s2'. as_execute … (ret_act (None ?)) s2' s2'' ∧ ∃t3: raw_trace S s2'' s2'''. Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3 ∧ Rrel … rel s1' s2'' ; simulate_io_in : ∀s1,s2,s1' : S.∀l. as_execute … (cost_act … (Some ? l)) s1 s1' → as_classify … s1 ≠ cl_io → as_classify … s1' = cl_io → Srel … rel s1 s2 → ∃s2',s2'' : S.∃t: raw_trace … s2 s2'. pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2' s2'' ∧ as_classify … s2'' = cl_io ∧ Srel … rel s1' s2'' ; simulate_io_out : ∀s1,s2,s1' : S.∀l. as_execute … (cost_act … (Some ? l)) s1 s1' → as_classify … s1 = cl_io → as_classify … s1' ≠ cl_io → Srel … rel s1 s2 → ∃s2',s2'' : S.∃t : raw_trace … s2' s2''. pre_silent_trace … t ∧ as_execute … (cost_act … (Some ? l)) s2 s2' ∧ as_classify … s2 = cl_io ∧ Srel … rel s1' s2'' }. let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S) (t : raw_trace S st1 st2) on t : list CostLabel ≝ match t with [ t_base st ⇒ [ ] | t_ind st1' st2' st3' l prf t' ⇒ let tl ≝ get_costlabels_of_trace … t' in match l with [ call_act f c ⇒ [ c ] | ret_act x ⇒ match x with [ Some c ⇒ [ a_return_post c ] | None ⇒ [] ] | cost_act x ⇒ match x with [ Some c ⇒ [ a_non_functional_label c ] | None ⇒ [] ] | init_act ⇒ [] ] @ tl ]. lemma append_premeasurable_silent : ∀S : abstract_status. ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. pre_measurable_trace … t → silent_trace … t' → pre_measurable_trace … (t' @ t). #S #st1' #st1 #st2 #t #t' lapply t -t elim t' [ #st #t #Hpre #_ whd in ⊢ (????%); assumption] #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?; [ #s #H1 #EQ1 #EQ2 destruct #EQ destruct] #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ whd in ⊢ (????%); %2 [ assumption | %{(None ?)} % | @IH try assumption ] % assumption qed. lemma pre_silent_is_premeasurable : ∀S : abstract_status. ∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t → pre_measurable_trace … t. #S #st1 #st2 #t elim t [ #st #H inversion H in ⊢ ?; [ #st' #Hst #EQ1 #EQ2 #EQ3 destruct #_ %1 @Hst ] #st' #st'' #st''' #prf #tl #Hst'' #pre_tl #_ #EQ1 #EQ2 #EQ3 destruct ] -t -st1 -st2 #st1 #st2 #st3 #l #prf #tl #IH #H inversion H in ⊢ ?; [ #st #H2 #EQ1 #EQ2 #EQ3 destruct] #st1' #st2' #st3' #prf' #tl' #Hst2' #pre_tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ] @IH assumption qed. lemma append_tind_commute : ∀S : abstract_status.∀st1,st2,st3,st4 : S.∀l. ∀prf : as_execute … l st1 st2. ∀t1 : raw_trace S st2 st3. ∀t2 : raw_trace S st3 st4.t_ind … prf (t1 @ t2) = (t_ind … prf t1) @ t2. #S #st1 #st2 #st3 #st4 #l #prf #t1 #t2 % qed. lemma append_silent_premeasurable : ∀S : abstract_status. ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. pre_measurable_trace … t' → silent_trace … t → pre_measurable_trace … (t' @ t). #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht' [ #st #Hst #r * [ #H1 @pre_silent_is_premeasurable assumption ] inversion r [2: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 cases H11 #ABS @⊥ @ABS % ] #s' #EQ1 #EQ2 #EQ3 destruct #_ %1 assumption |2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ] try ( %{x} %) try @IH try assumption % ] #s1 #s2 #s3 #s4 #s5 #l1 #l2 #pr1 #t1 #t2 #prf2 #Hs1 #Hs3 * #f * #l1' #EQ destruct #Hpost_s1 #pre_t1 #pre_t2 #Hs1_s4 #EQ destruct #IH1 #IH2 #r #pre_r normalize >append_tind_commute >append_tind_commute >append_associative (Hclass1 I) % #EQ destruct] @IH try assumption #_ assumption qed.*) (* lemma well_formed_append : ∀S : abstract_status. ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. well_formed_trace … (t1 @ t2) → well_formed_trace … t1 ∧ well_formed_trace … t2. #S #st1 #st2 #st3 #t1 #t2 #H % [ lapply H -H lapply t2 -t2 elim t1 [ //] #st1' #st2' #st3' #l #exe #tl #IH #r #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 #EQ3 normalize in EQ3; destruct ] #st1'' #st2'' #st3'' #l' #prf' #tl' #wf_tl' [#Hst1'' | * #x #EQ destruct] #_ #EQ1 #EQ2 normalize in ⊢ (% → ?); #EQ3 destruct #_ [ %2 [ @IH assumption ] assumption | %3 [ @IH assumption ] %{x} % ] ] lapply H lapply t2 -t2 elim t1 [ #st #r normalize //] #s1 #s2 #s3 #l #prf #tl #IH #r #H inversion H in ⊢ ?; [ #st #EQ1 #EQ2 normalize #EQ3 destruct ] #s1' #s2' #s3' #l' #prf' #tl' #wf_tl' #Hs1' #_ normalize #EQ1 #EQ2 #EQ3 destruct #_ @IH assumption qed. lemma append_well_formed : ∀S : abstract_status. ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. well_formed_trace … t1 → well_formed_trace … t2 → well_formed_trace … (t1 @ t2). #S #st1 #st2 #st3 #t1 #t2 #H lapply t2 -t2 elim H [ #st #r #H1 @H1 ] #s1 #s2 #s3 #l #prf #tl #wf_tl #Hs1 #IH #r #wf_r normalize [ %2 | %3] try @IH assumption qed. (* lemma silent_is_well_formed : ∀S : abstract_status. ∀st1,st2 : S.∀t : raw_trace … st1 st2.silent_trace … t → well_formed_trace … t. #S #st1 #st2 #t elim t [ #st #_ %] #s1 #s2 #s3 #l #prf #tl #IH * #H inversion H [ #st #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #Hs2' #tl' #_ #EQ1 #EQ2 #EQ3 destruct #_ #H1 %2 [ @IH % [2: #_ ] assumption | >(H1 I) % #EQ destruct] qed. *) *) lemma get_cost_label_invariant_for_append_silent_trace_l :∀S : abstract_status. ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. silent_trace … t1 → get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2. #S #st1 #st2 #st3 #t1 elim t1 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 * [2: whd in match is_trace_non_empty; normalize nodelta * #ABS @⊥ @ABS %] #H inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct] #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct #_ whd in ⊢ (??%?); >IH [%] %1 assumption qed. lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S. ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3. get_costlabels_of_trace … (t1 @ t2) = append … (get_costlabels_of_trace … t1) (get_costlabels_of_trace … t2). #S #st1 #st2 #st3 #t1 elim t1 [ #st #t2 % ] #st1' #st2' #st3' * [#f * #l | * [| * #l] | * [| #l] |] #prf #tl #IH #t2 normalize try @eq_f @IH qed. (* lemma raw_trace_ind_r : ∀S : abstract_status. ∀P : (∀st1,st2.raw_trace S st1 st2 → Prop). (∀st : S.P … (t_base … st)) → (∀st1,st2,st3,l. ∀prf : as_execute S l st2 st3. ∀tl : raw_trace S st1 st2. P … tl → P … (tl @ (t_ind … prf … (t_base … st3)))) → ∀st1,st2 : S.∀t : raw_trace S st1 st2.P … t. #S #P #base #ind #st1 #st2 #t elim t [ assumption] #st1 #st2 #st3 #l #prf #raw #IH *) lemma head_of_premeasurable_is_not_io : ∀S : abstract_status. ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → as_classify … st1 ≠ cl_io. #S #st1 #st2 #t #H inversion H // qed. theorem simulates_pre_mesurable: ∀S : abstract_status.∀rel : relations S. ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. simulation_conditions S rel → pre_measurable_trace … t1 → ∀s2 : S. as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → ∃s2'. ∃t2: raw_trace … s2 s2'. pre_measurable_trace … t2 ∧ get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ Srel … rel s1' s2'. #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)} /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/ | #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct #pre_measurable_tl #IH #s2 #classify_s2 #REL [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2'' #silent_ts2'' cases(IH … RELst2s2'') [2: cases silent_ts2'' /2 by pre_silent_io/ inversion t_s2'' [ #x #EQ1 #EQ2 #EQ3 destruct // ] #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct * #ABS @⊥ @ABS % ] #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3 %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/ whd in ⊢ (??%?); /2/ | cases(simulate_label … good … execute … REL) [2,3: /2/] #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2'''' #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by pre_silent_io/ #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3} %{(t_s2'' @ (t_ind … exe_s2''' …))} [ @(t_s2'''' @ t_s3) ] % [2: assumption] % [ @append_premeasurable_silent // %2 /2 by ex_intro/ [ cases sil_ts2'' [/2 by pre_silent_io/ ] inversion t_s2'' [ #H31 #H32 #H33 #H34 #H35 destruct assumption ] #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct cases H47 #ABS @⊥ @ABS % ] @append_premeasurable_silent // % // | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l [2: assumption] whd in ⊢ (???%); >get_cost_label_invariant_for_append_silent_trace_l // ] ] % assumption | #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ) #pre_meas_tl #IH #s2 #class_s2 #RELst1s2 cases(simulate_ret_l … good … exe_s2_s2' … RELst1s2) [2,3: /2/ ] #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2''' #sil_t1 #sil_t2 cases(IH … rel_s2_s2''') [2: @(pre_silent_io … sil_t2) assumption] #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % [2: whd in ⊢ (??%?); >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) whd in ⊢ (???%); >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) @eq_f assumption ] @append_premeasurable_silent [2: //] %3 [2,3: /3 by append_premeasurable_silent, ex_intro, or_introl/ ] cases sil_t1 [ /2 by pre_silent_io/ ] inversion t1 [ #H49 #H50 #H51 #H52 #H53 destruct //] #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 destruct cases H65 #ABS @⊥ @ABS % | #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2' cases(simulate_call_pl … good … post … exe_s1_s2 … REL_s1_s2') [2,3: /2 by head_of_premeasurable_is_not_io/ ] #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2 cases(IH … REL) [2: /2 by pre_silent_io/ ] #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % [2: whd in ⊢ (??%?); >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) whd in ⊢ (???%); >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) @eq_f assumption ] @append_premeasurable_silent try assumption %4 try assumption [ cases sil_t1 [/2 by pre_silent_io/ ] inversion t1 [#H67 #H68 #H69 #H70 #H71 destruct //] #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 destruct cases H83 #ABS @⊥ @ABS % | whd %{f} %{lab} % | @append_premeasurable_silent // % assumption ] | #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * #f * #l #EQ destruct #Hst1 #pre_t1 #pre_t2 #succ_14 whd in ⊢ (% → ?); #EQ destruct #IH1 #IH2 #st1' #Hst1' #REL cases(simulate_call_n … good … exe_12 … Hst1 … REL) [2,3: /2/ ] #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1 #sil_tr2 #call_rel cases(IH1 … REL1) [2: /2 by pre_silent_io/ ] #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2 cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ] #st3'' * #st4' * #st4'' * #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ] #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'} %{(tr1 @ (t_ind … exe_12' … ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} % [2: assumption] % [ @append_premeasurable_silent try assumption %5 [1,2: /2 by pre_silent_io/ cases sil_tr1 /2 by pre_silent_io/ inversion tr1 [ #H85 #H86 #H87 #H88 #H89 destruct // ] #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 destruct cases H107 #ABS @⊥ @ABS % | whd %{f} %{l} % | assumption | @append_premeasurable_silent try assumption [2: % //] @append_silent_premeasurable // % // | @append_premeasurable_silent try assumption | @(RET_REL … call_rel) assumption | % ] | >get_cost_label_invariant_for_append_silent_trace_l [2: // ] whd in ⊢ (??%%); @eq_f >append_associative >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); [2: % // ] >append_associative >get_cost_label_append in ⊢ (???%); >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); [2: % //] normalize >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2 assumption ] % // ] qed. (* IDEA: aggiungere stati di I/O e cambiare la semantica del linguaggio sorgente; aggiungere nella pre_measurable il vincolo nessuno stato e' di I/O; cambiare la definizione di traccia tornando a una sola etichetta sugli archi *) (* measurable fattorizzata sotto come measurable' definition measurable ≝ λL,s1,s2.λt: raw_trace … s1 s2. ∃L',s0,so. as_execute … s0 s1 L ∧ pre_measurable_trace … t ∧ well_formed_trace … t ∧ as_execute … s2 so L'. *) record measurable_trace (S : abstract_status) : Type[0] ≝ { L_label: ActionLabel ; R_label : option ActionLabel ; L_pre_state : option S ; L_s1 : S ; R_s2: S ; R_post_state : option S ; trace : raw_trace S L_s1 R_s2 ; pre_meas : pre_measurable_trace … trace ; L_init_ok : match L_pre_state with [ None ⇒ bool_to_Prop(as_initial … L_s1) ∧ L_label = init_act | Some s ⇒ is_costlabelled_act L_label ∧ as_execute … L_label s L_s1 ] ; R_fin_ok : match R_label with [ None ⇒ bool_to_Prop (as_final … R_s2) ∧ R_post_state = None ? | Some l ⇒ (is_costlabelled_act l ∨ is_unlabelled_ret_act l) ∧ (is_call_act l → bool_to_Prop (is_call_post_label … R_s2)) ∧ ∃ s'.R_post_state = Some ? s' ∧ as_execute … l R_s2 s' ] }. lemma cl_io_case : ∀P : status_class → Prop. P cl_io → (∀x.x≠cl_io → P x) → ∀s.P s. #P #H1 #H2 * // @H2 % #EQ destruct qed. lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io). * [2: %%] %2 % #EQ destruct qed. lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status. ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → as_classify … st2 ≠ cl_io. #S #st1 #st2 #t #H elim H // qed. lemma get_cost_label_silent_is_empty : ∀S : abstract_status. ∀st1,st2.∀t : raw_trace S st1 st2.silent_trace … t → get_costlabels_of_trace … t = [ ]. #S #st1 #st2 #t elim t [//] #s1 #s2 #s3 #l #prf #tl #IH * [2: * #ABS @⊥ @ABS % ] #H inversion H [#s #cl #EQ1 #EQ2 #EQ3 destruct] #s1' #s2' #s3' #prf' #tl' #cl' #Htl #_ #EQ1 #EQ2 #EQ3 destruct #_ @IH % assumption qed. lemma get_cost_label_invariant_for_append_silent_trace_r :∀S : abstract_status. ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. silent_trace … t2 → get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t1. #S #st1 #st2 #st3 #t1 #t2 #H >get_cost_label_append >(get_cost_label_silent_is_empty … H) // qed. lemma instr_execute_commute : ∀S :abstract_status. ∀rel : relations S. simulation_conditions … rel → ∀s1,s1': S.∀l.l ≠ init_act → l ≠ cost_act (None ?) → as_execute S l s1 s1' → (as_classify … s1 ≠ cl_io ∨ as_classify … s1' ≠ cl_io) → ∀s2. Srel … rel s1 s2 → ∃s2' : S.∃tr : raw_trace S s2 s2'.silent_trace … tr ∧ ∃s2'' : S.as_execute S l s2' s2'' ∧ ∃s2''' : S. ∃tr' : raw_trace S s2'' s2'''. silent_trace … tr' ∧ Srel … rel s1' s2''' ∧ (is_call_act l → is_call_post_label … s1 → is_call_post_label … s2') ∧ (as_classify … s1' ≠ cl_io → as_classify … s2'' ≠ cl_io). #S #rel #good #s1 #s1' #l #l_noinit #l_notau #prf #HIO #s2 #REL cases(case_cl_io … (as_classify … s1)) [ #EQs1_io cases(io_exiting … EQs1_io … prf) #lab #EQ destruct(EQ) cases HIO [ >EQs1_io * #EQ @⊥ @EQ % ] #Hio_s1' cases(simulate_io_out … good … prf … EQs1_io Hio_s1' … REL) #s2' * #s2'' * #t *** #sil_t #prf' #class_io #REL' %{s2} %{(t_base …)} % [ %2 % * ] %{s2'} % // %{s2''} %{t} % [2: #_ @(head_of_premeasurable_is_not_io … t) @pre_silent_is_premeasurable assumption ] % [ %// % // ] * #f * #l #EQ destruct | #Hclass_s1 cases(case_cl_io … (as_classify … s1')) [ #EQs1' cases(io_entering … EQs1' … prf) #l1 #EQ destruct(EQ) cases(simulate_io_in … good … prf … Hclass_s1 EQs1' … REL) #s2' * #s2'' * #t *** #sil_t #exe #Hclass_s2'' #REL' %{s2'} %{t} %{(or_introl … sil_t)} %{s2''} %{exe} %{s2''} %{(t_base …)} % [2: >EQs1' * #H @⊥ @H % ] % [ /4 by or_intror, conj, nmk/] * #f * #l #EQ destruct | #Hclass_s1' cases l in prf l_noinit l_notau; [ #f #l #prf #_ #_ inversion(is_call_post_label … s1) [ #Hpost cases(simulate_call_pl … good … prf … REL) [2: >Hpost % |3,4: assumption] #s2' * #s2'' * #s2''' * #t1 ** #exe #Hpost' * #t3 * * #REL #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ] % [ /4 by or_introl, conj/ ] /3 by / | #Hpost cases(simulate_call_n … good … prf … REL) [2: >Hpost % |3,4: // ] #s2' * #s2'' * #s2''' * #t1 ** #Hpost' #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ] % [2: #_ *] % // ] | * [ #prf #_ #_ cases(simulate_ret_n … good … prf … REL) [2,3: //] #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 *** #REL' #sil_t1 #sil_t3 #_ %{s2'} %{t1} %{(or_introl … sil_t1)} %{s2''} %{exe} %{s2'''} %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ] % [ % // % // ] * #f * #l #EQ destruct | #l #prf #_ #_ cases(simulate_ret_l … good … prf … REL) [2,3: //] #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ] % [ % // % //] * #f * #l #EQ destruct ] | * [ #_ #_ * #H @⊥ @H % ] #lab #prf #_ #_ cases(simulate_label … prf … REL) [2,3,4: // ] #s2' * #s2'' * #s2''' * #t1 * #exe * #t3 ** #REL' #sil_t1 #sil_t3 %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % [2: #_ @(head_of_premeasurable_is_not_io … t3) /2 by pre_silent_is_premeasurable/ ] % [% // % //] * #f * #l #EQ destruct | #_ * #H @⊥ @H % ] % // ] qed. theorem simulate_LR_trace : ∀S : abstract_status. ∀t : measurable_trace S. ∀rel : relations S. simulation_conditions … rel → ∀s2 : S. match L_pre_state … t with [ None ⇒ as_classify … s2 ≠ cl_io ∧ Srel … rel (L_s1 … t) s2 | Some s1 ⇒ Srel … rel s1 s2 ] → ∃t' : measurable_trace S. L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ get_costlabels_of_trace … (trace … t) = get_costlabels_of_trace … (trace … t') ∧ match L_pre_state … t with [ None ⇒ L_s1 … t' = s2 | Some s1 ⇒ ∃ pre_state : S. L_pre_state … t' = Some ? pre_state ∧ ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ] ∧ match R_post_state … t with [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') | Some s1' ⇒ ∃s2' : S. Srel … rel s1' s2' ∧ ∃ post_state : S. R_post_state … t' = Some ? post_state ∧ ∃tr : raw_trace S post_state s2'. silent_trace … tr ]. #S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [* #Hclass_s2 ] [2: #REL_pre cut (∃pre_state: S. ∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧ ∃middle_state: S. as_execute … (L_label … t) pre_state middle_state ∧ ∃final_state: S. ∃tr_i2: raw_trace S middle_state final_state. silent_trace … tr_i2 ∧ as_classify … final_state ≠ cl_io ∧ Srel … rel (L_s1 … t) final_state) [ lapply(L_init_ok … t) >EQpre normalize nodelta * #Hcost #exe cases(instr_execute_commute … good … (L_label … t) … exe … REL_pre) [2,3: % #EQ >EQ in Hcost; * |4: %2 @(head_of_premeasurable_is_not_io … (pre_meas … t)) ] #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} %{exe} %{s2'''} %{t3} % // % // cases sil_t3 [/2 by pre_silent_io/ ] inversion t3 [ #H109 #H110 #H111 #H112 #H113 destruct @Hclass @(head_of_premeasurable_is_not_io … (pre_meas … t)) ] #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 cases H125 #H @⊥ @H %] * #pre_state * #tr_i * #silent_i * #middle_state * #step_pre_middle * #final_state * #tr_i2 ** #silent_i2 #final_not_io #REL | #REL cut(bool_to_Prop (as_initial S s2)∧L_label S t=init_act) [ lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: //] @(initial_is_initial … good … H1) assumption ] * #initial_s2 #init_label ] cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) // #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL' inversion(R_post_state … t) [2,4: #post_s2] #EQpost normalize nodelta [3,4: cut (match R_label S t in option return λ_:(option ActionLabel).Prop with  [None⇒bool_to_Prop (as_final S fin_s2)∧None S=None S |Some (l:ActionLabel)⇒ (is_costlabelled_act l∨is_unlabelled_ret_act l) ∧(is_call_act l→is_call_post_label S fin_s2) ∧(∃s':S.None S=Some S s'∧as_execute S l fin_s2 s')]) [1,3: lapply(R_fin_ok … t) cases(R_label … t) normalize nodelta [1,3: * #H1 #H2 % [2,4: //] @(final_is_final … good … H1) assumption |*: #a ** #_ #_ * #x * >EQpost #EQ destruct ] ] #R_label_fin |*: cut(∃l.(R_label … t) = Some ? l) [1,3: lapply(R_fin_ok … t) cases(R_label… t) normalize nodelta [1,3: >EQpost * #_ #EQ destruct] #a #_ %{a} % ] * #final_label #EQfinal_label cut (∃middle_state: S. ∃tr : raw_trace S fin_s2 middle_state. silent_trace … tr ∧ ∃post_state : S. as_execute … final_label middle_state post_state ∧ (is_call_act final_label → bool_to_Prop (is_call_post_label … middle_state)) ∧ ∃final_state: S. ∃tr_f2: raw_trace S post_state final_state. silent_trace … tr_f2 ∧ Srel … rel post_s2 final_state) [1,3: lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H1 #H2 * #sfin * >EQpost #EQ destruct #exe cases(instr_execute_commute … good … final_label … exe … REL') [2,3,6,7: % #EQ destruct cases H1 [1,3,5,7: * |*: normalize #EQ destruct] |4,8: %1 @tail_of_premeasurable_is_not_io // ] #s2' * #t1 * #sil_t1 * #s2'' * #exe * #s2''' * #t3 *** #sil_t3 #REL' #Hcall #Hclass %{s2'} %{t1} %{sil_t1} %{s2''} % [2,4: %{s2'''} %{t3} % //] % // #H @Hcall // @H2 // ] * #middle_state' * #tr' * #sil_tr' * #post_state' ** #exe' #Hcall * #final_state' * #tr_f2 * #sil_tr_f2 #fin_rel ] [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (None ?) … pre_meas_t' …)} normalize nodelta /5 by conj/ |3: %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (Some ? post_state') … (tr_i2 @ t' @ tr') …)} normalize nodelta [2: % // lapply(L_init_ok … t) >EQpre normalize nodelta * // |3: /3 by append_silent_premeasurable, append_premeasurable_silent/ |4: % [2: %{final_state'} /5 by ex_intro, conj/ ] % /8 by ex_intro, conj/ % [ /3 by conj/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???(???%))); /2 by refl, pair_destruct_1/ | lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_ % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] // ] | %{(mk_measurable_trace … (L_label … t) (R_label … t) … (Some ? pre_state) … (None ?) … (tr_i2 @ t') …)} normalize nodelta [ assumption | % // lapply(L_init_ok … t) >EQpre normalize nodelta * // | /4 by append_premeasurable_silent/ | % // % [2: %{pre_state} /3/ ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???%); [2: //] /2 by refl, pair_destruct_1/ ] | %{(mk_measurable_trace … (L_label … t) (R_label … t) … (None ?) … (Some ? post_state') … (t' @ tr') …)} normalize nodelta [ lapply(R_fin_ok … t) >EQfinal_label normalize nodelta ** #H #_ #_ % [2: /3 by ex_intro, conj/ ] % [2: @Hcall ] // | /2/ | /3 by append_silent_premeasurable/ | % [2: %{final_state'} /5 by ex_intro, conj/ | % [2: % ] % [ /2/] >get_cost_label_append >get_cost_label_silent_is_empty in ⊢ (???(???%)); // ] ] ] qed. (* xxxxxxxxxxxxxxxxxxxx theorem simulate_LR_trace : ∀S : abstract_status. ∀t : measurable_trace S. ∀rel : relations S. simulation_conditions … rel → ∀s2 : S. match L_pre_state … t with [ None ⇒ as_classify … s2 ≠ cl_io → Srel … rel (L_s1 … t) s2 → ∃t' : measurable_trace S.L_s1 … t' = s2 ∧ L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ get_costlabels_of_trace … (trace … t) = get_costlabels_of_trace … (trace … t') ∧ match R_post_state … t with [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?). ∃post_state : S. ∃tr : raw_trace S (opt_safe … prf) post_state. silent_trace … tr ∧ Srel … rel s2' post_state ] | Some s1 ⇒ Srel … rel s1 s2 → ∃ pre_state : S.∃tr_i : raw_trace S s2 pre_state. silent_trace … tr_i ∧ ∃t' : measurable_trace S.L_pre_state … t' = Some ? pre_state ∧ L_label … t = L_label … t' ∧ R_label … t = R_label … t' ∧ get_costlabels_of_trace … (trace … t) = get_costlabels_of_trace … (trace … t') ∧ match R_post_state … t with [ None ⇒ Srel … rel (R_s2 … t) (R_s2 … t') | Some s2' ⇒ ∃prf : (R_post_state … t' ≠ None ?). ∃post_state : S. ∃tr : raw_trace S (opt_safe … prf) post_state. silent_trace … tr ∧ Srel … rel s2' post_state ] ]. #S #t #rel #good #s2 inversion(L_pre_state … t) [| #pre_s1] #EQpre normalize nodelta [ #Hclass_s2 ] #REL inversion(R_post_state … t) [2,4: #post_s2 ] #EQpost normalize nodelta [1,3: cases(simulates_pre_mesurable … good … (pre_meas … t) … REL) [2,4: assumption] #fin_s2 * #t' ** #pre_meas_t' #EQcost #REL [2: %{(mk_measurable_trace … (L_label … t) (R_label … t) (None ?) … (None ?) … pre_meas_t' …)} [ inversion(R_label … t) normalize nodelta [ #EQnone % // cases(final_is_final … good … REL) #H #_ @H lapply(R_fin_ok … t) >EQnone normalize nodelta * // | #r_lab #EQr_lab lapply(R_fin_ok … t) >EQr_lab normalize nodelta * #_ * #x * >EQpost #EQ destruct ] | normalize nodelta % [ -REL cases(initial_is_initial … good … REL) #H #_ @H ] lapply(L_init_ok … t) >EQpre normalize nodelta * // | /6 by conj/ ] | lapply(R_fin_ok … t) inversion(R_label … t) [ #_ normalize nodelta * #_ >EQpost #EQ destruct] #post_lab #EQpost_lab normalize nodelta *** #Hfin #Hpost_lab1 #Hpost_lab2 * #s2_post * >EQpost #EQ destruct(EQ) #exe cases(case_cl_io … (as_classify … s2_post)) [ #Hio lapply(io_entering … Hio … exe) [ /3 by pre_meas, tail_of_premeasurable_is_not_io/ ] * #c #EQ destruct(EQ) cases(simulate_io_in … good … exe … REL) // [2: /3 by pre_meas, tail_of_premeasurable_is_not_io/] #x1 * #x2 * #t1 * ** #sil_t1 #exe' #Hx2 #REL1 %{(mk_measurable_trace … (L_label … t) (Some ? (cost_act (Some ? c))) (None ?) … (Some ? x2) … (t'@t1) …)} [ normalize nodelta % [2: %{x2} % //] % [2: * #x3 * #x4 #EQ destruct] % [2: % %] @notb_Prop % #ABS @(as_final_ok … ABS exe') | normalize nodelta lapply(L_init_ok … t) >EQpre normalize nodelta * #H1 #H2 % [2: // ] -REL cases(initial_is_initial … good … REL) #H3 #_ @H3 assumption | /3 by append_silent_premeasurable/ | % [2: % [ % #EQ destruct] whd in match (opt_safe ???); assumption] % [% // % // ] >get_cost_label_invariant_for_append_silent_trace_r assumption ] | (*go by cases on the instruction executed TODO *) cases daemon ] ] |*: cases daemon (*TODO*) ] qed. #L_label * [| #R_label] * [2,4: #pre_s1] #L_s1 #R_s2 * [2,4,6,8: #post_s2] #t #pre_meas_t normalize nodelta * [1,2,5,6: * ] #Hinitial [1,2,3,4: #Hcost #pre_exe |*: #EQ destruct(EQ) ] * [2,4,6,8: ** ] #Hfinal [5,6,7,8: #EQ destruct(EQ) |*: whd in ⊢ (% → ?); (*CSC: oppure fare il merge di L_raw_trace e measurable in un'unico record se non c'e' nulla di interessante sulle L_raw_trace non measurabili. Per esempio il teorema sotto sembra suggerire il merge *) definition unmovable_entry_label ≝ λS : abstract_status.λl. match l with [ call_act _ _ ⇒ false | ret_act _ ⇒ false | cost_act x ⇒ match x with [Some c ⇒ is_io_exiting S c | None ⇒ false ] | init_act ⇒ true ]. definition unmovable_exit_label ≝ λS : abstract_status.λl. match l with [ call_act _ _ ⇒ false | ret_act _ ⇒ false | cost_act x ⇒ match x with [Some c ⇒ is_io_entering S c | None ⇒ false ] | init_act ⇒ false ]. theorem simulates_LR_raw_trace : ∀S : abstract_status. ∀t : LR_raw_trace S. ∀rel : relations S. simulation_conditions … rel → measurable S t → ∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' → ∃ t' : LR_raw_trace S. measurable S t' ∧ if as_initial … (LR_s1 … t) ∨ unmovable_entry_label S (L_label … t) then LR_s1 … t' = s1' else ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t') ∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧ if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then LR_s2 … t' = s1'' else ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t') ∧ get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). #S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL cases(simulates_pre_mesurable … (LR_t … t) … REL) [2: @good |3: @pre_t |4: @wf_t |5: @Hs1' ] #s2 * #t2 *** #pre_t2 #wf_t2 #EQcost #REL1 inversion(as_initial … (LR_s1 … t)) #Has_initial inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry inversion(as_final … (LR_s2 … t)) #Has_final inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit normalize nodelta [ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2: qed. xxxx theorem simulates_L_raw_trace: ∀t: L_raw_trace. pre_measurable_trace … (L_t t1) → well_formed_trace … (L_t t1) → ∀s1'. S (L_s1 t) s1' → s1' -flat-→ (L_s1 t2) → ∃s2',t2: L_raw_trace. pre_mesurable_trace … (L_t t2) ∧ well_formed_trace … (L_t t2) ∧ |t1| = |t2| ∧ S (L_s2 t1) s2' ∧ (L_s2 t2) -flat-→ s2'. (* o, nel caso in cui (L_label t1) e' unmovable_entry_label nessuna coda prefissa e nel caso in cui ??? e' unmovable_exit_label, nessuna coda suffissa *) (*********************************************************************) (* quello che segue tentava di permettere di evitare l'emissione di label associate a codice morto *) replace_last x : weak_trace → weak_trace [] ⇒ [], Some x | l::t ⇒ let 〈t',x'〉 ≝ replace_last x t in match x' with [ None ⇒ l::t', None | Some x'' ⇒ [], Some x'' theorem simulates: ∀s1,s2. ∀τ1: raw_trace … s1 s2. pre_measurable_trace … t1 → well_formed_trace … t1. ∀l1: option NonFunctionalLabel. ∀s1'. S s1 s1' → ∃dead_labels. ∃s2'. ∃t2: raw_trace … s1' s2'. pre_mesurable_trace … t2 ∧ well_formed_trace … t2. ∃l2: option NonFunctionalLabel. match l1 with [ None ⇒ match l2 with [ None ⇒ |t1| = |t2| | Some l2' ⇒ |t1| = l2'::|t2| ] | Some l1' ⇒ match l2 with [ None ⇒ |t1| = replace_last l1' |t2| ∧ ends_with l1' t1 | Some l2' ⇒ if |t2| = [] then |t1| = [l1'] ∧ l2' = l1' else |t1| = l2' :: replace_last l1' |t2| ∧ ends_with l1' t1 ] ] *)