| 1 | include "Common.ma". |
|---|
| 2 | include "Traces.ma". |
|---|
| 3 | |
|---|
| 4 | record relations (S : abstract_status) : Type[0] ≝ |
|---|
| 5 | { Srel: S → S → Prop |
|---|
| 6 | ; Crel: S → S → Prop |
|---|
| 7 | }. |
|---|
| 8 | |
|---|
| 9 | definition 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 | |
|---|
| 12 | record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝ |
|---|
| 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: |
|---|
| 18 | ∀s1,s2,s1' : S. |
|---|
| 19 | as_execute … (cost_act (None ?)) s1 s1'→ |
|---|
| 20 | Srel … rel s1 s2 → as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → |
|---|
| 21 | ∃s2'. ∃t: raw_trace S s2 s2'. |
|---|
| 22 | Srel … rel s1' s2' ∧ silent_trace … t |
|---|
| 23 | ; simulate_label: |
|---|
| 24 | ∀s1,s2,l,s1'. |
|---|
| 25 | as_execute S (cost_act (Some ? l)) s1 s1' → |
|---|
| 26 | as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → |
|---|
| 27 | Srel … rel s1 s2 → |
|---|
| 28 | ∃s2',s2'',s2'''. |
|---|
| 29 | ∃t1: raw_trace S s2 s2'. |
|---|
| 30 | as_execute … (cost_act (Some ? l)) s2' s2'' ∧ |
|---|
| 31 | ∃t3: raw_trace S s2'' s2'''. |
|---|
| 32 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 |
|---|
| 33 | ; simulate_call_pl: |
|---|
| 34 | ∀s1,s2,s1' : S.∀f,l. |
|---|
| 35 | is_call_post_label … s1 → |
|---|
| 36 | as_execute … (call_act f l) s1 s1' → |
|---|
| 37 | as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → |
|---|
| 38 | Srel … rel s1 s2 → |
|---|
| 39 | ∃s2',s2'',s2'''. |
|---|
| 40 | ∃t1: raw_trace S s2 s2'. |
|---|
| 41 | as_execute … (call_act f l) s2' s2'' ∧ |
|---|
| 42 | bool_to_Prop(is_call_post_label … s2') ∧ |
|---|
| 43 | ∃t3: raw_trace S s2'' s2'''. |
|---|
| 44 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 |
|---|
| 45 | ; simulate_ret_l: |
|---|
| 46 | ∀s1,s2,s1' : S.∀l. |
|---|
| 47 | as_execute S (ret_act (Some ? l)) s1 s1' → |
|---|
| 48 | as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → |
|---|
| 49 | Srel … rel s1 s2 → |
|---|
| 50 | ∃s2',s2'',s2'''. |
|---|
| 51 | ∃t1: raw_trace S s2 s2'. |
|---|
| 52 | as_execute … (ret_act (Some ? l)) s2' s2'' ∧ |
|---|
| 53 | ∃t3: raw_trace S s2'' s2'''. |
|---|
| 54 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_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 | as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → |
|---|
| 60 | Srel … rel s1 s2 → |
|---|
| 61 | ∃s2',s2'',s2'''. |
|---|
| 62 | ∃t1: raw_trace S s2 s2'. |
|---|
| 63 | bool_to_Prop (¬ is_call_post_label … s2') ∧ |
|---|
| 64 | as_execute … (call_act f l) s2' s2'' ∧ |
|---|
| 65 | ∃t3: raw_trace S s2'' s2'''. |
|---|
| 66 | Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_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 | as_classify … s1 ≠ cl_io → as_classify … s1' ≠ cl_io → |
|---|
| 72 | Srel … rel s1 s2 → |
|---|
| 73 | ∃s2',s2'',s2'''. |
|---|
| 74 | ∃t1: raw_trace S s2 s2'. |
|---|
| 75 | as_execute … (ret_act (None ?)) s2' s2'' ∧ |
|---|
| 76 | ∃t3: raw_trace S s2'' s2'''. |
|---|
| 77 | Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3 |
|---|
| 78 | ∧ Rrel … rel s1' s2'' |
|---|
| 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'' |
|---|
| 95 | }. |
|---|
| 96 | |
|---|
| 97 | let rec get_costlabels_of_trace (S : abstract_status) (st1 : S) (st2 : S) |
|---|
| 98 | (t : raw_trace S st1 st2) on t : list CostLabel ≝ |
|---|
| 99 | match 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 |
|---|
| 104 | [ call_act f c ⇒ [ c ] |
|---|
| 105 | | ret_act x ⇒ match x with |
|---|
| 106 | [ Some c ⇒ [ a_return_post c ] |
|---|
| 107 | | None ⇒ [] |
|---|
| 108 | ] |
|---|
| 109 | | cost_act x ⇒ match x with |
|---|
| 110 | [ Some c ⇒ [ a_non_functional_label c ] |
|---|
| 111 | | None ⇒ [] |
|---|
| 112 | ] |
|---|
| 113 | | init_act ⇒ [] |
|---|
| 114 | ] @ tl |
|---|
| 115 | ]. |
|---|
| 116 | |
|---|
| 117 | |
|---|
| 118 | lemma append_premeasurable_silent : ∀S : abstract_status. |
|---|
| 119 | ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. |
|---|
| 120 | pre_measurable_trace … t → silent_trace … t' → |
|---|
| 121 | pre_measurable_trace … (t' @ t). |
|---|
| 122 | #S #st1' #st1 #st2 #t #t' lapply t -t elim t' |
|---|
| 123 | [ #st #t #Hpre #_ whd in ⊢ (????%); assumption] |
|---|
| 124 | #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?; |
|---|
| 125 | [ #s #H1 #EQ1 #EQ2 destruct #EQ destruct] |
|---|
| 126 | #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 |
|---|
| 127 | destruct #_ whd in ⊢ (????%); %2 |
|---|
| 128 | [ assumption |
|---|
| 129 | | %{(None ?)} % |
|---|
| 130 | | @IH try assumption |
|---|
| 131 | ] |
|---|
| 132 | % assumption |
|---|
| 133 | qed. |
|---|
| 134 | |
|---|
| 135 | lemma pre_silent_is_premeasurable : ∀S : abstract_status. |
|---|
| 136 | ∀st1,st2 : S. ∀t : raw_trace S st1 st2.pre_silent_trace … t |
|---|
| 137 | → pre_measurable_trace … t. |
|---|
| 138 | #S #st1 #st2 #t elim t |
|---|
| 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' |
|---|
| 143 | #_ #EQ1 #EQ2 #EQ3 destruct #_ %2 [ assumption | whd %{(None ?)} % ] |
|---|
| 144 | @IH assumption |
|---|
| 145 | qed. |
|---|
| 146 | |
|---|
| 147 | lemma 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 | |
|---|
| 152 | lemma append_silent_premeasurable : ∀S : abstract_status. |
|---|
| 153 | ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. |
|---|
| 154 | pre_measurable_trace … t' → silent_trace … t → |
|---|
| 155 | pre_measurable_trace … (t' @ t). |
|---|
| 156 | #S #st1' #st1 #st2 #t #t' #Ht' lapply t -t elim Ht' |
|---|
| 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 |
|---|
| 161 | |2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [|| * #l' ] #EQ destruct |
|---|
| 162 | [|| #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2 | %3 | %4 ] |
|---|
| 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 |
|---|
| 166 | #r #pre_r normalize |
|---|
| 167 | >append_tind_commute >append_tind_commute >append_associative |
|---|
| 168 | <append_tind_commute in ⊢ (????(??????%)); %5 |
|---|
| 169 | try assumption [1,3: whd [ %{f} %{l1'} ] % ] @IH2 assumption |
|---|
| 170 | qed. |
|---|
| 171 | |
|---|
| 172 | (* |
|---|
| 173 | lemma append_well_formed_silent : ∀S : abstract_status. |
|---|
| 174 | ∀st1',st1,st2 : S.∀t : raw_trace S st1 st2.∀t' : raw_trace S st1' st1. |
|---|
| 175 | well_formed_trace … t → pre_silent_trace … t' → |
|---|
| 176 | (is_trace_non_empty … t' → as_classify … st) → |
|---|
| 177 | well_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 |
|---|
| 181 | inversion 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 |
|---|
| 187 | qed.*) |
|---|
| 188 | |
|---|
| 189 | (* |
|---|
| 190 | lemma well_formed_append : ∀S : abstract_status. |
|---|
| 191 | ∀st1,st2,st3 : S. ∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. |
|---|
| 192 | well_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 | ] |
|---|
| 200 | lapply 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 |
|---|
| 205 | qed. |
|---|
| 206 | |
|---|
| 207 | |
|---|
| 208 | lemma append_well_formed : ∀S : abstract_status. |
|---|
| 209 | ∀st1,st2,st3 : S.∀t1 : raw_trace S st1 st2.∀t2 : raw_trace S st2 st3. |
|---|
| 210 | well_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] |
|---|
| 214 | try @IH assumption |
|---|
| 215 | qed. |
|---|
| 216 | (* |
|---|
| 217 | lemma 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] |
|---|
| 223 | qed. |
|---|
| 224 | *) |
|---|
| 225 | *) |
|---|
| 226 | lemma 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. |
|---|
| 228 | silent_trace … t1 → |
|---|
| 229 | get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2. |
|---|
| 230 | #S #st1 #st2 #st3 #t1 elim t1 |
|---|
| 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] |
|---|
| 234 | #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct |
|---|
| 235 | #_ whd in ⊢ (??%?); >IH [%] %1 assumption |
|---|
| 236 | qed. |
|---|
| 237 | |
|---|
| 238 | lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S. |
|---|
| 239 | ∀t1 : raw_trace … st1 st2. ∀t2 : raw_trace … st2 st3. |
|---|
| 240 | get_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 |
|---|
| 244 | qed. |
|---|
| 245 | |
|---|
| 246 | (* |
|---|
| 247 | lemma 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 | |
|---|
| 258 | lemma head_of_premeasurable_is_not_io : ∀S : abstract_status. |
|---|
| 259 | ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → |
|---|
| 260 | as_classify … st1 ≠ cl_io. |
|---|
| 261 | #S #st1 #st2 #t #H inversion H // |
|---|
| 262 | qed. |
|---|
| 263 | |
|---|
| 264 | |
|---|
| 265 | theorem simulates_pre_mesurable: |
|---|
| 266 | ∀S : abstract_status.∀rel : relations S. |
|---|
| 267 | ∀s1,s1' : S. ∀t1: raw_trace S s1 s1'. |
|---|
| 268 | simulation_conditions S rel → |
|---|
| 269 | pre_measurable_trace … t1 → |
|---|
| 270 | ∀s2 : S. |
|---|
| 271 | as_classify … s2 ≠ cl_io → Srel … rel s1 s2 → |
|---|
| 272 | ∃s2'. ∃t2: raw_trace … s2 s2'. |
|---|
| 273 | pre_measurable_trace … t2 ∧ |
|---|
| 274 | get_costlabels_of_trace … t1 = get_costlabels_of_trace … t2 ∧ |
|---|
| 275 | Srel … rel s1' s2'. |
|---|
| 276 | #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable |
|---|
| 277 | [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)} |
|---|
| 278 | /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/ |
|---|
| 279 | | #st1 #st2 #st3 #l #execute #tl #ClASS ** [|#c] #EQ destruct |
|---|
| 280 | #pre_measurable_tl #IH #s2 #classify_s2 #REL |
|---|
| 281 | [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2'' |
|---|
| 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 % ] |
|---|
| 286 | #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3 |
|---|
| 287 | %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/ |
|---|
| 288 | whd in ⊢ (??%?); /2/ |
|---|
| 289 | | cases(simulate_label … good … execute … REL) |
|---|
| 290 | [2,3: /2/] |
|---|
| 291 | #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2'''' |
|---|
| 292 | #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by pre_silent_io/ |
|---|
| 293 | #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3} |
|---|
| 294 | %{(t_s2'' @ (t_ind … exe_s2''' …))} [ @(t_s2'''' @ t_s3) ] % [2: assumption] |
|---|
| 295 | % |
|---|
| 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 // % // |
|---|
| 302 | | whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l |
|---|
| 303 | [2: assumption] whd in ⊢ (???%); |
|---|
| 304 | >get_cost_label_invariant_for_append_silent_trace_l // |
|---|
| 305 | ] |
|---|
| 306 | ] |
|---|
| 307 | % assumption |
|---|
| 308 | | #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ) |
|---|
| 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''') |
|---|
| 313 | [2: @(pre_silent_io … sil_t2) assumption] |
|---|
| 314 | #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL |
|---|
| 315 | %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] |
|---|
| 316 | % [2: whd in ⊢ (??%?); |
|---|
| 317 | >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) |
|---|
| 318 | whd in ⊢ (???%); |
|---|
| 319 | >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) |
|---|
| 320 | @eq_f assumption ] |
|---|
| 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 % |
|---|
| 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) |
|---|
| 333 | [2: /2 by pre_silent_io/ ] |
|---|
| 334 | #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin} |
|---|
| 335 | %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % |
|---|
| 336 | [2: whd in ⊢ (??%?); |
|---|
| 337 | >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) |
|---|
| 338 | whd in ⊢ (???%); |
|---|
| 339 | >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) |
|---|
| 340 | @eq_f assumption ] |
|---|
| 341 | @append_premeasurable_silent try assumption |
|---|
| 342 | %4 try assumption |
|---|
| 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 % |
|---|
| 346 | | whd %{f} %{lab} % |
|---|
| 347 | | @append_premeasurable_silent // % assumption |
|---|
| 348 | ] |
|---|
| 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 |
|---|
| 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 |
|---|
| 353 | #sil_tr2 #call_rel cases(IH1 … REL1) |
|---|
| 354 | [2: /2 by pre_silent_io/ ] |
|---|
| 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'' * |
|---|
| 358 | #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ] |
|---|
| 359 | #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'} |
|---|
| 360 | %{(tr1 @ (t_ind … exe_12' … ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} |
|---|
| 361 | % [2: assumption] % |
|---|
| 362 | [ @append_premeasurable_silent try assumption %5 |
|---|
| 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 % |
|---|
| 368 | | whd %{f} %{l} % |
|---|
| 369 | | assumption |
|---|
| 370 | | @append_premeasurable_silent try assumption [2: % //] |
|---|
| 371 | @append_silent_premeasurable // % // |
|---|
| 372 | | @append_premeasurable_silent try assumption |
|---|
| 373 | | @(RET_REL … call_rel) assumption |
|---|
| 374 | | % |
|---|
| 375 | ] |
|---|
| 376 | | >get_cost_label_invariant_for_append_silent_trace_l [2: // ] |
|---|
| 377 | whd in ⊢ (??%%); @eq_f >append_associative |
|---|
| 378 | >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); |
|---|
| 379 | [2: % // ] >append_associative |
|---|
| 380 | >get_cost_label_append in ⊢ (???%); |
|---|
| 381 | >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); |
|---|
| 382 | [2: % //] normalize |
|---|
| 383 | >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); |
|---|
| 384 | [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2 |
|---|
| 385 | assumption |
|---|
| 386 | ] |
|---|
| 387 | % // |
|---|
| 388 | ] |
|---|
| 389 | qed. |
|---|
| 390 | |
|---|
| 391 | |
|---|
| 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' |
|---|
| 397 | definition 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 | |
|---|
| 404 | record measurable_trace (S : abstract_status) : Type[0] ≝ |
|---|
| 405 | { L_label: ActionLabel |
|---|
| 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 | |
|---|
| 426 | lemma 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 | |
|---|
| 429 | lemma case_cl_io : ∀s : status_class.decidable … (s = cl_io). |
|---|
| 430 | * [2: %%] %2 % #EQ destruct qed. |
|---|
| 431 | |
|---|
| 432 | lemma tail_of_premeasurable_is_not_io : ∀S : abstract_status. |
|---|
| 433 | ∀st1,st2 : S. ∀t : raw_trace … st1 st2.pre_measurable_trace … t → |
|---|
| 434 | as_classify … st2 ≠ cl_io. |
|---|
| 435 | #S #st1 #st2 #t #H elim H // |
|---|
| 436 | qed. |
|---|
| 437 | |
|---|
| 438 | lemma 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 |
|---|
| 443 | destruct #_ @IH % assumption |
|---|
| 444 | qed. |
|---|
| 445 | |
|---|
| 446 | lemma 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. |
|---|
| 448 | silent_trace … t2 → |
|---|
| 449 | get_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) // |
|---|
| 452 | qed. |
|---|
| 453 | |
|---|
| 454 | lemma instr_execute_commute : ∀S :abstract_status. |
|---|
| 455 | ∀rel : relations S. |
|---|
| 456 | simulation_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. |
|---|
| 460 | Srel … 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 | ] |
|---|
| 516 | qed. |
|---|
| 517 | |
|---|
| 518 | |
|---|
| 519 | theorem simulate_LR_trace : |
|---|
| 520 | ∀S : abstract_status. |
|---|
| 521 | ∀t : measurable_trace S. |
|---|
| 522 | ∀rel : relations S. |
|---|
| 523 | simulation_conditions … rel → |
|---|
| 524 | ∀s2 : S. |
|---|
| 525 | match 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') ∧ |
|---|
| 534 | match 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 | ] ∧ |
|---|
| 541 | match 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 | ] |
|---|
| 576 | cases(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 | ] |
|---|
| 644 | qed. |
|---|
| 645 | (* |
|---|
| 646 | xxxxxxxxxxxxxxxxxxxx |
|---|
| 647 | |
|---|
| 648 | theorem simulate_LR_trace : |
|---|
| 649 | ∀S : abstract_status. |
|---|
| 650 | ∀t : measurable_trace S. |
|---|
| 651 | ∀rel : relations S. |
|---|
| 652 | simulation_conditions … rel → |
|---|
| 653 | ∀s2 : S. |
|---|
| 654 | match 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 | ] |
|---|
| 719 | qed. |
|---|
| 720 | |
|---|
| 721 | |
|---|
| 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 |
|---|
| 725 | normalize 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 | |
|---|
| 729 | whd in ⊢ (% → ?); |
|---|
| 730 | |
|---|
| 731 | |
|---|
| 732 | |
|---|
| 733 | |
|---|
| 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 | |
|---|
| 738 | definition unmovable_entry_label ≝ |
|---|
| 739 | λS : abstract_status.λl. |
|---|
| 740 | match 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 | ]. |
|---|
| 748 | |
|---|
| 749 | definition unmovable_exit_label ≝ |
|---|
| 750 | λS : abstract_status.λl. |
|---|
| 751 | match 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 | ]. |
|---|
| 759 | |
|---|
| 760 | theorem simulates_LR_raw_trace : |
|---|
| 761 | ∀S : abstract_status. |
|---|
| 762 | ∀t : LR_raw_trace S. |
|---|
| 763 | ∀rel : relations S. |
|---|
| 764 | simulation_conditions … rel → |
|---|
| 765 | measurable S t → |
|---|
| 766 | ∀s1' : S.as_classify … s1' ≠ cl_io → Srel … rel (LR_s1 … t) s1' → |
|---|
| 767 | ∃ t' : LR_raw_trace S. |
|---|
| 768 | measurable S t' ∧ |
|---|
| 769 | if as_initial … (LR_s1 … t) ∨ unmovable_entry_label S (L_label … t) then |
|---|
| 770 | LR_s1 … t' = s1' |
|---|
| 771 | else |
|---|
| 772 | ∃pre : raw_trace … (LR_s1 … t') s1'.trace_prefix … pre (LR_t … t') |
|---|
| 773 | ∧ ∃s1''.Srel … rel (LR_s2 … t) s1'' ∧ |
|---|
| 774 | if as_final … (LR_s2 … t) ∨ unmovable_exit_label S (R_label … t) then |
|---|
| 775 | LR_s2 … t' = s1'' |
|---|
| 776 | else |
|---|
| 777 | ∃suff : raw_trace … s1'' (LR_s2 … t'). trace_suffix … suff (LR_t … t') |
|---|
| 778 | ∧ |
|---|
| 779 | get_costlabels_of_trace … (LR_t … t) = get_costlabels_of_trace … (LR_t … t'). |
|---|
| 780 | #S #t #rel #good * #pre_t #wf_t #s1' #Hs1' #REL |
|---|
| 781 | cases(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 |
|---|
| 784 | inversion(as_initial … (LR_s1 … t)) #Has_initial |
|---|
| 785 | inversion(unmovable_entry_label S (L_label … t)) #Hunmov_entry |
|---|
| 786 | inversion(as_final … (LR_s2 … t)) #Has_final |
|---|
| 787 | inversion(unmovable_exit_label S (R_label … t)) #Hunmov_exit |
|---|
| 788 | normalize nodelta |
|---|
| 789 | [ %{(mk_LR_raw_trace ? ?? s1' ? t2 ???)} [2: % [2: |
|---|
| 790 | |
|---|
| 791 | |
|---|
| 792 | |
|---|
| 793 | qed. |
|---|
| 794 | |
|---|
| 795 | xxxx |
|---|
| 796 | |
|---|
| 797 | theorem 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 | |
|---|
| 814 | (*********************************************************************) |
|---|
| 815 | |
|---|
| 816 | (* quello che segue tentava di permettere di evitare l'emissione di label |
|---|
| 817 | associate a codice morto *) |
|---|
| 818 | |
|---|
| 819 | replace_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 | |
|---|
| 827 | theorem simulates: |
|---|
| 828 | ∀s1,s2. ∀τ1: raw_trace … s1 s2. |
|---|
| 829 | pre_measurable_trace … t1 → |
|---|
| 830 | well_formed_trace … t1. |
|---|
| 831 | ∀l1: option NonFunctionalLabel. |
|---|
| 832 | ∀s1'. |
|---|
| 833 | S s1 s1' → |
|---|
| 834 | ∃dead_labels. |
|---|
| 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' ⇒ |
|---|
| 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 | ] |
|---|
| 851 | ] |
|---|
| 852 | *) |
|---|
