Changeset 1712
 Timestamp:
 Feb 21, 2012, 11:58:07 AM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1707 r1712 88 88 [ #H105 #H106 #H107 #H108 #H109 destruct 89 89  #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct // 90 ] qed. 91 92 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 ≝ 93  ftp_refl : ∀s,t. flat_trace_prefix o i ge s s t t 94  ftp_step : ∀s1,tr,s2,s3,t2,t3,EV. 95 flat_trace_prefix o i ge s2 s3 t2 t3 → 96 flat_trace_prefix o i ge s1 s3 (ft_step o i ge s1 tr s2 EV t2) t3 97 . 98 99 lemma concatenate_flat_trace_prefix : ∀o,i,ge,s1,s2,s3,t1,t2,t3. 100 flat_trace_prefix o i ge s1 s2 t1 t2 → 101 flat_trace_prefix o i ge s2 s3 t2 t3 → 102 flat_trace_prefix o i ge s1 s3 t1 t3. 103 #o #i #ge #s1 #s2 #s3 #t1 #t2 #t3 #p1 elim p1 104 [ // 105  #s1' #tr #s2' #s3' #t2' #t3' #EV #p2 #IH #p3 106 %2 /2/ 90 107 ] qed. 91 108 … … 596 613 termination. Note that we keep a proof that our upper bound on the length 597 614 of the termination proof is respected. *) 598 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) ( T:state → Type[0]) (limit:nat) : Type[0] ≝ {615 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] ≝ { 599 616 new_state : state; 600 617 remainder : flat_trace io_out io_in ge new_state; 618 is_remainder : flat_trace_prefix … full remainder; 601 619 cost_labelled : well_cost_labelled_state new_state; 602 620 new_trace : T new_state; … … 610 628 (* The same with a flag indicating whether the function returned, as opposed to 611 629 encountering a label. *) 612 record sub_trace_result (ge:genv) (depth:nat) (start:state) ( T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {630 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] ≝ { 613 631 ends : trace_ends_with_ret; 614 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) ends start (T ends) limit632 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) ends start full (T ends) limit 615 633 }. 616 634 … … 619 637 the size of the termination proof might need to be relaxed, too. *) 620 638 621 definition replace_trace : ∀ge,d,e1,e2,s1,s2,T1,T2,l1,l2. l2 ≥ l1 → 622 ∀r:trace_result ge d e1 s1 T1 l1. T2 (new_state … r) → stack_preserved e2 s2 (new_state … r) → trace_result ge d e2 s2 T2 l2 ≝ 623 λge,d,e1,e2,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP. 624 mk_trace_result ge d e2 s2 T2 l2 639 definition replace_trace : ∀ge,d,e1,e2,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 → 640 ∀r:trace_result ge d e1 s1 t1 T1 l1. 641 (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t) → 642 T2 (new_state … r) → 643 stack_preserved e2 s2 (new_state … r) → 644 trace_result ge d e2 s2 t2 T2 l2 ≝ 645 λge,d,e1,e2,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP. 646 mk_trace_result ge d e2 s2 t2 T2 l2 625 647 (new_state … r) 626 648 (remainder … r) 649 (PRE ?? (is_remainder ??????? r)) 627 650 (cost_labelled … r) 628 651 trace … … 630 653 (match d return λd'.match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → 631 654 match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with 632 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ?????? r)) 633 . @(transitive_le … lGE) @(pi2 … TM) qed. 634 635 definition replace_sub_trace : ∀ge,d,s1,s2,T1,T2,l1,l2. l2 ≥ l1 → 636 ∀r:sub_trace_result ge d s1 T1 l1. T2 (ends … r) (new_state … r) → stack_preserved (ends … r) s2 (new_state … r) → sub_trace_result ge d s2 T2 l2 ≝ 637 λge,d,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP. 638 mk_sub_trace_result ge d s2 T2 l2 655 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ??????? r)) 656 . 657 @(transitive_le … lGE) @(pi2 … TM) qed. 658 659 definition replace_sub_trace : ∀ge,d,s1,s2,t1,t2,T1,T2,l1,l2. l2 ≥ l1 → 660 ∀r:sub_trace_result ge d s1 t1 T1 l1. 661 (∀s,t. flat_trace_prefix … s1 s t1 t → flat_trace_prefix … s2 s t2 t) → 662 T2 (ends … r) (new_state … r) → 663 stack_preserved (ends … r) s2 (new_state … r) → 664 sub_trace_result ge d s2 t2 T2 l2 ≝ 665 λge,d,s1,s2,t1,t2,T1,T2,l1,l2,lGE,r,PRE,trace,SP. 666 mk_sub_trace_result ge d s2 t2 T2 l2 639 667 (ends … r) 640 (replace_trace … lGE … r trace SP).668 (replace_trace … lGE … r PRE trace SP). 641 669 642 670 (* Small syntax hack to avoid ambiguous input problems. *) … … 651 679 (TIME: nat) 652 680 (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) 653 on TIME : trace_result ge depth ends_with_ret s 681 on TIME : trace_result ge depth ends_with_ret s trace 654 682 (trace_label_return (RTLabs_status ge) s) 655 683 (will_return_length … TERMINATES) ≝ … … 666 694 TERMINATES 667 695 TIME ? in 668 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) x s (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s(trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with696 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 669 697 [ ends_with_ret ⇒ λr. 670 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r)698 replace_trace … r ? (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r) 671 699  doesnt_end_with_ret ⇒ λr. 672 700 let r' ≝ make_label_return ge depth (new_state … r) … … 675 703 (cost_labelled … r) ? 676 704 (pi1 … (terminates … r)) TIME ? in 677 replace_trace … r' 705 replace_trace … r' ? 678 706 (tlr_step (RTLabs_status ge) s (new_state … r) 679 707 (new_state … r') (new_trace … r) (new_trace … r')) ? … … 691 719 (TIME: nat) 692 720 (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) 693 on TIME : sub_trace_result ge depth s 721 on TIME : sub_trace_result ge depth s trace 694 722 (λends. trace_label_label (RTLabs_status ge) ends s) 695 723 (will_return_length … TERMINATES) ≝ … … 700 728 701 729 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in 702 replace_sub_trace … r 730 replace_sub_trace … r ? 703 731 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r) 704 732 … … 713 741 (TIME: nat) 714 742 (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) 715 on TIME : sub_trace_result ge depth s 743 on TIME : sub_trace_result ge depth s trace 716 744 (λends. trace_any_label (RTLabs_status ge) ends s) 717 745 (will_return_length … TERMINATES) ≝ … … 721 749  S TIME ⇒ λTERMINATES_IN_TIME. 722 750 723 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 (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with751 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 724 752 [ ft_stop st FINAL ⇒ 725 753 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ? 726 754 727 755  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 728 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) with756 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 729 757 [ cl_other ⇒ λCL. 730 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) with758 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 731 759 (* We're about to run into a label. *) 732 760 [ true ⇒ λCS. 733 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?761 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ? 734 762 doesnt_end_with_ret 735 (mk_trace_result ge … next trace' ? 763 (mk_trace_result ge … next trace' ?? 736 764 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??) 737 765 (* An ordinary step, keep going. *) 738 766  false ⇒ λCS. 739 767 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in 740 replace_sub_trace … r 768 replace_sub_trace … r ? 741 769 (tal_step_default (RTLabs_status ge) (ends … r) 742 770 start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ? … … 744 772 745 773  cl_jump ⇒ λCL. 746 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?774 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ? 747 775 doesnt_end_with_ret 748 (mk_trace_result ge ????? next trace'?776 (mk_trace_result ge ?????? next trace' ?? 749 777 (tal_base_not_return (RTLabs_status ge) start next ???) ??) 750 778 751 779  cl_call ⇒ λCL. 752 780 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in 753 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) with781 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 754 782 (* We're about to run into a label, use base case for call *) 755 783 [ true ⇒ λCS. 756 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?784 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ? 757 785 doesnt_end_with_ret 758 (replace_trace … r 786 (replace_trace … r ? 759 787 (tal_base_call (RTLabs_status ge) start next (new_state … r) 760 788 ? CL ? (new_trace … r) CS) ?) … … 764 792 (new_state … r) (remainder … r) ENV_COSTLABELLED ? 765 793 (pi1 … (terminates … r)) TIME ? in 766 replace_sub_trace … r' 794 replace_sub_trace … r' ? 767 795 (tal_step_call (RTLabs_status ge) (ends … r') 768 796 start next (new_state … r) (new_state … r') ? CL ? … … 771 799 772 800  cl_return ⇒ λCL. 773 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ?801 mk_sub_trace_result ge depth start ? (λends. trace_any_label (RTLabs_status ge) ends start) ? 774 802 ends_with_ret 775 (mk_trace_result ge ????? 803 (mk_trace_result ge ?????? 776 804 next 777 805 trace' 806 ? 778 807 ? 779 808 (tal_base_return (RTLabs_status ge) start next ? CL) … … 789 818 [ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] 790 819  // 791  cases r #H1 #H2 #H3 #H4 #H5 * #H6 @le_S_to_le 820  // 821  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 @le_S_to_le 822  #s0 #t @concatenate_flat_trace_prefix @(is_remainder … r) 792 823  @(stack_preserved_join … (stack_ok … r)) // 793 824  @(trace_label_label_label … (new_trace … r)) 794  cases r #H1 #H2 #H3 #H4 #H5 * #H6#LT825  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 #LT 795 826 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 796 827 @(transitive_le … (3*(will_return_length … TERMINATES))) … … 802 833  cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] 803 834  @le_n 835  // 804 836  @le_S_S_to_le @TERMINATES_IN_TIME 805 837  @(wrl_nonzero … TERMINATES_IN_TIME) … … 810 842  %{tr} @EV 811 843  @(well_cost_labelled_state_step … EV) // 844  %2 %1 812 845  whd @(will_return_notfn … TERMINATES) %2 @CL 813 846  @stack_preserved_step /2/ … … 816 849  @(well_cost_labelled_jump … EV) // 817 850  @(well_cost_labelled_state_step … EV) // 851  %2 %1 818 852  @(stack_preserved_call … EV (stack_ok … r)) // 819 853  %{tr} @EV 820 854  @RTLabs_after_call // 855  #s0 #t #p %2 @p 821 856  cases (will_return_call … TERMINATES) #H @le_S_to_le 822  cases r #H1 #H2 #H3 #H4 #H5 * #H6857  cases r #H1 #H2 #H3 #H4 #H5 #H6 * #H7 823 858 cases (will_return_call … CL TERMINATES) 824 859 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 860  #s0 #t #p1 %2 @(concatenate_flat_trace_prefix … p1) @(is_remainder … r) 825 861  @RTLabs_after_call // 826 862  %{tr} @EV 827 863  @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) // 828 864  @(cost_labelled … r) 829  cases r #H72 #H73 #H74 #H75 #HX * #H76 #H78865  cases r #H72 #H73 #H74 #H75 #HX #HY * #H76 #H78 830 866 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 831 867 cases (will_return_call … TERMINATES) in H78; … … 848 884  %2 whd @CL 849 885  @(well_cost_labelled_state_step … EV) // 886  %2 %1 850 887  cases (will_return_notfn … TERMINATES) #TM @le_S_to_le 888  #s0 #t #p %2 @p 851 889  @CL 852 890  %{tr} @EV … … 874 912 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 875 913 (TERMINATES: will_return ge depth s trace) 876 : trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝914 : trace_result ge depth ends_with_ret s trace (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 877 915 make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES 878 916 (2 + 3 * will_return_length … TERMINATES) ?.
Note: See TracChangeset
for help on using the changeset viewer.