 Timestamp:
 Feb 24, 2012, 1:19:10 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1719 r1736 43 43 [ Callstate fd args dst stk m ⇒ 44 44 λ_. match s' with 45 [ State f fs m ⇒ match stk with [ nil ⇒ False  cons h t ⇒ next h = next f ]46  Finalstate r ⇒ True45 [ State f fs m ⇒ match stk with [ nil ⇒ False  cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ] 46  Finalstate r ⇒ stk = [ ] 47 47  _ ⇒ False 48 48 ] … … 569 569  sp_finished : ∀s1,f,f',fs,m. 570 570 next f = next f' → 571 frame_rel f f' → 571 572 stack_of_state (f::fs) s1 → 572 573 stack_preserved ends_with_ret s1 (State f' fs m) 573  sp_stop : ∀e,s1,r. 574 stack_preserved e s1 (Finalstate r) 574  sp_stop : ∀s1,r. 575 stack_of_state [ ] s1 → 576 stack_preserved ends_with_ret s1 (Finalstate r) 577  sp_top : ∀fd,args,dst,m,r. 578 stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r) 575 579 . 576 580 … … 591 595 592 596 lemma stack_preserved_final : ∀e,r,s. 593 stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'.594 #e #r #s #H inversion H597 ¬stack_preserved e (Finalstate r) s. 598 #e #r #s % #H inversion H 595 599 [ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct 596 600 inversion SOS #a #b #c #d #e #f try #g try #h destruct 597  #H194 #H195 #H196 #H197 #H198 #H199 # SOS #H201 #H202 #H203 #H204 destruct601  #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct 598 602 inversion SOS #a #b #c #d #e #f try #g try #h destruct 599  #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl 603  #s' #r' #SOS #E1 #E2 #E3 #E4 destruct 604 inversion SOS #a #b #c #d #e #f try #g try #h destruct 605  #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct 600 606 ] qed. 601 607 … … 609 615 [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct 610 616 @(sp_normal fs) // <(stack_of_state_eq … S1' S2) // 611  #s1'' #f #f' #fs' #m #N # S1' #E1 #E2 #E3 #E4 destruct617  #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct 612 618 @(sp_finished … N) >(stack_of_state_eq … S1' S2) // 613  #s1'' #r #E1 #E2 #E3 #E4 destruct // 619  #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) // 620  #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct 621 inversion S2 622 [ #H34 #H35 #H36 #H37 #H38 #H39 destruct 623  #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct 624  #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct 625 ] 614 626 ] 615 627  #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct 616 628  #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H 617 cases (stack_preserved_final … H) #r #E destruct // 629 cases (stack_preserved_final … H) #r #E destruct 630  #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥ 631 @(absurd … F) // 618 632 ] qed. 619 633 … … 628 642  #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct 629 643  #res #dst * 630 [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct  * [ 2: * #r normalize #EV destruct //  *: normalize #a try #b destruct ] ] 644 [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; 645 [ normalize #EV destruct  * [ 2: * #r normalize #EV destruct /2/  *: normalize #a try #b destruct ] ] 631 646  #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV 632 647 whd in EV:(??%?); destruct @(sp_finished ? f) // 648 cases f // 633 649 ] 634 650  #r #s2 #tr #E normalize in E; destruct … … 660 676 inversion SP 661 677 [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct 662  #s2' #f #f' #fs #m' #N # S #E1 #E2 #E3 #E4 destruct678  #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct 663 679 inversion (eval_perserves … EV) 664 680 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct … … 674 690  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct 675 691 ] 676  #e #s1 #r #E1 #E2 #E3 #_ destruct // 692  #s1 #r #S1 #E1 #E2 #E3 #_ destruct 693 inversion (eval_perserves … EV) 694 [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct 695  #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct 696  #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct 697 inversion S1 698 [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/ 699  #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct 700  #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct 701 ] 702  #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct 703  #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct 704  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct 705 ] 706  #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct 677 707 ] qed. 678 708 … … 686 716 inversion S23 687 717 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct 688  #s2' #f #f' #fs #m' #N # S #E1 #E2 #E3 #E4 destruct718  #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct 689 719 inversion (eval_perserves … EV) 690 720 [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct … … 692 722  #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct 693 723 inversion S 694 [ #fy #fsy #my #E1 #E2 #E3 destruct @N724 [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N  inversion F // ] 695 725  #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct 696 726  #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct … … 700 730  #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct 701 731 ] 702  #e #s1 #r #E1 #E2 #E3 #E4 destruct // 732  #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd 733 inversion (eval_perserves … EV) 734 [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct 735  #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct 736  #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct 737 inversion S1 738 [ #H103 #H104 #H105 #H106 #H107 #H108 destruct // 739  #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct 740  #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct 741 ] 742  #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct 743  #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct 744  #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct 745 ] 746  #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct 703 747 ] qed. 704 748 … … 1244 1288 ] qed. 1245 1289 1290 lemma bound_after_call : ∀ge,s,s',n. 1291 state_bound_on_steps_to_cost s (S n) → 1292 ∀CL:RTLabs_classify s = cl_call. 1293 as_after_return (RTLabs_status ge) «s, CL» s' → 1294 RTLabs_cost s' = false → 1295 state_bound_on_steps_to_cost s' n. 1296 #ge #s #s' #n #H inversion H 1297 [ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL) 1298 #fn * #args * #dst * #stk * #m' #E destruct 1299  #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct 1300 whd in S; #CL cases s' 1301 [ #f' #fs' #m' * #N #F #CS 1302 %1 whd 1303 inversion S 1304 [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥ 1305 change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P * 1306  #l #n #B #E1 #E2 #_ destruct <N <F @B 1307 ] 1308  #fd' #args' #dst' #fs' #m' * 1309  #rv #dst' #fs' #m' * 1310  #r #E normalize in E; destruct 1311 ] 1312  #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct 1313 ] qed. 1314 1246 1315 lemma bound_after_step : ∀ge,s,tr,s',n. 1247 1316 state_bound_on_steps_to_cost s (S n) → … … 1291 1360  #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct 1292 1361 %1 whd in FS ⊢ %; 1293 inversion (stack_preserved_return … EVAL) [ @refl  #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct  4: #H276 #H277 #H278 #H279 #H280 #H281 #H282destruct ]1294 #s1 #f1 #f2 #fs #m #FE # SS1 #_ #E1 #E2 #_ destruct <FE1362 inversion (stack_preserved_return … EVAL) [ @refl  2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ] 1363 #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE 1295 1364 inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct  #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct  #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ] 1296 1365 inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct … … 1414 1483 cases (terminates … tlr) // 1415 1484  (* FIXME: postcall notwrong *) 1416  (* FIXME: bound on steps after call *) 1485  @(bound_after_call ge … LABEL_LIMIT CL ? CS) 1486 @(RTLabs_after_call … CL EV) @(stack_ok … tlr) 1417 1487  @(well_cost_labelled_state_step … EV) // 1418 1488  @(well_cost_labelled_call … EV) //
Note: See TracChangeset
for help on using the changeset viewer.