Changeset 2295


Ignore:
Timestamp:
Aug 13, 2012, 12:21:30 PM (7 years ago)
Author:
campbell
Message:

Start on showing unrepeating property of RTLabs structured traces: shadow
stack of function ids is preserved, traces follow successive instructions.

Location:
src/RTLabs
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/RTLabs/Traces.ma

    r2293 r2295  
    6565    #hd #tl #H @H
    6666  | #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct
    67   | #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct
     67  | #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct
    6868    cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %
    6969    [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // | @M2 ]
     
    204204].
    205205
     206(* After returning from a function, we should be ready to execute the next
     207   instruction of the caller and the shadow stack should be preserved (we have
     208   to take the top element off because the Callstate includes the callee); *or*
     209   we're in the final state.
     210 *)
     211
     212definition RTLabs_after_return : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → RTLabs_state ge → Prop ≝
     213λge,s,s'.
     214  match s with
     215  [ mk_Sig s p ⇒
     216    match s return λs. RTLabs_classify s = cl_call → ? with
     217    [ Callstate fd args dst stk m ⇒
     218      λ_. match s' with
     219      [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒
     220          next h = next f ∧
     221          f_graph (func h) = f_graph (func f) ∧
     222          match Ras_fn_stack … s with [ nil ⇒ False | cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]
     223      | Finalstate r ⇒ stk = [ ]
     224      | _ ⇒ False
     225      ]
     226   | State f fs m ⇒ λH.⊥
     227   | _ ⇒ λH.⊥
     228   ] p
     229 ].
     230[ whd in H:(??%?);
     231  cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
     232  normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
     233| normalize in H; destruct
     234| normalize in H; destruct
     235] qed.
     236
     237
    206238definition RTLabs_status : genv → abstract_status ≝
    207239λge.
     
    213245    (λs,c. RTLabs_classify s = c)
    214246    (RTLabs_pc_to_cost_label ge)
    215     (λs,s'. match s with
    216       [ mk_Sig s p ⇒
    217         match s return λs. RTLabs_classify s = cl_call → ? with
    218         [ Callstate fd args dst stk m ⇒
    219           λ_. match s' with
    220           [ State f fs m ⇒ match stk with [ nil ⇒ False | cons h t ⇒ next h = next f ∧ f_graph (func h) = f_graph (func f) ]
    221           | Finalstate r ⇒ stk = [ ]
    222           | _ ⇒ False
    223           ]
    224         | State f fs m ⇒ λH.⊥
    225         | _ ⇒ λH.⊥
    226         ] p
    227       ])
     247    (RTLabs_after_return ge)
    228248  (λs. RTLabs_is_final s ≠ None ?).
    229 [ normalize in H; destruct
    230 | normalize in H; destruct
    231 | whd in H:(??%?);
    232   cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;
    233   normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct
    234 ] qed.
    235249
    236250(* Allow us to move between the different notions of when a state is cost
     
    683697| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/
    684698| #ge #f #fs #m #rtv #dst #m' #Hge * #H1 #H2 @H2
    685 | #ge #f #fs #rtv #dst #f' #m * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
     699| #ge #f #fs #rtv #dst #f' #m #N * #func #locals #next #nok #sp #retdst #locals' #next' #nok' #Hge * #H1 #H2 % //
    686700| //
    687701] qed.
     
    779793
    780794
     795(* Extend our information about steps to states extended with the shadow stack. *)
     796
     797inductive state_rel_ext : ∀ge:genv. RTLabs_state ge → RTLabs_state ge → Prop ≝
     798| xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (State f fs m) S M) (mk_RTLabs_state ge (State f' fs m') S M')
     799| xto_call : ∀ge,f,fs,m,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_state ge (State f fs m) S M) (mk_RTLabs_state ge (Callstate fd args dst (f'::fs) m) (fn::S) M')
     800| xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_state ge (Callstate (Internal ? fn) args dst fs m) S M) (mk_RTLabs_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M')
     801| xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_state ge (State f fs m) (fn::S) M) (mk_RTLabs_state ge (Returnstate rtv dst fs m') S M')
     802| 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_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_state ge (State f' fs m) S M')
     803| xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_state ge (Finalstate r) [ ] M')
     804.
     805
     806lemma eval_preserves_ext : ∀ge,s,s'.
     807  as_execute (RTLabs_status ge) s s' →
     808  state_rel_ext ge s s'.
     809#ge0 * #s #S #M * #s' #S' #M' * #tr * #EX
     810generalize in match M'; -M'
     811generalize in match M; -M
     812generalize in match EX;
     813inversion (eval_preserves … EX)
     814[ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct
     815  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
     816  %1 //
     817| #ge #f #fs #m #fd #args #f' #dst #F #fn #FFP #E1 #E2 #E3 #E4 destruct
     818  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
     819  %2 //
     820| #ge #func #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
     821  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
     822  %3
     823| #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
     824  cases S [ #EX' * ] #fn #S
     825  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
     826  %4
     827| #ge #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
     828  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
     829  %5 //
     830| #ge #r #dst #m #E1 #E2 #E3 #E4 destruct
     831  cases S [ 2: #h #t #EX' * ]
     832  #EX' #M #M' whd in ⊢ (??%? → ?); generalize in ⊢ (??(????%)? → ?); #M'' #E destruct
     833  %6
     834] qed.
     835
     836
     837
    781838(* The preservation of (most of) the stack is useful to show as_after_return.
    782839   We do this by showing that during the execution of a function the lower stack
     
    784841   the identity of the next instruction to execute.
    785842   
    786    Note: since this was first written I've introduced the shadow stack of
    787    function blocks.  It might be possible to replace some or all of the stack
    788    preservation with that.
     843   We also show preservation of the shadow stack of function pointers.  As with
     844   the real stack, we ignore the current function.
    789845 *)
    790846
    791 inductive stack_of_state : list frame → state → Prop ≝
    792 | sos_State : ∀f,fs,m. stack_of_state fs (State f fs m)
    793 | sos_Callstate : ∀fd,args,dst,f,fs,m. stack_of_state fs (Callstate fd args dst (f::fs) m)
    794 | sos_Returnstate : ∀rtv,dst,fs,m. stack_of_state fs (Returnstate rtv dst fs m)
     847inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_state ge → Prop ≝
     848| sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_state ge (State f fs m) (fn::S) M)
     849| sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M)
     850| sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_state ge (Returnstate rtv dst fs m) S M)
    795851.
    796852
    797 inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝
    798 | sp_normal : ∀fs,s1,s2.
    799     stack_of_state fs s1 →
    800     stack_of_state fs s2 →
    801     stack_preserved doesnt_end_with_ret s1 s2
    802 | sp_finished : ∀s1,f,f',fs,m.
     853inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_state ge → RTLabs_state ge → Prop ≝
     854| sp_normal : ∀fs,S,s1,s2.
     855    stack_of_state ge fs S s1 →
     856    stack_of_state ge fs S s2 →
     857    stack_preserved ge doesnt_end_with_ret s1 s2
     858| sp_finished : ∀s1,f,f',fs,m,fn,S,M.
    803859    next f = next f' →
    804860    frame_rel f f' →
    805     stack_of_state (f::fs) s1 →
    806     stack_preserved ends_with_ret s1 (State f' fs m)
    807 | sp_stop : ∀s1,r.
    808     stack_of_state [ ] s1 →
    809     stack_preserved ends_with_ret s1 (Finalstate r)
    810 | sp_top : ∀fd,args,dst,m,r.
    811     stack_preserved doesnt_end_with_ret (Callstate fd args dst [ ] m) (Finalstate r)
     861    stack_of_state ge (f::fs) (fn::S) s1 →
     862    stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (State f' fs m) (fn::S) M)
     863| sp_stop : ∀s1,r,M.
     864    stack_of_state ge [ ] [ ] s1 →
     865    stack_preserved ge ends_with_ret s1 (mk_RTLabs_state ge (Finalstate r) [ ] M)
     866| sp_top : ∀fd,args,dst,m,r,fn,M1,M2.
     867    stack_preserved ge doesnt_end_with_ret (mk_RTLabs_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_state ge (Finalstate r) [ ] M2)
    812868.
    813869
    814870discriminator list.
    815871
    816 lemma stack_of_state_eq : ∀fs,fs',s.
    817   stack_of_state fs s →
    818   stack_of_state fs' s →
    819   fs = fs'.
    820 #fs0 #fs0' #s0 *
    821 [ #f #fs #m #H inversion H
    822   #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    823 | #fd #args #dst #f #fs #m #H inversion H
    824   #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    825 | #rtv #dst #fs #m #H inversion H
    826   #a #b #c #d try #e try #g try #h try #i try #j destruct @refl
    827 ] qed.
    828 
    829 lemma stack_preserved_final : ∀e,r,s.
    830   ¬stack_preserved e (Finalstate r) s.
    831 #e #r #s % #H inversion H
    832 [ #H184 #H185 #H186 #SOS #H188 #H189 #H190 #H191 #H192 destruct
    833   inversion SOS #a #b #c #d #e #f try #g try #h destruct
    834 | #H194 #H195 #H196 #H197 #H198 #H199 #H200 #SOS #H201 #H202 #H203 #H204 destruct
    835   inversion SOS #a #b #c #d #e #f try #g try #h destruct
    836 | #s' #r' #SOS #E1 #E2 #E3 #E4 destruct
    837   inversion SOS #a #b #c #d #e #f try #g try #h destruct
    838 | #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct
    839 ] qed.
    840 
    841 lemma stack_preserved_join : ∀e,s1,s2,s3.
    842   stack_preserved doesnt_end_with_ret s1 s2 →
    843   stack_preserved e s2 s3 →
    844   stack_preserved e s1 s3.
    845 #e1 #s1 #s2 #s3 #H1 inversion H1
    846 [ #fs #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
     872lemma stack_of_state_eq : ∀ge,fs,fs',S,S',s.
     873  stack_of_state ge fs S s →
     874  stack_of_state ge fs' S' s →
     875  fs = fs' ∧ S = S'.
     876#ge #fs0 #fs0' #S0 #S0' #s0 *
     877[ #f #fs #m #fn #S #M #H inversion H
     878  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
     879| #fd #args #dst #f #fs #m #fn #fn' #S #M #H inversion H
     880  #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/
     881| #rtv #dst #fs #m #S #M #H inversion H
     882  #a #b #c #d try #e try #g try #h try #i try #j try #k try #l try #n try #o destruct /2/
     883] qed.
     884
     885lemma stack_preserved_final : ∀ge,e,r,S,M,s.
     886  ¬stack_preserved ge e (mk_RTLabs_state ge (Finalstate r) S M) s.
     887#ge #e #r #S #M #s % #H inversion H
     888[ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct
     889  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
     890| #H194 #H195 #H196 #H197 #H198 #H199 #H200 #HX #HY #HZ #SOS #H201 #H202 #H203 #H204 destruct
     891  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #j try #k try #l try #m destruct
     892| #s' #r' #M' #SOS #E1 #E2 #E3 #E4 destruct
     893  inversion SOS #a #b #c #d #e #f try #g try #h try #i try #k try #l try #m try #o destruct
     894| #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 destruct
     895] qed.
     896
     897lemma stack_preserved_join : ∀ge,e,s1,s2,s3.
     898  stack_preserved ge doesnt_end_with_ret s1 s2 →
     899  stack_preserved ge e s2 s3 →
     900  stack_preserved ge e s1 s3.
     901#ge #e1 #s1 #s2 #s3 #H1 inversion H1
     902[ #fs #S #s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct
    847903  #H2 inversion H2
    848   [ #fs' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
    849     @(sp_normal fs) // <(stack_of_state_eq … S1' S2) //
    850   | #s1'' #f #f' #fs' #m #N #F #S1' #E1 #E2 #E3 #E4 destruct
    851     @(sp_finished … N) >(stack_of_state_eq … S1' S2) //
    852   | #s1'' #r #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop >(stack_of_state_eq … S1'' S2) //
    853   | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct
     904  [ #fs' #S' #s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct
     905    @(sp_normal ge fs S) // cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
     906  | #s1'' #f #f' #fs' #m #fn #S' #M #N #F #S1' #E1 #E2 #E3 #E4 destruct
     907    @(sp_finished … fn … N) cases (stack_of_state_eq … S1' S2) #E1 #E2 destruct //
     908  | #s1'' #r #M #S1'' #E1 #E2 #E3 #E4 destruct @sp_stop cases (stack_of_state_eq … S1'' S2) #E1 #E2 destruct //
     909  | #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct
    854910    inversion S2
    855     [ #H34 #H35 #H36 #H37 #H38 #H39 destruct
    856     | #fd' #args' #dst' #f #fs' #m' #E1 #E2 #E3 destruct
    857     | #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
     911    [ #H34 #H35 #H36 #H37 #H38 #H39 #H40 #H41 #H42 destruct
     912    | #fd' #args' #dst' #f #fs' #m' #fn' #fn'' #S' #M' #E1 #E2 #E3 destruct
     913    | #H41 #H42 #H43 #H44 #H45 #H46 #H47 #H48 #H49 #H50 destruct
    858914    ]
    859915  ]
    860916| #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
    861 | #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct #H
    862   cases (stack_preserved_final … H) #r #E destruct
    863 | #fd #args #dst #m #r #E1 #E2 #E3 #E4 destruct #F @⊥
     917| #H19 #H20 #H21 #H22 #H23 #H24 #H25 destruct
     918| #fd #args #dst #m #r #fn #M1 #M2 #E1 #E2 #E3 #E4 destruct #F @⊥
    864919  @(absurd … F) //
    865920] qed.
    866921
    867 lemma stack_preserved_return : ∀ge,s1,s2,tr.
    868   RTLabs_classify s1 = cl_return →
    869   eval_statement ge s1 = Value ??? 〈tr,s2〉 →
    870   stack_preserved ends_with_ret s1 s2.
    871 #ge *
    872 [ #f #fs #m #s2 #tr #E @⊥ whd in E:(??%?);
    873   cases (lookup_present ??? (next f) (next_ok f)) in E;
    874   normalize #a try #b try #c try #d try #e try #f try #g try #i try #j destruct
    875 | #fd #args #dst #fs #m #s2 #tr #E normalize in E; destruct
    876 | #res #dst *
    877   [ #m #s2 #tr #_ #EV whd in EV:(??%?); cases res in EV;
    878     [ normalize #EV destruct | * [ 2: * #r normalize #EV destruct /2/ | *: normalize #a try #b destruct ] ]
    879   | #f #fs #m #s2 #tr #_ whd in ⊢ (??%? → ?); @bind_res_value #locals #El #EV
    880     whd in EV:(??%?); destruct @(sp_finished ? f) //
    881     cases f //
    882   ]
    883 | #r #s2 #tr #E normalize in E; destruct
    884 ] qed.
    885 
    886 lemma stack_preserved_step : ∀ge,s1,s2,tr.
    887   RTLabs_classify s1 = cl_other ∨ RTLabs_classify s1 = cl_jump →
    888   eval_statement ge s1 = Value ??? 〈tr,s2〉 →
    889   stack_preserved doesnt_end_with_ret s1 s2.
    890 #ge0 #s1 #s2 #tr #CL #EV inversion (eval_preserves … EV)
    891 [ #ge #f #f' #fs #m #m' #F #E1 #E2 #E3 #E4 destruct /2/
    892 | #ge #f #fs #m #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 /2/
    893 | #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #E1 #E2 #E3 #E4 destruct
    894   normalize in CL; cases CL #E destruct
    895 | #ge #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct /2/
    896 | #ge #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct cases CL
    897   #E normalize in E; destruct
    898 | #ge #r #dst #m #E1 #E2 destruct @⊥ cases CL normalize #E destruct
    899 ] qed.
    900 
    901 lemma stack_preserved_call : ∀ge,s1,s2,s3,tr.
    902   RTLabs_classify s1 = cl_call →
    903   eval_statement ge s1 = Value ??? 〈tr,s2〉 →
    904   stack_preserved ends_with_ret s2 s3 →
    905   stack_preserved doesnt_end_with_ret s1 s3.
    906 #ge #s1 #s2 #s3 #tr #CL #EV #SP
    907 cases (rtlabs_call_inv … CL)
    908 #fd * #args * #dst * #stk * #m #E destruct
    909 inversion SP
    910 [ #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 destruct
    911 | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct
    912   inversion (eval_preserves … EV)
    913   [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
    914   | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
    915   | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
    916     inversion S
    917     [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
    918     | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
    919     | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
    920     ]
    921   | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
     922(* Proof that steps preserve the stack.  For calls we show that a stack
     923   preservation proof for the called function gives us enough to show
     924   stack preservation for the caller between the call and the state after
     925   returning. *)
     926
     927lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_state ge.∀cl.
     928  RTLabs_classify s1 = cl →
     929  as_execute (RTLabs_status ge) s1 s2 →
     930  match cl with
     931  [ cl_call ⇒ ∀s3. stack_preserved ge ends_with_ret s2 s3 →
     932                   stack_preserved ge doesnt_end_with_ret s1 s3
     933  | cl_return ⇒ stack_preserved ge ends_with_ret s1 s2
     934  | _ ⇒ stack_preserved ge doesnt_end_with_ret s1 s2
     935  ].
     936#ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX)
     937[ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct
     938  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
     939| #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4
     940  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) normalize /2/
     941| #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct
     942  * #s3 #S3 #M3 #SP inversion SP
     943  [ #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 destruct
     944  | #s1 #f #f' #fs' #m3 #fn3 #S3' #M3' #E1 #E2 #SOS #E4 #E5 #E6 #E7 destruct
     945    @(sp_normal … fs' S3') //
     946    inversion SOS
     947    [ #H12 #H13 #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 destruct //
     948    | #H23 #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 destruct
     949    | #H38 #H39 #H40 #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct
     950    ]
     951  | #sx #r #M3 #SOS #E1 #E2 #E3 #E4 destruct
     952    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/ ]
     953    * #fn * #E1 #E2 destruct
     954    @sp_top
    922955  | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
    923   | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
    924   ]
    925 | #s1 #r #S1 #E1 #E2 #E3 #_ destruct
    926   inversion (eval_preserves … EV)
    927   [ #H48 #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 #H58 destruct
    928   | #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 #H70 #H71 #H72 #H73 #H74 destruct
    929   | #ge' #fn #locals #next #nok #sp #fs1 #m1 #args1 #dst1 #m2 #E1 #E2 #E3 #E4 destruct
    930     inversion S1
    931     [ #fx #fsx #mx #E1 #E2 #E3 destruct /2/
    932     | #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 destruct
    933     | #H86 #H87 #H88 #H89 #H90 #H91 #H92 destruct
    934     ]
    935   | #H94 #H95 #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 destruct
    936   | #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 destruct
    937   | #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 destruct
    938   ]
    939 | #H49 #H50 #H51 #H52 #H53 #H54 #H55 #H56 #H57 destruct
    940 ] qed.
    941  
    942 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.∀tr.
     956  ]
     957| #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct
     958  whd in match (RTLabs_classify ?); cases (lookup_present ???? (next_ok ?)) /2/
     959| #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd
     960  cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) //
     961| #ge #r #dst #m #M #M' #E1 #E2 #E3 #E4 destruct whd /2/
     962] qed.
     963
     964lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_state ge.∀s2,tr.
     965  ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉.
     966  as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV).
     967#ge #s1 #s2 #tr #EV %{tr} %{EV} %
     968qed.
     969
     970lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.
    943971  ∀CL : RTLabs_classify s1 = cl_call.
    944   eval_statement ge s1 = Value ??? 〈tr,s2〉
    945   stack_preserved ends_with_ret s2 s3 →
     972  as_execute (RTLabs_status ge) s1 s2
     973  stack_preserved ge ends_with_ret s2 s3 →
    946974  as_after_return (RTLabs_status ge) «s1,CL» s3.
    947 #ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #tr #CL #EV #S23
     975#ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23
    948976cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct
    949977whd
    950978inversion S23
    951979[ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct
    952 | #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct whd
    953   inversion (eval_preserves … EV)
    954   [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct
    955   | #H151 #H152 #H153 #H154 #H155 #H156 #H157 #H158 #H159 #H160 #H161 #H162 #H163 #H164 #H165 destruct
    956   | #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #E1 #E2 #E3 #E4 destruct
     980| #s2' #f #f' #fs #m' #fn' #S #M #N #F #S #E1 #E2 #E3 #E4 destruct whd
     981  inversion (eval_preserves_ext … EV)
     982  [ 3: #gex #fnx #locals #next #nok #sp #fsx #mx #argsx #dstx #mx' #Sx #Mx #Mx' #E1 #E2 #E3 #_ destruct
    957983    inversion S
    958     [ #fy #fsy #my #E1 #E2 #E3 destruct whd % [ @N | inversion F // ]
    959     | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 destruct
    960     | #H177 #H178 #H179 #H180 #H181 #H182 #H183 destruct
    961     ]
    962   | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
    963   | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
    964   | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
    965   ]
    966 | #s1 #r #S1 #E1 #E2 #E3 #E4 destruct whd
    967   inversion (eval_preserves … EV)
    968   [ #H59 #H60 #H61 #H62 #H63 #H64 #H65 #H66 #H67 #H68 #H69 destruct
    969   | #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 #H83 #H84 #H85 destruct
    970   | #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 destruct
     984    [ #fy #fsy #my #fn #S0 #M0 #E1 #E2 #E3 #E4 destruct whd % [ % [ @N | inversion F // ] | whd % ]
     985    | #H167 #H168 #H169 #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 #H179 destruct
     986    | #H177 #H178 #H179 #H180 #H181 #H182 #H183 #H184 #H185 destruct
     987    ]
     988  | *: #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 try #H195 try #H196 try #H197 try #H198 try #H199 destruct
     989  ]
     990| #s1 #r #M #S1 #E1 #E2 #E3 #E4 destruct whd
     991  inversion (eval_preserves_ext … EV)
     992  [ 3: #ge' #fn' #locals #next #nok #sp #fs #m' #args' #dst' #m'' #S #M #M' #E1 #E2 #E3 #E4 destruct
    971993    inversion S1
    972     [ #H103 #H104 #H105 #H106 #H107 #H108 destruct //
    973     | #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 destruct
    974     | #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
    975     ]
    976   | #H185 #H186 #H187 #H188 #H189 #H190 #H191 #H192 #H193 #H194 #H195 destruct
    977   | #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206 #H207 #H208 destruct
    978   | #H10 #H11 #H12 #H13 #H14 #H15 #H16 #H17 destruct
     994    [ #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 destruct //
     995    | *: #H110 #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 #H119 try #H120 try #H121 try #H122 destruct
     996    ]
     997  | *: #H197 #H198 #H199 #H200 #H201 #H202 #H203 #H204 #H205 #H206  try #H195 try #H196 try #H197 try #H198 try #H199 destruct
    979998  ]
    980999| #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct
     
    9951014  cost_labelled : well_cost_labelled_state new_state;
    9961015  new_trace : T new_state;
    997   stack_ok : stack_preserved ends start new_state;
     1016  stack_ok : stack_preserved ge ends start new_state;
    9981017  terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth | _ ⇒ depth ]) with
    9991018               [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭
     
    10231042    will_return_end … TM1 = will_return_end … TM2 →
    10241043    T2 (new_state … r) →
    1025     stack_preserved e s2 (new_state … r) →
     1044    stack_preserved ge e s2 (new_state … r) →
    10261045    trace_result ge d e s2 t2 TM2 T2 l2 ≝
    10271046λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
     
    10521071    will_return_end … TM1 = will_return_end … TM2 →
    10531072    T2 (ends … r) (new_state … r) →
    1054     stack_preserved (ends … r) s2 (new_state … r) →
     1073    stack_preserved ge (ends … r) s2 (new_state … r) →
    10551074    sub_trace_result ge d s2 t2 TM2 T2 l2 ≝
    10561075λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP.
     
    12461265  ]
    12471266| @(will_return_return … CL TERMINATES)
    1248 | @(stack_preserved_return … EV) //
     1267| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    12491268| %{tr} %{EV} @refl
    12501269| @(well_cost_labelled_state_step  … EV) //
    12511270| whd @(will_return_notfn … TERMINATES) %2 @CL
    1252 | @(stack_preserved_step … EV) /2/
     1271| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    12531272| %{tr} %{EV} %
    12541273| %1 whd @CL
     
    12611280    #TM' * #_ #EQ' @EQ'
    12621281  ]
    1263 | @(stack_preserved_call … EV (stack_ok … r)) //
     1282| @(stack_preserved_step ge start' ?? CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
    12641283| %{tr} %{EV} %
    1265 | @(RTLabs_after_call … next') [2: @EV | skip | // ]
     1284| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
    12661285| @(cost_labelled … r)
    12671286| skip
     
    12711290| cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ
    12721291  cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ'
    1273 | @(RTLabs_after_call … next') [2: @EV | skip | // ]
     1292| @(RTLabs_after_call … next') [ @eval_to_as_exec | // ]
    12741293| %{tr} %{EV} %
    1275 | @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) //
     1294| @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) @(stack_ok … r)
    12761295| @(cost_labelled … r)
    12771296| cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78
     
    12911310  @(monotonic_le_times_r 3 … GT)
    12921311| whd @(will_return_notfn … TERMINATES) %1 @CL
    1293 | @(stack_preserved_step … EV) /2/
     1312| @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    12941313| %{tr} %{EV} %
    12951314| %2 whd @CL
     
    12991318| @CL
    13001319| %{tr} %{EV} %
    1301 | @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/
     1320| @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV))
    13021321| @(well_cost_labelled_state_step  … EV) //
    13031322| %1 @CL
     
    13541373lemma eval_successor : ∀ge,f,fs,m,tr,s'.
    13551374  eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 →
    1356   RTLabs_classify s' = cl_return
     1375  (RTLabs_classify s' = cl_return ∧ successors (lookup_present … (f_graph (func f)) (next f) (next_ok f)) = [ ])
    13571376  ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))).
    13581377#ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s'
     
    13771396  | #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El)
    13781397  ]*)
    1379 | #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl
     1398| #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 % %
    13801399] qed.
    13811400
     
    14651484  RTLabs_cost s' = false →
    14661485  state_bound_on_steps_to_cost s' n.
    1467 #ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); -stk -stk' lapply CL -CL inversion H
     1486#ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); lapply CL -CL inversion H
    14681487[ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL)
    14691488  #fn * #args * #dst * #stk * #m' #E destruct
    14701489| #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct
    14711490  whd in S; #CL cases s'
    1472   [ #f' #fs' #m' * #N #F #CS
     1491  [ #f' #fs' #m' * * #N #F #STK #CS
    14731492    %1 whd
    14741493    inversion S
    14751494    [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥
    14761495      change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P *
    1477     | #l #n #B #E1 #E2 #_ destruct <N <F @B
     1496    | #l #n #H #CS' #B #E1 #E2 #_ destruct <N <F @B
    14781497    ]
    14791498  | #fd' #args' #dst' #fs' #m' *
     
    14931512[ #f #fs #m #m #FS #E1 #E2 #_ destruct
    14941513  #EVAL cases (eval_successor … EVAL)
    1495   [ /3/
     1514  [ * /3/
    14961515  | * #l * #S1 #S2 #NC %2
    14971516  (*
     
    15071526        change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%);
    15081527        whd in S1:(??%?); destruct >NC in CSx; *
    1509       | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H73
     1528      | whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 destruct @H75
    15101529      ]
    15111530    | #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct
     
    15291548  | #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct
    15301549  | #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct
    1531   | #ge' #f' #fs' #rtv' #dst' #f'' #m' #F #E1 #E2 #E3 #_ destruct
     1550  | #ge' #f' #fs' #rtv' #dst' #f'' #m' #N #F #E1 #E2 #E3 #_ destruct
    15321551    %1 whd in FS ⊢ %;
    1533     inversion (stack_preserved_return … EVAL) [ @refl | 2,4,5: #H141 #H142 #H143 #H144 #H145 #H146 #H147 try #H148 try #H149 destruct ]
    1534     #s1 #f1 #f2 #fs #m #FE #FR #SS1 #_ #E1 #E2 #_ destruct <FE
    1535     inversion SS1 [ #H163 #H164 #H165 #H166 #H167 #H168 destruct | #H170 #H171 #H172 #H173 #H174 #H175 #H176 #H177 #H178 destruct | #rtv #dst #fs0 #m0 #E1 #E2 #_ destruct ]
     1552    <N
    15361553    inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct
    15371554    inversion FS
    15381555    [ #lx #nx #LPx #CSx #E1x #E2x @⊥ destruct
    1539         change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs m0)) in CSx:(?%);
     1556        change with (RTLabs_cost (State (mk_frame func locals' lx ? sp retdst) fs' m')) in CSx:(?%);
    15401557        >NC in CSx; *
    1541     | #lx #nx #H #E1x #E2x #_ destruct @H
     1558    | #lx #nx #P #CS #H #E1x #E2x #_ destruct @H
    15421559    ]
    15431560  | #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct
     
    15881605| #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct
    15891606  whd in S ⊢ %; cases S //
    1590 | #ge' #f #fs #rtv #dst #f' #m #F #E1 #E2 #E3 #E4 destruct
     1607| #ge' #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct
    15911608  whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S
    15921609| #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I
    15931610] qed.
    15941611
    1595 lemma soundly_labelled_state_preserved : ∀s,s'.
    1596   stack_preserved ends_with_ret s s' →
     1612lemma soundly_labelled_state_preserved : ∀ge,s,s'.
     1613  stack_preserved ge ends_with_ret s s' →
    15971614  soundly_labelled_state s →
    15981615  soundly_labelled_state s'.
    1599 #s0 #s0' #SP inversion SP
     1616#ge #s0 #s0' #SP inversion SP
    16001617[ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct
    1601 | #s1 #f #f' #fs #m #N #F #S1 #E1 #E2 #E3 #E4 destruct
     1618| #s1 #f #f' #fs #m #fn #S #M #N #F #S1 #E1 #E2 #E3 #E4 destruct
    16021619  inversion S1
    1603   [ #f1 #fs1 #m1 #E1 #E2 #E3 destruct
     1620  [ #f1 #fs1 #m1 #fn1 #S1 #M1 #E1 #E2 #E3 #E4 destruct
    16041621    * #_ #S whd in S;
    16051622    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
    16061623    destruct @S
    1607   | #fd #args #dst #f1 #fs1 #m1 #E1 #E2 #E3 destruct * #_ * #_ #S
     1624  | #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S
    16081625    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
    16091626    destruct @S
    1610   | #rtv #dst #fs1 #m1 #E1 #E2 #E3 destruct #S
     1627  | #rtv #dst #fs1 #m1 #S1 #M1 #E1 #E2 #E3 #E4 destruct #S
    16111628    inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107
    16121629    destruct @S
     
    17501767    | @(not_return_to_not_final … EV) >CL % #E destruct
    17511768    ]
    1752 | @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
    1753 | @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
     1769| @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
     1770| @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
    17541771| @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS)
    1755   @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr))
     1772  @(RTLabs_after_call ge start' next' … (stack_ok … tlr)) //
    17561773| % [ /2/
    17571774    | @(soundly_labelled_state_preserved … (stack_ok … tlr))
     
    17641781      inversion (stack_ok … tlr)
    17651782      [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct
    1766       | #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
    1767       | #s1 #r #S #E1 #E2 #E3 #E4 -TERMINATES destruct whd in S:(??%); -next' -s0
     1783      | #s1 #f #f' #fs #m #fn #S #M #N #F #S #E1 #E2 #E3 #E4 -TERMINATES destruct @refl
     1784      | #s1 #r #M #S #E1 #E2 #E3 #E4 change with (next_state ?????) in E2:(??%??); -TERMINATES destruct -next' -s0
    17681785        cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct
    17691786        inversion (eval_preserves … EV)
     
    17711788        #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 -TRACE_OK destruct
    17721789        inversion S
    1773         [ #f #fs0 #m #E1 #E2 #E3 destruct | *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ]
     1790        [ #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 ]
    17741791        (* state_bound_on_steps_to_cost needs to know about the current stack frame,
    17751792           so we can use it as a witness that at least one frame exists *)
     
    18591876] qed.
    18601877
    1861 lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'.
     1878lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_state ge.
     1879  as_execute (RTLabs_status ge) s1 s2 →
    18621880  make_initial_state p = OK ? s1 →
    1863   eval_statement ge s1 = Value ??? 〈tr,s2〉 →
    1864   stack_preserved ends_with_ret s2 s' →
     1881  stack_preserved ge ends_with_ret s2 s' →
    18651882  RTLabs_is_final s' ≠ None ?.
    1866 #ge #p #s1 #tr #s2 #s' whd in ⊢ (??%? → ?);
     1883#ge #p * #s1 #S1 #M1 * #s2 #S2 #M2 * #s' #S' #M' #EV whd in ⊢ (??%? → ?);
    18671884@bind_ok #m #_
    18681885@bind_ok #b #_
    18691886@bind_ok #f #_
    18701887#E destruct
    1871 #EV #SP inversion (eval_preserves … EV)
    1872 [ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #E1 #E2 #E3 #_ destruct
     1888#SP inversion (eval_preserves_ext … EV)
     1889[ 3: #ge' #fn #locals #next #nok #sp #fs #m1 #args #dst #m2 #S #M #M0' #E1 #E2 #E3 #_ destruct
    18731890     inversion SP
    1874      [ 3: #s1 #r #S #_ #_ #_ #_ % #E whd in E:(??%?); destruct
    1875      | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct
    1876           inversion H35 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 destruct
     1891     [ 3: #s1 #r #M0 #S #E1 #E2 #E3 #E4 destruct % #E whd in E:(??%?); destruct
     1892     | *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 try #H41 destruct @⊥
     1893          inversion H39 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70 try #H71 try #H72 try #H73 try #H74 destruct
    18771894     ]
    1878 | *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct
     1895| *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 destruct
    18791896] qed.
    18801897
     
    19311948  cases FINAL #E @E @refl
    19321949| %{tr} %{EV} %
    1933 | @(after_the_initial_call_is_the_final_state … INITIAL EV)
    1934   @(stack_ok … tlr)
     1950| @(after_the_initial_call_is_the_final_state … p s' next')
     1951  [ %{tr} %{EV} % | @INITIAL | @(stack_ok … tlr) ]
    19351952| @(well_cost_labelled_state_step … EV) //
    19361953| @(well_cost_labelled_call … EV) //
     
    22592276: equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?.
    22602277@flat_traces_are_determined_by_starting_point
    2261 qed.
     2278qed.
     2279
     2280
     2281(* We still need to link tal_unrepeating to our definition of cost soundness.
     2282
     2283   First, let's link unrepeating to our PCs and successors. *)
     2284
     2285definition RTLabs_pc_lookup : ∀ge. RTLabs_pc → option statement ≝
     2286λge,pc.
     2287match pc with
     2288[ rapc_state b l ⇒
     2289  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
     2290    match fd with [ Internal f ⇒ lookup ?? (f_graph f) l | _ ⇒ None ? ] ]
     2291| _ ⇒ None ?
     2292].
     2293
     2294definition genv_lookup : ∀ge. block → label → option statement ≝
     2295λge,b,l.
     2296  match find_funct_ptr … ge b with [ None ⇒ None ? | Some fd ⇒
     2297    match fd with [ Internal f ⇒ lookup ?? (f_graph f) l | _ ⇒ None ? ] ]
     2298.
     2299
     2300inductive good_pc_list (ge:genv) : option block → list (as_pc (RTLabs_status ge)) → Prop ≝
     2301| g_pc_end : ∀pc,b. good_pc_list ge b [pc]
     2302| g_pc_step : ∀b,l1,st,l2,tl.
     2303    genv_lookup ge b l1 = Some ? st →
     2304    l2 ∈ successors st →
     2305    good_pc_list ge (Some ? b) (rapc_state b l2::tl) →
     2306    good_pc_list ge (Some ? b) (rapc_state b l1::rapc_state b l2::tl)
     2307| g_pc_call : ∀b,l1,st,l2,b',tl.
     2308    genv_lookup ge b l1 = Some ? st →
     2309    l2 ∈ successors st →
     2310    good_pc_list ge (Some ? b) (rapc_call (Some ? l2) b'::tl) →
     2311    good_pc_list ge (Some ? b) (rapc_state b l1::rapc_call (Some ? l2) b'::tl)
     2312| g_pc_cret : ∀b,l,b',tl.
     2313    good_pc_list ge (Some ? b) (rapc_state b l::tl) →
     2314    good_pc_list ge (Some ? b) (rapc_call (Some ? l) b'::rapc_state b l::tl)
     2315| g_pc_return : ∀b,l1,st,caller.
     2316    genv_lookup ge b l1 = Some ? st →
     2317    successors st = [ ] →
     2318    good_pc_list ge (Some ? b) [rapc_state b l1; rapc_ret caller]
     2319.
     2320
     2321definition state_fn : ∀ge. RTLabs_status ge → option block ≝
     2322λge,s. match Ras_fn_stack … s with [ nil ⇒ None ? | cons h t ⇒
     2323  match Ras_state … s with
     2324  [ Callstate _ _ _ _ _ ⇒ match t with [ cons h' _ ⇒ Some ? h' | nil ⇒ None ? ]
     2325  | _ ⇒  Some ? h ] ].
     2326
     2327(* After returning from a function we're either in the final state, or we're
     2328   back in the caller at the correct instruction. *)
     2329
     2330lemma pc_after_return : ∀ge,pre,post,CL,ret,callee.
     2331  as_after_return (RTLabs_status ge) «pre,CL» post →
     2332  as_pc_of (RTLabs_status ge) pre = rapc_call ret callee →
     2333  match ret with
     2334  [ None ⇒ RTLabs_is_final (Ras_state … post) ≠ None ?
     2335  | Some retl ⇒
     2336    ∃fn. state_fn … pre = Some ? fn ∧
     2337         state_fn … post = Some ? fn ∧
     2338         as_pc_of (RTLabs_status ge) post = rapc_state fn retl
     2339  ].
     2340#ge #pre #post #CL #ret #callee #AF
     2341cases pre in CL AF ⊢ %;
     2342* [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?);
     2343    cases (lookup_present ???? (next_ok f)) in CL;
     2344    normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct
     2345  | #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL
     2346  | #ret #dst #fs #m #S #M #CL normalize in CL; destruct
     2347  | #r #S #M #CL normalize in CL; destruct
     2348  ]
     2349cases post
     2350* [ #postf #postfs #postm * [*] #fn' #S' #M'
     2351  | 5: #postf #postfs #postm * [*] #fn' #S' #M' *
     2352  | 2,6: #A #B #C #D #E #F #G *
     2353  | 3,7: #A #B #C #D #E #F *
     2354  | #r #S' #M' #AF whd in AF; destruct
     2355  | #r #S' #M'
     2356  ]
     2357#AF #PC normalize in PC; destruct whd
     2358[ %{fn'} cases AF * #A #B #C destruct % [ % % | whd in ⊢ (??%?); >A % ]
     2359| % #E normalize in E; destruct
     2360] qed.
     2361
     2362lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_state ge.
     2363  as_execute (RTLabs_status ge) s s' →
     2364  RTLabs_classify s = cl →
     2365  match cl with
     2366  [ cl_call ⇒ ∀caller,callee. P (rapc_call caller callee)
     2367  | cl_return ⇒ ∀fn. P (rapc_ret fn)
     2368  | cl_other ⇒ ∀fn,l. P (rapc_state fn l)
     2369  | cl_jump ⇒ ∀fn,l. P (rapc_state fn l)
     2370  ] → P (as_pc_of (RTLabs_status ge) s).
     2371#ge #cl #P * *
     2372[ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%);
     2373  cases (lookup_present ???? (next_ok f)) normalize
     2374  #A #B try #C try #D try #E try #F try #G try #H try #J destruct //
     2375| #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct //
     2376| #ret #dst #fs #m * [ | #fn #S ] #M #s' #EX #CL normalize in CL; destruct //
     2377| #r #S #M #s' * #tr * #EX normalize in EX; destruct
     2378] qed.
     2379
     2380lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_state ge.
     2381  as_execute (RTLabs_status ge) s s' →
     2382  RTLabs_classify s = cl →
     2383  match cl with
     2384  [ cl_call ⇒ ∃caller,callee. as_pc_of (RTLabs_status ge) s = rapc_call caller callee
     2385  | cl_return ⇒ ∃fn. as_pc_of (RTLabs_status ge) s = rapc_ret fn
     2386  | cl_other ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
     2387  | cl_jump ⇒ ∃fn,l. as_pc_of (RTLabs_status ge) s = rapc_state fn l
     2388  ] .
     2389#ge * #s #s' #EX #CL whd
     2390@(declassify_pc … EX CL) whd
     2391[ #fn %{fn} % | #fn #l %{fn} %{l} % | #caller #callee %{caller} %{callee} % | #fn #l %{fn} %{l} % ]
     2392qed.
     2393
     2394lemma tal_pc_list_start : ∀ge,fl,s1,s2. ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
     2395  ∃tl. tal_pc_list (RTLabs_status ge) … tal = (as_pc_of (RTLabs_status ge) s1)::tl.
     2396#ge #fl0 #s10 #s20 *
     2397[ #s1 #s2 #EX #CL #CS
     2398| #s1 #s2 #EX #CL
     2399| #s1 #s2 #s3 #EX #CL #AF #tlr #CS
     2400| #fl #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal
     2401| #fl #s1 #s2 #s3 #EX #tal #CL #CS
     2402] whd in ⊢ (??(λ_.??%?)); % [ 2,4,6,8,10: % | *: skip ]
     2403qed.
     2404
     2405(* XXX move *)
     2406lemma step_not_final : ∀ge,s,tr,s'.
     2407  eval_statement ge s = Value … 〈tr,s'〉 →
     2408  RTLabs_is_final s = None ?.
     2409#ge #s #tr #s' #EX
     2410lapply (final_cannot_move ge s)
     2411cases (RTLabs_is_final s)
     2412[ // | #r #F cases (F ?) [ #m #E >E in EX; #EX destruct | % #E destruct ]
     2413qed.
     2414
     2415lemma tal_not_final : ∀ge,fl,s1,s2.
     2416  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
     2417  RTLabs_is_final (Ras_state … s1) = None ?.
     2418#ge #flx #s1x #s2x *
     2419[ #s1 #s2 * #tr * #EX #NX #CL #CS
     2420| #s1 #s2 * #tr * #EX #NX #CL
     2421| #s1 #s2 #s3 * #tr * #EX #NX #CL #AF #tlr #CS
     2422| #fl #s1 #s2 #s3 #s4 * #tr * #EX #NX #CL #AF #tlr #CS #tal
     2423| #fl #s1 #s2 #s3 * #tr * #EX #NX #tal #CL #CS
     2424] @(step_not_final … EX)
     2425qed.
     2426
     2427lemma State_not_callreturn : ∀f,fs,m,cl.
     2428  RTLabs_classify (State f fs m) = cl →
     2429  match cl with
     2430  [ cl_return ⇒ False
     2431  | cl_call ⇒ False
     2432  | _ ⇒ True
     2433  ].
     2434#f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?);
     2435cases (lookup_present … (next_ok f)) //
     2436qed.
     2437
     2438(* TODO: move *)
     2439lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
     2440  Exists S (λy. y = x) l →
     2441  x ∈ l.
     2442#S #x #l elim l
     2443[ //
     2444| #h #t #IH
     2445  normalize lapply (eqb_true … x h)
     2446  cases (x==h) *
     2447  [ #E #_ >(E (refl ??)) //
     2448  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
     2449            | #H @IH @H
     2450            ]
     2451  ]
     2452] qed.
     2453
     2454(* invert traces ending in a return *)
     2455
     2456lemma tal_return : ∀ge,fl,s1,s2.
     2457  as_classifier (RTLabs_status ge) s1 cl_return →
     2458  ∀tal: trace_any_label (RTLabs_status ge) fl s1 s2.
     2459  ∃EX,CL. fl = ends_with_ret ∧ tal ≃ tal_base_return (RTLabs_status ge) s1 s2 EX CL.
     2460#ge #flx #s1x #s2x #CL #tal @(trace_any_label_inv_ind … tal)
     2461[ #s1 #s2 #EX #CL' #CS #E1 #E2 #E3 #E4 destruct
     2462  whd in CL CL':(?%%); @⊥ >CL in CL'; * #E destruct
     2463| #s1 #s2 #EX #CL #E1 #E2 #E3 #E4 destruct
     2464  %{EX} %{CL} % %
     2465| #s1 #s2 #s3 #EX #CL' #AF #tlr #CS #E1 #E2 #E3 #E4 destruct @⊥
     2466  whd in CL CL'; >CL in CL'; #E destruct
     2467| #fl #s1 #s2 #s3 #s4 #EX #CL' #AF #tlr #CS #tal #E1 #E2 #E3 #_ @⊥ destruct
     2468  whd in CL CL'; >CL in CL'; #E destruct
     2469| #fl #s1 #s2 #s3 #EX #tal #CL' #CS #E1 #E2 #E3 #_ @⊥ destruct
     2470  whd in CL CL'; >CL in CL'; #E destruct
     2471] qed.
     2472
     2473let rec tal_pc_list_succs ge fl s1 s2
     2474  (tal: trace_any_label (RTLabs_status ge) fl s1 s2)
     2475  on tal : good_pc_list ge (state_fn … s1) (tal_pc_list (RTLabs_status ge) fl s1 s2 tal) ≝
     2476?.
     2477cases tal
     2478[ #s1' #s2' #EX #CL #CS whd in ⊢ (???%); @g_pc_end
     2479| #s1' #s2' #EX #CL @g_pc_end
     2480| #pre #start #final #EX #CL #AF #tlr #CS @g_pc_end
     2481| #fl' #pre #start #after #final #EX #CL #AF #tlr #CS #tal'
     2482  whd in ⊢ (???%); lapply (declassify_pc' … EX CL) * * [2: #ret ] * #fn2 #PC >PC
     2483  [ cases (pc_after_return … AF PC) #fn' * * #SF #SF' #PC'
     2484    lapply (tal_pc_list_succs … tal')
     2485    cases (tal_pc_list_start … tal')
     2486    #tl' #E >E >PC' >SF' #IH >SF @g_pc_cret @IH
     2487  | cases (pc_after_return … AF PC) >(tal_not_final … tal') #SF'
     2488    cases (SF' ?) %
     2489  ]
     2490| #fl' #pre #init #end #EX #tal' #CL #CS
     2491  whd in ⊢ (???%);
     2492  lapply (tal_pc_list_succs … tal')
     2493  cases (tal_pc_list_start … tal')
     2494  #tl' #E >E #IH
     2495  inversion (eval_preserves_ext … EX)
     2496  [ #ge' #f #f' #fs #m #m' * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #_ destruct
     2497    cases EX #tr * #EV #NX
     2498    cases (eval_successor … EV)
     2499    [ * #CL' cases (State_not_callreturn … CL')
     2500    | * #l * #AS #SC
     2501      @(g_pc_step … (lookup_present … (next_ok f)))
     2502      [ whd in ⊢ (??%?); cases M #FFP #M >FFP
     2503        whd in ⊢ (??%?); //
     2504      | whd in AS:(??%?); destruct @Exists_memb @SC
     2505      | assumption
     2506      ]
     2507    ]
     2508  | #ge' #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #_ destruct
     2509    cases EX #tr * #EV #NX
     2510    cases (eval_successor … EV)
     2511    [ * #CL' normalize in CL'; destruct
     2512    | * #l * #AS #SC
     2513      @(g_pc_call … (lookup_present … (next_ok f)))
     2514      [ whd in ⊢ (??%?); cases M #FFP #M >FFP
     2515        whd in ⊢ (??%?); //
     2516      | whd in AS:(??%?); destruct @Exists_memb @SC
     2517      | assumption
     2518      ]
     2519    ]
     2520  | #ge' #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #_ destruct
     2521    normalize in CL; destruct
     2522  | #ge' #f #fs #m #rtv #dst #m' #fn * [2: #fn' #S ] #M #M' #E1 #E2 #E3 #_ destruct
     2523    cases EX #tr * #EV #NX
     2524    cases (eval_successor … EV)
     2525    [ 1,3: * #CL' #SC
     2526      cases (tal_return … tal') [2,4: % ]
     2527      #EX' * #CL'' * #FL #TAL' destruct whd in E:(??%%); destruct
     2528      @(g_pc_return … (lookup_present … (next_ok f)))
     2529      [ 1,3: whd in ⊢ (??%?); cases M #FFP #M >FFP
     2530        whd in ⊢ (??%?); //
     2531      | 2,4: whd in AS:(??%?); destruct @SC
     2532      ]
     2533    | *: * #l * whd in ⊢ (??%% → ?); #E destruct
     2534    ]
     2535  | #ge' #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #_ destruct
     2536    normalize in CL; destruct
     2537  | #ge' #r #dst #m #M #M' #E1 #E2 #E3 #_ destruct
     2538    normalize in CL; destruct
     2539  ]
     2540] qed.
  • src/RTLabs/semantics.ma

    r2288 r2295  
    251251| 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')
    252252| to_ret : ∀ge,f,fs,m,rtv,dst,m'. state_rel ge (State f fs m) (Returnstate rtv dst fs m')
    253 | from_ret : ∀ge,f,fs,rtv,dst,f',m. frame_rel f f' → state_rel ge (Returnstate rtv dst (f::fs) m) (State f' fs m)
     253| 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)
    254254| finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r)
    255255.
Note: See TracChangeset for help on using the changeset viewer.