Changeset 2295 for src/RTLabs
 Timestamp:
 Aug 13, 2012, 12:21:30 PM (8 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2293 r2295 65 65 #hd #tl #H @H 66 66  #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 destruct67  #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct 68 68 cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 % 69 69 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ] … … 204 204 ]. 205 205 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 212 definition 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 206 238 definition RTLabs_status : genv → abstract_status ≝ 207 239 λge. … … 213 245 (λs,c. RTLabs_classify s = c) 214 246 (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) 228 248 (λs. RTLabs_is_final s ≠ None ?). 229 [ normalize in H; destruct230  normalize in H; destruct231  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 destruct234 ] qed.235 249 236 250 (* Allow us to move between the different notions of when a state is cost … … 683 697  #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #Hge * #H1 #H2 % /2/ 684 698  #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 % // 686 700  // 687 701 ] qed. … … 779 793 780 794 795 (* Extend our information about steps to states extended with the shadow stack. *) 796 797 inductive 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 806 lemma 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 810 generalize in match M'; M' 811 generalize in match M; M 812 generalize in match EX; 813 inversion (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 781 838 (* The preservation of (most of) the stack is useful to show as_after_return. 782 839 We do this by showing that during the execution of a function the lower stack … … 784 841 the identity of the next instruction to execute. 785 842 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. 789 845 *) 790 846 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)847 inductive 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) 795 851 . 796 852 797 inductive stack_preserved : trace_ends_with_ret → state → state → Prop ≝798  sp_normal : ∀fs, s1,s2.799 stack_of_state fss1 →800 stack_of_state fss2 →801 stack_preserved doesnt_end_with_ret s1 s2802  sp_finished : ∀s1,f,f',fs,m .853 inductive 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. 803 859 next f = next f' → 804 860 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) 812 868 . 813 869 814 870 discriminator list. 815 871 816 lemma stack_of_state_eq : ∀ fs,fs',s.817 stack_of_state fss →818 stack_of_state fs' s →819 fs = fs' .820 # fs0 #fs0' #s0 *821 [ #f #fs #m # H inversion H822 #a #b #c #d try #e try #g try #h try #i try #j destruct @refl823  #fd #args #dst #f #fs #m # H inversion H824 #a #b #c #d try #e try #g try #h try #i try #j destruct @refl825  #rtv #dst #fs #m # H inversion H826 #a #b #c #d try #e try #g try #h try #i try #j destruct @refl827 ] qed. 828 829 lemma stack_preserved_final : ∀ e,r,s.830 ¬stack_preserved e (Finalstate r) s.831 # e #r#s % #H inversion H832 [ #H184 #H185 #H186 # SOS #H188 #H189 #H190 #H191 #H192destruct833 inversion SOS #a #b #c #d #e #f try #g try #hdestruct834  #H194 #H195 #H196 #H197 #H198 #H199 #H200 # SOS #H201 #H202 #H203 #H204 destruct835 inversion SOS #a #b #c #d #e #f try #g try #h destruct836  #s' #r' # SOS #E1 #E2 #E3 #E4 destruct837 inversion SOS #a #b #c #d #e #f try #g try #h destruct838  #H24 #H25 #H26 #H27 #H28 #H29 #H30 #H31 #H32 destruct839 ] 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 H1846 [ #fs # s1' #s2' #S1 #S2 #E1 #E2 #E3 #E4 destruct872 lemma 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 885 lemma 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 897 lemma 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 847 903 #H2 inversion H2 848 [ #fs' # s1'' #s2'' #S1' #S2' #E1 #E2 #E3 #E4 destruct849 @(sp_normal fs) // <(stack_of_state_eq … S1' S2)//850  #s1'' #f #f' #fs' #m # N #F #S1' #E1 #E2 #E3 #E4 destruct851 @(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 destruct904 [ #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 854 910 inversion S2 855 [ #H34 #H35 #H36 #H37 #H38 #H39 destruct856  #fd' #args' #dst' #f #fs' #m' # E1 #E2 #E3 destruct857  #H41 #H42 #H43 #H44 #H45 #H46 #H47 destruct911 [ #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 858 914 ] 859 915 ] 860 916  #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 @⊥ 864 919 @(absurd … F) // 865 920 ] qed. 866 921 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 927 lemma 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 922 955  #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 964 lemma 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} % 968 qed. 969 970 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge. 943 971 ∀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 → 946 974 as_after_return (RTLabs_status ge) «s1,CL» s3. 947 #ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 # tr #CL #EV #S23975 #ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #CL #EV #S23 948 976 cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct 949 977 whd 950 978 inversion S23 951 979 [ #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 957 983 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 971 993 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 979 998 ] 980 999  #H128 #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 destruct … … 995 1014 cost_labelled : well_cost_labelled_state new_state; 996 1015 new_trace : T new_state; 997 stack_ok : stack_preserved ends start new_state;1016 stack_ok : stack_preserved ge ends start new_state; 998 1017 terminates : match (match ends with [ doesnt_end_with_ret ⇒ S depth  _ ⇒ depth ]) with 999 1018 [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭ … … 1023 1042 will_return_end … TM1 = will_return_end … TM2 → 1024 1043 T2 (new_state … r) → 1025 stack_preserved e s2 (new_state … r) →1044 stack_preserved ge e s2 (new_state … r) → 1026 1045 trace_result ge d e s2 t2 TM2 T2 l2 ≝ 1027 1046 λge,d,e,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP. … … 1052 1071 will_return_end … TM1 = will_return_end … TM2 → 1053 1072 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) → 1055 1074 sub_trace_result ge d s2 t2 TM2 T2 l2 ≝ 1056 1075 λge,d,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2,lGE,r,TME,trace,SP. … … 1246 1265 ] 1247 1266  @(will_return_return … CL TERMINATES) 1248  @(stack_preserved_ return … EV) //1267  @(stack_preserved_step ge start' … CL (eval_to_as_exec ge start' ?? EV)) 1249 1268  %{tr} %{EV} @refl 1250 1269  @(well_cost_labelled_state_step … EV) // 1251 1270  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)) 1253 1272  %{tr} %{EV} % 1254 1273  %1 whd @CL … … 1261 1280 #TM' * #_ #EQ' @EQ' 1262 1281 ] 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) 1264 1283  %{tr} %{EV} % 1265  @(RTLabs_after_call … next') [ 2: @EV  skip // ]1284  @(RTLabs_after_call … next') [ @eval_to_as_exec  // ] 1266 1285  @(cost_labelled … r) 1267 1286  skip … … 1271 1290  cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ 1272 1291 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  // ] 1274 1293  %{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) 1276 1295  @(cost_labelled … r) 1277 1296  cases r #H72 #H73 #H74 #H75 #HX * #HY * #GT #H78 … … 1291 1310 @(monotonic_le_times_r 3 … GT) 1292 1311  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)) 1294 1313  %{tr} %{EV} % 1295 1314  %2 whd @CL … … 1299 1318  @CL 1300 1319  %{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)) 1302 1321  @(well_cost_labelled_state_step … EV) // 1303 1322  %1 @CL … … 1354 1373 lemma eval_successor : ∀ge,f,fs,m,tr,s'. 1355 1374 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)) = [ ]) ∨ 1357 1376 ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (lookup_present … (f_graph (func f)) (next f) (next_ok f))). 1358 1377 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' … … 1377 1396  #l #El whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // @(nth_opt_Exists … El) 1378 1397 ]*) 1379  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 @refl1398  #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev whd in ⊢ (??%? → ?); #E destruct %1 % % 1380 1399 ] qed. 1381 1400 … … 1465 1484 RTLabs_cost s' = false → 1466 1485 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 H1486 #ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); lapply CL CL inversion H 1468 1487 [ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL) 1469 1488 #fn * #args * #dst * #stk * #m' #E destruct 1470 1489  #fd #args #dst #f #fs #m #n' #S #E1 #E2 #_ destruct 1471 1490 whd in S; #CL cases s' 1472 [ #f' #fs' #m' * #N #F#CS1491 [ #f' #fs' #m' * * #N #F #STK #CS 1473 1492 %1 whd 1474 1493 inversion S 1475 1494 [ #l #n #P #CS' #E1 #E2 #_ destruct @⊥ 1476 1495 change with (is_cost_label ?) in CS:(??%?); >N in P CS'; >F >CS #P * 1477  #l #n # B #E1 #E2 #_ destruct <N <F @B1496  #l #n #H #CS' #B #E1 #E2 #_ destruct <N <F @B 1478 1497 ] 1479 1498  #fd' #args' #dst' #fs' #m' * … … 1493 1512 [ #f #fs #m #m #FS #E1 #E2 #_ destruct 1494 1513 #EVAL cases (eval_successor … EVAL) 1495 [ /3/1514 [ * /3/ 1496 1515  * #l * #S1 #S2 #NC %2 1497 1516 (* … … 1507 1526 change with (RTLabs_cost (State (mk_frame H1 H7 lx LPx H5 H6) fs' m')) in CSx:(?%); 1508 1527 whd in S1:(??%?); destruct >NC in CSx; * 1509  whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 destruct @H731528  whd in S1:(??%?); destruct #H71 #H72 #H73 #H74 #H75 #H76 #H77 #H78 destruct @H75 1510 1529 ] 1511 1530  #ge0 #f0 #fs' #m0 #fd #args #f' #dst #F #b #FFP #E4 #E5 #E6 #_ destruct … … 1529 1548  #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 #H110 #H111 #H112 #H113 #H114 destruct 1530 1549  #H116 #H117 #H118 #H119 #H120 #H121 #H122 #H123 #H124 #H125 #H126 destruct 1531  #ge' #f' #fs' #rtv' #dst' #f'' #m' # F #E1 #E2 #E3 #_ destruct1550  #ge' #f' #fs' #rtv' #dst' #f'' #m' #N #F #E1 #E2 #E3 #_ destruct 1532 1551 %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 1536 1553 inversion F #func #locals #next #next_ok #sp #retdst #locals' #next' #next_ok' #E1 #E2 #_ destruct 1537 1554 inversion FS 1538 1555 [ #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:(?%); 1540 1557 >NC in CSx; * 1541  #lx #nx # H #E1x #E2x #_ destruct @H1558  #lx #nx #P #CS #H #E1x #E2x #_ destruct @H 1542 1559 ] 1543 1560  #H284 #H285 #H286 #H287 #H288 #H289 #H290 #H291 destruct … … 1588 1605  #ge' #f #fs #m #rtv #dst #m' #E1 #E2 #E3 #E4 destruct 1589 1606 whd in S ⊢ %; cases S // 1590  #ge' #f #fs #rtv #dst #f' #m # F #E1 #E2 #E3 #E4 destruct1607  #ge' #f #fs #rtv #dst #f' #m #N #F #E1 #E2 #E3 #E4 destruct 1591 1608 whd in S ⊢ %; inversion F #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 #H25 #H26 #H27 #H28 destruct @S 1592 1609  #ge' #r #dst #m #E1 #E2 #E3 #E4 destruct @I 1593 1610 ] qed. 1594 1611 1595 lemma soundly_labelled_state_preserved : ∀ s,s'.1596 stack_preserved ends_with_ret s s' →1612 lemma soundly_labelled_state_preserved : ∀ge,s,s'. 1613 stack_preserved ge ends_with_ret s s' → 1597 1614 soundly_labelled_state s → 1598 1615 soundly_labelled_state s'. 1599 # s0 #s0' #SP inversion SP1616 #ge #s0 #s0' #SP inversion SP 1600 1617 [ #H73 #H74 #H75 #H76 #H77 #H78 #H79 #H80 #H81 #H82 destruct 1601  #s1 #f #f' #fs #m # N #F #S1 #E1 #E2 #E3 #E4 destruct1618  #s1 #f #f' #fs #m #fn #S #M #N #F #S1 #E1 #E2 #E3 #E4 destruct 1602 1619 inversion S1 1603 [ #f1 #fs1 #m1 # E1 #E2 #E3destruct1620 [ #f1 #fs1 #m1 #fn1 #S1 #M1 #E1 #E2 #E3 #E4 destruct 1604 1621 * #_ #S whd in S; 1605 1622 inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 1606 1623 destruct @S 1607  #fd #args #dst #f1 #fs1 #m1 # E1 #E2 #E3destruct * #_ * #_ #S1624  #fd #args #dst #f1 #fs1 #m1 #fn1 #fn1' #S1 #M1 #E1 #E2 #E3 #E4 destruct * #_ * #_ #S 1608 1625 inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 1609 1626 destruct @S 1610  #rtv #dst #fs1 #m1 # E1 #E2 #E3destruct #S1627  #rtv #dst #fs1 #m1 #S1 #M1 #E1 #E2 #E3 #E4 destruct #S 1611 1628 inversion F #H96 #H97 #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 #H106 #H107 1612 1629 destruct @S … … 1750 1767  @(not_return_to_not_final … EV) >CL % #E destruct 1751 1768 ] 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)) // 1754 1771  @(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)) // 1756 1773  % [ /2/ 1757 1774  @(soundly_labelled_state_preserved … (stack_ok … tlr)) … … 1764 1781 inversion (stack_ok … tlr) 1765 1782 [ #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 @refl1767  #s1 #r # S #E1 #E2 #E3 #E4 TERMINATES destruct whd in S:(??%);next' s01783  #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 1768 1785 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct 1769 1786 inversion (eval_preserves … EV) … … 1771 1788 #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 TRACE_OK destruct 1772 1789 inversion S 1773 [ #f #fs0 #m # E1 #E2 #E3 destruct  *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130destruct ]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 ] 1774 1791 (* state_bound_on_steps_to_cost needs to know about the current stack frame, 1775 1792 so we can use it as a witness that at least one frame exists *) … … 1859 1876 ] qed. 1860 1877 1861 lemma after_the_initial_call_is_the_final_state : ∀ge,p,s1,tr,s2,s'. 1878 lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_state ge. 1879 as_execute (RTLabs_status ge) s1 s2 → 1862 1880 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' → 1865 1882 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 ⊢ (??%? → ?); 1867 1884 @bind_ok #m #_ 1868 1885 @bind_ok #b #_ 1869 1886 @bind_ok #f #_ 1870 1887 #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 #_ destruct1888 #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 1873 1890 inversion SP 1874 [ 3: #s1 #r # S #_ #_ #_ #_% #E whd in E:(??%?); destruct1875  *: #H28 #H29 #H30 #H31 #H32 #H33 #H34 #H35 #H36 try #H38 try #H39 try #H40 destruct1876 inversion H3 5 #H61 #H62 #H63 #H64 #H65 #H66 try #H68 try #H69 try #H70destruct1891 [ 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 1877 1894 ] 1878  *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 destruct1895  *: #H98 #H99 #H100 #H101 #H102 #H103 #H104 #H105 try #H106 try #H107 try #H108 try #H109 try #H110 try #H111 try #H112 destruct 1879 1896 ] qed. 1880 1897 … … 1931 1948 cases FINAL #E @E @refl 1932 1949  %{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) ] 1935 1952  @(well_cost_labelled_state_step … EV) // 1936 1953  @(well_cost_labelled_call … EV) // … … 2259 2276 : equal_flat_traces … (flat_trace_of_whole_program … str) tr ≝ ?. 2260 2277 @flat_traces_are_determined_by_starting_point 2261 qed. 2278 qed. 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 2285 definition RTLabs_pc_lookup : ∀ge. RTLabs_pc → option statement ≝ 2286 λge,pc. 2287 match 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 2294 definition 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 2300 inductive 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 2321 definition 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 2330 lemma 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 2341 cases 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 ] 2349 cases 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 2362 lemma 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 2380 lemma 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} % ] 2392 qed. 2393 2394 lemma 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 ] 2403 qed. 2404 2405 (* XXX move *) 2406 lemma 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 2410 lapply (final_cannot_move ge s) 2411 cases (RTLabs_is_final s) 2412 [ //  #r #F cases (F ?) [ #m #E >E in EX; #EX destruct  % #E destruct ] 2413 qed. 2414 2415 lemma 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) 2425 qed. 2426 2427 lemma 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 ?); 2435 cases (lookup_present … (next_ok f)) // 2436 qed. 2437 2438 (* TODO: move *) 2439 lemma 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 2456 lemma 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 2473 let 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 ?. 2477 cases 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 251 251  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') 252 252  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) 254 254  finish : ∀ge,r,dst,m. state_rel ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) (Finalstate r) 255 255 .
Note: See TracChangeset
for help on using the changeset viewer.