 Timestamp:
 Feb 1, 2012, 4:16:04 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1656 r1670 54 54 normalize try #a try #b try #c try #d try #e try #g try #h destruct 55 55 ] qed. 56 57 lemma RTLabs_not_cost : ∀ge,s. 58 RTLabs_cost s = false → 59 ¬ as_costed (RTLabs_status ge) s. 60 #ge #s #E % whd in ⊢ (% → ?); >E #E' destruct 61 qed. 56 62 57 63 (* Before attempting to construct a structured trace, let's show that we can … … 580 586 doesnt_end_with_ret 581 587 (mk_trace_result ge ??? next trace' ? 582 (tal_base_not_return (RTLabs_status ge) start next ?? ?) ?)588 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ?) 583 589 (* An ordinary step, keep going. *) 584 590  false ⇒ λCS. … … 586 592 replace_sub_trace … r 587 593 (tal_step_default (RTLabs_status ge) (ends … r) 588 start next (new_state … r) ? (new_trace … r) ? ?)594 start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) 589 595 ] (refl ??) 590 596 … … 613 619 (tal_step_call (RTLabs_status ge) (ends … r') 614 620 start next (new_state … r) (new_state … r') ? CL ? 615 (new_trace … r) ?(new_trace … r'))621 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) 616 622 ] (refl ??) 617 623 … … 664 670 cases (will_return_call … CL TERMINATES) 665 671 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 666  whd in ⊢ (?%); >CS % #E destruct667 672  (* TODO oh dear *) 668 673  %{tr} @EV … … 687 692  %{tr} @EV 688 693  %2 whd @CL 689  @CS690 694  @(well_cost_labelled_state_step … EV) // 691 695  cases (will_return_notfn … TERMINATES) #TM @le_S_to_le 692  % whd in ⊢ (% → ?); >CS #E destruct693 696  @CL 694 697  %{tr} @EV … … 770 773 use the fact that the trace is soundly labelled to achieve this. *) 771 774 772 inductive finite_prefix (ge:genv) : state → Type[0]≝775 inductive finite_prefix (ge:genv) : state → Prop ≝ 773 776  fp_tal : ∀s,s'. 774 777 trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → … … 790 793 match fp return λs'.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s' = false → finite_prefix ge s with 791 794 [ fp_tal s' sf TAL rem ⇒ λEVAL, NOT_COST. fp_tal ge s sf 792 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER ?)795 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST)) 793 796 rem 794 797  fp_tac s' sf TAC rem ⇒ λEVAL, NOT_COST. fp_tac ge s sf 795 (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER ?) rem798 (tac_step_default (RTLabs_status ge) s sf s' EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) rem 796 799 ]. 797 % whd in ⊢ (% → ?); >NOT_COST #E destruct 798 qed. 799 (* I'll come back to this. 800 800 801 definition fp_add_terminating_call : ∀ge,s,s1,s'. 801 802 (∃t. eval_statement ge s = Value ??? 〈t,s1〉) → … … 804 805 trace_label_return (RTLabs_status ge) s1 s' → 805 806 as_after_return (RTLabs_status ge) (mk_Sig ?? s CALL) s' → 807 RTLabs_cost s' = false → 806 808 finite_prefix ge s ≝ 807 809 λge,s,s1,s',EVAL,CALL,fp. 808 match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → finite_prefix ge s with809 [ fp_tal s' sf TAL rem ⇒ λTLR,RET . fp_tal ge s sf810 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR TAL)810 match fp return λs'.λ_. trace_label_return (RTLabs_status ge) ? s' → as_after_return (RTLabs_status ge) ? s' → RTLabs_cost s' = false → finite_prefix ge s with 811 [ fp_tal s' sf TAL rem ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf 812 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL) 811 813 rem 812  fp_tac s' sf TAC rem ⇒ λTLR,RET . fp_tac ge s sf813 (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR TAC)814  fp_tac s' sf TAC rem ⇒ λTLR,RET,NOT_COST. fp_tac ge s sf 815 (tac_step_call (RTLabs_status ge) s s' sf s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC) 814 816 rem 815 817 ]. 816 *) 818 819 definition termination_oracle ≝ ∀ge,depth,s,trace. 820 inhabited (will_return ge depth s trace) ⊎ ¬ inhabited (will_return ge depth s trace). 821 822 let rec finite_segment ge s n trace 823 (ORACLE: termination_oracle) 824 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 825 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 826 (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) 827 (LABEL_LIMIT: ∃s'. And (nth_state ge s trace (S n) = Some ? s') (RTLabs_cost s' = true)) 828 : finite_prefix ge s ≝ 829 match n return λn. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S n) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with 830 [ O ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ? 831  S n' ⇒ 832 match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → (∃s'. nth_state ge s trace (S (S n')) = Some ? s' ∧ RTLabs_cost s' = true) → finite_prefix ge s with 833 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ 834  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. 835 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 836 [ cl_other ⇒ λCL. 837 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 838 [ true ⇒ λCS. 839 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' 840  false ⇒ λCS. 841 let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ?? LABEL_LIMIT in 842 fp_add_default ge ?? CL fs ? CS 843 ] (refl ??) 844  cl_jump ⇒ λCL. 845 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' 846  cl_call ⇒ λCL. 847 match ORACLE ge O next trace' with 848 [ inl TERMINATES ⇒ 849 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ??? in 850 ? 851  inr NO_TERMINATION ⇒ ? 852 ] 853  cl_return ⇒ λCL. ⊥ 854 ] (refl ??) 855  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ 856 ] 857 ] STATE_COSTLABELLED NO_TERMINATION LABEL_LIMIT. 858 [ 2,17: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct 859  3: @(absurd ?? NO_TERMINATION) 860 %{0} % @wr_base // 861  4: @(well_cost_labelled_jump … EV) // 862  5,6: /2/ 863  8: @(well_cost_labelled_state_step … EV) // 864  9: @(well_cost_labelled_call … EV) // 865  10: cases TERMINATES // 866  12,13,14: /2/ 867  15: @(well_cost_labelled_state_step … EV) // 868  16: @(not_to_not … NO_TERMINATION) 869 * #depth * #TERM %{depth} % @wr_step /2/ 870 ] cases daemon qed. 871 817 872 (* 818 873 let corec make_label_diverges ge s
Note: See TracChangeset
for help on using the changeset viewer.