Changeset 1681 for src/RTLabs
 Timestamp:
 Feb 9, 2012, 1:22:32 PM (9 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r1675 r1681 347 347 [ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % // 348 348  #ge #f #fs #m * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/ 349 (* 349 350  #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/ 351 *) 350 352  #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ 351 353  #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2 … … 442 444 ] qed. 443 445 446 447 (* The preservation of (most of) the stack is useful to show as_after_return. 448 This is a partial closure of the state_rel relation in semantics.ma  we only 449 accumulate information up to the first return. *) 450 inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝ 451  sp_normal : ∀f,f',fs,m,m'. frame_rel f f' → stack_preserved doesnt_end_with_ret (State f fs m) (State f' fs m') 452  sp_to_call : ∀f,f',fs,m,m',fd,args,dst. frame_rel f f' → stack_preserved doesnt_end_with_ret (State f fs m) (Callstate fd args dst (f'::fs) m') 453 (* Remember that this is one *after* the state just considered, so the trace 454 doesn't end with return, the return is the next state *) 455  sp_to_return : ∀f,fs,m,rtv,dst,m'. stack_preserved doesnt_end_with_ret (State f fs m) (Returnstate rtv dst fs m') 456  sp_from_return : ∀f,f',fs,m,rtv,dst,m'. (next f = next f') → frame_rel f f' → stack_preserved ends_with_ret (Returnstate rtv dst (f::fs) m) (State f' fs m') 457 (* A combination of the above *) 458  sp_over_return : ∀f1,f2,f3,fs,m,m'. (next f2 = next f3) → frame_rel f2 f3 → stack_preserved ends_with_ret (State f1 (f2::fs) m) (State f3 fs m'). 459 460 lemma frame_rel_trans : transitive ? frame_rel. 461 #x #y #z * 462 #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 inversion H10 463 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct // 464 qed. 465 466 lemma stack_preserved_join : ∀e,s1,s2,s3. 467 stack_preserved doesnt_end_with_ret s1 s2 → 468 stack_preserved e s2 s3 → 469 stack_preserved e s1 s3. 470 #e1 #s1 #s2 #s3 #H1 inversion H1 471 [ #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct #H2 inversion H2 472 [ #f2 #f2' #fs2 #m2 #m2' #F2 #E1 #E2 #E3 #E4 destruct % /2/ 473  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct %2 /2/ 474  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct /2/ 475  #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H145 #H146 destruct 476  #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H148 #H149 #H150 destruct /2/ 477 ] 478  #f #f' #fs #m #m' #fd #args #dst #F #E1 #E2 #E3 #E4 destruct #H2 inversion H2 479 [ #f2 #f2' #fs2 #m2 #m2' #F2 #H2' #E1 #E2 #E3 destruct 480  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct 481  #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 destruct 482  #H113 #H114 #H115 #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H145 #H146 destruct 483  #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H148 #H149 destruct 484 ] 485  #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct #H2 inversion H2 486 [ #f2 #f2' #fs2 #m2 #m2' #F2 #H2' #E1 #E2 #E3 destruct 487  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct 488  #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 destruct 489  #H124 #H125 #H126 #H127 #H128 #H129 #H130 #H131 #H132 #H133 #H151 #H152 destruct /2/ 490  #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 #H154 #H155 destruct 491 ] 492  #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct 493  #H52 #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 destruct 494 ] qed. 495 496 lemma stack_preserved_ret : ∀ge,s1,s2,tr. 497 RTLabs_classify s1 = cl_return → 498 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 499 stack_preserved ends_with_ret s1 s2. 500 #ge * 501 [ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?); 502 cases (lookup_present ??? (next f) (next_ok f)) in E; 503 normalize #a try #b try #c try #d try #e try #f try #g destruct 504  #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct 505  #res #dst * 506 [ #m #s2 #tr #_ #EV whd in EV:(??%?); destruct 507  #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_value #locals #El #EV 508 whd in EV:(??%?); destruct @sp_from_return cases f // 509 ] 510 ] qed. 511 512 lemma stack_preserved_step : ∀ge,s1,s2,tr. 513 RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump → 514 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 515 stack_preserved doesnt_end_with_ret s1 s2. 516 #ge0 #s1 #s2 #tr #CL #EV inversion (eval_perserves … EV) 517 [ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/ 518  #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/ 519  #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct 520 normalize in CL; cases CL #E destruct 521  #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/ 522  #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL 523 #E normalize in E; destruct 524 ] qed. 525 526 lemma stack_preserved_call : ∀ge,s1,s2,s3,tr. 527 RTLabs_classify s1 = cl_call → 528 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 529 stack_preserved ends_with_ret s2 s3 → 530 stack_preserved doesnt_end_with_ret s1 s3. 531 #ge #s1 #s2 #s3 #tr #CL #EV #SP 532 cases (rtlabs_call_inv … CL) 533 #fd * #args * #dst * #stk * #m #E destruct 534 444 535 (* Don't need to know that labels break loops because we have termination. *) 445 536 … … 447 538 termination. Note that we keep a proof that our upper bound on the length 448 539 of the termination proof is respected. *) 449 record trace_result (ge:genv) (depth:nat) ( T:state → Type[0]) (limit:nat) : Type[0] ≝ {540 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (T:state → Type[0]) (limit:nat) : Type[0] ≝ { 450 541 new_state : state; 451 542 remainder : flat_trace io_out io_in ge new_state; 452 543 cost_labelled : well_cost_labelled_state new_state; 453 544 new_trace : T new_state; 545 stack_ok : stack_preserved ends start new_state; 454 546 terminates : match depth with 455 547 [ O ⇒ True … … 460 552 (* The same with a flag indicating whether the function returned, as opposed to 461 553 encountering a label. *) 462 record sub_trace_result (ge:genv) (depth:nat) ( T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {554 record sub_trace_result (ge:genv) (depth:nat) (start:state) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ { 463 555 ends : trace_ends_with_ret; 464 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) (T ends) limit556 trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) ends start (T ends) limit 465 557 }. 466 558 … … 469 561 the size of the termination proof might need to be relaxed, too. *) 470 562 471 definition replace_trace : ∀ge,d, T1,T2,l1,l2. l2 ≥ l1 →472 ∀r:trace_result ge d T1 l1. T2 (new_state … r) → trace_result ge dT2 l2 ≝473 λge,d, T1,T2,l1,l2,lGE,r,trace.474 mk_trace_result ge d T2 l2563 definition replace_trace : ∀ge,d,e1,e2,s1,s2,T1,T2,l1,l2. l2 ≥ l1 → 564 ∀r:trace_result ge d e1 s1 T1 l1. T2 (new_state … r) → stack_preserved e2 s2 (new_state … r) → trace_result ge d e2 s2 T2 l2 ≝ 565 λge,d,e1,e2,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP. 566 mk_trace_result ge d e2 s2 T2 l2 475 567 (new_state … r) 476 568 (remainder … r) 477 569 (cost_labelled … r) 478 570 trace 571 SP 479 572 (match d return λd'.match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] → 480 573 match d' with [ O ⇒ True  S d'' ⇒ ΣTM.l2 > will_return_length ge d'' (new_state … r) (remainder … r) TM] with 481 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ???? r))574 [O ⇒ λ_. I  _ ⇒ λTM. «pi1 … TM, ?» ] (terminates ?????? r)) 482 575 . @(transitive_le … lGE) @(pi2 … TM) qed. 483 576 484 definition replace_sub_trace : ∀ge,d, T1,T2,l1,l2. l2 ≥ l1 →485 ∀r:sub_trace_result ge d T1 l1. T2 (ends … r) (new_state … r) → sub_trace_result ge dT2 l2 ≝486 λge,d, T1,T2,l1,l2,lGE,r,trace.487 mk_sub_trace_result ge d T2 l2577 definition replace_sub_trace : ∀ge,d,s1,s2,T1,T2,l1,l2. l2 ≥ l1 → 578 ∀r:sub_trace_result ge d s1 T1 l1. T2 (ends … r) (new_state … r) → stack_preserved (ends … r) s2 (new_state … r) → sub_trace_result ge d s2 T2 l2 ≝ 579 λge,d,s1,s2,T1,T2,l1,l2,lGE,r,trace,SP. 580 mk_sub_trace_result ge d s2 T2 l2 488 581 (ends … r) 489 (replace_trace … lGE … r trace ).582 (replace_trace … lGE … r trace SP). 490 583 491 584 (* Small syntax hack to avoid ambiguous input problems. *) … … 500 593 (TIME: nat) 501 594 (TERMINATES_IN_TIME: myge TIME (plus 2 (times 3 (will_return_length … TERMINATES)))) 502 on TIME : trace_result ge depth 595 on TIME : trace_result ge depth ends_with_ret s 503 596 (trace_label_return (RTLabs_status ge) s) 504 597 (will_return_length … TERMINATES) ≝ … … 515 608 TERMINATES 516 609 TIME ? in 517 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) with610 match ends … r return λx. trace_result ge (match x with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth]) x s (trace_label_label (RTLabs_status ge) x s) ? → trace_result ge depth ends_with_ret s (trace_label_return (RTLabs_status ge) s) (will_return_length … TERMINATES) with 518 611 [ ends_with_ret ⇒ λr. 519 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) 612 replace_trace … r (tlr_base (RTLabs_status ge) s (new_state … r) (new_trace … r)) (stack_ok … r) 520 613  doesnt_end_with_ret ⇒ λr. 521 614 let r' ≝ make_label_return ge depth (new_state … r) … … 526 619 replace_trace … r' 527 620 (tlr_step (RTLabs_status ge) s (new_state … r) 528 (new_state … r') (new_trace … r) (new_trace … r')) 621 (new_state … r') (new_trace … r) (new_trace … r')) ? 529 622 ] (trace_res … r) 530 623 … … 540 633 (TIME: nat) 541 634 (TERMINATES_IN_TIME: myge TIME (plus 1 (times 3 (will_return_length … TERMINATES)))) 542 on TIME : sub_trace_result ge depth 635 on TIME : sub_trace_result ge depth s 543 636 (λends. trace_label_label (RTLabs_status ge) ends s) 544 637 (will_return_length … TERMINATES) ≝ … … 550 643 let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in 551 644 replace_sub_trace … r 552 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) 645 (tll_base (RTLabs_status ge) (ends … r) s (new_state … r) (new_trace … r) STATEMENT_COSTLABEL) (stack_ok … r) 553 646 554 647 ] TERMINATES_IN_TIME … … 562 655 (TIME: nat) 563 656 (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) 564 on TIME : sub_trace_result ge depth 657 on TIME : sub_trace_result ge depth s 565 658 (λends. trace_any_label (RTLabs_status ge) ends s) 566 659 (will_return_length … TERMINATES) ≝ … … 570 663  S TIME ⇒ λTERMINATES_IN_TIME. 571 664 572 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) with665 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 s (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with 573 666 [ ft_stop st FINAL ⇒ 574 667 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ? 575 668 576 669  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 577 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) with670 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 578 671 [ cl_other ⇒ λCL. 579 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) with672 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 580 673 (* We're about to run into a label. *) 581 674 [ true ⇒ λCS. 582 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?675 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? 583 676 doesnt_end_with_ret 584 (mk_trace_result ge ???next trace' ?585 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ? )677 (mk_trace_result ge … next trace' ? 678 (tal_base_not_return (RTLabs_status ge) start next ?? CS) ??) 586 679 (* An ordinary step, keep going. *) 587 680  false ⇒ λCS. … … 589 682 replace_sub_trace … r 590 683 (tal_step_default (RTLabs_status ge) (ends … r) 591 start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) 684 start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost … CS)) ? 592 685 ] (refl ??) 593 686 594 687  cl_jump ⇒ λCL. 595 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?688 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? 596 689 doesnt_end_with_ret 597 (mk_trace_result ge ??? next trace' ?598 (tal_base_not_return (RTLabs_status ge) start next ???) ? )690 (mk_trace_result ge ????? next trace' ? 691 (tal_base_not_return (RTLabs_status ge) start next ???) ??) 599 692 600 693  cl_call ⇒ λCL. 601 694 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … TERMINATES) TIME ? in 602 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with695 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 603 696 (* We're about to run into a label, use base case for call *) 604 697 [ true ⇒ λCS. 605 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?698 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? 606 699 doesnt_end_with_ret 607 700 (replace_trace … r 608 701 (tal_base_call (RTLabs_status ge) start next (new_state … r) 609 ? CL ? (new_trace … r) CS) )702 ? CL ? (new_trace … r) CS) ?) 610 703 (* otherwise use step case *) 611 704  false ⇒ λCS. … … 616 709 (tal_step_call (RTLabs_status ge) (ends … r') 617 710 start next (new_state … r) (new_state … r') ? CL ? 618 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) 711 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ? 619 712 ] (refl ??) 620 713 621 714  cl_return ⇒ λCL. 622 mk_sub_trace_result ge depth (λends. trace_any_label (RTLabs_status ge) ends start) ?715 mk_sub_trace_result ge depth start (λends. trace_any_label (RTLabs_status ge) ends start) ? 623 716 ends_with_ret 624 (mk_trace_result ge ??? 717 (mk_trace_result ge ????? 625 718 next 626 719 trace' 627 720 ? 628 721 (tal_base_return (RTLabs_status ge) start next ? CL) 722 ? 629 723 ?) 630 724 ] (refl ? (RTLabs_classify start)) … … 637 731 [ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ] 638 732  // 639  cases r #H1 #H2 #H3 #H4 * #x @le_S_to_le 733  cases r #H1 #H2 #H3 #H4 #H5 * #H6 @le_S_to_le 734  @(stack_preserved_join … (stack_ok … r)) // 640 735  @(trace_label_label_label … (new_trace … r)) 641  cases r #H1 #H2 #H3 #H4 * #H5 #H6736  cases r #H1 #H2 #H3 #H4 #H5 * #H6 #LT 642 737 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) 643 738 @(transitive_le … (3*(will_return_length … TERMINATES))) 644 739 [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times 645 @(monotonic_le_times_r 3 … H6)740 @(monotonic_le_times_r 3 … LT) 646 741  @le_S @le_S @le_n 647 742 ] … … 654 749 this can't happen *) 655 750  @(will_return_return … CL TERMINATES) 751  /2/ 656 752  %{tr} @EV 657 753  @(well_cost_labelled_state_step … EV) // 658 754  whd @(will_return_notfn … TERMINATES) %2 @CL 755  @stack_preserved_step /2/ 659 756  %{tr} @EV 660 757  %1 whd @CL 661 758  @(well_cost_labelled_jump … EV) // 662 759  @(well_cost_labelled_state_step … EV) // 760  @sp_over_return 663 761  %{tr} @EV 664  (* TODO oh dear *)762  (* TODO oh dear *) 665 763  cases (will_return_call … TERMINATES) #H @le_S_to_le 666 764  cases r #H1 #H2 #H3 #H4 * #H5 
src/RTLabs/semantics.ma
r1680 r1681 245 245  normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m') 246 246  to_call : ∀ge,f,fs,m,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst (f'::fs) m) 247 (* 247 248  tail_call : ∀ge,f,fs,m,fd,args,dst,m'. ∀b. find_funct_ptr ?? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate fd args dst fs m') 249 *) 248 250  from_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m') 249 251  to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m') … … 301 303  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % % 302 304  #r #ls #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 ] 303  #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 % 5305  #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 %4 304 306 ] 305 307  * #fn #args #retdst #stk #m #tr #s' 306 308 whd in ⊢ (??%? → ?); 307 309 [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); 308 #E destruct % 4310 #E destruct %3 309 311  @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct 310 312 ] … … 312 314 whd in ⊢ (??%? → ?); 313 315 [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct 314 % 6cases f #func #locals #next #next_ok #sp #retdst %316 %5 cases f #func #locals #next #next_ok #sp #retdst % 315 317  #E destruct 316 318 ]
Note: See TracChangeset
for help on using the changeset viewer.