Changeset 1713 for src/RTLabs/Traces.ma
 Timestamp:
 Feb 21, 2012, 11:58:12 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1712 r1713 18 18  Callstate _ _ _ _ _ ⇒ cl_call 19 19  Returnstate _ _ _ _ ⇒ cl_return 20  Finalstate _ ⇒ cl_other 20 21 ]. 21 22 … … 43 44 λ_. match s' with 44 45 [ State f fs m ⇒ match stk with [ nil ⇒ False  cons h t ⇒ next h = next f ] 46  Finalstate r ⇒ True 45 47  _ ⇒ False 46 48 ] … … 50 52 ]). 51 53 [ normalize in H; destruct 54  normalize in H; destruct 52 55  whd in H:(??%?); 53 56 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H; … … 369 372 All ? (λf. well_cost_labelled_fn (func f)) fs 370 373  Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs 374  Finalstate _ ⇒ True 371 375 ]. 372 376 … … 385 389  #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 386 390  #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % // 391  // 387 392 ] qed. 388 393 … … 404 409  normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct 405 410  normalize #H8 #H9 #H10 #H11 #H12 destruct 411  #r #E normalize in E; destruct 406 412 ] qed. 407 413 … … 453 459  #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl 454 460  normalize #H411 #H412 #H413 #H414 #H415 destruct 461  normalize #H1 #H2 destruct 455 462 ] qed. 456 463 … … 497 504 next f = next f' → 498 505 stack_of_state (f::fs) s1 → 499 stack_preserved ends_with_ret s1 (State f' fs m). 506 stack_preserved ends_with_ret s1 (State f' fs m) 507  sp_stop : ∀e,s1,r. 508 stack_preserved e s1 (Finalstate r) 509 . 500 510 501 511 discriminator list. … … 507 517 #fs0 #fs0' #s0 * 508 518 [ #f #fs #m #H inversion H 509 #a #b #c #d #e#g try #h try #i try #j destruct @refl519 #a #b #c #d try #e try #g try #h try #i try #j destruct @refl 510 520  #fd #args #dst #f #fs #m #H inversion H 511 #a #b #c #d #e#g try #h try #i try #j destruct @refl521 #a #b #c #d try #e try #g try #h try #i try #j destruct @refl 512 522  #rtv #dst #fs #m #H inversion H 513 #a #b #c #d #e #g try #h try #i try #j destruct @refl 523 #a #b #c #d try #e try #g try #h try #i try #j destruct @refl 524 ] qed. 525 526 lemma stack_preserved_final : ∀e,r,s. 527 stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'. 528 #e #r #s #H inversion H 529 [ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct 530 inversion SOS #a #b #c #d #e #f try #g try #h destruct 531  #H194 #H195 #H196 #H197 #H198 #H199 #SOS #H201 #H202 #H203 #H204 destruct 532 inversion SOS #a #b #c #d #e #f try #g try #h destruct 533  #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl 514 534 ] qed. 515 535 … … 525 545  #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct 526 546 @(sp_finished … N) >(stack_of_state_eq … S1' S2) // 547  #s1'' #r #E1 #E2 #E3 #E4 destruct // 527 548 ] 528 549  #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct 550  #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H 551 cases (stack_preserved_final … H) #r #E destruct // 529 552 ] qed. 530 553 … … 539 562  #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct 540 563  #res #dst * 541 [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct564 [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct  * [ 2: * #r normalize #EV destruct //  *: normalize #a try #b destruct ] ] 542 565  #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV 543 566 whd in EV:(??%?); destruct @(sp_finished ? f) // 544 567 ] 568  #r #s2 #tr #E normalize in E; destruct 545 569 ] qed. 546 570 … … 557 581  #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL 558 582 #E normalize in E; destruct 583  #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct 559 584 ] qed. 560 585 … … 581 606  #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct 582 607  #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct 583 ] 608  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct 609 ] 610  #e #s1 #r #E1 #E2 #E3 #_ destruct // 584 611 ] qed. 585 612 … … 605 632  #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct 606 633  #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct 607 ] 634  #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct 635 ] 636  #e #s1 #r #E1 #E2 #E3 #E4 destruct // 608 637 ] qed. 609 638 … … 751 780 match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth s trace (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with 752 781 [ ft_stop st FINAL ⇒ 753 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?782 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ 754 783 755 784  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. … … 836 865  @le_S_S_to_le @TERMINATES_IN_TIME 837 866  @(wrl_nonzero … TERMINATES_IN_TIME) 838  (* Bad  we've reached the end of the trace; need to fix semantics so that 839 this can't happen *) 867  (* We can't reach the final state because the function terminates with a 868 return *) 869 inversion TERMINATES 870 [ #H214 #H215 #H216 #H217 #H218 #H219 #H220 #H221 #H222 #H223 #H224 #H225 #_ TERMINATES TERMINATES destruct 871  #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 #H236 #H237 #H238 #H239 #H240 TERMINATES TERMINATES destruct 872  #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 #H250 #H251 #H252 #H253 #H254 TERMINATES TERMINATES destruct 873  #H256 #H257 #H258 #H259 #H260 #H261 #H262 #H263 #H264 #H265 TERMINATES TERMINATES destruct 874 ] 840 875  @(will_return_return … CL TERMINATES) 841 876  /2 by stack_preserved_return/ … … 902 937  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 TERMINATES TERMINATES destruct 903 938 ] 904 ] cases daemonqed.939 ] qed. 905 940 906 941 (* We can initialise TIME with a suitably large value based on the length of the … … 918 953 qed. 919 954 920 (* FIXME: there's trouble at the end of the program because we can't make a step 921 away from the final return. 922 923 We need to show that the "next pc" is preserved through a function call. 924 925 Tailcalls are not handled properly (which means that if we try to show the 955 (* Tailcalls would not be handled properly (which means that if we try to show the 926 956 full version with nontermination we'll fail because calls and returns aren't 927 957 balanced. … … 990 1020  Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f)  _ ⇒ None ? ] 991 1021  Returnstate _ _ _ _ ⇒ None ? 1022  Finalstate _ ⇒ None ? 992 1023 ]. 993 1024 … … 1098 1129 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 1099 1130 steps_for_statement (lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) = 1100 match s' with [ State _ _ _ ⇒ 1  Callstate _ _ _ _ _ ⇒ 2  Returnstate _ _ _ _ ⇒ 2 ].1131 match s' with [ State _ _ _ ⇒ 1  Callstate _ _ _ _ _ ⇒ 2  Returnstate _ _ _ _ ⇒ 2  Finalstate _ ⇒ 1 ]. 1101 1132 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' 1102 1133 whd in ⊢ (??%? → ?); … … 1157 1188 normalize in S1; destruct 1158 1189  #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct 1190  #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 destruct 1159 1191 ] 1160 1192 ] … … 1169 1201  #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct 1170 1202 %1 whd in FS ⊢ %; 1171 inversion (stack_preserved_return … EVAL) [ @refl  #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct ]1203 inversion (stack_preserved_return … EVAL) [ @refl  #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct  4: #H276 #H277 #H278 #H279 #H280 #H281 #H282 destruct ] 1172 1204 #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE 1173 1205 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 ] … … 1179 1211  #lx #nx #H #E1x #E2x #_ destruct @H 1180 1212 ] 1213  #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct 1181 1214 ] 1182 1215 ] qed.
Note: See TracChangeset
for help on using the changeset viewer.