Changeset 2553 for src/common/StatusSimulation.ma
 Timestamp:
 Dec 12, 2012, 2:43:03 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/StatusSimulation.ma
r2540 r2553 82 82 sim_status_rel st1 st2 → 83 83 match as_classify … st1 with 84 [ cl_call ⇒ ∀prf. 85 (* 86 st1' S\ 87 ↑ \ \ 88 st1 \L\ \ 89  \ \ \ 90 S \C\ st2_after_call →taa→ st2' 91  \ ↑ 92 st2 →taa→ st2_pre_call 93 *) 94 ∃st2_pre_call. 95 as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ 96 call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ 97 ∃st2_after_call,st2'. 98 ∃taa2 : trace_any_any … st2 st2_pre_call. 99 ∃taa2' : trace_any_any … st2_after_call st2'. 100 as_execute … st2_pre_call st2_after_call ∧ 101 sim_status_rel st1' st2' ∧ 102 label_rel … st1' st2_after_call 103  cl_return ⇒ 104 (* 105 st1 106 / ↓ 107  st1'S,L\ 108 S \ \ 109 \ \R\  110 \   111 st2 →taa→ st2_ret   112 ↓ /  113 st2_after_ret →taaf→ st2' 114 115 we also ask that st2_after_ret be not labelled if the taaf tail is 116 not empty 117 *) 118 ∃st2_ret,st2_after_ret,st2'. 119 ∃taa2 : trace_any_any … st2 st2_ret. 120 ∃taa2' : trace_any_any_free … st2_after_ret st2'. 121 (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ 122 as_classifier … st2_ret cl_return ∧ 123 as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ 124 ret_rel … sim_status_rel st1' st2_after_ret ∧ 125 label_rel … st1' st2' 126  cl_other ⇒ 127 (* 128 st1 → st1' 129  \ 130 S S,L 131  \ 132 st2 →taaf→ st2' 133 134 the taaf can be empty (e.g. tunneling) but we ask it must not be the 135 case when both st1 and st1' are labelled (we would be able to collapse 136 labels otherwise) 137 *) 138 ∃st2'. 139 ∃taa2 : trace_any_any_free … st2 st2'. 140 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ 141 sim_status_rel st1' st2' ∧ 142 label_rel … st1' st2' 143  cl_jump ⇒ 144 (* just like cl_other, but with a hypothesis more *) 145 as_costed … st1' → 146 ∃st2'. 147 ∃taa2 : trace_any_any_free … st2 st2'. 148 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ 149 sim_status_rel st1' st2' ∧ 150 label_rel … st1' st2' 84 [ None ⇒ True 85  Some cl ⇒ 86 match cl with 87 [ cl_call ⇒ ∀prf. 88 (* 89 st1' S\ 90 ↑ \ \ 91 st1 \L\ \ 92  \ \ \ 93 S \C\ st2_after_call →taa→ st2' 94  \ ↑ 95 st2 →taa→ st2_pre_call 96 *) 97 ∃st2_pre_call. 98 as_call_ident ? st2_pre_call = as_call_ident ? («st1, prf») ∧ 99 call_rel ?? sim_status_rel «st1, prf» st2_pre_call ∧ 100 ∃st2_after_call,st2'. 101 ∃taa2 : trace_any_any … st2 st2_pre_call. 102 ∃taa2' : trace_any_any … st2_after_call st2'. 103 as_execute … st2_pre_call st2_after_call ∧ 104 sim_status_rel st1' st2' ∧ 105 label_rel … st1' st2_after_call 106  cl_tailcall ⇒ ∀prf. 107 (* 108 st1' S\ 109 ↑ \ \ 110 st1 \L\ \ 111  \ \ 112 S st2_after_call →taa→ st2' 113  ↑ 114 st2 →taa→ st2_pre_call 115 *) 116 ∃st2_pre_call. 117 as_tailcall_ident ? st2_pre_call = as_tailcall_ident ? («st1, prf») ∧ 118 ∃st2_after_call,st2'. 119 ∃taa2 : trace_any_any … st2 st2_pre_call. 120 ∃taa2' : trace_any_any … st2_after_call st2'. 121 as_execute … st2_pre_call st2_after_call ∧ 122 sim_status_rel st1' st2' ∧ 123 label_rel … st1' st2_after_call 124  cl_return ⇒ 125 (* 126 st1 127 / ↓ 128  st1'S,L\ 129 S \ \ 130 \ \R\  131 \   132 st2 →taa→ st2_ret   133 ↓ /  134 st2_after_ret →taaf→ st2' 135 136 we also ask that st2_after_ret be not labelled if the taaf tail is 137 not empty 138 *) 139 ∃st2_ret,st2_after_ret,st2'. 140 ∃taa2 : trace_any_any … st2 st2_ret. 141 ∃taa2' : trace_any_any_free … st2_after_ret st2'. 142 (if taaf_non_empty … taa2' then ¬as_costed … st2_after_ret else True) ∧ 143 as_classifier … st2_ret cl_return ∧ 144 as_execute … st2_ret st2_after_ret ∧ sim_status_rel st1' st2' ∧ 145 ret_rel … sim_status_rel st1' st2_after_ret ∧ 146 label_rel … st1' st2' 147  cl_other ⇒ 148 (* 149 st1 → st1' 150  \ 151 S S,L 152  \ 153 st2 →taaf→ st2' 154 155 the taaf can be empty (e.g. tunneling) but we ask it must not be the 156 case when both st1 and st1' are labelled (we would be able to collapse 157 labels otherwise) 158 *) 159 ∃st2'. 160 ∃taa2 : trace_any_any_free … st2 st2'. 161 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ 162 sim_status_rel st1' st2' ∧ 163 label_rel … st1' st2' 164  cl_jump ⇒ 165 (* just like cl_other, but with a hypothesis more *) 166 as_costed … st1' → 167 ∃st2'. 168 ∃taa2 : trace_any_any_free … st2 st2'. 169 (if taaf_non_empty … taa2 then True else (¬as_costed … st1 ∨ ¬as_costed … st1')) ∧ 170 sim_status_rel st1' st2' ∧ 171 label_rel … st1' st2' 172 ] 151 173 ]. 152 174 … … 202 224  tal_base_return st1 st1' _ _ ⇒ ? 203 225  tal_base_call st1 st1' st1'' _ prf _ tlr1 _ ⇒ ? 226  tal_base_tailcall st1 st1' st1'' _ prf tlr1 ⇒ ? 204 227  tal_step_call fl1 st1 st1' st1'' st1''' _ prf _ tlr1 _ tl1 ⇒ ? 205 228  tal_step_default fl1 st1 st1' st1'' _ tl1 _ _ ⇒ ? … … 211 234  *#st2mid'' *#K2 *#tlr2 *#L2 *#tl2 ** #EQ #EQ' #coll 212 235 ] 236  * #EQfl *#st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 *#tlr2 * #EQ #EQ' 213 237  * #st2mid *#G2 *#EQcall *#taa2' *#st2mid' *#H2 * 214 238 [ * #EQfl *#K2 *#tlr2 *#L2 ** #EQ #coll #EQ' … … 219 243 destruct 220 244 <associative_taa_append_tal 221 [1,2,3,4 :%{(refl …)}] %{st2mid}245 [1,2,3,4,5:%{(refl …)}] %{st2mid} 222 246 [1,2:*: %{G2} %{EQcall} ] 223 247 %{(taa_append_taa … taa2 taa2')} 224 248 [1,2: %{H2} %{G2} [%{K2}] % 249 5: %{st2mid'} %{H2} %{tlr2} % // 225 250 *: %{st2mid'} %{H2} 226 251 [1,3: %1 [%{(refl …)}] *: %2 %{st2mid''} ] … … 229 254 qed. 230 255 256 (* 257 check trace_any_label_label 231 258 let rec tal_end_costed S st1 st2 (tal : trace_any_label S doesnt_end_with_ret st1 st2) 232 259 on tal : as_costed … st2 ≝ … … 242 269 ] 243 270 qed. 271 *) 244 272 245 273 lemma taa_end_not_costed : ∀S,s1,s2.∀taa : trace_any_any S s1 s2. … … 451 479  tal_base_return st1' st1'' H G ⇒ ? 452 480  tal_base_call st1_pre_call st1_after_call st1' H G K tlr1 L ⇒ ? 481  tal_base_tailcall st1_pre_call st1_after_call st1' H G tlr1 ⇒ ? 453 482  tal_step_call fl1' st1' st1'' st1''' st1'''' H G L tlr1 K tl1 ⇒ ? 454 483  tal_step_default fl1' st1' st1'' st1''' H tl1 G K ⇒ ? … … 485 514 lapply (sim_execute … H st1_R_st2) 486 515 (* without try it fails... why? *) 487 try >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?);516 try >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); normalize nodelta 488 517 [ #H lapply (H K) H ] * 489 518 #st2' ** st2 st2' … … 502 531  (* tal_base_return *) whd 503 532 lapply (sim_execute … H st1_R_st2) 504 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?]→?); *533 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); * 505 534 #st2_pre_ret * #st2_after_ret * #st2' * #taa2 * #taa2' 506 535 ***** #ncost #J2 #K2 … … 511 540  (* tal_base_call *) whd 512 541 lapply (sim_execute … H st1_R_st2) 513 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?]→?);542 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); 514 543 #H elim (H G) H 515 544 * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 … … 538 567 *: whd <st1_L_st2' assumption 539 568 ] 569  (* tal_base_tailcall *) whd 570 lapply (sim_execute … H st1_R_st2) 571 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); 572 #H elim (H G) H 573 * #st2_pre_call #G2 * #EQcall * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 574 #st1_R_st2_mid #st1_L_st2_after_call 575 elim (status_simulation_produce_tlr … tlr1 taa2' sim_execute st1_R_st2_mid st1_L_st2_after_call) 576 #st2_after_ret * #st2' * #tlr2 * #taa2'' 577 * #props #S 578 %{st2_after_ret} %{st2'} 579 %{(taa2 @ tal_base_tailcall ???? H2 G2 tlr2)} 580 %{taa2''} 581 %{props} 582 % [%] %[%[ %{EQcall} %[%[%[%[ %{S} % ]]]]]] 540 583  (* tal_step_call *) 541 584 lapply (sim_execute … H st1_R_st2) 542 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?]→?);585 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); 543 586 #H elim (H G) H 544 587 * #st2_pre_call #G2 ** #EQcall #st1_C_st2 * #st2_after_call * #st2_mid *#taa2 *#taa2' ** #H2 … … 585 628 ] 586 629 3,6: @if_else_True whd in ⊢ (?%); <st1_L_st2' assumption 587 *: whd <st1_L_st2'' @(t al_end_costed… tl1)630 *: whd <st1_L_st2'' @(trace_any_label_label … tl1) 588 631 ] 589 632  (* step_default *) 590 633 lapply (sim_execute … H st1_R_st2) 591 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?]→?); *634 >G in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); * 592 635 #st2_mid *#taa2 ** #ncost #st1_R_st2_mid #st1_L_st2_mid 593 636 lapply (status_simulation_produce_tal … tl1 sim_execute st1_R_st2_mid) … … 603 646  (* can't happen *) 604 647 *** #_ #L' elim (absurd ?? K) 605 whd >st1_L_st2_mid <L' @(t al_end_costed… tl1)648 whd >st1_L_st2_mid <L' @(trace_any_label_label … tl1) 606 649 ] 607 650 @if_else_True whd in ⊢ (?%); <st1_L_st2_mid assumption … … 622 665 ∀prf : as_classifier ? st1 cl_call. 623 666 flat_trace S start st2 (as_call_ident ? «st1, prf» :: stack) 667  ft_advance_tailcall : 668 ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 → 669 ∀prf : as_classifier ? st1 cl_tailcall. 670 flat_trace S start st2 (as_tailcall_ident ? «st1, prf» :: stack) 624 671  ft_advance_ret : 625 672 ∀st1,st2,stack,f.flat_trace S start st1 (f :: stack) → as_execute S st1 st2 → … … 664 711  IEVcost : costlabel → intensional_event 665 712  IEVcall : ident → intensional_event 713  IEVtailcall : ident → ident → intensional_event 666 714  IEVret : ident → intensional_event. 667 715 … … 677 725 let add ≝ add @ [IEVcall (as_call_ident ? «st1_mid, prf»)] in 678 726 ft_observables_aux (add @ acc) … pre1 727  ft_advance_tailcall st1_mid st1' stack f pre1 _ prf ⇒ 728 let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in 729 let add ≝ add @ [IEVtailcall f (as_tailcall_ident ? «st1_mid, prf»)] in 730 ft_observables_aux (add @ acc) … pre1 679 731  ft_advance_ret st1_mid st1' stack f pre1 _ _ ⇒ 680 732 let add ≝ option_to_list … (! l ← as_label … st1_mid ; return IEVcost l) in … … 689 741 #acc #S #st1 #st2 #stack #ft lapply acc acc elim ft st2 stack 690 742 [ // ] 691 #st2 #st3 #stack [3 : #f ] #pre #H #G #IH #acc743 #st2 #st3 #stack [3,4: #f ] #pre #H #G #IH #acc 692 744 whd in ⊢ (??%(??%?)); 693 745 >IH >IH >append_nil // … … 718 770 [IEVcall (as_call_ident … «st3, G»)]. 719 771 #S #st1 #st2 #stack #st3 #st4 #ft #taa #H #G 772 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 773 >ft_extend_taa_obs 774 lapply G lapply H lapply ft lapply (taa_end_not_costed … taa) cases taa st2 st3 775 [ #st2 * #ft #H #G >append_nil % 776  #st2 #st2' #st3 #H' #G' #K' #taa #K #ft #H #G 777 >(not_costed_no_label … K) 778 normalize nodelta // 779 ] 780 qed. 781 782 lemma ft_extend_taa_advance_tailcall_obs : ∀S,st1,st2,stack,f,st3,st4. 783 ∀ft : flat_trace S st1 st2 (f :: stack). 784 ∀taa : trace_any_any S st2 st3. 785 ∀H : as_execute S st3 st4.∀G. 786 ft_observables … (ft_advance_tailcall … (ft_extend_taa … ft taa) H G) = 787 ft_observables … ft @ 788 option_to_list … (!l←as_label … st2;return IEVcost l) @ 789 [IEVtailcall f (as_tailcall_ident … «st3, G»)]. 790 #S #st1 #st2 #stack #f #st3 #st4 #ft #taa #H #G 720 791 whd in ⊢ (??%?); >ft_observables_aux_def >append_nil 721 792 >ft_extend_taa_obs … … 805 876 #S1 #S2 #R #st1 #st1' #stack #st2 #ft1 #sim_execute #H #G elim ft1 st1' stack 806 877 [ %{st2} %{st2} %{(ft_start …)} %{(taa_base …)} % [%{H G}] % 807 *: #st1_mid #st1' #stack [3 : #f] #ft1 #ex [2: * [*]] #cl [#ncost_st1']878 *: #st1_mid #st1' #stack [3,4: #f] #ft1 #ex [3: * [*]] #cl [#ncost_st1'] 808 879 (* IH *) * #st2_lab * #st2_mid * #ft2 * #taa ** #L' #G' #S 809 880 [1,2: (* other/jump *) 810 881 lapply (sim_execute … ex G') 811 try >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?);882 try >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); normalize nodelta 812 883 [ #H lapply (H ncost_st1') H ] * 813 884 #st2' *#taaf ** #ncost #G'' #H'' … … 838 909 >S >L' % 839 910 ] 840 3: (* ret*)911 3: (* tailcall *) 841 912 lapply (sim_execute … ex G') 842 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]→?); * 913 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); #H elim (H cl) H 914 * #st2_pre_call #cl' * #EQcall * #st2_after_call * #st2' 915 * #taa2 * #taa2' ** #ex' #G'' #H'' 916 lapply (refl_jmeq … (ft_advance_tailcall … ft1 ex cl)) 917 generalize in match (ft_advance_tailcall … ft1 ex cl) in ⊢ (????%→%); 918 <EQcall in ⊢ (%→???%%→%); 919 #ft1' #EQft1' 920 %{st2_after_call} %{st2'} 921 %[@(ft_advance_tailcall … f … ex' cl') 922 @(ft_extend_taa … (taa_append_taa … taa taa2)) 923 assumption] 924 %{taa2'} 925 % [ %{H'' G''} ] 926 >ft_extend_taa_advance_tailcall_obs 927 lapply EQft1' lapply ft1' ft1' 928 >EQcall in ⊢ (%→???%%→%); 929 #ft1' #EQft1' destruct (EQft1') 930 whd in ⊢ (??%?); 931 >ft_observables_aux_def >append_nil 932 >S >L' % 933 4: (* ret *) 934 lapply (sim_execute … ex G') 935 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); * 843 936 #st2_ret * #st2_after_ret * #st2' * #taa2 * #taa2' 844 937 ***** #ncost #cl' #ex' #G'' #_ #H'' %{st2'} %{st2'} … … 860 953 ] 861 954 >S >L' % 862  4: (* call *)955 5: (* call *) 863 956 lapply (sim_execute … ex G') 864 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?]→?); #H elim (H cl) H957 >cl in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]→?); #H elim (H cl) H 865 958 * #st2_pre_call #cl' ** #EQcall #_ * #st2_after_call * #st2' 866 959 * #taa2 * #taa2' ** #ex' #G'' #H''
Note: See TracChangeset
for help on using the changeset viewer.