Changeset 1736 for src/RTLabs/Traces.ma


Ignore:
Timestamp:
Feb 24, 2012, 1:19:10 PM (8 years ago)
Author:
campbell
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

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1719 r1736  
    4343        [ Callstate fd args dst stk m ⇒
    4444          λ_. match s' with
    45           [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ]
    46           | Finalstate r ⇒ True
     45          [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
     46          | Finalstate r ⇒ stk = [ ]
    4747          | _ ⇒ False
    4848          ]
     
    569569| sp_finished : ∀s1,f,f',fs,m.
    570570    next f = next f' →
     571    frame_rel f f' →
    571572    stack_of_state (f::fs) s1 →
    572573    stack_preserved ends_with_ret s1 (State f' fs m)
    573 | sp_stop : ∀e,s1,r.
    574     stack_preserved e s1 (Finalstate r)
     574| sp_stop : ∀s1,r.
     575    stack_of_state [ ] s1 →
     576    stack_preserved ends_with_ret s1 (Finalstate r)
     577| sp_top : ∀fd,args,dst,m,r.
     578    stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
    575579.
    576580
     
    591595
    592596lemma stack_preserved_final : ∀e,r,s.
    593   stack_preserved e (Finalstate r) s → ∃r'. s = Finalstate r'.
    594 #e #r #s #H inversion H
     597  ¬stack_preserved e (Finalstate r) s.
     598#e #r #s % #H inversion H
    595599[ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
    596600  inversion SOS #a #b #c #d #e #f try #g try #h destruct
    597 | #H194 #H195 #H196 #H197 #H198 #H199 #SOS #H201 #H202 #H203 #H204 destruct
     601| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
    598602  inversion SOS #a #b #c #d #e #f try #g try #h destruct
    599 | #e' #s' #r' #E1 #E2 #E3 #E4 destruct %{r'} @refl
     603| #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
     604  inversion SOS #a #b #c #d #e #f try #g try #h destruct
     605| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
    600606] qed.
    601607
     
    609615  [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
    610616    @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
    611   | #s1'' #f #f' #fs' #m #N #S1' #E1 #E2 #E3 #E4 destruct
     617  | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
    612618    @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
    613   | #s1'' #r #E1 #E2 #E3 #E4 destruct //
     619  | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
     620  | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
     621    inversion S2
     622    [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
     623    | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
     624    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
     625    ]
    614626  ]
    615627| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
    616628| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
    617   cases (stack_preserved_final … H) #r #E destruct //
     629  cases (stack_preserved_final … H) #r #E destruct
     630| #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
     631  @(absurd … F) //
    618632] qed.
    619633
     
    628642| #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
    629643| #res #dst *
    630   [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV; [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct // | *: normalize #a try #b destruct ] ]
     644  [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
     645    [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
    631646  | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV
    632647    whd in EV:(??%?); destruct @(sp_finished ? f) //
     648    cases f //
    633649  ]
    634650| #r #s2 #tr #E normalize in E; destruct
     
    660676inversion SP
    661677[ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
    662 | #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
     678| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
    663679  inversion (eval_perserves … EV)
    664680  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
     
    674690  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
    675691  ]
    676 | #e #s1 #r #E1 #E2 #E3 #_ destruct //
     692| #s1 #r #S1 #E1 #E2 #E3 #_ destruct
     693  inversion (eval_perserves … EV)
     694  [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
     695  | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
     696  | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
     697    inversion S1
     698    [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
     699    | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
     700    | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
     701    ]
     702  | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
     703  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
     704  | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
     705  ]
     706| #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
    677707] qed.
    678708 
     
    686716inversion S23
    687717[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
    688 | #s2' #f #f' #fs #m' #N #S #E1 #E2 #E3 #E4 destruct
     718| #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
    689719  inversion (eval_perserves … EV)
    690720  [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
     
    692722  | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
    693723    inversion S
    694     [ #fy #fsy #my #E1 #E2 #E3 destruct @N
     724    [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
    695725    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
    696726    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
     
    700730  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
    701731  ]
    702 | #e #s1 #r #E1 #E2 #E3 #E4 destruct //
     732| #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
     733  inversion (eval_perserves … EV)
     734  [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
     735  | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
     736  | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
     737    inversion S1
     738    [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
     739    | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
     740    | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
     741    ]
     742  | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
     743  | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
     744  | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
     745  ]
     746| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
    703747] qed.
    704748
     
    12441288] qed.
    12451289
     1290lemma bound_after_call : ∀ge,s,s',n.
     1291  state_bound_on_steps_to_cost s (S n) →
     1292  ∀CL:RTLabs_classify s = cl_call.
     1293  as_after_return (RTLabs_status ge) «s, CL» s' →
     1294  RTLabs_cost s' = false →
     1295  state_bound_on_steps_to_cost s' n.
     1296#ge #s #s' #n #H inversion H
     1297[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
     1298  #fn * #args * #dst * #stk * #m' #E destruct
     1299| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
     1300  whd in S; #CL cases s'
     1301  [ #f' #fs' #m' * #N #F #CS
     1302    %1 whd
     1303    inversion S
     1304    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
     1305      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
     1306    | #l #n #B #E1 #E2 #_ destruct <N <F @B
     1307    ]
     1308  | #fd' #args' #dst' #fs' #m' *
     1309  | #rv #dst' #fs' #m' *
     1310  | #r #E normalize in E; destruct
     1311  ]
     1312| #rtv #dst #f #fs #m #n' #S #E1 #E2 #E3 destruct #CL normalize in CL; destruct
     1313] qed.
     1314
    12461315lemma bound_after_step : ∀ge,s,tr,s',n.
    12471316  state_bound_on_steps_to_cost s (S n) →
     
    12911360  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
    12921361    %1 whd in FS ⊢ %;
    1293     inversion (stack_preserved_return … EVAL) [ @refl | #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct | 4: #H276 #H277 #H278 #H279 #H280 #H281 #H282 destruct ]
    1294     #s1 #f1 #f2 #fs #m #FE #SS1 #_ #E1 #E2 #_ destruct <FE
     1362    inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
     1363    #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
    12951364    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 ]
    12961365    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
     
    14141483  cases (terminates … tlr) //
    14151484| (* FIXME: post-call not-wrong *)
    1416 | (* FIXME: bound on steps after call *)
     1485| @(bound_after_call ge … LABEL_LIMIT CL ? CS)
     1486  @(RTLabs_after_call … CL EV) @(stack_ok … tlr)
    14171487| @(well_cost_labelled_state_step … EV) //
    14181488| @(well_cost_labelled_call … EV) //
Note: See TracChangeset for help on using the changeset viewer.