Changeset 2677 for src/RTLabs


Ignore:
Timestamp:
Feb 19, 2013, 12:23:50 PM (7 years ago)
Author:
campbell
Message:

Retain the pointer for the function called in front-end call states
so that we can do sensible stack costs.

Location:
src/RTLabs
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/RTLabs_abstract.ma

    r2601 r2677  
    3535  match state with
    3636  [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack
    37   | Callstate fd _ _ fs _ ⇒
     37  | Callstate _ fd _ _ fs _ ⇒
    3838      match fn_stack with
    3939      [ nil ⇒ False
     
    5858  eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_ext_state ge ≝
    5959λge,s,s',t,EX. mk_RTLabs_ext_state ge s'
    60  (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
     60 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s | Callstate _ _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s | Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s) | Finalstate _ ⇒ λ_. [ ] ] EX)
    6161 ?.
    6262cases s' in EX ⊢ %;
     
    6767    | @M2 ]
    6868  | #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct
    69   | #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
     69  | #ge' #vf #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct
    7070    whd cases stk in mtc ⊢ %; [ * ]
    7171    #hd #tl #H @H
     
    7676  | #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct
    7777  ]
    78 | -s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
     78| -s' #vf #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP
    7979  whd % // -func_block cases s in EX ⊢ %; -s #s #stk #mtc #EX inversion (eval_preserves … EX)
    8080  [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct
    81   | #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
     81  | #ge' #vf1 #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct
    8282    cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %
    8383    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     
    111111    | _ ⇒ cl_other
    112112    ]
    113 | Callstate _ _ _ _ _ ⇒ cl_call
     113| Callstate _ _ _ _ _ _ ⇒ cl_call
    114114| Returnstate _ _ _ _ ⇒ cl_return
    115115| Finalstate _ ⇒ cl_other
     
    179179match s' return λs'. Ras_Fn_Match ? s' ? → ? with
    180180[ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_state b (next … f) ]
    181 | Callstate _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
     181| Callstate _ _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  | cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ? | cons f _ ⇒ Some ? (next f) ]) b ]
    182182| Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?) | cons b _ ⇒ λ_. rapc_ret (Some ? b) ]
    183183| Finalstate _ ⇒ λmtc. rapc_fin
     
    206206  [ mk_Sig s p ⇒
    207207    match s return λs. Some ? (RTLabs_classify s) = Some ? cl_call → ? with
    208     [ Callstate fd args dst stk m ⇒
     208    [ Callstate _ fd args dst stk m ⇒
    209209      λ_. match s' with
    210210      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
     
    233233    [ mk_RTLabs_ext_state s' stk mtc0 ⇒
    234234      match s' return λs'. Ras_Fn_Match ? s' ? → Some ? (RTLabs_classify s') = Some ? cl_call → ident with
    235       [ Callstate fd _ _ _ _ ⇒
     235      [ Callstate _ fd _ _ _ _ ⇒
    236236        match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with
    237237        [ nil ⇒ λmtc. ⊥
     
    304304  try (% #E' destruct)
    305305  cases (NONE ?) assumption
    306 | #fd #args #dst #fs #m #stk #mtc %
     306| #vf #fd #args #dst #fs #m #stk #mtc %
    307307  [ #E normalize in E; destruct
    308308  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
  • src/RTLabs/RTLabs_semantics.ma

    r2645 r2677  
    3030   state
    3131| Callstate :
     32   ∀  vf : val. (* fn pointer; only used for instrumentation, not the semantics *)
    3233   ∀  fd : fundef internal_function.
    3334   ∀args : list val.
     
    109110      ! fd ← opt_to_res … [MSG BadFunction; CTX ? id] (find_funct_ptr … ge b);
    110111      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    111       return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     112      return 〈E0, Callstate (Vptr (mk_pointer b zero_offset)) fd vs dst (adv l f ?::fs) m〉
    112113  | St_call_ptr frs args dst l ⇒ λH.
    113114      ! fv ← reg_retrieve (locals f) frs;
    114115      ! fd ← opt_to_res … (msg BadFunction) (find_funct … ge fv);
    115116      ! vs ← m_list_map … (reg_retrieve (locals f)) args;
    116       return 〈E0, Callstate fd vs dst (adv l f ?::fs) m〉
     117      return 〈E0, Callstate fv fd vs dst (adv l f ?::fs) m〉
    117118(*
    118119  | St_tailcall_id id args ⇒ λH.
     
    153154      return 〈E0, Returnstate v (retdst f) fs (free m (sp f))〉
    154155  ] (f_closed (func f) (next f) s ?)
    155 | Callstate fd params dst fs m ⇒
     156| Callstate _ fd params dst fs m ⇒
    156157    match fd return λ_. IO ??? with
    157158    [ Internal fn ⇒
     
    213214  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main);
    214215  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b);
    215   OK ? (Callstate f (nil ?) (None ?) (nil ?) m).
     216  OK ? (Callstate (Vptr (mk_pointer b zero_offset)) f (nil ?) (None ?) (nil ?) m).
    216217
    217218definition RTLabs_fullexec : fullexec io_out io_in ≝
     
    232233inductive state_rel : genv → state → state → Prop ≝
    233234| normal : ∀ge,f,f',fs,m,m'. frame_rel f f' → state_rel ge (State f fs m) (State f' fs m')
    234 | 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)
     235| to_call : ∀ge,f,fs,m,vf,fd,args,f',dst. frame_rel f f' → ∀b. find_funct_ptr ? ge b = Some ? fd → state_rel ge (State f fs m) (Callstate vf fd args dst (f'::fs) m)
    235236(*
    236237| 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')
    237238*)
    238 | 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')
     239| from_call : ∀ge,vf,fn,locals,next,nok,sp,fs,m,args,dst,m'. state_rel ge (Callstate vf (Internal ? fn) args dst fs m) (State (mk_frame fn locals next nok sp dst) fs m')
    239240| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
    240241| from_ret : ∀ge,f,fs,rtv,dst,f',m. next f = next f' → frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
     
    276277  | #LP whd in ⊢ (??%? → ?); @bind_res_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
    277278  ]
    278 | * #fn #args #retdst #stk #m #tr #s'
     279| #vf * #fn #args #retdst #stk #m #tr #s'
    279280  whd in ⊢ (??%? → ?);
    280281  [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?);
     
    293294(* Show that, in principle at least, we can calculate which function we called
    294295   on a transition. The proof is a functional inversion similar to eval_preserves,
    295    above. *)
    296 
    297 definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m.
    298   eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 →
     296   above.  Note: this was originally done before the value was added to
     297   Callstate. *)
     298
     299(* Hack due to lack of discriminator for large inductive types *)
     300lemma jmeq_hackT : ∀T:Type[0]. ∀x,y:T. ∀P:Type[0].
     301  (x ≃ y → P) →
     302  (x = y → P).
     303/2/
     304qed.
     305
     306definition func_block_of_exec : ∀ge,s,t,vf,fd,args,dst,fs,m.
     307  eval_statement ge s = Value ??? 〈t,Callstate vf fd args dst fs m〉 →
    299308  Σb:block. find_funct_ptr … ge b = Some ? fd.
    300309#ge *
    301 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m'
     310[ * #func #locals #next #nok #sp #dst #fs #m #tr #vf #fd #args #dst' #fs' #m'
    302311  whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?);
    303312  cases (next_instruction ?)
    304313  (* Function call cases. *)
    305   [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
     314  [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs @jmeq_hackT #E normalize in E; destruct
    306315    [ %{v} @Efd
    307     | cases v in Efd;
     316    | cases vf in Efd;
    308317      [ 4: * #b #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd;
    309318           [ #E @E | #E normalize in E; destruct ]
     
    313322  (* and everything else cannot occur, but we need to work through the
    314323     definition to find the resulting state to demonstrate that. *)
    315   | #l #LP whd in ⊢ (??%? → ?); #E destruct
    316   | #c #l #LP whd in ⊢ (??%? → ?); #E destruct
    317   | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct
    318   | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    319   | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    320   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    321   | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc #E whd in E:(??%?); destruct
    322   | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct
     324  | #l #LP whd in ⊢ (??%? → ?); @jmeq_hackT #E destruct
     325  | #c #l #LP whd in ⊢ (??%? → ?); @jmeq_hackT #E destruct
     326  | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
     327  | #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
     328  | #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
     329  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
     330  | #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev'  @bind_ok #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
     331  | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb @jmeq_hackT #E whd in E:(??%??); destruct
    323332(*  | #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_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 ] | *: [1,3: #vl] #E whd in E:(??%?); destruct ]*)
    324   | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct
    325   ]
    326 | * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m'
     333  | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); @jmeq_hackT #E' whd in E':(??%??); destruct
     334  ]
     335| #vf * #fn #args #retdst #stk #m #tr #vf' #fd' #args' #dst' #fs' #m'
    327336  whd in ⊢ (??%? → ?);
    328337  [ @bind_res_value #loc #Eloc cases (alloc m O ?(*?*)) #m' #b whd in ⊢ (??%? → ?);
    329     #E destruct
     338    @jmeq_hackT #E destruct
    330339  | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct
    331340  ]
    332 | #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m'
    333   whd in ⊢ (??%? → ?);
    334   [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct
    335   | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct | *: normalize #a try #b destruct ] ]
    336   ]
    337 | #r #tr #fd' #args' #dst' #fs' #m'
     341| #v #r * [2: #f #fs ] #m #tr #vf' #fd' #args' #dst' #fs' #m'
     342  whd in ⊢ (??%? → ?);
     343  [ @bind_res_value #loc #Eloc @jmeq_hackT #E whd in E:(??%??); destruct
     344  | cases v [ normalize #E destruct | * [ 2: * #r normalize @jmeq_hackT #E destruct | *: normalize #a try #b destruct ] ]
     345  ]
     346| #r #tr #vf' #fd' #args' #dst' #fs' #m'
    338347  normalize #E destruct
    339348] qed.
     
    344353#ge *
    345354[ #f #fs #m * #F cases (F ?) @refl
    346 | #a #b #c #d #e * #F cases (F ?) @refl
     355| #a #b #c #d #e #f * #F cases (F ?) @refl
    347356| #a #b #c #d * #F cases (F ?) @refl
    348357| #r #F % [2: @refl | skip ]
  • src/RTLabs/RTLabs_traces.ma

    r2608 r2677  
    2626  try (% #E' destruct)
    2727  cases (NONE ?) assumption
    28 | #fd #args #dst #fs #m #stk #mtc %
     28| #vf #fd #args #dst #fs #m #stk #mtc %
    2929  [ #E normalize in E; destruct
    3030  | whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??);
     
    437437λs. match s with
    438438[ State f fs m ⇒ well_cost_labelled_fn (func f) ∧ All ? (λf. well_cost_labelled_fn (func f)) fs
    439 | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
     439| Callstate _ fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ well_cost_labelled_fn fn | External _ ⇒ True ] ∧
    440440                          All ? (λf. well_cost_labelled_fn (func f)) fs
    441441| Returnstate _ _ fs _ ⇒ All ? (λf. well_cost_labelled_fn (func f)) fs
     
    450450#ge #s #tr' #s' #EV cases (eval_preserves … EV)
    451451[ #ge #f #f' #fs #m #m' * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #Hge * #H1 #H2 % //
    452 | #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/
     452| #ge #f #fs #m #vf * #fn #args #f' #dst * #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #b #Hfn #Hge * #H1 #H2 % /2/
    453453(*
    454454| #ge #f #fs #m * #fn #args #f' #dst #m' #b #Hge * #H1 #H2 % /2/
    455455*)
    456 | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
     456| #ge #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
    457457| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
    458458| #ge #f #fs #rtv #dst #f' #m #N * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
     
    474474    ]*)
    475475  ]
    476 | normalize #H1 #H2 #H3 #H4 #H5 #H6 destruct
     476| normalize #H1 #H2 #H3 #H4 #H5 #H6 #H7 destruct
    477477| normalize #H8 #H9 #H10 #H11 #H12 destruct
    478478| #r #E normalize in E; destruct
     
    520520lemma rtlabs_call_inv : ∀s.
    521521  RTLabs_classify s = cl_call →
    522   ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m.
     522  ∃vf,fd,args,dst,stk,m. s = Callstate vf fd args dst stk m.
    523523* [ #f #fs #m whd in ⊢ (??%? → ?);
    524524    cases (next_instruction f) normalize
    525525    try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct
    526   | #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl
     526  | #vf #fd #args #dst #stk #m #E %{vf} %{fd} %{args} %{dst} %{stk} %{m} @refl
    527527  | normalize #H411 #H412 #H413 #H414 #H415 destruct
    528528  | normalize #H1 #H2 destruct
     
    536536#ge #s #tr #s' #EV #WCL #CL
    537537cases (rtlabs_call_inv s CL)
    538 #fd * #args * #dst * #stk * #m #E >E in EV WCL;
     538#vf * #fd * #args * #dst * #stk * #m #E >E in EV WCL;
    539539whd in ⊢ (??%? → % → ?);
    540540cases fd
     
    555555inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝
    556556| xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (State f' fs m') S M')
    557 | xto_call : ∀ge,f,fs,m,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (Callstate fd args dst (f'::fs) m) (fn::S) M')
    558 | xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate (Internal ? fn) args dst fs m) S M) (mk_RTLabs_ext_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
     557| xto_call : ∀ge,f,fs,m,vf,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (Callstate vf fd args dst (f'::fs) m) (fn::S) M')
     558| xfrom_call : ∀ge,vf,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate vf (Internal ? fn) args dst fs m) S M) (mk_RTLabs_ext_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
    559559| xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m') S M')
    560560| xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_ext_state ge (State f' fs m) S M')
     
    573573  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
    574574  %1 //
    575 | #ge #f #fs #m #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
     575| #ge #f #fs #m #vf #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
    576576  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
    577577  %2 //
    578 | #ge #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
     578| #ge #vf #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
    579579  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
    580580  %3
     
    605605inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝
    606606| sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M)
    607 | sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M)
     607| sos_Callstate : ∀vf,fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate vf fd args dst (f::fs) m) (fn::fn'::S) M)
    608608| sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m) S M)
    609609.
     
    622622    stack_of_state ge [ ] [ ] s1 →
    623623    stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M)
    624 | sp_top : ∀fd,args,dst,m,r,fn,M1,M2.
    625     stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2)
     624| sp_top : ∀vf,fd,args,dst,m,r,fn,M1,M2.
     625    stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate vf fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2)
    626626.
    627627
     
    634634#ge #fs0 #fs0' #S0 #S0' #s0 *
    635635[ #f #fs #m #fn #S #M #H inversion H
    636   #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
    637 | #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
    638   #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #m try #o destruct /2/
     636  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o try #p destruct /2/
     637| #vf #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
     638  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #m try #o try #p destruct /2/
    639639| #rtv #dst #fs #m #S #M #H inversion H
    640   #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
     640  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o try #p destruct /2/
    641641] qed.
    642642
     
    645645#ge #e #r #S #M #s % #H inversion H
    646646[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
    647   inversion SOS #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l try #m destruct
     647  inversion SOS #a #b #c #d try #e try #f try #g try #h try #i try #j try #k try #l try #m try #o destruct
    648648| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #HX #HY #HZ #SOS #H201 #H202 #H203 #H204 destruct
    649   inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m destruct
     649  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m try #p destruct
    650650| #s' #r' #M' #SOS #E1 #E2 #E3 #E4 destruct
    651   inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o destruct
     651  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o try #p destruct
    652652| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
    653653] qed.
     
    665665    @(sp_finished … fn … N) cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
    666666  | #s1'' #r #M #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop cases (stack_of_state_eq … S1'' S2) #E1 #E2 destruct //
    667   | #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct
     667  | #vf #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct
    668668    inversion S2
    669669    [ #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
    670     | #fd' #args' #dst' #f #fs' #m' #fn' #fn'' #S' #M' #E1 #E2 #E3 destruct
     670    | #vf' #fd' #args' #dst' #f #fs' #m' #fn' #fn'' #S' #M' #E1 #E2 #E3 destruct
    671671    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct
    672672    ]
     
    674674| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
    675675| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
    676 | #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct #F @⊥
     676| #vf #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct #F @⊥
    677677  @(absurd … F) //
    678678] qed.
     
    695695[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
    696696  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
    697 | #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
     697| #ge #f #fs #m #vf #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
    698698  whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/
    699 | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
     699| #ge #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
    700700  * #s3 #S3 #M3 #SP inversion SP
    701701  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 destruct
     
    708708    ]
    709709  | #sx #r #M3 #SOS #E1 #E2 #E3 #E4 destruct
    710     cut (∃fn. fs = [ ] ∧ S = [fn]) [ inversion SOS #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 try #H105 try #H106 try #H107 destruct /3/ ]
     710    cut (∃fn. fs = [ ] ∧ S = [fn]) [ inversion SOS #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 try #H105 try #H106 try #H107 try #H108 destruct /3/ ]
    711711    * #fn * #E1 #E2 destruct
    712712    @sp_top
     
    734734  as_after_return (RTLabs_status ge) «s1,lift_classify … CL» s3.
    735735#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
    736 cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
     736cases (rtlabs_call_inv … CL) #vf * #fn * #args * #dst * #stk * #m #E destruct
    737737whd
    738738inversion S23
     
    740740| #s2' #f #f' #fs #m' #fn' #S #M #N #F #S #E1 #E2 #E3 #E4 destruct whd
    741741  inversion (eval_preserves_ext … EV)
    742   [ 3: #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
     742  [ 3: #gex #vfx #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
    743743    inversion S
    744744    [ #fy #fsy #my #fn #S0 #M0 #E1 #E2 #E3 #E4 destruct whd % [ % [ @N | inversion F // ] | whd % ]
    745     | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 destruct
     745    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 destruct
    746746    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 destruct
    747747    ]
    748   | *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 destruct
     748  | *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 try #H200 try #H201 destruct
    749749  ]
    750750| #s1 #r #M #S1 #E1 #E2 #E3 #E4 destruct whd
    751751  inversion (eval_preserves_ext … EV)
    752   [ 3: #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
     752  [ 3: #ge' #vf' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
    753753    inversion S1
    754754    [ #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 destruct //
    755     | *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 destruct
    756     ]
    757   | *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206  try #H195 try #H196 try #H197 try #H198 try #H199 destruct
    758   ]
    759 | #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
     755    | *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 try #H123 destruct
     756    ]
     757  | *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206  try #H195 try #H196 try #H197 try #H198 try #H199 try #H200 try #H201 destruct
     758  ]
     759| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
    760760] qed.
    761761
     
    11211121λs. match s with
    11221122[ State f fs m ⇒ Some ? (next f)
    1123 | Callstate _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
     1123| Callstate _ _ _ _ fs _ ⇒ match fs with [ cons f _ ⇒ Some ? (next f) | _ ⇒ None ? ]
    11241124| Returnstate _ _ _ _ ⇒ None ?
    11251125| Finalstate _ ⇒ None ?
     
    12281228inductive state_bound_on_steps_to_cost : state → nat → Prop ≝
    12291229| sbostc_state : ∀f,fs,m,n. frame_bound_on_steps_to_cost1 f n → state_bound_on_steps_to_cost (State f fs m) n
    1230 | sbostc_call : ∀fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate fd args dst (f::fs) m) (S n)
     1230| sbostc_call : ∀vf,fd,args,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Callstate vf fd args dst (f::fs) m) (S n)
    12311231| sbostc_ret : ∀rtv,dst,f,fs,m,n. frame_bound_on_steps_to_cost f n → state_bound_on_steps_to_cost (Returnstate rtv dst (f::fs) m) (S n)
    12321232.
     
    12451245  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    12461246  steps_for_statement (next_instruction f) =
    1247   match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
     1247  match s' with [ State _ _ _ ⇒ 1 | Callstate _ _ _ _ _ _ ⇒ 2 | Returnstate _ _ _ _ ⇒ 2 | Finalstate _ ⇒ 1 ].
    12481248#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
    12491249whd in ⊢ (??%? → ?);
     
    12781278#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); lapply CL -CL inversion H
    12791279[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
    1280   #fn * #args * #dst * #stk * #m' #E destruct
    1281 | #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
     1280  #vf * #fn * #args * #dst * #stk * #m' @jmeq_hackT #E destruct
     1281| #vf #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
    12821282  whd in S; #CL cases s'
    12831283  [ #f' #fs' #m' * * #N #F #STK #CS
     
    12881288    | #l #n #H #CS' #B #E1 #E2 #_ destruct <N <F @B
    12891289    ]
    1290   | #fd' #args' #dst' #fs' #m' *
     1290  | #vf' #fd' #args' #dst' #fs' #m' *
    12911291  | #rv #dst' #fs' #m' *
    12921292  | #r #E normalize in E; destruct
     
    13201320      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 destruct @H75
    13211321      ]
    1322     | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
     1322    | #ge0 #f0 #fs' #m0 #vf #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
    13231323      >(eval_steps … EVAL) in E2; #En normalize in En;
    13241324      inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct
     
    13631363λs. match s with
    13641364[ State f fs m ⇒ soundly_labelled_fn (func f) ∧ All ? (λf. soundly_labelled_fn (func f)) fs
    1365 | Callstate fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
    1366                           All ? (λf. soundly_labelled_fn (func f)) fs
     1365| Callstate _ fd _ _ fs _ ⇒ match fd with [ Internal fn ⇒ soundly_labelled_fn fn | External _ ⇒ True ] ∧
     1366                            All ? (λf. soundly_labelled_fn (func f)) fs
    13671367| Returnstate _ _ fs _ ⇒ All ? (λf. soundly_labelled_fn (func f)) fs
    13681368| Finalstate _ ⇒ True
     
    13731373  soundly_labelled_state s →
    13741374  ∃n. state_bound_on_steps_to_cost s n.
    1375 * [ #f #fs #m #CS | #a #b #c #d #e #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
     1375* [ #f #fs #m #CS | #a #b #c #d #e #f #E normalize in E; destruct | #a #b #c #d #E normalize in E; destruct | #a #E normalize in E; destruct ]
    13761376whd in ⊢ (% → ?); * #SLF #_
    13771377cases (SLF (next f) (next_ok f)) #n #B1
     
    13881388[ #ge' #f #f' #fs #m #m' #F #E1 #E2 #E3 #_ destruct
    13891389  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
    1390 | #ge' #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
     1390| #ge' #f #fs #m #vf #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #_ destruct
    13911391  whd in S ⊢ %; %
    13921392  [ cases fd in FFP ⊢ %; // #fn #FFP @ENV //
    13931393  | inversion F #H30 #H31 #H32 #H33 #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 destruct @S
    13941394  ]
    1395 | #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
     1395| #ge' #vf #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
    13961396  whd in S ⊢ %; @S
    13971397| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
     
    14141414    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
    14151415    destruct @S
    1416   | #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S
     1416  | #vf #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S
    14171417    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
    14181418    destruct @S
     
    15771577      | #s1 #f #f' #fs #m #fn #S #M #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
    15781578      | #s1 #r #M #S #E1 #E2 #E3 #E4 change with (next_state ?????) in E2:(??%??); -TERMINATES destruct -next' -s0
    1579         cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
     1579        cases (rtlabs_call_inv … CL) #vf * #fd * #args * #dst * #stk * #m #E destruct
    15801580        inversion (eval_preserves … EV)
    1581         [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 @⊥ -next destruct ]
    1582         #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
     1581        [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 try #H124 @⊥ -next destruct ]
     1582        #ge' #vf' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
    15831583        inversion S
    1584         [ #f #fs0 #m #fn0 #S0 #M0 #E1 #E2 whd in ⊢ (??%?% → ?); generalize in ⊢ (??(????%)?? → ?); #M'' #E3 #_ destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H1 #H2 #H3 try #H130 try #H4 try #H5 [ whd in H5:(??%?%); | whd in H2:(??%?%); ] destruct ]
     1584        [ #f #fs0 #m #fn0 #S0 #M0 #E1 #E2 whd in ⊢ (??%?% → ?); generalize in ⊢ (??(????%)?? → ?); #M'' #E3 #_ destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 #H1 #H2 #H3 try #H130 try #H4 try #H5 try #H6 [ whd in H6:(??%?%); | whd in H2:(??%?%); ] destruct ]
    15851585        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
    15861586           so we can use it as a witness that at least one frame exists *)
    15871587        inversion LABEL_LIMIT
    1588         #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 destruct
    1589       | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 destruct
     1588        #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 try #H150 try #H151 destruct
     1589      | #H173 #H174 #H175 #H176 #H177 #H178 #H179 #H180 #H181 #H182 destruct
    15901590      ]
    15911591    ]
     
    17091709#E destruct
    17101710#SP inversion (eval_preserves_ext … EV)
    1711 [ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct
     1711[ 3: #ge' #vf #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct
    17121712     inversion SP
    17131713     [ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct
    17141714     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 try #H41 destruct @⊥
    1715           inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 destruct
     1715          inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 try #H75 destruct
    17161716     ]
    1717 | *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 destruct
     1717| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 try #H113 destruct
    17181718] qed.
    17191719
     
    17671767| ft_stop st FINAL ⇒ λmtc,INITIAL. ⊥
    17681768] mtc0 ].
    1769 [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct
     1769[ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #vf * #fn * #args * #dst * #stk * #m #E destruct
    17701770  cases FINAL #E @E @refl
    17711771| %{tr} %{EV} %
     
    17851785lemma init_state_is : ∀p,s.
    17861786  make_initial_state p = OK ? s →
    1787   𝚺b. match s with [ Callstate fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
     1787  𝚺b. match s with [ Callstate _ fd _ _ fs _ ⇒ fs = [ ] ∧ find_funct_ptr ? (make_global p) b = Some ? fd
    17881788   | _ ⇒ False ].
    17891789#p #s
     
    18011801cases s
    18021802[ #f #fs #m *
    1803 | #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
     1803| #vf #fd #args #dst #fs #m * #E1 #E2 destruct whd % //
    18041804| #rv #rr #fs #m *
    18051805| #r *
     
    21022102λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
    21032103  match Ras_state … s with
    2104   [ Callstate _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
     2104  [ Callstate _ _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
    21052105  | _ ⇒  Some ? h ] ].
    21062106
     
    21212121  cases (next_instruction f) normalize
    21222122  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
    2123 | #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
     2123| #vf #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
    21242124| #ret #dst #fs #m * [ | #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
    21252125| #r #S #M #s' * #tr * #EX normalize in EX; destruct
     
    21472147  RTLabs_classify s = cl →
    21482148  match cl with
    2149   [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate fd args dst fs m) S M
     2149  [ cl_call ⇒ ∃vf,fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate vf fd args dst fs m) S M
    21502150  | cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M
    21512151  | _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M
    21522152  ] .
    2153 #ge #cl * * [ #f #fs #m | #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
     2153#ge #cl * * [ #f #fs #m | #vf #fd #args #dst #fs #m | #ret #dst #fs #m | #r ]
    21542154#S #M * #s' #S' #M' #EX #CL
    21552155whd in CL:(??%?);
     
    21582158    normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ]
    21592159  * #E >E %{f} %{fs} %{m} %{S} %{M} %
    2160 | <CL %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
     2160| <CL %{vf} %{fd} %{args} %{dst} %{fs} %{m} %{S} %{M} %
    21612161| <CL %{ret} %{dst} %{fs} %{m} %{S} %{M} %
    21622162| @⊥ cases EX #tr * #EV #_ normalize in EV; destruct
     
    22572257inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV))
    22582258[ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
    2259 | #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
     2259| #ge' #f' #f'' #m' #vf #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct %
    22602260| #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 #H18 destruct
    22612261| #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
     
    22792279    cases (next_instruction f) in CL;
    22802280    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
    2281   | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
     2281  | #vf #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
    22822282  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
    22832283  | #r #S #M #CL normalize in CL; destruct
     
    22862286* [ #postf #postfs #postm * [*] #fn' #S' #M'
    22872287  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
    2288   | 2,6: #A #B #C #D #E #F #G *
     2288  | 2,6: #A #B #C #D #E #F #G #H *
    22892289  | 3,7: #A #B #C #D #E #F *
    22902290  | #r #S' #M' #AF whd in AF; destruct
     
    23012301#ge * *
    23022302[ #f #fs #m * [*] #fn #S #M #l #AS
    2303 | #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
     2303| #vf #fd #args #dst * [2: #f #fs] #m * [1,3:*] #fn #S #M #l #AS
    23042304| #ret #dst #fs #m #S #M #l #AS
    23052305| #r #S #M #l #AS
     
    24352435  as_pc_of (RTLabs_status ge) s3 = as_pc_of (RTLabs_status ge) s4.
    24362436#ge * #s1 #S1 #M1 #CL1
    2437 cases (rtlabs_call_inv … (simplify_cl … CL1)) #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
     2437cases (rtlabs_call_inv … (simplify_cl … CL1)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 #E destruct
    24382438* #s2 #S2 #M2 #CL2
    2439 cases (rtlabs_call_inv … (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
    2440 * * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
    2441 * * [ 1,5: #f4 #fs4 #m4 #S4 #M4 | 2,6: #a #b #c #d #e #f #g #h * | 3,7: #a #b #c #d #e #f #g * | 4,8: #r4 #S4 #M4 ]
     2439cases (rtlabs_call_inv … (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 #E destruct
     2440* * [ #f3 #fs3 #m3 #S3 #M3 | #a #b #c #d #e #f #g #h #i * | #a #b #c #d #e #f #g * | #r3 #S3 #M3 ]
     2441* * [ 1,5: #f4 #fs4 #m4 #S4 #M4 | 2,6: #a #b #c #d #e #f #g #h #i * | 3,7: #a #b #c #d #e #f #g * | 4,8: #r4 #S4 #M4 ]
    24422442whd in ⊢ (% → ?);
    24432443[ 1,3: cases fs1 in M1 ⊢ %; [1,3: #M *] #f1' #fs1 cases S1 [1,3:*] #fn1 * [1,3:* #X *] #fn1' #S1' #M1 whd in ⊢ (% → ?);
     
    24622462  RTLabs_classify (Ras_state … s1) = RTLabs_classify (Ras_state … s2).
    24632463#ge
    2464 * * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #fd1 #args1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 * [2: #fn1 #S1 #E normalize in E; destruct] #M1 ]
    2465 * * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 2,6,10,14: #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 #S2 #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
     2464* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #vf1 #fd1 #args1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 * [2: #fn1 #S1 #E normalize in E; destruct] #M1 ]
     2465* * [ 1,5,9,13: * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 2,6,10,14: #vf2 #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 #S2 #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
    24662466whd in ⊢ (??%% → ?); #E destruct try %
    24672467[ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%);
     
    24872487  as_costed (RTLabs_status ge) s →
    24882488  RTLabs_classify (Ras_state … s) = cl_other.
    2489 #ge * * [ #f #fs #m #S #M | #fd #args #dst #fs #m #S #M | #ret #dst #fs #m #S #M | #r #S #M ]
     2489#ge * * [ #f #fs #m #S #M | #vf #fd #args #dst #fs #m #S #M | #ret #dst #fs #m #S #M | #r #S #M ]
    24902490#CS lapply (proj2 … (RTLabs_costed …) … CS)
    24912491whd in ⊢ (??%? → %);
     
    25002500  as_costed (RTLabs_status ge) s2.
    25012501#ge
    2502 * * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 #S1 #M1 ]
     2502* * [ * #func1 #regs1 #next1 #nok1 #sp1 #dst1 #fs1 #m1 * [*] #fn1 #S1 #M1 | #vf1 #fd1 #args1 #dst1 #fs1 #m1 #S1 #M1 | #ret1 #dst1 #fs1 #m1 #S1 #M1 | #r1 #S1 #M1 ]
    25032503[ 2,3,4: #s2 #PC #CS1 lapply (proj2 … (RTLabs_costed …) … CS1) whd in ⊢ (??%% → ?); #E destruct ]
    2504 * * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [*] #fn2 #S2 #M2 | 2,6,10,14: #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 * [2: #fn2 #S2] #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
     2504* * [ * #func2 #regs2 #next2 #nok2 #sp2 #dst2 #fs2 #m2 * [*] #fn2 #S2 #M2 | 2,6,10,14: #vf2 #fd2 #args2 #dst2 #fs2 #m2 * [1,3,5,7:*] #fn2 #S2 #M2 | 3,7,11,15: #ret2 #dst2 #fs2 #m2 * [2: #fn2 #S2] #M2 | 4,8,12,16: #r2 * [2,4,6,8: #fn2 #S2 #E normalize in E; destruct] #M2 ]
    25052505whd in ⊢ (??%% → ?); #E destruct
    25062506#CS1 @(proj1 … (RTLabs_costed …)) lapply (proj2 … (RTLabs_costed …) … CS1)
     
    25272527  state_fn … pre = state_fn … post.
    25282528#ge * #pre #preS #preM * #post #postS #postM #CL #AF
    2529 cases (rtlabs_call_inv … (simplify_cl … CL)) #fd * #args * #dst * #fs * #m #E destruct
     2529cases (rtlabs_call_inv … (simplify_cl … CL)) #vf * #fd * #args * #dst * #fs * #m #E destruct
    25302530cases post in postM AF ⊢ %;
    25312531[ #postf #postfs #postm cases postS [*] #postfn #S' #M' #AF
     
    25372537    #f #fs' #M * * #N #F #PC destruct %
    25382538  ]
    2539 | #A #B #C #D #E #F *
     2539| #A #B #C #D #E #F #G *
    25402540| #A #B #C #D #E *
    25412541| #r #M' #AF whd in AF; destruct
     
    25542554inversion (eval_preserves_ext … EX)
    25552555[ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 destruct %2 %
    2556 | #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct %2 %
     2556| #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 destruct %2 %
    25572557| #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 #H51 destruct
    25582558| #H53 #H54 #H55 #H56 #H57 #H58 #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 destruct %1 %
     
    26392639  #IN' destruct
    26402640| #s2 #s3 #s4 #EX2 #CL2 #AF2 #tlr3 #CS4 #EX1 #AF1 #CS2 @⊥
    2641   cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
    2642   cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
     2641  cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
     2642  cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
    26432643  cases AF1
    26442644| #s1 #s2 #s3 #EX #CL #tlr @⊥ @(RTLabs_notail' … CL)
    26452645| #fl #s2 #s3 #s3' #s4 #EX2 #CL2 #AF2 #tlr3 #CS3' #tal3' #EX1 #AF1 #CS2 @⊥
    2646   cases (declassify_state … EX1 (simplify_cl … CL)) #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
    2647   cases (declassify_state … EX2 (simplify_cl … CL2)) #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
     2646  cases (declassify_state … EX1 (simplify_cl … CL)) #vf1 * #fd1 * #args1 * #dst1 * #fs1 * #m1 * #S * #M #E destruct
     2647  cases (declassify_state … EX2 (simplify_cl … CL2)) #vf2 * #fd2 * #args2 * #dst2 * #fs2 * #m2 * #S2 * #M2 #E destruct
    26482648  cases AF1
    26492649| #fl #s2 #s3 #s4 #EX2 #tal3 #CL2 #CS3 #EX1 #AF1 #CS2 #IN
Note: See TracChangeset for help on using the changeset viewer.