Changeset 3394 for LTS/Simulation.ma
 Timestamp:
 Oct 30, 2013, 10:29:47 AM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

LTS/Simulation.ma
r3391 r3394 11 11 12 12 record simulation_conditions (S : abstract_status) (rel : relations S) : Prop ≝ 13 { simulate_tau: 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: 14 18 ∀s1,s2,s1' : S. 15 19 as_execute … (cost_act (None ?)) s1 s1'→ … … 26 30 as_execute … (cost_act (Some ? l)) s2' s2'' ∧ 27 31 ∃t3: raw_trace S s2'' s2'''. 28 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t332 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 29 33 ; simulate_call_pl: 30 34 ∀s1,s2,s1' : S.∀f,l. … … 38 42 bool_to_Prop(is_call_post_label … s2') ∧ 39 43 ∃t3: raw_trace S s2'' s2'''. 40 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t344 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 41 45 ; simulate_ret_l: 42 46 ∀s1,s2,s1' : S.∀l. … … 48 52 as_execute … (ret_act (Some ? l)) s2' s2'' ∧ 49 53 ∃t3: raw_trace S s2'' s2'''. 50 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t354 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 51 55 ; simulate_call_n: 52 56 ∀s1,s2,s1' : S.∀f,l. … … 60 64 as_execute … (call_act f l) s2' s2'' ∧ 61 65 ∃t3: raw_trace S s2'' s2'''. 62 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ silent_trace … t366 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧ pre_silent_trace … t3 63 67 ∧ Crel … rel s1 s2' 64 68 ; simulate_ret_n: … … 71 75 as_execute … (ret_act (None ?)) s2' s2'' ∧ 72 76 ∃t3: raw_trace S s2'' s2'''. 73 Srel … rel s1' s2''' ∧ silent_trace … t1 ∧silent_trace … t377 Srel … rel s1' s2''' ∧ pre_silent_trace … t1 ∧ pre_silent_trace … t3 74 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'' 75 95 }. 76 96 … … 102 122 #S #st1' #st1 #st2 #t #t' lapply t t elim t' 103 123 [ #st #t #Hpre #_ whd in ⊢ (????%); assumption] 104 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre #H inversion H in ⊢ ?;124 #s1 #s2 #s3 #l #prf #tl #IH #t #Hpre * [2: * #H @⊥ @H %] #H inversion H in ⊢ ?; 105 125 [ #s #H1 #EQ1 #EQ2 destruct #EQ destruct] 106 126 #s1' #s2' #s3' #prf' #tl' #Hclass #silent_tl' #_ #EQ1 #EQ2 #EQ3 … … 110 130  @IH try assumption 111 131 ] 112 qed. 113 114 lemma silent_is_premeasurable : ∀S : abstract_status. 115 ∀st1,st2 : S. ∀t : raw_trace S st1 st2.silent_trace … t 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 116 137 → pre_measurable_trace … t. 117 138 #S #st1 #st2 #t elim t … … 134 155 pre_measurable_trace … (t' @ t). 135 156 #S #st1' #st1 #st2 #t #t' #Ht' lapply t t elim Ht' 136 [ normalize #st #Hst #r #H1 @silent_is_premeasurable assumption 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 137 161 2,3,4: #s1 #s2 #s3 #l #prf #tl #Hs1 * #x [ * #l' ] #EQ destruct 138 162 [ #Hs1_post ] #pre_tl #IH #r #pre_sil_r [ %2  %3  %4 ] … … 205 229 get_costlabels_of_trace … (t1 @ t2) = get_costlabels_of_trace … t2. 206 230 #S #st1 #st2 #st3 #t1 elim t1 207 [#st #t2 #_ %] #st1' #st2' #st3' #l' #prf #tl #IH #t2 #H 208 inversion H in ⊢ ?; [ #st #H1 #EQ1 #EQ2 #EQ3 destruct] 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] 209 234 #st1'' #st2'' #st3'' #prf'' #tl'' #Hclass #Htl'' #_ #EQ1 #EQ2 #EQ3 destruct 210 #_ whd in ⊢ (??%?); >IH [%] assumption211 qed. 235 #_ whd in ⊢ (??%?); >IH [%] %1 assumption 236 qed. 212 237 213 238 lemma get_cost_label_append : ∀S : abstract_status.∀st1,st2,st3 : S. … … 251 276 #S #rel #s1 #s1' #t1 #good #pre_measurable elim pre_measurable 252 277 [ #st #H1 #s2 #REL #Hs2 %{s2} %{(t_base …)} 253 /8 by refl, silent_empty, conj, silent_is_premeasurable/278 /8 by refl, silent_empty, conj, pre_silent_is_premeasurable/ 254 279  #st1 #st2 #st3 #l #execute #tl #ClASS ** [#c] #EQ destruct 255 280 #pre_measurable_tl #IH #s2 #classify_s2 #REL 256 281 [ cases(simulate_tau … good … execute … REL) /2/ #s2'' * #t_s2'' * #RELst2s2'' 257 #silent_ts2'' cases(IH … RELst2s2'') /2 by silent_io/ 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 % ] 258 286 #s3 * #ts3 ** #pre_meas_ts3 #EQcost #RELst3s3 259 287 %{s3} %{(t_s2'' @ ts3)} % [2: assumption] % /2 by append_premeasurable_silent/ … … 262 290 [2,3: /2/] 263 291 #s2'' * #s2''' * #s2'''' * #t_s2'' * #exe_s2''' * #t_s2'''' ** #RELst2_s2'''' 264 #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 bysilent_io/292 #sil_ts2'' #sil_t_s2'''' cases(IH … RELst2_s2'''') /2 by pre_silent_io/ 265 293 #s3 * #t_s3 ** #pre_s3 #EQcost #RElst3s3 %{s3} 266 294 %{(t_s2'' @ (t_ind … exe_s2''' …))} [ @(t_s2'''' @ t_s3) ] % [2: assumption] 267 295 % 268 [ /4 by pm_cons_cost_act, silent_io, ex_intro, append_premeasurable_silent/ 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 // % // 269 302  whd in ⊢ (??%?); >EQcost >get_cost_label_invariant_for_append_silent_trace_l 270 303 [2: assumption] whd in ⊢ (???%); … … 272 305 ] 273 306 ] 307 % assumption 274 308  #s2 #s2' #s2'' #l #class_s2 #exe_s2_s2' #tl whd in ⊢ (% → ?); * #ret_lab #EQ destruct(EQ) 275 309 #pre_meas_tl #IH #s2 #class_s2 #RELst1s2 … … 277 311 #st1 * #st2 * #st3 * #t1 * #exe_s2'' * #t2 ** #rel_s2_s2''' 278 312 #sil_t1 #sil_t2 cases(IH … rel_s2_s2''') 279 [2: @( silent_io … sil_t2) assumption]313 [2: @(pre_silent_io … sil_t2) assumption] 280 314 #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL 281 315 %{s2_fin} %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] … … 283 317 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) 284 318 whd in ⊢ (???%); 285 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)319 >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) 286 320 @eq_f assumption ] 287 /4 by pm_cons_lab_ret, silent_io, ex_intro, append_premeasurable_silent/ 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 % 288 327  #s1 #s2 #s3 #l #exe_s1_s2 #tl #class_s1 * #f * #lab #EQ destruct 289 328 #post #pre_tl #IH #s2' #io_s2' #REL_s1_s2' … … 292 331 #s' * #s2'' * #s2''' * #t1 ** #exe_s2'' #post' * #t2 ** #REL #sil_t1 #sil_t2 293 332 cases(IH … REL) 294 [2: /2 by silent_io/ ]333 [2: /2 by pre_silent_io/ ] 295 334 #s2_fin * #t_fin ** #pre_t_fin #EQcost #REL1 %{s2_fin} 296 335 %{(t1 @ (t_ind … exe_s2'' … t2) @ t_fin)} % [2: assumption] % … … 298 337 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t1) 299 338 whd in ⊢ (???%); 300 >(get_cost_label_invariant_for_append_silent_trace_l … sil_t2)339 >(get_cost_label_invariant_for_append_silent_trace_l … (or_introl … sil_t2)) 301 340 @eq_f assumption ] 302 341 @append_premeasurable_silent try assumption 303 342 %4 try assumption 304 [ /2 by silent_io/ 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 % 305 346  whd %{f} %{lab} % 306  /2 by append_premeasurable_silent/347  @append_premeasurable_silent // % assumption 307 348 ] 308 349  #st1 #st2 #st3 #st4 #st5 #l1 #l2 #exe_12 #t1 #t2 #exe_34 #class_1 #class_3 * … … 311 352 #st1'' * #st1''' * #st2' * #tr1 ** #nps_st1'' #exe_12' * #tr2 *** #REL1 #sil_tr1 312 353 #sil_tr2 #call_rel cases(IH1 … REL1) 313 [2: /2 by silent_io/ ]354 [2: /2 by pre_silent_io/ ] 314 355 #st3' * #tr3 ** #pre_tr3 #EQcost_tr3 #REL2 315 356 cases(simulate_ret_n … good … exe_34 … REL2) [2,3: /2 by head_of_premeasurable_is_not_io/ ] 316 357 #st3'' * #st4' * #st4'' * 317 #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by silent_io/ ]358 #tr4 * #exe_34' * #tr5 *** #REL3 #sil_tr4 #sil_tr5 #RET_REL cases(IH2 … REL3) [2: /2 by pre_silent_io/ ] 318 359 #st5' * #tr6 ** #pre_tr6 #EQcost_tr6 #REL4 %{st5'} 319 360 %{(tr1 @ (t_ind … exe_12' … ((tr2 @ tr3 @ tr4) @ (t_ind … exe_34' … (tr5 @tr6)))))} 320 361 % [2: assumption] % 321 362 [ @append_premeasurable_silent try assumption %5 322 [1,2: /2 by silent_io/ 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 % 323 368  whd %{f} %{l} % 324 369  assumption 325  @append_premeasurable_silent try assumption 326 @append_silent_premeasurable assumption370  @append_premeasurable_silent try assumption [2: % //] 371 @append_silent_premeasurable // % // 327 372  @append_premeasurable_silent try assumption 328 373  @(RET_REL … call_rel) assumption … … 332 377 whd in ⊢ (??%%); @eq_f >append_associative 333 378 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 334 [2: // ] >append_associative379 [2: % // ] >append_associative 335 380 >get_cost_label_append in ⊢ (???%); 336 381 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 337 [2: //] normalize382 [2: % //] normalize 338 383 >get_cost_label_invariant_for_append_silent_trace_l in ⊢ (???%); 339 [2: // ] >get_cost_label_append in ⊢ (??%?); @eq_f2384 [2: % // ] >get_cost_label_append in ⊢ (??%?); @eq_f2 340 385 assumption 341 386 ] 387 % // 342 388 ] 343 389 qed. 344 345 sxxxxx346 390 347 391 … … 358 402 as_execute … s2 so L'. *) 359 403 360 record LR_raw_trace (S : abstract_status) : Type[0] ≝404 record measurable_trace (S : abstract_status) : Type[0] ≝ 361 405 { L_label: ActionLabel 362 ; R_label : ActionLabel 363 ; LR_s1: S 364 ; LR_s2: S 365 ; LR_t : raw_trace S LR_s1 LR_s2 366 ; L_init_ok : bool_to_Prop(as_initial … LR_s1) → L_label = init_act 367 ; L_noinit_ok : 368 bool_to_Prop (¬ as_initial … LR_s1) → 369 ∃s0. as_execute … L_label s0 LR_s1 ∧ is_costlabelled_act L_label 370 ∧ ¬ bool_to_Prop (is_act_io_entering S L_label) 371 ; R_nonfin_ok : 372 bool_to_Prop (¬ as_final … (LR_s2)) → 373 ∃so.as_execute … R_label LR_s2 so ∧ is_costlabelled_act R_label 374 ∧ ¬ bool_to_Prop (is_act_io_exiting S R_label) 375 }. 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 376 647 377 definition measurable ≝ λS : abstract_status.λt : LR_raw_trace S. 378 pre_measurable_trace … (LR_t … t) ∧ well_formed_trace … (LR_t … t). 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 379 732 380 733 … … 497 850 ] 498 851 ] 852 *)
Note: See TracChangeset
for help on using the changeset viewer.