Changeset 1681


Ignore:
Timestamp:
Feb 9, 2012, 1:22:32 PM (6 years ago)
Author:
campbell
Message:

Checkpoint of stack preservation work in RTLabs.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r1675 r1681  
    347347[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
    348348| #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(*
    349350| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
     351*)
    350352| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
    351353| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
     
    442444] qed.
    443445
     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. *)
     450inductive 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
     460lemma 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 //
     464qed.
     465
     466lemma 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
     496lemma 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
     512lemma 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
     526lemma 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
     532cases (rtlabs_call_inv … CL)
     533#fd * #args * #dst * #stk * #m #E destruct
     534
    444535(* Don't need to know that labels break loops because we have termination. *)
    445536
     
    447538   termination.  Note that we keep a proof that our upper bound on the length
    448539   of the termination proof is respected. *)
    449 record trace_result (ge:genv) (depth:nat) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
     540record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) (start:state) (T:state → Type[0]) (limit:nat) : Type[0] ≝ {
    450541  new_state : state;
    451542  remainder : flat_trace io_out io_in ge new_state;
    452543  cost_labelled : well_cost_labelled_state new_state;
    453544  new_trace : T new_state;
     545  stack_ok : stack_preserved ends start new_state;
    454546  terminates : match depth with
    455547               [ O ⇒ True
     
    460552(* The same with a flag indicating whether the function returned, as opposed to
    461553   encountering a label. *)
    462 record sub_trace_result (ge:genv) (depth:nat) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
     554record sub_trace_result (ge:genv) (depth:nat) (start:state) (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝ {
    463555  ends : trace_ends_with_ret;
    464   trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) (T ends) limit
     556  trace_res :> trace_result ge (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth]) ends start (T ends) limit
    465557}.
    466558
     
    469561   the size of the termination proof might need to be relaxed, too. *)
    470562
    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 d T2 l2 ≝
    473 λge,d,T1,T2,l1,l2,lGE,r,trace.
    474   mk_trace_result ge d T2 l2
     563definition 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
    475567    (new_state … r)
    476568    (remainder … r)
    477569    (cost_labelled … r)
    478570    trace
     571    SP
    479572    (match d return λd'.match d' with [ O ⇒ True | S d'' ⇒ ΣTM.l1 > will_return_length ge d'' (new_state … r) (remainder … r) TM] →
    480573                        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))
    482575. @(transitive_le … lGE) @(pi2 … TM) qed.
    483576
    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 d T2 l2 ≝
    486 λge,d,T1,T2,l1,l2,lGE,r,trace.
    487   mk_sub_trace_result ge d T2 l2
     577definition 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
    488581    (ends … r)
    489     (replace_trace … lGE … r trace).
     582    (replace_trace … lGE … r trace SP).
    490583
    491584(* Small syntax hack to avoid ambiguous input problems. *)
     
    500593  (TIME: nat)
    501594  (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
    503596              (trace_label_return (RTLabs_status ge) s)
    504597              (will_return_length … TERMINATES) ≝
     
    515608            TERMINATES
    516609            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) with
     610  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
    518611  [ 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)
    520613  | doesnt_end_with_ret ⇒ λr.
    521614      let r' ≝ make_label_return ge depth (new_state … r)
     
    526619        replace_trace … r'
    527620          (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')) ?
    529622  ] (trace_res … r)
    530623
     
    540633  (TIME: nat)
    541634  (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
    543636              (λends. trace_label_label (RTLabs_status ge) ends s)
    544637              (will_return_length … TERMINATES) ≝
     
    550643let r ≝ make_any_label ge depth s trace ENV_COSTLABELLED STATE_COSTLABELLED TERMINATES TIME ? in
    551644  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)
    553646
    554647] TERMINATES_IN_TIME
     
    562655  (TIME: nat)
    563656  (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
    565658              (λends. trace_any_label (RTLabs_status ge) ends s)
    566659              (will_return_length … TERMINATES) ≝
     
    570663| S TIME ⇒ λTERMINATES_IN_TIME.
    571664
    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) with
     665  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
    573666  [ ft_stop st FINAL ⇒
    574667      λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ?
    575668
    576669  | 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) with
     670    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
    578671    [ 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) with
     672        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
    580673        (* We're about to run into a label. *)
    581674        [ 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) ?
    583676              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) ??)
    586679        (* An ordinary step, keep going. *)
    587680        | false ⇒ λCS.
     
    589682                replace_sub_trace … r
    590683                  (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)) ?
    592685        ] (refl ??)
    593686       
    594687    | 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) ?
    596689          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 ???) ??)
    599692           
    600693    | cl_call ⇒ λCL.
    601694        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) with
     695        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
    603696        (* We're about to run into a label, use base case for call *)
    604697        [ 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) ?
    606699            doesnt_end_with_ret
    607700            (replace_trace … r
    608701              (tal_base_call (RTLabs_status ge) start next (new_state … r)
    609                 ? CL ? (new_trace … r) CS))
     702                ? CL ? (new_trace … r) CS) ?)
    610703        (* otherwise use step case *)
    611704        | false ⇒ λCS.
     
    616709              (tal_step_call (RTLabs_status ge) (ends … r')
    617710                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')) ?
    619712        ] (refl ??)
    620713
    621714    | 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) ?
    623716          ends_with_ret
    624           (mk_trace_result ge ???
     717          (mk_trace_result ge ?????
    625718            next
    626719            trace'
    627720            ?
    628721            (tal_base_return (RTLabs_status ge) start next ? CL)
     722            ?
    629723            ?)
    630724    ] (refl ? (RTLabs_classify start))
     
    637731[ cases (not_le_Sn_O ?) [ #H @H @TERMINATES_IN_TIME ]
    638732| //
    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)) //
    640735| @(trace_label_label_label … (new_trace … r))
    641 | cases r #H1 #H2 #H3 #H4 * #H5 #H6
     736| cases r #H1 #H2 #H3 #H4 #H5 * #H6 #LT
    642737  @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME)
    643738  @(transitive_le …  (3*(will_return_length … TERMINATES)))
    644739  [ >commutative_times change with ((S ?) * 3 ≤ ?) >commutative_times
    645     @(monotonic_le_times_r 3 … H6)
     740    @(monotonic_le_times_r 3 … LT)
    646741  | @le_S @le_S @le_n
    647742  ]
     
    654749     this can't happen *)
    655750| @(will_return_return … CL TERMINATES)
     751| /2/
    656752| %{tr} @EV
    657753| @(well_cost_labelled_state_step  … EV) //
    658754| whd @(will_return_notfn … TERMINATES) %2 @CL
     755| @stack_preserved_step /2/
    659756| %{tr} @EV
    660757| %1 whd @CL
    661758| @(well_cost_labelled_jump … EV) //
    662759| @(well_cost_labelled_state_step  … EV) //
     760| @sp_over_return
    663761| %{tr} @EV
    664 | (* TODO oh dear *)
     762|  (* TODO oh dear *)
    665763| cases (will_return_call … TERMINATES) #H @le_S_to_le
    666764| cases r #H1 #H2 #H3 #H4 * #H5
  • src/RTLabs/semantics.ma

    r1680 r1681  
    245245| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
    246246| 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(*
    247248| 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*)
    248250| 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')
    249251| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
     
    301303  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct % %
    302304  | #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 %5
     305  | #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
    304306  ]
    305307| * #fn #args #retdst #stk #m #tr #s'
    306308  whd in ⊢ (??%? → ?);
    307309  [ @bind_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?);
    308     #E destruct %4
     310    #E destruct %3
    309311  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
    310312  ]
     
    312314  whd in ⊢ (??%? → ?);
    313315  [ @bind_value #loc #Eloc #E whd in E:(??%?); destruct
    314     %6 cases f #func #locals #next #next_ok #sp #retdst %
     316    %5 cases f #func #locals #next #next_ok #sp #retdst %
    315317  | #E destruct
    316318  ]
Note: See TracChangeset for help on using the changeset viewer.