Changeset 1595


Ignore:
Timestamp:
Dec 7, 2011, 4:24:42 PM (8 years ago)
Author:
campbell
Message:

We don't need an explicit termination count when building traces.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1594 r1595  
    204204*)
    205205
    206 (* [nth_is_return ge n depth s trace] says that after [n] steps of [trace] from
    207    [s] we reach the return state for the current function.  [depth] performs
    208    the call/return counting necessary for handling deeper function calls.
    209    It should be zero at the top level. *)
    210 inductive nth_is_return (ge:genv) : nat → nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
    211 | nir_step : ∀n,s,tr,s',depth,EX,trace.
     206(* [will_return ge depth s trace] says that after a finite number of steps of
     207   [trace] from [s] we reach the return state for the current function.  [depth]
     208   performs the call/return counting necessary for handling deeper function
     209   calls.  It should be zero at the top level. *)
     210inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop ≝
     211| wr_step : ∀s,tr,s',depth,EX,trace.
    212212    RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
    213     nth_is_return ge n depth s' trace →
    214     nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
    215 | nir_call : ∀n,s,tr,s',depth,EX,trace.
     213    will_return ge depth s' trace →
     214    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
     215| wr_call : ∀s,tr,s',depth,EX,trace.
    216216    RTLabs_classify s = cl_call →
    217     nth_is_return ge n (S depth) s' trace →
    218     nth_is_return ge (S n) depth s (ft_step ?? ge s tr s' EX trace)
    219 | nir_ret : ∀n,s,tr,s',depth,EX,trace.
     217    will_return ge (S depth) s' trace →
     218    will_return ge depth s (ft_step ?? ge s tr s' EX trace)
     219| wr_ret : ∀s,tr,s',depth,EX,trace.
    220220    RTLabs_classify s = cl_return →
    221     nth_is_return ge n depth s' trace →
    222     nth_is_return ge (S n) (S depth) s (ft_step ?? ge s tr s' EX trace)
     221    will_return ge depth s' trace →
     222    will_return ge (S depth) s (ft_step ?? ge s tr s' EX trace)
    223223    (* Note that we require the ability to make a step after the return (this
    224224       corresponds to somewhere that will be guaranteed to be a label at the
    225225       end of the compilation chain). *)
    226 | nir_base : ∀s,tr,s',EX,trace.
     226| wr_base : ∀s,tr,s',EX,trace.
    227227    RTLabs_classify s = cl_return →
    228     nth_is_return ge O O s (ft_step ?? ge s tr s' EX trace)
     228    will_return ge O s (ft_step ?? ge s tr s' EX trace)
    229229.
    230230
    231231discriminator nat.
     232
     233lemma will_return_call : ∀ge,depth,s,trace.
     234  will_return ge depth s trace →
     235  will_return ge (pred depth) s trace.
     236#ge #depth #s #trace #H elim H
     237[ #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %1 //
     238| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2 %2 //
     239  cases d in H1 H2 ⊢ %; //
     240| #s1 #tr #s2 #d #EX #trc #CL #H1 #H2
     241  cases d in H1 H2 ⊢ %; [ #H1 #H2 %4 // | /2/ ]
     242| #s1 #tr #s2 #EX #trc #CL %4 //
     243] qed.
     244
     245(*
     246(* If we'll return then we must return from calls. *)
     247lemma will_return_call : ∀ge,depth,s,trace.
     248  will_return ge (S depth) s trace →
     249  will_return ge depth s trace.
     250#ge #depth #s #trace #H elim H in ⊢ ?;
     251[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
     252| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #H4 /2/
     253| #H204 #H205 #H206 #H207 #H208 #H209 #H210 #H211 #H212 #H213 /2/
     254| #H215 #H216 #H217 #H218 #H219 #H220 #H221
     255  inversion H221
     256  [ #H223 #H224 #H225 #H226 #H227 #H228 #H229 #H230 #H231 #H232 #H233 #H234 #H235 destruct >H220 in H229; * #E destruct
     257  | #H237 #H238 #H239 #H240 #H241 #H242 #H243 #H244 #H245 #H246 #H247 #H248 #H249 destruct >H220 in H243; #E destruct
     258  | #H265 #H266 #H267 #H268 #H269 #H270 #H271 #H272 #H273 #H274 #H275 #H276 #H277 destruct
     259  | #H279 #H280 #H281 #H282 #H283 #H284 #H285 #H286 #H287 #H288 destruct
     260] qed. check will_return_call.
     261| #H130 #H131 #H132 #H133 #H134 #H135
     262  inversion H
     263  [ #H190 #H191 #H192 #H193 #H194 #H195 #H196 #H197 #H198 #H199 #H200 #H201 #H202 destruct
     264    cases H196 #E destruct
     265 
     266
     267let rec will_return_call ge depth s trace (H:will_return ge (S depth) s trace)
     268  on H : will_return ge depth s trace ≝
     269match H return λSdepth,s,trace. λ_. S depth = Sdepth → will_return ge depth s trace with
     270[ wr_step s tr s' d EX trace CL H' ⇒ λE. wr_step ge s tr s' ? EX trace CL ?
     271| wr_call s tr s' d EX trace CL H' ⇒ λE. ?
     272| wr_ret s tr s' d EX trace CL H' ⇒ λE. ?
     273| wr_base s tr s' EX trace CL ⇒ λE. ?
     274] (refl ? (S depth)).
     275[ @(match E return λx,E. will_return ? x ?? → will_return ge ??? with [ refl ⇒ λH''.? ] H')
     276  @(will_return_call … H'')
     277| *: cases daemon ] qed.
     278| %2 /2/
     279| destruct cases d in H' ⊢ %;
     280  [ #H' @wr_base //
     281  | #d' #H' %3 /2/
     282  ]
     283| destruct
     284] qed.
     285
     286(* If we'll return then we must return from calls. *)
     287lemma will_return_call : ∀ge,depth,s,trace.
     288  will_return ge (S depth) s trace →
     289  will_return ge depth s trace.
     290#ge #depth #s #trace #H lapply (refl ? (S depth))
     291generalize in ⊢ (???(?%) → ??%??); elim H in ⊢ (∀_.???% → %);
     292[ #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %1 /2/
     293| #s1 #tr #s2 #d1 #EX #tr1 #H1 #H2 #H3 #n #H4 destruct %2 /2/ @H3
     294 
     295discriminator nat.
     296
     297
    232298
    233299(* Find time until a nested call completes. *)
     
    294360| #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 destruct
    295361| #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 destruct >H130 in CL; #E destruct
     362] qed.
     363*)
     364
     365lemma will_return_notfn : ∀ge,s,tr,s',EX,trace.
     366  RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump →
     367  will_return ge O s (ft_step ?? ge s tr s' EX trace) →
     368  will_return ge O s' trace.
     369#ge #s #tr #s' #EX #trace * #CL #TERM inversion TERM
     370[ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //
     371| #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct
     372| #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct
     373| #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct
     374| #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //
     375| #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct
     376| #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct
     377| #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct
    296378] qed.
    297379
     
    407489] qed.
    408490
     491lemma rtlabs_call_inv : ∀s.
     492  RTLabs_classify s = cl_call →
     493  ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
     494* [ #f #fs #m whd in ⊢ (??%? → ?);
     495    cases (lookup_present … (next f) (next_ok f)) normalize
     496    try #A try #B try #C try #D try #E try #F try #G destruct
     497  | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
     498  | normalize #H411 #H412 #H413 #H414 #H415 destruct
     499  ] qed.
     500
     501lemma well_cost_labelled_call : ∀ge,s,tr,s'.
     502  eval_statement ge s = Value ??? 〈tr,s'〉 →
     503  well_cost_labelled_state s →
     504  RTLabs_classify s = cl_call →
     505  RTLabs_cost s' = true.
     506#ge #s #tr #s' #EV #WCL #CL
     507cases (rtlabs_call_inv s CL)
     508#fd * #args * #dst * #stk * #m #E >E in EV WCL;
     509whd in ⊢ (??%? → % → ?);
     510cases fd
     511[ #fn whd in ⊢ (??%? → % → ?);
     512  @bindIO_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any)
     513  #m' #b whd in ⊢ (??%? → ?); #E' destruct
     514  * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3
     515  @WCL2
     516| #fn whd in ⊢ (??%? → % → ?);
     517  @bindIO_value #evargs #Eargs
     518  @bindIO_value #evres #Eres
     519  normalize in Eres; destruct
     520] qed.
    409521
    410522(* Don't need to know that labels break loops because we have termination. *)
     
    412524record trace_result (ge:genv) (T:state → Type[0]) : Type[0] ≝ {
    413525  new_state : state;
    414   termination_count : nat;
    415526  remainder : flat_trace io_out io_in ge new_state;
    416527  cost_labelled : well_cost_labelled_state new_state;
     
    424535    (* We handle returns specially *)
    425536    match ends with
    426     [ doesnt_end_with_ret ⇒ nth_is_return ge (termination_count ?? trace_res) O (new_state ?? trace_res) (remainder ?? trace_res)
     537    [ doesnt_end_with_ret ⇒ will_return ge O (new_state ?? trace_res) (remainder ?? trace_res)
    427538    | ends_with_ret ⇒ True
    428539    ]
     
    436547    (mk_trace_result ge (T2 (ends … r))
    437548      (new_state … r)
    438       (termination_count … r)
    439549      (remainder … r)
    440550      (cost_labelled … r)
     
    449559  mk_trace_result ge T2
    450560    (new_state … r)
    451     (termination_count … r)
    452561    (remainder … r)
    453562    (cost_labelled … r)
     
    455564.
    456565
    457 let rec make_label_return n ge s
     566let rec make_label_return ge s
    458567  (trace: flat_trace io_out io_in ge s)
    459568  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    460569  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    461570  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    462   (TERMINATES: nth_is_return ge n O s trace)
     571  (TERMINATES: will_return ge O s trace)
    463572  : trace_result ge (trace_label_return (RTLabs_status ge) s) ≝
    464573
    465   let r ≝ make_label_label n ge s trace ???? in
     574  let r ≝ make_label_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in
    466575  match ends … r return λx. trace_label_label ? x ?? → match x with [doesnt_end_with_ret⇒ ?|_⇒ ?] → ? with
    467576  [ ends_with_ret ⇒ λtll,term.
    468577      replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) tll)
    469578  | doesnt_end_with_ret ⇒ λtll,term.
    470       let r' ≝ make_label_return (termination_count … r) ge (new_state … r)
    471                  (remainder … r) ??? term in
     579      let r' ≝ make_label_return ge (new_state … r)
     580                 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? term in
    472581        replace_trace … r'
    473582          (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') tll (new_trace … r'))
    474583  ] (new_trace … r) (terminates … r)
    475584
    476 and make_label_label n ge s
     585and make_label_label ge s
    477586  (trace: flat_trace io_out io_in ge s)
    478587  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    479588  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    480589  (STATEMENT_COSTLABEL: RTLabs_cost s = true)       (* current statement is a cost label *)
    481   (TERMINATES: nth_is_return ge n O s trace)
     590  (TERMINATES: will_return ge O s trace)
    482591  : sub_trace_result ge (λends. trace_label_label (RTLabs_status ge) ends s) ≝
    483 let r ≝ make_any_label n ge s trace ??? in
     592let r ≝ make_any_label ge s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in
    484593  replace_sub_trace ??? r
    485594    (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL)
    486595
    487 and make_any_label n ge s
     596and make_any_label ge s
    488597  (trace: flat_trace io_out io_in ge s)
    489598  (ENV_COSTLABELLED: well_cost_labelled_ge ge)
    490599  (STATE_COSTLABELLED: well_cost_labelled_state s)  (* functions in the state *)
    491   (TERMINATES: nth_is_return ge n O s trace)
     600  (TERMINATES: will_return ge O s trace)
    492601  : sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) ≝
    493 match trace return λs,trace. well_cost_labelled_state s → nth_is_return ???? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with
     602match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends s) with
    494603[ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ?
    495604| ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES.
     
    498607        match RTLabs_cost next return λx. RTLabs_cost next = x → ? with
    499608        [ true ⇒ λCS.
    500             mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
     609            mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
    501610        | false ⇒ λCS.
    502             let r ≝ make_any_label (pred n) ge next trace' ENV_COSTLABELLED ?? in
     611            let r ≝ make_any_label ge next trace' ENV_COSTLABELLED ?? in
    503612                replace_sub_trace ??? r
    504613                  (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??)
    505614        ] (refl ??)
    506615    | cl_jump ⇒ λCL.
    507         mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
    508     | cl_call ⇒ λCL. ?
     616        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) doesnt_end_with_ret (mk_trace_result ge ? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???)) ?
     617    | cl_call ⇒ λCL.
     618        let r ≝ make_label_return ge next trace' ENV_COSTLABELLED ??? in
     619        let r' ≝ make_any_label ge (new_state … r) (remainder … r) ENV_COSTLABELLED ?? in
     620        replace_sub_trace ??? r'
     621          (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r'))
    509622    | cl_return ⇒ λCL.
    510         mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next (pred n) trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?
     623        mk_sub_trace_result ge (λends. trace_any_label (RTLabs_status ge) ends start) ends_with_ret (mk_trace_result ge ? next trace' ? (tal_base_return (RTLabs_status ge) start next ? CL)) ?
    511624    ] (refl ? (RTLabs_classify start))
    512625| ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥
    513626] STATE_COSTLABELLED TERMINATES.
    514627
    515 [ //
    516 | //
    517 | @(trace_label_label_label … tll)
    518 | //
    519 | //
    520 | //
    521 | //
    522 | //
    523 | //
    524 | //
     628[ @(trace_label_label_label … tll)
    525629|
    526630| %{tr} @EV
     
    531635| @(well_cost_labelled_jump … EV) //
    532636| @(well_cost_labelled_state_step  … EV) //
    533 | @(nth_is_return_notfn … TERMINATES) %2 @CL
     637| @(will_return_notfn … TERMINATES) %2 @CL
     638| (* oh dear *)
     639| %{tr} @EV
     640| @(cost_labelled … r)
    534641|
    535 | %{tr} @EV
     642|
     643|
     644
     645 @(well_cost_labelled_state_step  … EV) //
    536646| % whd in ⊢ (% → ?); >CL #E destruct
    537647| @CS
    538 | @(well_cost_labelled_state_step  … EV) //
    539648| @(nth_is_return_notfn … TERMINATES) %1 @CL
    540649| % whd in ⊢ (% → ?); >CS #E destruct
Note: See TracChangeset for help on using the changeset viewer.