Changeset 1707 for src/RTLabs

Ignore:
Timestamp:
Feb 16, 2012, 6:05:57 PM (9 years ago)
Message:

Progress on finite segments of infinite RTLabs structured trace.

File:
1 edited

Unmodified
Removed
• src/RTLabs/Traces.ma

 r1706 | ft_step : ∀s,tr,s'. eval_statement ge s = Value ??? 〈tr,s'〉 → flat_trace o i ge s' → flat_trace o i ge s | ft_wrong : ∀s,m. eval_statement ge s = Wrong ??? m → flat_trace o i ge s. coinductive not_wrong (o:Type[0]) (i:o → Type[0]) (ge:genv) : ∀s. flat_trace o i ge s → Type[0] ≝ | nw_stop : ∀s,H. not_wrong o i ge s (ft_stop o i ge s H) | nw_step : ∀s,tr,s',H,tr'. not_wrong o i ge s' tr' → not_wrong o i ge s (ft_step o i ge s tr s' H tr'). lemma still_not_wrong : ∀o,i,ge,s,tr,s',H,tr'. not_wrong o i ge s (ft_step o i ge s tr s' H tr') → not_wrong o i ge s' tr'. #o #i #ge #s #tr #s' #H #tr' #NW inversion NW [ #H105 #H106 #H107 #H108 #H109 destruct | #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 destruct // ] qed. let corec make_flat_trace ge s λs. S (match s with [ St_call_id _ _ _ _ ⇒ 1 | St_call_ptr _ _ _ _ ⇒ 1 | St_return ⇒ 1 | _ ⇒ 0 ]). inductive steps_to_label_bound (g:graph statement) : label → nat → Prop ≝ | stlb_step : ∀l,n,H. inductive bound_on_steps_to_cost (g:graph statement) : label → nat → Prop ≝ | bostc_here : ∀l,n,H. is_cost_label (lookup_present … g l H) → bound_on_steps_to_cost g l n | bostc_later : ∀l,n. bound_on_steps_to_cost1 g l n → bound_on_steps_to_cost g l n with bound_on_steps_to_cost1 : label → nat → Prop ≝ | bostc_step : ∀l,n,H. let stmt ≝ lookup_present … g l H in (∀l'. Exists label (λl0. l0 = l') (successors stmt) → (∃H'. bool_to_Prop (is_cost_label (lookup_present … g l' H'))) ∨ steps_to_label_bound g l' n) → steps_to_label_bound g l (steps_for_statement stmt + n). bound_on_steps_to_cost g l' n) → bound_on_steps_to_cost1 g l (steps_for_statement stmt + n). (* lemma steps_to_label_bound_inv : ∀g,l,n. steps_to_label_bound g l n → % [2: % [ @refl | #l' #EX cases (IH l' EX) /2/ ] | skip ] qed. *) discriminator nat. (* definition soundly_labelled_pc ≝ λg,l. ∃n. steps_to_label_bound g l n. | Returnstate _ _ stk _ ⇒ match stk with [ nil ⇒ False | cons f _ ⇒ soundly_labelled_frame f ] ]. definition frame_steps_to_label_bound : frame → nat → Prop ≝ λf. steps_to_label_bound (f_graph (func f)) (next f). inductive state_steps_to_label_bound : state → nat → Prop ≝ | sstlb_state : ∀f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (State f fs m) n | sstlb_call : ∀fd,args,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Callstate fd args dst (f::fs) m) (S n) | sstlb_ret : ∀rtv,dst,f,fs,m,n. frame_steps_to_label_bound f n → state_steps_to_label_bound (Returnstate rtv dst (f::fs) m) (S n) *) definition frame_bound_on_steps_to_cost : frame → nat → Prop ≝ λf. bound_on_steps_to_cost (f_graph (func f)) (next f). definition frame_bound_on_steps_to_cost1 : frame → nat → Prop ≝ λf. bound_on_steps_to_cost1 (f_graph (func f)) (next f). inductive state_bound_on_steps_to_cost : state → nat → Prop ≝ | sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n | sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n) | sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n) . lemma state_steps_to_label_bound_zero : ∀s. ¬ state_steps_to_label_bound s O. lemma state_bound_on_steps_to_cost_zero : ∀s. ¬ state_bound_on_steps_to_cost s O. #s % #H inversion H [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct inversion H52 #H68 #H69 #H70 #H71 #H72 #H73 #H74 normalize in H73; destruct [ #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 destruct whd in H50; @(bound_on_steps_to_cost1_inv_ind … H50) (* XXX inversion H50*) #H55 #H56 #H57 #H58 #H59 #H60 #H61 normalize in H60; destruct | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 destruct | #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 destruct ] qed. lemma state_steps_to_label_bound_step : ∀ge,s,tr,s',n. state_steps_to_label_bound s (S n) → lemma bound_after_step : ∀ge,s,tr,s',n. state_bound_on_steps_to_cost s (S n) → eval_statement ge s = Value ??? 〈tr, s'〉 → RTLabs_cost s' = false → (RTLabs_classify s' = cl_return ∨ RTLabs_classify s = cl_call) ∨ state_steps_to_label_bound s' n. #ge #s #tr #s' #n #STEPS inversion STEPS state_bound_on_steps_to_cost s' n. #ge #s #tr #s' #n #BOUND1 inversion BOUND1 [ #f #fs #m #m #FS #E1 #E2 #_ destruct #EVAL cases (eval_successor … EVAL) [ /3/ | * #l * #S1 #S2 #NC %2 cases (steps_to_label_bound_inv … FS ?) [2: @(next_ok f) ] #n' (* cases (bound_on_steps_to_cost1_inv … FS ?) [2: @(next_ok f) ] *) @(bound_on_steps_to_cost1_inv_ind … FS) #next #n' #next_ok #IH #E1 #E2 #E3 destruct inversion (eval_perserves … EVAL) [ #ge0 #f0 #f' #fs' #m0 #m' #F #E1 #E2 #E3 #_ destruct >(eval_steps … EVAL) * #En normalize in En; #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct whd in S1:(??%?); destruct %1 cases (H l S2) [ * #LP change with (RTLabs_cost (State (mk_frame H1 H7 l H9 H5 H6) fs' m')) in ⊢ (?% → ?); >NC * | // [ #ge0 #f0 #f' #fs' #m0 #m' #F #E4 #E5 #E6 #_ destruct >(eval_steps … EVAL) in E2; #En normalize in En; inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct %1 inversion (IH … S2) [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%); whd in S1:(??%?); destruct >NC in CSx; * | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73 ] | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct >(eval_steps … EVAL) * #En normalize in En; #H inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct %2 whd lapply (H l S2) @FS // | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct >(eval_steps … EVAL) in E2; #En normalize in En; inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct %2 @IH normalize in S1; destruct @S2 | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct | #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct normalize in S1; destruct | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 destruct | #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 destruct ] ] 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 ] inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct @FS inversion FS [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%); >NC in CSx; * | #lx #nx #H #E1x #E2x #_ destruct @H ] ] ] qed. (* lemma state_steps_to_label_step : ∀ge,f,fs,m,n,tr,s'. state_steps_to_label_bound (State f fs m) (S (S n)) → ¬ (bool_to_Prop (RTLabs_cost (State f fs m))) → eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → state_steps_to_label_bound s' (match s' with [ State _ _ _ ⇒ n | _ ⇒ S n ]). #ge #f0 #fs0 #m0 #n0 #tr #s' #H inversion H [ * #func #locals #next #next_ok #sp #dst #fs #m #n #H1 #E1 #E2 #_ destruct cases n in H1 E2; [ #H1 #E2 normalize in E2; destruct | #n' #H1 #E2 normalize in E2; destruct ] #NC whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); lapply (steps_to_label_bound_inv_step … H1 next_ok NC) cases (lookup_present ??? next next_ok) [ #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl | #cl #l #H2 #LP whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl | #r #cs #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #E3 @bind_ok #locals' #E4 whd in ⊢ (??%? → ?); #E destruct normalize %1 whd @H2 %1 @refl | #t1 #t2 #op #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl | #op #r1 #r2 #r3 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl | #ch #r1 #r2 #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct  normalize %1 whd @H2 %1 @refl | #id #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl | #r #rs #or #l #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl | #id #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #b #Eb @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct normalize %2 whd @H2 %1 @refl | #r #rs #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #fd #Efd  @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ??) [ #r * #b * #c * #Ev' #Efn %3 [ @b | @Efn ] | ||| cases (find_funct ????) in Efd ⊢ %; [2:#x] normalize #E' destruct @refl ] | #r #l1 #l2 #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % | #r #ls #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev cases v [ #E whd in E:(??%?); destruct | #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?|_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct | #l' #e #E whd in E:(??%?); destruct % % ] | *: #vl #E whd in E:(??%?); destruct ] | #H2 #LP whd in ⊢ (??%? → ?); @bind_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %5 ] *) (* When constructing an infinite trace, we need to be able to grab the finite portion of the trace for the next [trace_label_diverges] constructor.  We (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *) (NO_TERMINATION: Not (∃depth. inhabited (will_return ge depth s trace))) (LABEL_LIMIT: state_steps_to_label_bound s n) (NOT_UNDEFINED: not_wrong … trace) (LABEL_LIMIT: state_bound_on_steps_to_cost s n) on n : finite_prefix ge s ≝ match n return λn. state_steps_to_label_bound s n → finite_prefix ge s with match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with [ O ⇒ λLABEL_LIMIT. ⊥ | S n' ⇒ match trace return λs,trace. well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_steps_to_label_bound s (S n') → finite_prefix ge s with [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ | ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. match trace return λs,trace. not_wrong ??? s trace → well_cost_labelled_state s → (Not (∃depth. inhabited (will_return ge depth s trace))) → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ ft_stop st FINAL ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ | ft_step start tr next EV trace' ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. match RTLabs_classify start return λx. RTLabs_classify start = x → ? with [ cl_other ⇒ λCL. fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? CS) trace' | false ⇒ λCS. let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ??? in let fs ≝ finite_segment ge next n' trace' ORACLE ENV_COSTLABELLED ???? in fp_add_default ge ?? CL fs ? CS ] (refl ??) | cl_jump ⇒ λCL. fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? ?) trace' | cl_call ⇒ λCL.?(* | cl_call ⇒ λCL. match ORACLE ge O next trace' return λ_. finite_prefix ge start with [ or_introl TERMINATES ⇒ match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) CS) (remainder … tlr) | false ⇒ λCS. ? (* broken - we don't know the new value of n *) (*let fs ≝ finite_segment ge (new_status … tlr) ?????????????? fp_add_terminating_call … (new_trace … tlr) ? CS*) | false ⇒ λCS. let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE ENV_COSTLABELLED ???? in fp_add_terminating_call … fs (new_trace … tlr) ? CS ] (refl ??) ] | or_intror NO_TERMINATION ⇒ fp_tac ??? (tac_base (RTLabs_status ge) start CL) (ft_step io_out io_in ge start tr next EV trace') ]*) ] | cl_return ⇒ λCL. ⊥ ] (refl ??) | ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ ] STATE_COSTLABELLED NO_TERMINATION | ft_wrong start m EV ⇒ λNOT_UNDEFINED,STATE_COSTLABELLED,NO_TERMINATION,LABEL_LIMIT. ⊥ ] NOT_UNDEFINED STATE_COSTLABELLED NO_TERMINATION ] LABEL_LIMIT. [ cases (state_steps_to_label_bound_zero s) /2/ [ cases (state_bound_on_steps_to_cost_zero s) /2/ | (* TODO: how do we know that we're not at the final state? *) | @(absurd ?? NO_TERMINATION) %{0} % @wr_base // | @(well_cost_labelled_jump … EV) // | 5,6,8,9,10: /2/ | | 5,6,7,8,9,10: /2/ | /2/ | // | (* FIXME: post-call non-termination *) | (* FIXME: post-call not-wrong *) | (* FIXME: bound on steps after call *) | @(well_cost_labelled_state_step … EV) // | @(well_cost_labelled_call … EV) // | 18,19,20: /2/ | @(well_cost_labelled_state_step … EV) // | @(not_to_not … NO_TERMINATION) * #depth * #TERM %{depth} % @wr_step /2/ | cases (state_steps_to_label_bound_step … LABEL_LIMIT EV ?) @(well_cost_labelled_call … EV) // | 2,14: cases LABEL_LIMIT #s' * #NTH #_ whd in NTH:(??%?); destruct | 5,6,8: /2/ | |*) | 12,13,14: /2/ | @(well_cost_labelled_state_step … EV) // | @(not_to_not … NO_TERMINATION) * #depth * #TERM %{depth} % @wr_step /2/ | @(still_not_wrong … NOT_UNDEFINED) | cases (bound_after_step … LABEL_LIMIT EV ?) [ * [ #TERMINATES @⊥ @(absurd ?? NO_TERMINATION) %{0} % @wr_step [ %1 // | inversion trace' [ cases daemon (* TODO again *) | #s1 #tr1 #s2 #EVAL' #trace'' #E1 #E2 destruct @wr_base // | #H99 #H100 #H101 #H102 #H103 destruct inversion NOT_UNDEFINED [ #H137 #H138 #H139 #H140 #H141 destruct | #H143 #H144 #H145 #H146 #H147 #H148 #H149 #H150 #H151 destruct inversion H148 [ #H153 #H154 #H155 #H156 #H157 destruct | #H159 #H160 #H161 #H162 #H163 #H164 #H165 #H166 #H167 destruct ] ] ] ] | >CL #E destruct ] | // | // ] | inversion NOT_UNDEFINED [ #H169 #H170 #H171 #H172 #H173 destruct | #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct ] ] cases daemon qed.
Note: See TracChangeset for help on using the changeset viewer.