Changeset 2457 for src/common
- Timestamp:
- Nov 13, 2012, 11:30:23 AM (7 years ago)
- File:
-
- 1 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/StatusSimulation.ma
r2436 r2457 31 31 necessary for as_after_return (typically just the program counter) 32 32 maybe what function is called too? *) 33 ; call_rel : (Σs.as_classifier S1 s cl_call) → 34 (Σs.as_classifier S2 s cl_call) → Prop 33 ; ret_rel : S1 → S2 → Prop 35 34 ; sim_final : 36 35 ∀st1,st2.sem_rel st1 st2 → as_final … st1 ↔ as_final … st2 … … 48 47 definition label_rel ≝ λS1,S2,st1,st2.as_label S1 st1 = as_label S2 st2. 49 48 50 definition ret_rel ≝ λS1,S2.λR : status_rel S1 S2.λs1,s2. 51 ∀s1_pre,s2_pre.call_rel … R s1_pre s2_pre → 52 as_after_return S1 s1_pre s1 → 53 as_after_return S2 s2_pre s2. 49 definition call_rel ≝ λS1,S2.λR : status_rel S1 S2. 50 λs1_pre,s2_pre. 51 ∀s1_ret,s2_ret.as_after_return S1 s1_pre s1_ret → 52 ret_rel ?? R s1_ret s2_ret → 53 as_after_return S2 s2_pre s2_ret. 54 54 55 55 (* the equivalent of a collapsable trace_any_label where we do not force … … 70 70 S will mark semantic relation, C call relation, L label relation, R return relation *) 71 71 72 record status_simulation 73 (S1 : abstract_status) 74 (S2 : abstract_status) 75 : Type[1] ≝ 76 { sim_status_rel :> status_rel S1 S2 77 ; sim_execute : 72 definition status_simulation ≝ 73 λS1 : abstract_status. 74 λS2 : abstract_status. 75 λsim_status_rel : status_rel S1 S2. 78 76 ∀st1,cl,st1',st2.as_execute S1 st1 st1' → 79 77 sim_status_rel st1 st2 → … … 141 139 sim_status_rel st1' st2' ∧ 142 140 label_rel … st1' st2' 143 ] prf 144 }. 141 ] prf. 145 142 146 143 … … 287 284 include alias "basics/logic.ma". 288 285 289 let rec status_simulation_produce_tlr S1 S2 (R : status_simulation S1 S2)286 let rec status_simulation_produce_tlr S1 S2 R 290 287 (* we start from this situation 291 288 st1 →→→→tlr→→→→ st1' … … 306 303 (tlr1 : trace_label_return S1 st1 st1') 307 304 (taa2_pre : trace_any_any S2 st2_lab st2) 305 (sim_execute : status_simulation S1 S2 R) 308 306 on tlr1 : R st1 st2 → label_rel … st1 st2_lab → 309 307 ∃st2_mid.∃st2'. … … 317 315 | tlr_step st1 st1_mid st1' tll1 tl1 ⇒ ? 318 316 ] 319 and status_simulation_produce_tll S1 S2 (R : status_simulation S1 S2)317 and status_simulation_produce_tll S1 S2 R 320 318 (* we start from this situation 321 319 st1 →→→→tll→→→ st1' … … 336 334 (tll1 : trace_label_label S1 fl st1 st1') 337 335 (taa2_pre : trace_any_any S2 st2_lab st2) 338 on tll1 : R st1 st2 → label_rel … st1 st2_lab → 336 (sim_execute : status_simulation S1 S2 R) 337 on tll1 : R st1 st2 → label_rel … st1 st2_lab → 339 338 match fl with 340 339 [ ends_with_ret ⇒ … … 352 351 [ tll_base fl1' st1' st1'' tal1 H ⇒ ? 353 352 ] 354 and status_simulation_produce_tal S1 S2 (R : status_simulation S1 S2)353 and status_simulation_produce_tal S1 S2 R 355 354 (* we start from this situation 356 355 st1 →→tal→→ st1' … … 380 379 fl st1 st1' st2 381 380 (tal1 : trace_any_label S1 fl st1 st1') 382 on tal1 : R st1 st2 → 381 (sim_execute : status_simulation S1 S2 R) 382 on tal1 : R st1 st2 → 383 383 match fl with 384 384 [ ends_with_ret ⇒ … … 405 405 [1,2,3: #st1_L_st2_lab ] 406 406 [ (* tlr_base *) 407 elim (status_simulation_produce_tll … tll1 taa2_pre s t1_R_st2 st1_L_st2_lab)407 elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab) 408 408 #st2_mid * #st2' * #tll2 #H 409 409 %{st2_mid} %{st2'} %{(tlr_base … tll2)} @H 410 410 | (* tlr_step *) 411 elim (status_simulation_produce_tll … tll1 taa2_pre s t1_R_st2 st1_L_st2_lab)411 elim (status_simulation_produce_tll … tll1 taa2_pre sim_execute st1_R_st2 st1_L_st2_lab) 412 412 #st2_mid * #tll2 ** #H1 #H2 #H3 413 elim (status_simulation_produce_tlr … tl1 (taa_base …) H1 H2)413 elim (status_simulation_produce_tlr … tl1 (taa_base …) sim_execute H1 H2) 414 414 #st2_mid' * #st2' * #tl2 * #taa2 * #H4 #H5 415 415 %{st2_mid'} %{st2'} %{(tlr_step … tll2 tl2)} %{taa2} 416 416 %{H4} %{H3 H5} 417 417 | (* tll_base *) 418 lapply (status_simulation_produce_tal ?? R ??? st2 tal1st1_R_st2)418 lapply (status_simulation_produce_tal … st2 tal1 sim_execute st1_R_st2) 419 419 cases fl1' in tal1; normalize nodelta #tal1 * 420 420 [3: * #_ #ABS elim (absurd … H ABS) ] … … 431 431 | (* tal_base_non_return *) whd 432 432 cases G #G' 433 elim (sim_execute … R …H st1_R_st2 G')433 elim (sim_execute … H st1_R_st2 G') 434 434 #st2' ** -st2 -st2' 435 435 [1,3: #st2 (* taa2 empty → st1' must be not cost_labelled *) … … 445 445 ] 446 446 | (* tal_base_return *) whd 447 elim (sim_execute … R …H st1_R_st2 G)447 elim (sim_execute … H st1_R_st2 G) 448 448 #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2' 449 449 ***** #ncost #J2 #K2 … … 453 453 %[ % | %[|%[|%[|%[| % ]]]]]]] 454 454 | (* tal_base_call *) whd 455 elim (sim_execute … R …H st1_R_st2 G)455 elim (sim_execute … H st1_R_st2 G) 456 456 * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 457 457 #st1_R_st2_mid #st1_L_st2_after_call 458 elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2'st1_R_st2_mid st1_L_st2_after_call)458 elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) 459 459 #st2_after_ret * #st2' * #tlr2 * #taa2'' lapply tlr2 cases taa2'' -st2_after_ret -st2' 460 460 [ #st2' #tlr2 ***** … … 474 474 ] 475 475 ] 476 [1,3: @(st1_ Rret_st2' … st1_C_st2) assumption476 [1,3: @(st1_C_st2 … st1_Rret_st2') assumption 477 477 |*: whd <st1_L_st2' assumption 478 478 ] 479 479 | (* tal_step_call *) 480 elim (sim_execute … R …H st1_R_st2 G)480 elim (sim_execute … H st1_R_st2 G) 481 481 * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 482 482 #st1_R_st2_mid #st1_L_st2_after_call 483 elim (status_simulation_produce_tlr ?? R ???? tlr1 taa2'st1_R_st2_mid st1_L_st2_after_call)483 elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) 484 484 #st2_after_ret * #st2' * #tlr2 * #taa2'' 485 485 **** 486 486 #taa_ncost #st1_R_st2' #st1_Rret_st2' #st1_L_st2' #S 487 lapply (status_simulation_produce_tal … tl1 s t1_R_st2')487 lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2') 488 488 cases fl1' in tl1; #tl1 * 489 489 [ #st2'' * #st2''' * #tl2 * #taa2''' **** #ncost' #st1_R_st2''' #st1_Rret_st2'' #st1_L_st2''' #S' … … 514 514 ] 515 515 ] 516 [1,4,7,9: @(st1_ Rret_st2' … st1_C_st2) assumption516 [1,4,7,9: @(st1_C_st2 … st1_Rret_st2') assumption 517 517 |2,5: lapply st1_L_st2' lapply taa_ncost cases taa2'' -st2_after_ret -st2' 518 518 [1,3: #st2_after_ret * #L whd in ⊢ (?%); <L assumption … … 523 523 ] 524 524 | (* step_default *) 525 elim (sim_execute … R …H st1_R_st2 G)525 elim (sim_execute … H st1_R_st2 G) 526 526 #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid 527 lapply (status_simulation_produce_tal … tl1 s t1_R_st2_mid)527 lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid) 528 528 cases fl1' in tl1; #tl1 * 529 529 [ #st2_mid' *#st2' *#tal2 *#taa2' * #H #G … … 728 728 *) 729 729 ∀S1,S2. 730 ∀R : status_simulation S1 S2.730 ∀R. 731 731 ∀st1,st1',stack,st2.∀ft1 : flat_trace S1 st1 st1' stack. 732 label_rel … st1 st2 → R st1 st2 →732 status_simulation S1 S2 R → label_rel … st1 st2 → R st1 st2 → 733 733 ∃st2_lab,st2'. 734 734 ∃ft2 : flat_trace S2 st2 st2_lab stack. 735 735 ∃taa : trace_any_any S2 st2_lab st2'. 736 736 label_rel … st1' st2_lab ∧ R st1' st2' ∧ ft_observables … ft1 = ft_observables … ft2. 737 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 # H #G elim ft1 -st1' -stack737 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 -st1' -stack 738 738 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % 739 739 |*: #st1_mid #st1' #stack [3: #f] #ft1 #ex [2: *] #cl
Note: See TracChangeset
for help on using the changeset viewer.