 Timestamp:
 Jan 10, 2012, 11:26:48 AM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1617 r1637 208 208 performs the call/return counting necessary for handling deeper function 209 209 calls. It should be zero at the top level. *) 210 inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Prop≝210 inductive will_return (ge:genv) : nat → ∀s. flat_trace io_out io_in ge s → Type[0] ≝ 211 211  wr_step : ∀s,tr,s',depth,EX,trace. 212 212 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump → … … 229 229 . 230 230 231 let rec will_return_length ge d s tr (T:will_return ge d s tr) on T : nat ≝ 232 match T with 233 [ wr_step _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') 234  wr_call _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') 235  wr_ret _ _ _ _ _ _ _ T' ⇒ S (will_return_length … T') 236  wr_base _ _ _ _ _ _ ⇒ S O 237 ]. 238 include alias "arithmetics/nat.ma". 239 240 lemma wrl_nonzero : ∀ge,d,s,tr,T. O ≥ 3 * (will_return_length ge d s tr T) → False. 241 #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] 242 whd in ⊢ (??(??%) → ?); 243 >commutative_times 244 #H lapply (le_plus_b … H) 245 #H lapply (le_to_leb_true … H) 246 normalize #E destruct 247 qed. 248 (* 249 lemma wrl_nonzero : ∀ge,d,s,tr,T. ∀P:nat → Prop. (∀x. P (S x)) → P (will_return_length ge d s tr T). 250 #ge #d #s #tr * #s1 #tr1 #s2 [ 1,2,3: #d ] #EX #tr' #CL [1,2,3:#IH] #P #H @H 251 qed. 252 *) 231 253 discriminator nat. 232 254 … … 243 265 ] qed. 244 266 267 lemma will_return_call' : ∀ge,d,s,tr,s',EX,trace. 268 RTLabs_classify s = cl_call → 269 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). 270 ΣTM':will_return ge (S d) s' trace. will_return_length … TM > will_return_length … TM'. 271 #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM 272 [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct 273  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 destruct % // 274  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 @⊥ destruct >CL in H53; #E destruct 275  #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 @⊥ destruct >CL in H66; #E destruct 276 ] qed. 277 278 lemma will_return_return : ∀ge,d,s,tr,s',EX,trace. 279 RTLabs_classify s = cl_return → 280 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). 281 match d with 282 [ O ⇒ True 283  S d' ⇒ 284 ΣTM':will_return ge d' s' trace. will_return_length … TM > will_return_length … TM' 285 ]. 286 #ge #d #s #tr #s' #EX #trace #CL #TERM inversion TERM 287 [ #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 @⊥ destruct >CL in H25; * #E destruct 288  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 @⊥ destruct >CL in H39; #E destruct 289  #H47 #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 destruct % // 290  #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 destruct @I 291 ] qed. 245 292 246 293 lemma will_return_notfn : ∀ge,d,s,tr,s',EX,trace. 247 RTLabs_classify s = cl_other ∨ RTLabs_classify s = cl_jump→248 will_return ge d s (ft_step ?? ge s tr s' EX trace) →249 will_return ge d s' trace.294 (RTLabs_classify s = cl_other) ⊎ (RTLabs_classify s = cl_jump) → 295 ∀TM:will_return ge d s (ft_step ?? ge s tr s' EX trace). 296 ΣTM':will_return ge d s' trace. will_return_length … TM > will_return_length … TM'. 250 297 #ge #d #s #tr #s' #EX #trace * #CL #TERM inversion TERM 251 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct //252  #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 destruct >CL in H310; #E destruct253  #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 destruct >CL in H324; #E destruct254  #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 destruct >CL in H337; #E destruct255  #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct //256  #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 destruct >CL in H363; #E destruct257  #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 destruct >CL in H377; #E destruct258  #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 destruct >CL in H390; #E destruct298 [ #H290 #H291 #H292 #H293 #H294 #H295 #H296 #H297 #H298 #H299 #H300 #H301 #H302 destruct % // 299  #H304 #H305 #H306 #H307 #H308 #H309 #H310 #H311 #H312 #H313 #H314 #H315 #H316 @⊥ destruct >CL in H310; #E destruct 300  #H318 #H319 #H320 #H321 #H322 #H323 #H324 #H325 #H326 #H327 #H328 #H329 #H330 @⊥ destruct >CL in H324; #E destruct 301  #H332 #H333 #H334 #H335 #H336 #H337 #H338 #H339 #H340 #H341 @⊥ destruct >CL in H337; #E destruct 302  #H343 #H344 #H345 #H346 #H347 #H348 #H349 #H350 #H351 #H352 #H353 #H354 #H355 destruct % // 303  #H357 #H358 #H359 #H360 #H361 #H362 #H363 #H364 #H365 #H366 #H367 #H368 #H369 @⊥ destruct >CL in H363; #E destruct 304  #H371 #H372 #H373 #H374 #H375 #H376 #H377 #H378 #H379 #H380 #H381 #H382 #H383 @⊥ destruct >CL in H377; #E destruct 305  #H385 #H386 #H387 #H388 #H389 #H390 #H391 #H392 #H393 #H394 @⊥ destruct >CL in H390; #E destruct 259 306 ] qed. 260 307 … … 405 452 (* A bit of mucking around with the depth to avoid proving termination after 406 453 termination. *) 407 record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) : Type[0] ≝ {454 record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ { 408 455 new_state : state; 409 456 remainder : flat_trace io_out io_in ge new_state; … … 412 459 terminates : match depth with 413 460 [ O ⇒ True 414  S d ⇒ will_return ge d new_state remainder461  S d ⇒ ΣTM:will_return ge d new_state remainder. limit > will_return_length … TM 415 462 ] 416 463 }. 417 464 418 record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) : Type[0] ≝ {465 record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ { 419 466 ends : trace_ends_with_ret; 420 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (T ends) 467 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (T ends) limit 421 468 }. 422 469 423 definition replace_sub_trace : ∀ge,trm,T1,T2. 424 ∀r:sub_trace_result ge trm T1. T2 (ends … r) (new_state … r) → sub_trace_result ge trm T2 ≝ 425 λge,trm,T1,T2,r,trace. 426 mk_sub_trace_result ge trm T2 427 (ends … r) 428 (mk_trace_result ge ? (T2 (ends … r)) 429 (new_state … r) 430 (remainder … r) 431 (cost_labelled … r) 432 trace 433 (terminates … r) 434 ) 435 . 436 437 definition replace_trace : ∀ge,trm,T1,T2. 438 ∀r:trace_result ge trm T1. T2 (new_state … r) → trace_result ge trm T2 ≝ 439 λge,trm,T1,T2,r,trace. 440 mk_trace_result ge trm T2 470 definition replace_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 → 471 ∀r:trace_result ge d T1 l1. T2 (new_state … r) → trace_result ge d T2 l2 ≝ 472 λge,d,T1,T2,l1,l2,lGE,r,trace. 473 mk_trace_result ge d T2 l2 441 474 (new_state … r) 442 475 (remainder … r) 443 476 (cost_labelled … r) 444 477 trace 445 (terminates … r) 446 . 478 (match d return λd'.match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → 479 match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with 480 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???? r)) 481 . @(transitive_le … lGE) @(pi2 … TM) qed. 482 483 definition replace_sub_trace : ∀ge,d,T1,T2,l1,l2. l2 ≥ l1 → 484 ∀r:sub_trace_result ge d T1 l1. T2 (ends … r) (new_state … r) → sub_trace_result ge d T2 l2 ≝ 485 λge,d,T1,T2,l1,l2,lGE,r,trace. 486 mk_sub_trace_result ge d T2 l2 487 (ends … r) 488 (replace_trace … lGE … r trace). 489 490 definition myge : nat → nat → Prop ≝ ge. 447 491 448 492 let rec make_label_return ge depth s … … 452 496 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 453 497 (TERMINATES: will_return ge depth s trace) 454 : trace_result ge depth (trace_label_return (RTLabs_status ge) s) ≝ 455 456 let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES in 457 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) → ? with 498 (TIME: nat) 499 (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) 500 on TIME : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 501 match TIME return λTIME. TIME ≥ ? → ? with 502 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 503  S TIME ⇒ λTERMINATES_IN_TIME. 504 let r ≝ make_label_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES TIME ? in 505 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with 458 506 [ ends_with_ret ⇒ λr. 459 507 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) 460 508  doesnt_end_with_ret ⇒ λr. 461 509 let r' ≝ make_label_return ge depth (new_state … r) 462 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? ( terminates ??? r)in510 (remainder … r) ENV_COSTLABELLED (cost_labelled … r) ? (pi1 … (terminates … r)) TIME ? in 463 511 replace_trace … r' 464 512 (tlr_step (RTLabs_status ge) s (new_state … r) (new_state … r') (new_trace … r) (new_trace … r')) 465 513 ] (trace_res … r) 514 ] TERMINATES_IN_TIME 466 515 467 516 and make_label_label ge depth s … … 471 520 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 472 521 (TERMINATES: will_return ge depth s trace) 473 : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) ≝ 474 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES in 522 (TIME: nat) 523 (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) 524 on TIME : sub_trace_result ge depth (λends. trace_label_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝ 525 match TIME return λTIME. TIME ≥ ? → ? with 526 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 527  S TIME ⇒ λTERMINATES_IN_TIME. 528 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in 475 529 replace_sub_trace … r 476 530 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) 531 ] TERMINATES_IN_TIME 477 532 478 533 and make_any_label ge depth s … … 481 536 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 482 537 (TERMINATES: will_return ge depth s trace) 483 : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) ≝ 484 match trace return λs,trace. well_cost_labelled_state s → will_return ??? trace → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) with 485 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 486  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES. 487 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 538 (TIME: nat) 539 (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) 540 on TIME : sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TERMINATES) ≝ 541 542 match TIME return λTIME. TIME ≥ ? → ? with 543 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 544  S TIME ⇒ λTERMINATES_IN_TIME. 545 match trace return λs,trace. well_cost_labelled_state s → ∀TM:will_return ??? trace. myge ? (times 3 (will_return_length ??? trace TM)) → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with 546 [ ft_stop st FINAL ⇒ λSTATE_COSTLABELLED,TERMINATES. ? 547  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 548 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 488 549 [ cl_other ⇒ λCL. 489 match RTLabs_cost next return λx. RTLabs_cost next = x → ?with550 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 490 551 [ true ⇒ λCS. 491 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) 552 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ? 492 553 doesnt_end_with_ret 493 (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)554 (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 494 555  false ⇒ λCS. 495 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? in556 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ?? TIME ? in 496 557 replace_sub_trace … r 497 558 (tal_step_default (RTLabs_status ge) (ends … r) start next (new_state … r) ? (new_trace … r) ??) 498 559 ] (refl ??) 499 560  cl_jump ⇒ λCL. 500 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) 561 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ? 501 562 doesnt_end_with_ret 502 (mk_trace_result ge ?? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?)563 (mk_trace_result ge ??? next trace' ? (tal_base_not_return (RTLabs_status ge) start next ???) ?) 503 564  cl_call ⇒ λCL. 504 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? in505 let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ? ? in506 replace_sub_trace ????r'565 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ??? TIME ? in 566 let r' ≝ make_any_label ge depth (new_state … r) (remainder … r) ENV_COSTLABELLED ? (pi1 … (terminates … r)) TIME ? in 567 replace_sub_trace … r' 507 568 (tal_step_call (RTLabs_status ge) (ends … r') start next (new_state … r) (new_state … r') ? CL ? (new_trace … r) (new_trace … r')) 508 569  cl_return ⇒ λCL. 509 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) 570 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ? 510 571 ends_with_ret 511 (mk_trace_result ge ?? 572 (mk_trace_result ge ??? 512 573 next 513 574 trace' … … 516 577 ?) 517 578 ] (refl ? (RTLabs_classify start)) 518  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 519 ] STATE_COSTLABELLED TERMINATES. 520 521 [ @(trace_label_label_label … (new_trace … r)) 579  ft_wrong start m EV ⇒ λSTATE_COSTLABELLED,TERMINATES. ⊥ 580 ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME 581 ] TERMINATES_IN_TIME. 582 583 [ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] 584  // 585  cases r #H1 #H2 #H3 #H4 * #x @le_S_to_le 586  @(trace_label_label_label … (new_trace … r)) 587  cases r #H1 #H2 #H3 #H4 * #H5 #H6 588 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 589 @(transitive_le … (3*(will_return_length … TERMINATES))) 590 [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times 591 @(monotonic_le_times_r 3 … H6) 592  @le_S @le_S @le_n 593 ] 594  @le_S_S_to_le @TERMINATES_IN_TIME 595  cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] 596  @le_n 597  @le_S_S_to_le @TERMINATES_IN_TIME 598  @(wrl_nonzero … TERMINATES_IN_TIME) 522 599  523  inversion TERMINATES 524 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 TERMINATES destruct >CL in H7; * #E destruct 525  #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 TERMINATES destruct >CL in H21; #E destruct 526  #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 TERMINATES destruct @H36 527  #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 #H52 whd @I 528 ] 600  @(will_return_return … CL TERMINATES) 529 601  %{tr} @EV 530 602  @(well_cost_labelled_state_step … EV) // … … 534 606  @(well_cost_labelled_jump … EV) // 535 607  @(well_cost_labelled_state_step … EV) // 608  27: @(will_return_call' … CL TERMINATES) 609  cases r #H1 #H2 #H3 #H4 * #H5 610 cases (will_return_call' … CL TERMINATES) 611 #TM #X #Y @le_S_to_le @(transitive_lt … Y X) 536 612  (* oh dear *) 537 613  %{tr} @EV 538 614  @(cost_labelled … r) 539  @(terminates … r) 615  cases r #H72 #H73 #H74 #H75 * #H76 #H78 616 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 617 cases (will_return_call' … TERMINATES) in H78; 618 #X #Y #Z 619 @(transitive_le … (monotonic_lt_times_r 3 … Y)) 620 [ @(transitive_le … (monotonic_lt_times_r 3 … Z)) // 621  // 622 ] 540 623  @(well_cost_labelled_state_step … EV) // 541 624  @(well_cost_labelled_call … EV) // 542  inversion TERMINATES 543 [ #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 TERMINATES destruct >CL in H60; * #E destruct 544  #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 TERMINATES destruct @H75 545  #H82 #H83 #H84 #H85 #H86 #H87 #H88 #H89 #H90 #H91 #H92 #H93 #H94 TERMINATES destruct >CL in H88; #E destruct 546  #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 TERMINATES destruct >CL in H101; #E destruct 547 ] 625  cases (will_return_call' … TERMINATES) 626 #TM #GT @le_S_S_to_le 627 >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times 628 @(transitive_le … TERMINATES_IN_TIME) 629 @(monotonic_le_times_r 3 … GT) 548 630  whd @(will_return_notfn … TERMINATES) %1 @CL 549 631  %{tr} @EV … … 551 633  @CS 552 634  @(well_cost_labelled_state_step … EV) // 635  39: @(will_return_notfn … TERMINATES) %1 @CL 636  cases (will_return_notfn … TERMINATES) #TM @le_S_to_le 553 637  % whd in ⊢ (% → ?); >CS #E destruct 554 638  @CL 555 639  %{tr} @EV 556 640  @(well_cost_labelled_state_step … EV) // 557  @(will_return_notfn … TERMINATES) %1 @CL 641  cases (will_return_notfn … TERMINATES) #TM #GT 642 @le_S_S_to_le 643 @(transitive_le … (monotonic_lt_times_r … GT) TERMINATES_IN_TIME) 644 // 558 645  inversion TERMINATES 559 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 TERMINATES destruct 560  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 TERMINATES destruct 561  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 TERMINATES destruct 562  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 TERMINATES destruct 563 ] 564  565 566 646 [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 TERMINATES TERMINATES destruct 647  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 TERMINATES TERMINATES destruct 648  #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 TERMINATES TERMINATES destruct 649  #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 TERMINATES TERMINATES destruct 650 ] 651 ] cases daemon qed. 652 653 let rec make_label_return' ge depth s 654 (trace: flat_trace io_out io_in ge s) 655 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 656 (STATE_COSTLABELLED: well_cost_labelled_state s) (* functions in the state *) 657 (STATEMENT_COSTLABEL: RTLabs_cost s = true) (* current statement is a cost label *) 658 (TERMINATES: will_return ge depth s trace) 659 : trace_result ge depth (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) ≝ 660 make_label_return ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED STATEMENT_COSTLABEL TERMINATES 661 (2 + 3 * will_return_length … TERMINATES) ?. 662 @le_n 663 qed. 567 664 568 665 (* FIXME: there's trouble at the end of the program because we can't make a step
Note: See TracChangeset
for help on using the changeset viewer.