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.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.