Changeset 1719
 Timestamp:
 Feb 22, 2012, 2:06:52 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1713 r1719 93 93 ] qed. 94 94 95 inductive flat_trace_prefix (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s,s'. flat_trace o i ge s → flat_trace o i ge s' → Prop ≝96  ftp_refl : ∀s,t. flat_trace_prefix o i ge s s t t97  ftp_step : ∀s1,tr,s2,s3,t2,t3,EV.98 flat_trace_prefix o i ge s2 s3 t2 t3 →99 flat_trace_prefix o i ge s1 s3 (ft_step o i ge s1 tr s2 EV t2) t3100 .101 102 lemma concatenate_flat_trace_prefix : ∀o,i,ge,s1,s2,s3,t1,t2,t3.103 flat_trace_prefix o i ge s1 s2 t1 t2 →104 flat_trace_prefix o i ge s2 s3 t2 t3 →105 flat_trace_prefix o i ge s1 s3 t1 t3.106 #o #i #ge #s1 #s2 #s3 #t1 #t2 #t3 #p1 elim p1107 [ //108  #s1' #tr #s2' #s3' #t2' #t3' #EV #p2 #IH #p3109 %2 /2/110 ] qed.111 112 95 let corec make_flat_trace ge s 113 96 (H:exec_no_io … (exec_inf_aux … RTLabs_fullexec ge (eval_statement ge s))) : … … 291 274 normalize #E destruct 292 275 qed. 276 277 let rec will_return_end ge d s tr (T:will_return ge d s tr) on T : 𝚺s'.flat_trace io_out io_in ge s' ≝ 278 match T with 279 [ wr_step _ _ _ _ _ _ _ T' ⇒ will_return_end … T' 280  wr_call _ _ _ _ _ _ _ T' ⇒ will_return_end … T' 281  wr_ret _ _ _ _ _ _ _ T' ⇒ will_return_end … T' 282  wr_base _ _ _ _ tr' _ ⇒ mk_DPair ? (λs.flat_trace io_out io_in ge s) ? tr' 283 ]. 293 284 294 285 (* Inversion lemmas on [will_return] that also note the effect on the length … … 297 288 RTLabs_classify s = cl_call → 298 289 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). 299 ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' .290 ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'. 300 291 #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM 301 292 [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct 302  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % / /293  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % /2/ 303 294  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct 304 295  #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct … … 309 300 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). 310 301 match d with 311 [ O ⇒ True302 [ O ⇒ will_return_end … TM = ❬s', trace❭ 312 303  S d' ⇒ 313 ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' 304 ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM' 314 305 ]. 315 306 #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM 316 307 [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct 317 308  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥ destruct >CL in H39; #E destruct 318  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % / /319  #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @ I309  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % /2/ 310  #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @refl 320 311 ] qed. 321 312 … … 323 314 (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) → 324 315 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). 325 ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' .316 ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM' ∧ will_return_end … TM = will_return_end … TM'. 326 317 #ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM 327 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % / /318 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % /2/ 328 319  #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct 329 320  #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct 330 321  #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct 331  #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % / /322  #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % /2/ 332 323  #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct 333 324  #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct 334 325  #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct 326 ] qed. 327 328 (* When it comes to building bits of nonterminating executions we'll need to be 329 able to glue termination proofs together. *) 330 331 lemma will_return_prepend : ∀ge,d1,s1,t1. 332 ∀T1:will_return ge d1 s1 t1. 333 ∀d2,s2,t2. 334 will_return ge d2 s2 t2 → 335 will_return_end … T1 = ❬s2, t2❭ → 336 will_return ge (d1 + S d2) s1 t1. 337 #ge #d1 #s1 #tr1 #T1 elim T1 338 [ #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E 339 %1 // @(IH … T2) @E 340  #s #tr #s' #depth #EX #t #CL #T #IH #d2 #s2 #t2 #T2 #E %2 // @(IH … T2) @E 341  #s #tr #s' #depth #EX #t #CL #T #IH #s2 #s2 #t2 #T2 #E %3 // @(IH … T2) @E 342  #s #tr #s' #EX #t #CL #d2 #s2 #t2 #T2 #E normalize in E; destruct %3 // 343 ] qed. 344 345 discriminator nat. 346 347 lemma will_return_remove_call : ∀ge,d1,s1,t1. 348 ∀T1:will_return ge d1 s1 t1. 349 ∀d2. 350 will_return ge (d1 + S d2) s1 t1 → 351 ∀s2,t2. 352 will_return_end … T1 = ❬s2, t2❭ → 353 will_return ge d2 s2 t2. 354 (* The key part of the proof is to show that the two termination proofs follow 355 the same pattern. *) 356 #ge #d1x #s1x #t1x #T1 elim T1 357 [ #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH 358 [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 destruct // 359  #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct 360 >H21 in CL; * #E destruct 361  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct 362 >H35 in CL; * #E destruct 363  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct 364 >H48 in CL; * #E destruct 365 ] 366  @E 367 ] 368  #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH 369 [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct 370 >CL in H7; * #E destruct 371  #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 destruct // 372  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 @⊥ destruct 373 >H35 in CL; #E destruct 374  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 @⊥ destruct 375 >H48 in CL; #E destruct 376 ] 377  @E 378 ] 379  #s #tr #s' #d1 #EX #t #CL #T #IH #d2 #T2 #s2 #t2 #E @IH 380 [ inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct 381 >CL in H7; * #E destruct 382  #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct 383 >H21 in CL; #E destruct 384  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 385 whd in H38:(??%??); destruct // 386  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 387 whd in H49:(??%??); @⊥ destruct 388 ] 389  @E 390 ] 391  #s #tr #s' #EX #t #CL #d2 #T2 #s2 #t2 #E whd in E:(??%?); destruct 392 inversion T2 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 @⊥ destruct 393 >CL in H7; * #E destruct 394  #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 @⊥ destruct 395 >H21 in CL; #E destruct 396  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 397 whd in H38:(??%??); destruct // 398  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 399 whd in H49:(??%??); @⊥ destruct 400 ] 335 401 ] qed. 336 402 … … 642 708 termination. Note that we keep a proof that our upper bound on the length 643 709 of the termination proof is respected. *) 644 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (full:flat_trace io_out io_in ge start) (T:state → Type[0]) (limit:nat) : Type[0] ≝ { 710 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) 711 (start:state) (full:flat_trace io_out io_in ge start) 712 (original_terminates: will_return ge depth start full) 713 (T:state → Type[0]) (limit:nat) : Type[0] ≝ 714 { 645 715 new_state : state; 646 716 remainder : flat_trace io_out io_in ge new_state; 647 is_remainder : flat_trace_prefix … full remainder;648 717 cost_labelled : well_cost_labelled_state new_state; 649 718 new_trace : T new_state; 650 719 stack_ok : stack_preserved ends start new_state; 651 terminates : match depth with 652 [ O ⇒ True 653  S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM 720 terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth ]) with 721 [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭ 722  S d ⇒ ΣTM:will_return ge d new_state remainder. 723 limit > will_return_length … TM ∧ 724 will_return_end … original_terminates = will_return_end … TM 654 725 ] 655 726 }. … … 657 728 (* The same with a flag indicating whether the function returned, as opposed to 658 729 encountering a label. *) 659 record sub_trace_result (ge:genv) (depth:nat) (start:state) (full:flat_trace io_out io_in ge start) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ { 730 record sub_trace_result (ge:genv) (depth:nat) 731 (start:state) (full:flat_trace io_out io_in ge start) 732 (original_terminates: will_return ge depth start full) 733 (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ 734 { 660 735 ends : trace_ends_with_ret; 661 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) ends start full(T ends) limit736 trace_res :> trace_result ge depth ends start full original_terminates (T ends) limit 662 737 }. 663 738 … … 666 741 the size of the termination proof might need to be relaxed, too. *) 667 742 668 definition replace_trace : ∀ge,d,e 1,e2,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 →669 ∀r:trace_result ge d e 1 s1 t1 T1 l1.670 (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t)→743 definition replace_trace : ∀ge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → 744 ∀r:trace_result ge d e s1 t1 TM1 T1 l1. 745 will_return_end … TM1 = will_return_end … TM2 → 671 746 T2 (new_state … r) → 672 stack_preserved e 2s2 (new_state … r) →673 trace_result ge d e 2 s2 t2 T2 l2 ≝674 λge,d,e 1,e2,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP.675 mk_trace_result ge d e 2 s2 t2 T2 l2747 stack_preserved e s2 (new_state … r) → 748 trace_result ge d e s2 t2 TM2 T2 l2 ≝ 749 λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP. 750 mk_trace_result ge d e s2 t2 TM2 T2 l2 676 751 (new_state … r) 677 752 (remainder … r) 678 (PRE ?? (is_remainder ??????? r))679 753 (cost_labelled … r) 680 754 trace 681 755 SP 682 (match d return λd'.match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → 756 ? 757 (*(match d return λd'.match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → 683 758 match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with 684 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ??????? r)) 685 . 686 @(transitive_le … lGE) @(pi2 … TM) qed. 687 688 definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 → 689 ∀r:sub_trace_result ge d s1 t1 T1 l1. 690 (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t) → 759 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???????? r))*) 760 . 761 cases e in r ⊢ %; 762 [ <TME TME * cases d in TM1 TM2 ⊢ %; 763 [ #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); #TMS @TMS 764  #d' #TM1 #TM2 #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); * #TMa * #L1 #TME 765 %{TMa} % // @(transitive_le … lGE) @L1 766 ] 767  <TME TME * #ns #rem #WCLS #T1NS #SP whd in ⊢ (% → %); 768 * #TMa * #L1 #TME 769 %{TMa} % // @(transitive_le … lGE) @L1 770 ] qed. 771 772 definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → 773 ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1. 774 will_return_end … TM1 = will_return_end … TM2 → 691 775 T2 (ends … r) (new_state … r) → 692 776 stack_preserved (ends … r) s2 (new_state … r) → 693 sub_trace_result ge d s2 t2 T 2 l2 ≝694 λge,d,s1,s2,t1,t2,T 1,T2,l1,l2,lGE,r,PRE,trace,SP.695 mk_sub_trace_result ge d s2 t2 T 2 l2777 sub_trace_result ge d s2 t2 TM2 T2 l2 ≝ 778 λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP. 779 mk_sub_trace_result ge d s2 t2 TM2 T2 l2 696 780 (ends … r) 697 (replace_trace … lGE … r PRE trace SP).781 (replace_trace … lGE … r TME trace SP). 698 782 699 783 (* Small syntax hack to avoid ambiguous input problems. *) … … 708 792 (TIME: nat) 709 793 (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) 710 on TIME : trace_result ge depth ends_with_ret s trace 794 on TIME : trace_result ge depth ends_with_ret s trace TERMINATES 711 795 (trace_label_return (RTLabs_status ge) s) 712 796 (will_return_length … TERMINATES) ≝ … … 723 807 TERMINATES 724 808 TIME ? in 725 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) x s trace (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with 809 match ends … r return λx. trace_result ge depth x s trace TERMINATES (trace_label_label (RTLabs_status ge) x s) ? → 810 trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with 726 811 [ ends_with_ret ⇒ λr. 727 812 replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r) … … 748 833 (TIME: nat) 749 834 (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) 750 on TIME : sub_trace_result ge depth s trace 835 on TIME : sub_trace_result ge depth s trace TERMINATES 751 836 (λends. trace_label_label (RTLabs_status ge) ends s) 752 837 (will_return_length … TERMINATES) ≝ … … 770 855 (TIME: nat) 771 856 (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) 772 on TIME : sub_trace_result ge depth s trace 857 on TIME : sub_trace_result ge depth s trace TERMINATES 773 858 (λends. trace_any_label (RTLabs_status ge) ends s) 774 859 (will_return_length … TERMINATES) ≝ … … 778 863  S TIME ⇒ λTERMINATES_IN_TIME. 779 864 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 865 match trace return λs,trace. well_cost_labelled_state s → 866 ∀TM:will_return ??? trace. 867 myge ? (times 3 (will_return_length ??? trace TM)) → 868 sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with 781 869 [ ft_stop st FINAL ⇒ 782 870 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ 783 871 784 872  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 785 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with873 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 786 874 [ cl_other ⇒ λCL. 787 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with875 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 788 876 (* We're about to run into a label. *) 789 877 [ true ⇒ λCS. 790 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?878 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? 791 879 doesnt_end_with_ret 792 (mk_trace_result ge … next trace' ? ?880 (mk_trace_result ge … next trace' ? 793 881 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??) 794 882 (* An ordinary step, keep going. *) … … 801 889 802 890  cl_jump ⇒ λCL. 803 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?891 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? 804 892 doesnt_end_with_ret 805 (mk_trace_result ge ?????? next trace' ??893 (mk_trace_result ge … next trace' ? 806 894 (tal_base_not_return (RTLabs_status ge) start next ???) ??) 807 895 808 896  cl_call ⇒ λCL. 809 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in810 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with897 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in 898 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 811 899 (* We're about to run into a label, use base case for call *) 812 900 [ true ⇒ λCS. 813 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?901 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? 814 902 doesnt_end_with_ret 815 ( replace_trace … r ?903 (mk_trace_result ge … 816 904 (tal_base_call (RTLabs_status ge) start next (new_state … r) 817 ? CL ? (new_trace … r) CS) ? )905 ? CL ? (new_trace … r) CS) ??) 818 906 (* otherwise use step case *) 819 907  false ⇒ λCS. … … 828 916 829 917  cl_return ⇒ λCL. 830 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ?918 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ? 831 919 ends_with_ret 832 (mk_trace_result ge ??????920 (mk_trace_result ge … 833 921 next 834 922 trace' 835 ?836 923 ? 837 924 (tal_base_return (RTLabs_status ge) start next ? CL) … … 848 935  // 849 936  // 850  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 @le_S_to_le851  #s0 #t @concatenate_flat_trace_prefix @(is_remainder … r)937  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #GT #_ @(le_S_to_le … GT) 938  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ // 852 939  @(stack_preserved_join … (stack_ok … r)) // 853 940  @(trace_label_label_label … (new_trace … r)) 854  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 #LT941  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_ 855 942 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 856 943 @(transitive_le … (3*(will_return_length … TERMINATES))) … … 877 964  %{tr} @EV 878 965  @(well_cost_labelled_state_step … EV) // 879  %2 %1880 966  whd @(will_return_notfn … TERMINATES) %2 @CL 881 967  @stack_preserved_step /2/ … … 884 970  @(well_cost_labelled_jump … EV) // 885 971  @(well_cost_labelled_state_step … EV) // 886  %2 %1 972  whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} % 973 [ @(transitive_lt … LTr) cases (will_return_call … CL TERMINATES) 974 #TMx * #LT' #_ @LT' 975  <EQr cases (will_return_call … CL TERMINATES) 976 #TM' * #_ #EQ' @EQ' 977 ] 887 978  @(stack_preserved_call … EV (stack_ok … r)) // 888 979  %{tr} @EV 889 980  @RTLabs_after_call // 890  #s0 #t #p %2 @p 891  cases (will_return_call … TERMINATES) #H @le_S_to_le 892  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 893 cases (will_return_call … CL TERMINATES) 894 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 895  #s0 #t #p1 %2 @(concatenate_flat_trace_prefix … p1) @(is_remainder … r) 981  @(cost_labelled … r) 982  skip 983  cases r #ns #rm #WS #TLR #SP * #TM * #LT #_ @le_S_to_le 984 @(transitive_lt … LT) 985 cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT' 986  cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ 987 cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' // 896 988  @RTLabs_after_call // 897 989  %{tr} @EV 898 990  @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) // 899 991  @(cost_labelled … r) 900  cases r #H72 #H73 #H74 #H75 #HX #HY * #H76#H78992  cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78 901 993 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 902 cases (will_return_call … TERMINATES) in H78;903 #X #Y#Z994 cases (will_return_call … TERMINATES) in GT; 995 #X * #Y #_ #Z 904 996 @(transitive_le … (monotonic_lt_times_r 3 … Y)) 905 997 [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) // … … 908 1000  @(well_cost_labelled_state_step … EV) // 909 1001  @(well_cost_labelled_call … EV) // 910  skip911 1002  cases (will_return_call … TERMINATES) 912 #TM #GT@le_S_S_to_le1003 #TM * #GT #_ @le_S_S_to_le 913 1004 >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times 914 1005 @(transitive_le … TERMINATES_IN_TIME) … … 919 1010  %2 whd @CL 920 1011  @(well_cost_labelled_state_step … EV) // 921  %2 %1 922  cases (will_return_notfn … TERMINATES) #TM @le_S_to_le 923  #s0 #t #p %2 @p 1012  cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT) 1013  cases (will_return_notfn … TERMINATES) #TM * #_ #EQ // 924 1014  @CL 925 1015  %{tr} @EV … … 927 1017  @(well_cost_labelled_state_step … EV) // 928 1018  %1 @CL 929  cases (will_return_notfn … TERMINATES) #TM #GT1019  cases (will_return_notfn … TERMINATES) #TM * #GT #_ 930 1020 @le_S_S_to_le 931 1021 @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME) … … 947 1037 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 948 1038 (TERMINATES: will_return ge depth s trace) 949 : trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝1039 : trace_result ge depth ends_with_ret s trace TERMINATES (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 950 1040 make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES 951 1041 (2 + 3 * will_return_length … TERMINATES) ?. … … 1087 1177 qed. 1088 1178 *) 1089 discriminator nat. 1179 1090 1180 (* 1091 1181 definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. … … 1319 1409  /2/ 1320 1410  // 1321  (* FIXME: postcall nontermination *) 1411  @(not_to_not … NO_TERMINATION) * #depth * #TM1 %{depth} % 1412 @wr_call // 1413 @(will_return_prepend … TERMINATES … TM1) 1414 cases (terminates … tlr) // 1322 1415  (* FIXME: postcall notwrong *) 1323 1416  (* FIXME: bound on steps after call *)
Note: See TracChangeset
for help on using the changeset viewer.