Changeset 708
 Timestamp:
 Mar 23, 2011, 2:28:55 PM (9 years ago)
 Location:
 src/Clight
 Files:

 4 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/Cexec.ma
r702 r708 667 667 OK ? 〈ge,Callstate f (nil ?) Kstop m0〉. 668 668 669 let rec is_final (s:state) : option int ≝ 670 match s with 671 [ Returnstate res k m ⇒ 672 match k with 673 [ Kstop ⇒ 674 match res with 675 [ Vint r ⇒ Some ? r 676  _ ⇒ None ? 677 ] 678  _ ⇒ None ? 679 ] 680  _ ⇒ None ? 681 ]. 682 669 683 definition is_final_state : ∀st:state. (Sig ? (final_state st)) + (¬∃r. final_state st r). 670 684 #st elim st; … … 713 727 λs.match s with [ State f s k e m ⇒ m  Callstate f a k m ⇒ m  Returnstate r k m ⇒ m ]. 714 728 715 definition is_final : state → option int ≝716 λs.match is_final_state s with717 [ inl r ⇒ Some ? (sig_eject … r)718  inr _ ⇒ None ?719 ].720 721 729 definition clight_exec : execstep ≝ 722 730 mk_execstep … is_final mem_of_state exec_step. 
src/Clight/CexecComplete.ma
r700 r708 455 455  #f #l #s #k #env #m @refl 456 456 ] qed. 457 458 lemma is_final_complete : ∀s,r. final_state s r → is_final s = Some ? r. 459 #s0 #r0 * #r #m @refl qed. 460 
src/Clight/CexecEquiv.ma
r702 r708 53 53 ((¬∃r.final_state s r) → P (None ?)) → 54 54 P (is_final clight_exec s). 55 #s #P #F #NF whd in ⊢ (?%) cases (is_final_state s) 56 [ * #r #FINAL @F @FINAL 57  #NOTFINAL @NF @NOTFINAL 55 #s #P #F #NF lapply (refl ? (is_final clight_exec s)) 56 cases (is_final clight_exec s) in ⊢ (???% → %) 57 [ #E @NF % * #r #H > (is_final_complete … H) in E #H destruct 58  #r #E @F @is_final_sound @E 58 59 ] qed. 59 60 … … 64 65 >(exec_inf_aux_unfold …) cases x; 65 66 [ #o #k #EXEC whd in EXEC:(??%?); destruct 66  #y cases y ;#tr' #s' whd in ⊢ (??%? → ?)67  #y cases y #tr' #s' whd in ⊢ (??%? → ?) 67 68 @is_final_elim 68 69 [ #r #FINAL  #FINAL ] 69 (* Some trickery to prevent destruct normalizing clight_exec *) 70 #EXEC whd in EXEC:(??%?); [ @False_ind destruct  71 cut (s = s') [ generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #E destruct @refl ] 72 #Es <Es in EXEC #EXEC 73 generalize in EXEC:(??(??????%)?) ⊢ (??%?) 74 #e0 #E destruct @refl 75 ] 70 #EXEC whd in EXEC:(??%?); destruct @refl 76 71  #EXEC whd in EXEC:(??%?); destruct 77 72 ] qed. … … 85 80  #y cases y; #tr' #s' whd in ⊢ (??%? → ?); 86 81 @is_final_elim 87 [ #r ] #FINAL #EXEC whd in EXEC:(??%?) 88 (* Again, prevent destruct blowing up *) 89 [ 2: generalize in EXEC:(??(??????%)?) ⊢ ? #e0 #EXEC ] 90 destruct; 91 @refl 82 [ #r ] #FINAL #EXEC whd in EXEC:(??%?); 83 destruct @refl 92 84  #EXEC whd in EXEC:(??%?); destruct 93 85 ] qed. … … 100 92 [ #o #k #EXEC whd in EXEC:(??%?); destruct 101 93  #y cases y; #tr' #s' whd in ⊢ (??%? → ?) 102 @is_final_elim [ #r #F #EXEC whd in EXEC:(??%?); destruct 103  #F whd in ⊢ (??%? → ?) generalize in ⊢ (??(??????%)? → ?) #e0 #EXEC destruct @F ] 94 @is_final_elim [ #r ] #F #EXEC whd in EXEC:(??%?); destruct @F 104 95  #EXEC whd in EXEC:(??%?); destruct 105 96 ] qed. … … 111 102 se_step tr s e = se_step tr' s' e' → 112 103 tr = tr' ∧ s = s' ∧ e = e'. 113 #tr #s #e #tr' #s' #e' #E 114 (* destruct This takes a hideous amount of time, not sure why. *) 115 @(match E return λl.λ_. match l with [ se_step tr0 s0 e0 ⇒ tr = tr0 ∧ s = s0 ∧ e = e0  _ ⇒ False ] with [ refl ⇒ ? ]) 116 whd % try % @refl qed. 104 #tr #s #e #tr' #s' #e' #E destruct 105 % try % @refl qed. 117 106 118 107 lemma exec_from_step : ∀ge,s,tr,s',e. … … 121 110 #ge #s0 #tr0 #s0' #e0 #H inversion H; 122 111 [ #tr #r #m #E1 #E2 destruct 123  #tr #s #e #se #H1 #H2 #E (* destruct (E);*)124 lapply (se_step_eq … E) ** #E1 #E2 #E3 >E1 >E2 >E3112  #tr #s #e #se #H1 #H2 #E (* destruct (E) ;*) 113 cases (se_step_eq … E) * #E1 #E2 #E3 >E1 >E2 >E3 125 114 >(exec_e_step_inv … H2) 126 115 <(exec_e_step … H2) in H1 #H1 % // … … 129 118 ] qed. 130 119 131 axiomexec_from_interact : ∀ge,s,o,k,i,tr,s',e.120 lemma exec_from_interact : ∀ge,s,o,k,i,tr,s',e. 132 121 exec_from ge s (se_interact o k i (se_step tr s' e)) → 133 122 step ge s tr s' ∧ 134 123 (*exec_step ge s = Value ??? 〈tr,s'〉 ∧*) exec_from ge s' e. 135 (*136 124 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; 137 125 [ #tr #r #m #E1 #E2 destruct 138 126  #tr #s #e #se #H1 #H2 #E destruct (E) 139 127  #_ #E destruct 140  #o #k #i #se #H1 #H2 #E (*destruct (E);*)128  #o #k #i #se #H1 #H2 #E destruct (E); 141 129 lapply (exec_step_sound ge s0); 142 130 cases (exec_step ge s0) in H2 ⊢ %; … … 147 135 [ #tr #r #m #E1 #E2 destruct 148 136  #tr' #s' #e' #se' #H2 #H3 #E2 destruct (E2); 149 <(exec_e_step … H3) in H2 #H2 % //;137 <(exec_e_step … H3) in H2 #H2 % [ 2: @H2 ] 150 138 lapply (STEP i); 151 139 >(exec_e_step_inv … H3) … … 155 143 ] 156 144  #x cases x; #tr' #s' >(exec_inf_aux_unfold …) 157 whd in ⊢ (??%? → ?); cases (is_final_state s');158 #F #E whd in E:(??%?); destruct145 whd in ⊢ (??%? → ?); @is_final_elim 146 [ #r ] #F #E whd in E:(??%?); destruct 159 147  >(exec_inf_aux_unfold …) 160 148 #E' whd in E':(??%?); destruct (E'); 161 149 ] 162 ] qed. *)163 164 axiomexec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m.150 ] qed. 151 152 lemma exec_from_interact_stop : ∀ge,s,o,k,i,tr,r,m. 165 153 exec_from ge s (se_interact o k i (se_stop tr r m)) → 166 154 step ge s tr (Returnstate (Vint r) Kstop m). 167 (*168 155 #ge #s0 #o0 #k0 #i0 #tr0 #s0' #e0 #H inversion H; 169 156 [ #tr #r #m #E1 #E2 destruct … … 183 170 [ #o2 #k2 #E whd in E:(??%?); destruct (E) 184 171  #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?); 185 cases (is_final_state s2);186 [ # F cases F; #r' #FINAL #E whd in E:(??%?);172 @is_final_elim 173 [ #r' #FINAL #E whd in E:(??%?); 187 174 destruct (E); 188 175 inversion FINAL; … … 197 184 ] 198 185  #x cases x; #tr #s whd in ⊢ (??%? → ?); 199 cases (is_final_state s);#F #E whd in E:(??%?); destruct (E)186 @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct (E) 200 187  #E whd in E:(??%?); destruct (E) 201 188 ] 202 ] qed. *)189 ] qed. 203 190 204 191 (* NB: the E0 in the execs are irrelevant. *) … … 282 269 ] qed. 283 270 284 axiomfinal_step: ∀ge,tr,r,m,s.271 lemma final_step: ∀ge,tr,r,m,s. 285 272 exec_from ge s (se_stop tr r m) → 286 273 step ge s tr (Returnstate (Vint r) Kstop m). 287 (*288 274 #ge #tr #r #m #s #EXEC 289 275 whd in EXEC; … … 295 281 [ #o #k #EXEC' whd in EXEC':(??%?); destruct (EXEC'); 296 282  #x cases x; #tr'' #s' whd in ⊢ (??%? → ?); 297 cases (is_final_state s'); #F [ 1: cases F; #r'' #FINAL]283 @is_final_elim [ #r'' #FINAL  #F ] 298 284 #EXEC' whd in EXEC':(??%?); destruct (EXEC'); 299 285  #EXEC' whd in EXEC':(??%?); destruct (EXEC'); … … 304 290  #EXEC' #E destruct 305 291  #o #k #i #e #H #EXEC #E destruct 306 ] qed. *)292 ] qed. 307 293 308 294 … … 396 382 [ #o #k #EXEC whd in EXEC:(??%?); destruct 397 383  #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?) @is_final_elim 398 [ #r ] #F #E whd in E:(??%?); [ destruct  generalize in E:(??(??????%)?) ⊢ ? #e0 #E destruct; @F ]384 [ #r ] #F #E whd in E:(??%?); destruct @F 399 385  #E whd in E:(??%?); destruct 400 386 ] … … 423 409 [ #o2 #k2 #EXECK whd in EXECK:(??%?); destruct 424 410  #x cases x; #tr2 #s2 whd in ⊢ (??%? → ?); 425 cases (is_final_state s2);#F #EXECK411 @is_final_elim [ #r ] #F #EXECK 426 412 whd in EXECK:(??%?); destruct; 427 413 @(absurd ?? F) … … 433 419 ] 434 420  #x cases x; #tr1 #s1 whd in ⊢ (??%? → ?); 435 cases (is_final_state s1);#F #E whd in E:(??%?); destruct;421 @is_final_elim [ #r ] #F #E whd in E:(??%?); destruct; 436 422  #E whd in E:(??%?); destruct 437 423 ] … … 465 451 @IH 466 452 [ @(exec_from_interact_step_notfinal … EXEC) 467  cases (exec_from_interact … EXEC) ; //;453  cases (exec_from_interact … EXEC) #STEP #EF1 @EF1 468 454 ] 469 455 ] … … 714 700 >E2 in H1 #H1 whd in H1:(?%?); >K' in H1 715 701 >(exec_inf_aux_unfold …) whd in ⊢ (?%? → ?); 716 cases (is_final_state s'');717 [ # F whd in ⊢ (?%? → ?); #S702 @is_final_elim 703 [ #r #F whd in ⊢ (?%? → ?); #S 718 704 @False_ind @(absurd ? S) cases (se_inv … S) 719 705  #NF #S whd in S:(?%?); cases (se_inv … S); 720 706 *; #E1 #E2 #S' <E1 @TR 721 707 ] 722  #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?) ;723 cases (is_final_state s'');#F #E whd in E:(?%?);708  #x cases x; #tr' #s'' #H whd in ⊢ (?%? → ?) 709 @is_final_elim [ #r ] #F #E whd in E:(?%?); 724 710 inversion E; 725 711 [ 1,5: #tr1 #e1 #m1 #E1 #E2 destruct … … 909 895 cases (H i); #tr1 *; #s1 *; #K #E >K in H2 910 896 >(exec_inf_aux_unfold …) 911 whd in ⊢ (?%? → ?) ; cases (is_final_state s1);897 whd in ⊢ (?%? → ?) @is_final_elim [ #r ] 912 898 #F #S whd in S:(?%?); cases (se_inv … S); 913  #x cases x; #tr' #s' whd in ⊢ (?%? → ?) ;914 cases (is_final_state s');#F #S whd in S:(?%?);899  #x cases x; #tr' #s' whd in ⊢ (?%? → ?) 900 @is_final_elim [ #r ] #F #S whd in S:(?%?); 915 901 cases (se_inv … S); 916 902  #S cases (se_inv … S); … … 926 912 cases (H i); #tr1 *; #s1 *; #K #E >K in H2 927 913 >(exec_inf_aux_unfold …) 928 whd in ⊢ (?%? → ?) ; cases (is_final_state s1);914 whd in ⊢ (?%? → ?) @is_final_elim [ #r ] 929 915 #F #S whd in S:(?%?); cases (se_inv … S); 930  #x cases x; #tr' #s' whd in ⊢ (?%? → ?) ;931 cases (is_final_state s');#F #S whd in S:(?%?);916  #x cases x; #tr' #s' whd in ⊢ (?%? → ?) 917 @is_final_elim [ #r ] #F #S whd in S:(?%?); 932 918 cases (se_inv … S); 933 919  #S cases (se_inv … S); … … 1005 991 1006 992 lemma initial_step: ∀ge,s,e. 1007 exec_inf_aux ge (Value ??? 〈E0,s〉) = e →993 exec_inf_aux clight_exec ge (Value ??? 〈E0,s〉) = e → 1008 994 ¬(∃r.final_state s r) → 1009 ∃e'.e = e_step E0 s e'.995 ∃e'.e = e_step ??? E0 s e'. 1010 996 #ge #s #e >(exec_inf_aux_unfold …) 1011 whd in ⊢ (??%? → ?) ; cases (is_final_state s);1012 [ # FINAL #EXEC #NOTFINAL997 whd in ⊢ (??%? → ?) @is_final_elim 998 [ #r #FINAL #EXEC #NOTFINAL 1013 999 @False_ind @(absurd ?? NOTFINAL) 1014 cases FINAL; 1015 #r #F %{r} @F 1000 %{r} @FINAL 1016 1001  #F1 #EXEC #F2 whd in EXEC:(??%?); % [ 2: <EXEC @refl ] 1017 1002 qed. … … 1030 1015 cases INITIAL; #Ege #INITIAL'' 1031 1016 >(exec_inf_aux_unfold …) 1032 whd in ⊢ (?%? → ?) ;1033 cases (is_final_state s);1034 [ # F @False_ind1017 whd in ⊢ (?%? → ?) 1018 @is_final_elim 1019 [ #r #F @False_ind 1035 1020 @(absurd ?? (initial_state_not_final … INITIAL'')) 1036 cases F; #r #F' %{r} @F'1021 %{r} @F 1037 1022  #NOTFINAL whd in ⊢ (?%? → ?); cases e; 1038 1023 [ #tr #r #m #EXEC0  #tr #s' #e0 #EXEC0  #EXEC0  #o #k #i #e #EXEC0 ] 
src/Clight/CexecSound.ma
r700 r708 536 536 ] 537 537 qed. 538 539 lemma is_final_sound: ∀s,r. is_final s = Some ? r → final_state s r. 540 * [ 3: #v * [ #m #r cases v [ 2: #r' #E normalize in E; destruct % 541  *: normalize #x1 try #x2 try #x3 try #x4 try #x5 destruct 542 ] 543  *: normalize #x1 try #x2 try #x3 try #x4 try #x5 try #x6 try #x7 destruct 544 ] 545  *: normalize #x1 #x2 #x3 #x4 #x5 #x6 try #x7 destruct 546 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.