Changeset 1736 for src/RTLabs/Traces.ma

Ignore:
Timestamp:
Feb 24, 2012, 1:19:10 PM (8 years ago)
Message:

Show that the bound on the number of instructions until a cost label is
preserved by function calls in RTLabs structured traces.

File:
1 edited

Unmodified
Added
Removed
• src/RTLabs/Traces.ma

 r1719 [ Callstate fd args dst stk m ⇒ λ_. match s' with [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ] | Finalstate r ⇒ True [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ] | Finalstate r ⇒ stk = [ ] | _ ⇒ False ] | sp_finished : ∀s1,f,f',fs,m. next f = next f' → frame_rel f f' → stack_of_state (f::fs) s1 → stack_preserved ends_with_ret s1 (State f' fs m) | sp_stop : ∀e,s1,r. stack_preserved e s1 (Finalstate r) | sp_stop : ∀s1,r. stack_of_state [ ] s1 → stack_preserved ends_with_ret s1 (Finalstate r) | sp_top : ∀fd,args,dst,m,r. stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r) . lemma stack_preserved_final : ∀e,r,s. stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'. #e #r #s #H inversion H ¬stack_preserved e (Finalstate r) s. #e #r #s % #H inversion H [ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct inversion SOS #a #b #c #d #e #f try #g try #h destruct | #H194 #H195 #H196 #H197 #H198 #H199 #SOS #H201 #H202 #H203 #H204 destruct | #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct inversion SOS #a #b #c #d #e #f try #g try #h destruct | #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl | #s' #r' #SOS #E1 #E2 #E3 #E4 destruct inversion SOS #a #b #c #d #e #f try #g try #h destruct | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct ] qed. [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct @(sp_normal fs) // <(stack_of_state_eq … S1' S2) // | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct @(sp_finished … N) >(stack_of_state_eq … S1' S2) // | #s1'' #r #E1 #E2 #E3 #E4 destruct // | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) // | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct inversion S2 [ #H34 #H35 #H36 #H37 #H38 #H39 destruct | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct ] ] | #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct | #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H cases (stack_preserved_final … H) #r #E destruct // cases (stack_preserved_final … H) #r #E destruct | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥ @(absurd … F) // ] qed. | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct | #res #dst * [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct // | *: normalize #a try #b destruct ] ] [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ] | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV whd in EV:(??%?); destruct @(sp_finished ? f) // cases f // ] | #r #s2 #tr #E normalize in E; destruct inversion SP [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct | #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct inversion (eval_perserves … EV) [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct ] | #e #s1 #r #E1 #E2 #E3 #_ destruct // | #s1 #r #S1 #E1 #E2 #E3 #_ destruct inversion (eval_perserves … EV) [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct inversion S1 [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/ | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct ] | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct ] | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct ] qed. inversion S23 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct | #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct inversion (eval_perserves … EV) [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct inversion S [ #fy #fsy #my #E1 #E2 #E3 destruct @N [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ] | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct ] | #e #s1 #r #E1 #E2 #E3 #E4 destruct // | #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd inversion (eval_perserves … EV) [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct inversion S1 [ #H103 #H104 #H105 #H106 #H107 #H108 destruct // | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct ] | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct ] | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct ] qed. ] qed. lemma bound_after_call : ∀ge,s,s',n. state_bound_on_steps_to_cost s (S n) → ∀CL:RTLabs_classify s = cl_call. as_after_return (RTLabs_status ge) «s, CL» s' → RTLabs_cost s' = false → state_bound_on_steps_to_cost s' n. #ge #s #s' #n #H inversion H [ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m' #E destruct | #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct whd in S; #CL cases s' [ #f' #fs' #m' * #N #F #CS %1 whd inversion S [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥ change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P * | #l #n #B #E1 #E2 #_ destruct
Note: See TracChangeset for help on using the changeset viewer.