Changeset 797 for src/Clight/CexecEquiv.ma
 Timestamp:
 May 13, 2011, 1:10:23 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/CexecEquiv.ma
r732 r797 9 9  se_stop : trace → int → mem → s_execution 10 10  se_step : trace → state → s_execution → s_execution 11  se_wrong : s_execution11  se_wrong : errmsg → s_execution 12 12  se_interact : ∀o:io_out. (io_in o → execution state io_out io_in) → io_in o → s_execution → s_execution. 13 13 … … 17 17 single_exec_of e se → 18 18 single_exec_of (e_step ??? tr s e) (se_step tr s se) 19  seo_wrong : single_exec_of (e_wrong ???) se_wrong19  seo_wrong : ∀msg:errmsg. single_exec_of (e_wrong ??? msg) (se_wrong msg) 20 20  seo_interact : ∀o,k,i,se. 21 21 single_exec_of (k i) se → … … 69 69 [ #r #FINAL  #FINAL ] 70 70 #EXEC whd in EXEC:(??%?); destruct @refl 71  # EXEC whd in EXEC:(??%?); destruct71  #msg #EXEC whd in EXEC:(??%?); destruct 72 72 ] qed. 73 73 … … 82 82 [ #r ] #FINAL #EXEC whd in EXEC:(??%?); 83 83 destruct @refl 84  # EXEC whd in EXEC:(??%?); destruct84  #msg #EXEC whd in EXEC:(??%?); destruct 85 85 ] qed. 86 86 … … 93 93  #y cases y; #tr' #s' whd in ⊢ (??%? → ?) 94 94 @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F 95  # EXEC whd in EXEC:(??%?); destruct95  #msg #EXEC whd in EXEC:(??%?); destruct 96 96 ] qed. 97 97 … … 114 114 >(exec_e_step_inv … H2) 115 115 <(exec_e_step … H2) in H1 #H1 % // 116  # _ #E destruct116  #msg #_ #E destruct 117 117  #o #k #i #se #H1 #H2 #E destruct 118 118 ] qed. … … 125 125 [ #tr #r #m #E1 #E2 destruct 126 126  #tr #s #e #se #H1 #H2 #E destruct (E) 127  # _ #E destruct127  #msg #_ #E destruct 128 128  #o #k #i #se #H1 #H2 #E destruct (E); 129 129 lapply (exec_step_sound ge s0); … … 139 139 >(exec_e_step_inv … H3) 140 140 #S @S 141  # _ #E destruct141  #msg #_ #E destruct 142 142  #o #k #i #se #H1 #H2 #E destruct 143 143 ] … … 145 145 whd in ⊢ (??%? → ?); @is_final_elim 146 146 [ #r ] #F #E whd in E:(??%?); destruct 147  >(exec_inf_aux_unfold …)147  #msg >(exec_inf_aux_unfold …) 148 148 #E' whd in E':(??%?); destruct (E'); 149 149 ] … … 156 156 [ #tr #r #m #E1 #E2 destruct 157 157  #tr #s #e #se #H1 #H2 #E destruct (E) 158  # _ #E destruct158  #msg #_ #E destruct 159 159  #o #k #i #se #H1 #H2 #E destruct (E); 160 160 lapply (exec_step_sound ge s0); … … 177 177  #NF #E whd in E:(??%?); destruct (E) 178 178 ] 179  # E whd in E:(??%?); destruct (E)179  #msg #E whd in E:(??%?); destruct (E) 180 180 ] 181 181  #tr #s #e #e' #H #EXEC #E destruct (E) 182  # EXEC #E destruct (E)182  #msg #EXEC #E destruct (E) 183 183  #o2 #k2 #i2 #e2 #H #EXEC #E destruct (E) 184 184 ] 185 185  #x cases x; #tr #s whd in ⊢ (??%? → ?); 186 186 @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E) 187  # E whd in E:(??%?); destruct (E)187  #msg #E whd in E:(??%?); destruct (E) 188 188 ] 189 189 ] qed. … … 250 250 251 251 inductive execution_goes_wrong: trace → state → s_execution → state → Prop ≝ 252  go_wrong: ∀tr,s,s',e .253 execution_isteps tr s e s' se_wrong→252  go_wrong: ∀tr,s,s',e,msg. 253 execution_isteps tr s e s' (se_wrong msg) → 254 254 execution_goes_wrong tr s (se_step E0 s e) s'. 255 255 … … 283 283 @is_final_elim [ #r'' #FINAL  #F ] 284 284 #EXEC' whd in EXEC':(??%?); destruct (EXEC'); 285  # EXEC' whd in EXEC':(??%?); destruct (EXEC');285  #msg #EXEC' whd in EXEC':(??%?); destruct (EXEC'); 286 286 ] 287 287 inversion FINAL; #r''' #m' #E1 #E2 #H destruct (E1 E2); 288 288 @H 289 289  #tr' #s' #e' #se' #H #EXEC' #E destruct 290  # EXEC' #E destruct290  #msg #EXEC' #E destruct 291 291  #o #k #i #e #H #EXEC #E destruct 292 292 ] qed. … … 304 304  #F #EXEC whd in EXEC:(??%?); destruct (EXEC); 305 305 ] 306  # EXEC whd in EXEC:(??%?); destruct (EXEC);306  #msg #EXEC whd in EXEC:(??%?); destruct (EXEC); 307 307 ] qed. 308 308 … … 355 355 qed. 356 356 357 lemma exec_from_wrong: ∀ge,s .358 exec_from ge s se_wrong→359 exec_step ge s = Wrong ??? .360 #ge #s # H whd in H;357 lemma exec_from_wrong: ∀ge,s,msg. 358 exec_from ge s (se_wrong msg) → 359 exec_step ge s = Wrong ??? msg. 360 #ge #s #msg #H whd in H; 361 361 inversion H; 362 362 [ #tr #r #m #EXEC #E destruct (E) … … 364 364  >(exec_inf_aux_unfold …) 365 365 cases (exec_step ge s); 366 [ #o #k # EXEC whd in EXEC:(??%?); destruct367  #x cases x; #tr #s' whd in ⊢ (??%? → ?) @is_final_elim366 [ #o #k #msg' #EXEC whd in EXEC:(??%?); destruct 367  #x cases x; #tr #s' #msg' whd in ⊢ (??%? → ?) @is_final_elim 368 368 [ #r ] #F #EXEC whd in EXEC:(??%?); destruct 369  //369  #msg1 #msg2 #EXEC #E whd in EXEC:(??%?) destruct @refl 370 370 ] 371 371  #o #k #i #e #H #EXEC #E destruct … … 383 383  #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim 384 384 [ #r ] #F #E whd in E:(??%?); destruct @F 385  # E whd in E:(??%?); destruct386 ] 387  # EXEC #E destruct385  #msg #E whd in E:(??%?); destruct 386 ] 387  #msg #EXEC #E destruct 388 388  #o #k #i #e' #H #EXEC #E destruct 389 389 ] qed. … … 397 397 [ #tr' #r #m #EXEC #E destruct 398 398  #tr' #s'' #e' #e'' #H #EXEC #E destruct (E); 399  # EXEC #E destruct399  #msg #EXEC #E destruct 400 400  #o' #k' #i' #e' #H #EXEC #E destruct; 401 401 >(exec_inf_aux_unfold …) in EXEC; … … 413 413 @(absurd ?? F) 414 414 %{ r'} //; 415  # E whd in E:(??%?); destruct415  #msg #E whd in E:(??%?); destruct 416 416 ] 417  # EXECK #E whd in E:(??%?); destruct417  #msg #EXECK #E whd in E:(??%?); destruct 418 418  #o2 #k2 #i2 #e2 #H2 #EXECK #E destruct 419 419 ] 420 420  #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?); 421 421 @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct; 422  # E whd in E:(??%?); destruct422  #msg #E whd in E:(??%?); destruct 423 423 ] 424 424 ] qed. … … 432 432 (¬∃r. final_state s' r). 433 433 #ge #tr0 #s0 #s0' #e0 #WRONG inversion WRONG; 434 #tr #s #s' #e # ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4);434 #tr #s #s' #e #msg #ESTEPS #E1 #E2 #E3 #E4 #EXEC #NOTFINAL destruct (E1 E2 E3 E4); 435 435 cases (several_steps … ESTEPS EXEC); 436 436 #STAR #EXEC' % … … 492 492 cases e1; //; qed. 493 493 494 lemma opt_does_not_interact: ∀A,B,P,e1,e2 .494 lemma opt_does_not_interact: ∀A,B,P,e1,e2,msg. 495 495 (∀x:B.interact_prop A P (e2 x)) → 496 interact_prop A P (bindIO ?? B A (opt_to_io ??? e1) e2).497 #A #B #P #e1 #e2 # H496 interact_prop A P (bindIO ?? B A (opt_to_io ??? msg e1) e2). 497 #A #B #P #e1 #e2 #msg #H 498 498 cases e1; //; qed. 499 499 … … 609 609 ] qed. 610 610 611 lemma eno_wrong: execution_not_over se_wrong→ False.612 # H inversion H;611 lemma eno_wrong: ∀msg. execution_not_over (se_wrong msg) → False. 612 #msg #H inversion H; 613 613 [ #tr #s #e #E destruct 614 614  #o #k #tr #s #e #i #E destruct … … 641 641 ] 642 642 ] 643  # _ #_ #_ #ENO elim (eno_wrong … ENO);643  #msg #_ #_ #_ #ENO elim (eno_wrong … ENO); 644 644  #o #k #i #e' #UNREACTIVE #NONTERMINATING #CONTINUES #_ 645 645 lapply (CONTINUES E0 s o k i e' (isteps_none …)); … … 678 678 [ e_stop tr r m ⇒ match e2 with [ se_stop tr' r' m' ⇒ tr = tr' ∧ r = r' ∧ m = m'  _ ⇒ False ] 679 679  e_step tr s e1' ⇒ match e2 with [ se_step tr' s' e2' ⇒ tr = tr' ∧ s = s' ∧ single_exec_of e1' e2'  _ ⇒ False ] 680  e_wrong ⇒ match e2 with [ se_wrong⇒ True  _ ⇒ False ]680  e_wrong _ ⇒ match e2 with [ se_wrong _ ⇒ True  _ ⇒ False ] 681 681  e_interact o k ⇒ match e2 with [ se_interact o' k' i e ⇒ o' = o ∧ k' ≃ k ∧ single_exec_of (k' i) e  _ ⇒ False ] 682 682 ]. … … 685 685 [ #tr #r #m whd; % [ % ] // 686 686  #tr #s #e1' #e2' #H' whd; % [ % ] // 687  whd; //687  #msg whd; // 688 688  #o #k #i #e #H' whd; % [ % ] // 689 689 ] qed. … … 711 711 [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct 712 712  2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct 713  3,7: # E destruct713  3,7: #msg #E destruct 714 714  4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct 715 715 ] 716  # _ #E whd in E:(?%?);716  #msg #_ #E whd in E:(?%?); 717 717 inversion E; 718 718 [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct 719 719  2,6: #tr #s1 #e1 #e2 #H #E1 #E2 destruct 720  3,7: # E1 #E2 destruct720  3,7: #msg #E1 #E2 destruct 721 721  4,8: #o1 #k1 #i1 #e1 #H1 #E1 #E2 destruct 722 722 ] … … 874 874  #tr' #s'' #e' #STEPS *; #NOSTEP @False_rect_Type0 875 875 @NOSTEP // 876  # STEPS #NOSTEP876  #msg #STEPS #NOSTEP 877 877 @(ec_wrong ? s s' tr) % //; 878 878 (* The following is stupidly complicated when most of the cases are impossible. … … 885 885  #tr1 #s1 #e1 #STEPS *; #NOSTEP 886 886 @False_ind @NOSTEP // 887  # STEPS #NOSTEP887  #msg #STEPS #NOSTEP 888 888 lapply (exec_step_interaction ge s'); 889 889 cases (several_steps … STEPS EXEC); #_ … … 900 900 @is_final_elim [ #r ] #F #S whd in S:(?%?); 901 901 cases (se_inv … S); 902  # S cases (se_inv … S);902  #msg #S cases (se_inv … S); 903 903 ] 904 904  #o1 #k1 #i1 #e1 #STEPS #NOSTEP … … 917 917 @is_final_elim [ #r ] #F #S whd in S:(?%?); 918 918 cases (se_inv … S); 919  # S cases (se_inv … S);919  #msg #S cases (se_inv … S); 920 920 ] 921 921 ] … … 937 937 execution_goes_wrong tr s e s' → 938 938 execution_matches_behavior e (Goes_wrong tr) 939  emb_initially_wrong: 940 execution_matches_behavior se_wrong(Goes_wrong E0).939  emb_initially_wrong: ∀msg. 940 execution_matches_behavior (se_wrong msg) (Goes_wrong E0). 941 941 942 942 lemma exec_state_terminates: ∀tr,tr',s,s',e,r,m. … … 960 960 execution_goes_wrong tr s (se_step tr' s' e) s'' → s = s'. 961 961 #tr #tr' #s #s' #s'' #e #H inversion H; 962 #tr1 #s1 #s2 #e1 # H' #E1 #E2 #E3 #E4 destruct; @refl qed.962 #tr1 #s1 #s2 #e1 #msg #H' #E1 #E2 #E3 #E4 destruct; @refl qed. 963 963 964 964 lemma behavior_of_execution: ∀s,e. … … 1021 1021 %{r} @F 1022 1022  #NOTFINAL whd in ⊢ (?%? → ?); cases e; 1023 [ #tr #r #m #EXEC0  #tr #s' #e0 #EXEC0  # EXEC0  #o #k #i #e #EXEC0 ]1023 [ #tr #r #m #EXEC0  #tr #s' #e0 #EXEC0  #msg #EXEC0  #o #k #i #e #EXEC0 ] 1024 1024 cases (se_inv … EXEC0); *; #E1 #E2 <E1 <E2 #EXEC' 1025 1025 lapply (behavior_of_execution ?? … … 1060 1060 lapply (exec_state_wrong … WRONG); 1061 1061 #E1 >E1 in WRONG #WRONG 1062 inversion WRONG; #tr' #s1' #s2' #e'' # GOESWRONG #E4 #E5 #E6 #E71062 inversion WRONG; #tr' #s1' #s2' #e'' #msg #GOESWRONG #E4 #E5 #E6 #E7 1063 1063 <E4 in GOESWRONG ⊢ % <E5 <E7 #GOESWRONG 1064 1064 cut (e0 = e''); [ destruct (E6) skip (INITIAL Ege MATCHES EXEC0 EXEC'); // ] … … 1067 1067 @(program_goes_wrong (mk_transrel … step) ?? ge s … INITIAL'' STAR STOP) 1068 1068 #r % #F @(absurd ?? FINAL) %{r} @F 1069  # E destruct (E);1069  #msg #E destruct (E); 1070 1070 ] 1071 1071 ] 1072  whd in ⊢ ((∀_.? → %) → ?);1072  #msg whd in ⊢ ((∀_.? → %) → ?); 1073 1073 #NOINIT #_ #EXEC 1074 1074 %{ (Goes_wrong E0)} % 1075 1075 [ whd in EXEC:(?%?); 1076 1076 cases e in EXEC; 1077 [ #tr #r #m #EXEC0  #tr #s' #e0 #EXEC0  # EXEC0  #o #k #i #e #EXEC0 ]1077 [ #tr #r #m #EXEC0  #tr #s' #e0 #EXEC0  #msg #EXEC0  #o #k #i #e #EXEC0 ] 1078 1078 cases (se_inv … EXEC0); 1079 1079 @emb_initially_wrong
Note: See TracChangeset
for help on using the changeset viewer.