 Timestamp:
 Nov 28, 2012, 12:52:12 PM (7 years ago)
 Location:
 src/RTLabs
 Files:

 1 added
 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2439 r2499 1 1 2 include "RTLabs/ semantics.ma".2 include "RTLabs/abstract.ma". 3 3 include "RTLabs/CostSpec.ma". 4 4 include "RTLabs/CostMisc.ma". 5 include "common/StructuredTraces.ma".6 5 include "common/Executions.ma". 7 include "utilities/deqsets.ma".8 6 include "utilities/listb.ma". 9 7 10 discriminator status_class.11 12 (* We augment states with a stack of function blocks (i.e. pointers) so that we13 can make sensible "program counters" for the abstract state definition, along14 with a proof that we will get the correct code when we do the lookup (which15 is done to find cost labels given a pc).16 17 Adding them to the semantics is an alternative, more direct approach.18 However, it makes animating the semantics extremely difficult, because it19 is hard to avoid normalising and displaying irrelevant parts of the global20 environment and proofs.21 22 We use blocks rather than identifiers because the global environments go23 24 identifier → block → definition25 26 and we'd have to introduce backwards lookups to find identifiers for27 function pointers.28 *)29 30 definition Ras_Fn_Match ≝31 λge,state,fn_stack.32 match state with33 [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack34  Callstate fd _ _ fs _ ⇒35 match fn_stack with36 [ nil ⇒ False37  cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧38 All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t39 ]40  Returnstate _ _ fs _ ⇒41 All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack42  Finalstate _ ⇒ fn_stack = [ ]43 ].44 45 record RTLabs_state (ge:genv) : Type[0] ≝ {46 Ras_state :> state;47 Ras_fn_stack : list block;48 Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack49 }.50 51 (* Given a plain step of the RTLabs semantics, give the next state along with52 the shadow stack of function block numbers. Carefully defined so that the53 coercion back to the plain state always reduces. *)54 definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t.55 eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝56 λge,s,s',t,EX. mk_RTLabs_state ge s'57 (match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → ? with [ State _ _ _ ⇒ λ_. Ras_fn_stack … s  Callstate _ _ _ _ _ ⇒ λEX. func_block_of_exec … EX::Ras_fn_stack … s  Returnstate _ _ _ _ ⇒ λ_. tail … (Ras_fn_stack … s)  Finalstate _ ⇒ λ_. [ ] ] EX)58 ?.59 cases s' in EX ⊢ %;60 [ s' #f #fs #m cases s s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX)61 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct62 whd cases stk in mtc ⊢ %; [ * ]63 #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //64  @M2 ]65  #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct66  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct67 whd cases stk in mtc ⊢ %; [ * ]68 #hd #tl #H @H69  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct70  #ge' #f0 #fs0 #rtv #dst #f' #m0 #N #F #E1 #E2 #E3 #E4 destruct71 cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 %72 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ]73  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct74 ]75  s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP76 whd % // func_block cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX)77 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct78  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct79 cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 %80 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ]81  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct82  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct83  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct84  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct85 ]86  s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX)87 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct88  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct89  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct90  #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct91 cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H92  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct93  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct94 ]95  #r #EX whd @refl96 ] qed.97 98 99 (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps100 will be added later (LTL → LIN). *)101 102 definition RTLabs_classify : state → status_class ≝103 λs. match s with104 [ State f _ _ ⇒105 match lookup_present ?? (f_graph (func f)) (next f) (next_ok f) with106 [ St_cond _ _ _ ⇒ cl_jump107 (*  St_jumptable _ _ ⇒ cl_jump*)108  _ ⇒ cl_other109 ]110  Callstate _ _ _ _ _ ⇒ cl_call111  Returnstate _ _ _ _ ⇒ cl_return112  Finalstate _ ⇒ cl_other113 ].114 115 (* As with is_cost_label/cost_label_of we define a boolean function as well116 as one which extracts the cost label so that we can use it in hypotheses117 without naming the cost label. *)118 119 definition RTLabs_cost : state → bool ≝120 λs. match s with121 [ State f fs m ⇒122 is_cost_label (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))123  _ ⇒ false124 ].125 126 definition RTLabs_cost_label : state → option costlabel ≝127 λs. match s with128 [ State f fs m ⇒129 cost_label_of (lookup_present ?? (f_graph (func f)) (next f) (next_ok f))130  _ ⇒ None ?131 ].132 133 (* "Program counters" need to identify the current state, either as a pair of134 the function and current instruction, or the function being entered or135 left. Functions are identified by their function pointer block because136 this avoids introducing functions to map back pointers to function ids using137 the global environment. (See the comment at the start of this file, too.)138 139 Calls also get the caller's instruction label (or None for the initial call)140 so that we can distinguish different calls. This is used only for the141 t.*_unrepeating property, which includes the pc for call states.142 *)143 144 inductive RTLabs_pc : Type[0] ≝145  rapc_state : block → label → RTLabs_pc146  rapc_call : option label → block → RTLabs_pc147  rapc_ret : option block → RTLabs_pc148  rapc_fin : RTLabs_pc149 .150 151 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝152 λx,y. match x with153 [ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2  _ ⇒ false ]154  rapc_call o1 b1 ⇒ match y with [ rapc_call o2 b2 ⇒155 eqb ? o1 o2156 ∧ eq_block b1 b2157  _ ⇒ false ]158  rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eqb ? b1 b2  _ ⇒ false ]159  rapc_fin ⇒ match y with [ rapc_fin ⇒ true  _ ⇒ false ]160 ].161 162 definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?.163 whd in match RTLabs_pc_eq;164 * [ #b1 #l1  #bl1 #b1  #ob1  ]165 * [ 1,5,9,13: #b2 #l2  2,6,10,14: #bl2 #b2  3,7,11,15: #ob2  *: ]166 normalize nodelta167 [ @eq_block_elim [ #E destruct  * #NE ] ]168 [ @eq_identifier_elim [ #E destruct  *: * #NE ] ]169 [ 8,13: @eqb_elim [ 1,3: #E destruct  *: * #NE ] ]170 [ @eq_block_elim [ #E destruct  * #NE ] ]171 normalize % #E destruct try (cases (NE (refl ??))) @refl172 qed.173 174 definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝175 λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒176 match s' return λs'. Ras_Fn_Match ? s' ? → ? with177 [ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_state b (next … f) ]178  Callstate _ _ _ fs _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_call (match fs with [ nil ⇒ None ?  cons f _ ⇒ Some ? (next f) ]) b ]179  Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?)  cons b _ ⇒ λ_. rapc_ret (Some ? b) ]180  Finalstate _ ⇒ λmtc. rapc_fin181 ] mtc0 ].182 whd in mtc; cases mtc183 qed.184 185 definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝186 λge,pc.187 match pc with188 [ rapc_state b l ⇒189 match find_funct_ptr … ge b with [ None ⇒ None ?  Some fd ⇒190 match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s  _ ⇒ None ? ]  _ ⇒ None ? ] ]191  _ ⇒ None ?192 ].193 194 (* After returning from a function, we should be ready to execute the next195 instruction of the caller and the shadow stack should be preserved (we have196 to take the top element off because the Callstate includes the callee); *or*197 we're in the final state.198 *)199 200 definition RTLabs_after_return : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → RTLabs_state ge → Prop ≝201 λge,s,s'.202 match s with203 [ mk_Sig s p ⇒204 match s return λs. RTLabs_classify s = cl_call → ? with205 [ Callstate fd args dst stk m ⇒206 λ_. match s' with207 [ State f fs m ⇒ match stk with [ nil ⇒ False  cons h t ⇒208 next h = next f ∧209 f_graph (func h) = f_graph (func f) ∧210 match Ras_fn_stack … s with [ nil ⇒ False  cons _ stk' ⇒ stk' = Ras_fn_stack … s' ] ]211  Finalstate r ⇒ stk = [ ]212  _ ⇒ False213 ]214  State f fs m ⇒ λH.⊥215  _ ⇒ λH.⊥216 ] p217 ].218 [ whd in H:(??%?);219 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;220 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct221  normalize in H; destruct222  normalize in H; destruct223 ] qed.224 225 definition RTLabs_call_ident : ∀ge. (Σs:RTLabs_state ge. RTLabs_classify s = cl_call) → ident ≝226 λge,s.227 match s with228 [ mk_Sig s p ⇒229 match s return λs':RTLabs_state ge. RTLabs_classify s' = cl_call → ident with230 [ mk_RTLabs_state s' stk mtc0 ⇒231 match s' return λs'. Ras_Fn_Match ? s' ? → RTLabs_classify s' = cl_call → ident with232 [ Callstate fd _ _ _ _ ⇒233 match stk return λstk. Ras_Fn_Match ?? stk → ? → ident with234 [ nil ⇒ λmtc. ⊥235  cons b _ ⇒ λmtc. λX. symbol_of_function_block … ge b ?236 ]237  State f _ _ ⇒ λ_. λH.⊥238  _ ⇒ λ_. λH.⊥239 ] mtc0240 ] p241 ].242 [ whd in H:(??%?);243 cases (lookup_present LabelTag statement (f_graph (func f)) (next f) (next_ok f)) in H;244 normalize try #a try #b try #c try #d try #e try #g try #h try #i try #j destruct245  4,5: normalize in H; destruct (H)246  cases mtc247  cases mtc #FFP #_ >FFP % #E destruct (E)248 ] qed.249 250 251 definition RTLabs_status : genv → abstract_status ≝252 λge.253 mk_abstract_status254 (RTLabs_state ge)255 (λs,s'. ∃t,EX. next_state ge s s' t EX = s')256 RTLabs_deqset257 (RTLabs_state_to_pc ge)258 RTLabs_classify259 (RTLabs_pc_to_cost_label ge)260 (RTLabs_after_return ge)261 (λs. RTLabs_is_final s ≠ None ?)262 (RTLabs_call_ident ge).263 8 264 9 (* Allow us to move between the different notions of when a state is cost 265 10 labelled. *) 266 11 267 lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ state ge.12 lemma RTLabs_costed : ∀ge. ∀s:RTLabs_ext_state ge. 268 13 RTLabs_cost s = true ↔ 269 14 as_costed (RTLabs_status ge) s. … … 275 20 cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2 276 21 whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?))); 277 >(lookup_lookup_present … nok)278 whd in ⊢ (?(??%?)(?(??%?)));22 whd in ⊢ (?(??%?)?); change with (lookup_present ?????) in match (next_instruction ?); 23 >(lookup_lookup_present … nok) whd in ⊢ (?(??%?)(?(??%?))); 279 24 % cases (lookup_present ?? (f_graph func) ??) normalize 280 25 #A try #B try #C try #D try #E try #F try #G try #H try #G destruct … … 299 44 ] qed. 300 45 301 lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ state ge.46 lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_ext_state ge. 302 47 RTLabs_cost s = false → 303 48 ¬ as_costed (RTLabs_status ge) s. … … 718 463 RTLabs_classify s = cl_jump → 719 464 ∃f,fs,m. s = State f fs m ∧ 720 let stmt ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f) in 721 (∃r,l1,l2. stmt = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*). 465 (∃r,l1,l2. next_instruction f = St_cond r l1 l2) (*∨ (∃r,ls. stmt = St_jumptable r ls)*). 722 466 * 723 467 [ #f #fs #m #E 724 468 %{f} %{fs} %{m} % 725 469 [ @refl 726  whd in E:(??%?); cases ( lookup_present ? statement ???) in E ⊢ %;470  whd in E:(??%?); cases (next_instruction f) in E ⊢ %; 727 471 try (normalize try #A try #B try #C try #D try #F try #G try #H try #I try #J destruct) 728 472 (*[ %1*) %{A} %{B} %{C} @refl … … 751 495 lapply (Hbody (next fr) (next_ok fr)) 752 496 generalize in ⊢ (?(???%) → ?); 497 change with (next_instruction fr) in match (lookup_present ?????); 753 498 >Estmt #LP' #WS 754 499 cases (andb_Prop_true … WS) #H1 #H2 [ @H1  @H2 ] … … 777 522 ∃fd,args,dst,stk,m. s = Callstate fd args dst stk m. 778 523 * [ #f #fs #m whd in ⊢ (??%? → ?); 779 cases ( lookup_present … (next f) (next_ok f)) normalize524 cases (next_instruction f) normalize 780 525 try #A try #B try #C try #D try #E try #F try #G try #I try #J destruct 781 526  #fd #args #dst #stk #m #E %{fd} %{args} %{dst} %{stk} %{m} @refl … … 808 553 (* Extend our information about steps to states extended with the shadow stack. *) 809 554 810 inductive state_rel_ext : ∀ge:genv. RTLabs_ state ge → RTLabs_state ge → Prop ≝811  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')812  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')813  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')814  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')815  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')816  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')555 inductive state_rel_ext : ∀ge:genv. RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝ 556  xnormal : ∀ge,f,f',fs,m,m',S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (State f' fs m') S M') 557  xto_call : ∀ge,f,fs,m,fd,args,f',dst,fn,S,M,M'. frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) S M) (mk_RTLabs_ext_state ge (Callstate fd args dst (f'::fs) m) (fn::S) M') 558  xfrom_call : ∀ge,fn,locals,next,nok,sp,fs,m,args,dst,m',S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Callstate (Internal ? fn) args dst fs m) S M) (mk_RTLabs_ext_state ge (State (mk_frame fn locals next nok sp dst) fs m') S M') 559  xto_ret : ∀ge,f,fs,m,rtv,dst,m',fn,S,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m') S M') 560  xfrom_ret : ∀ge,f,fs,rtv,dst,f',m,S,M,M'. next f = next f' → frame_rel f f' → state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate rtv dst (f::fs) m) S M) (mk_RTLabs_ext_state ge (State f' fs m) S M') 561  xfinish : ∀ge,r,dst,m,M,M'. state_rel_ext ge (mk_RTLabs_ext_state ge (Returnstate (Some ? (Vint I32 r)) dst [ ] m) [ ] M) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M') 817 562 . 818 563 … … 858 603 *) 859 604 860 inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ state ge → Prop ≝861  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)862  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)863  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)605 inductive stack_of_state (ge:genv) : list frame → list block → RTLabs_ext_state ge → Prop ≝ 606  sos_State : ∀f,fs,m,fn,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) 607  sos_Callstate : ∀fd,args,dst,f,fs,m,fn,fn',S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Callstate fd args dst (f::fs) m) (fn::fn'::S) M) 608  sos_Returnstate : ∀rtv,dst,fs,m,S,M. stack_of_state ge fs S (mk_RTLabs_ext_state ge (Returnstate rtv dst fs m) S M) 864 609 . 865 610 866 inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ state ge → RTLabs_state ge → Prop ≝611 inductive stack_preserved (ge:genv) : trace_ends_with_ret → RTLabs_ext_state ge → RTLabs_ext_state ge → Prop ≝ 867 612  sp_normal : ∀fs,S,s1,s2. 868 613 stack_of_state ge fs S s1 → … … 873 618 frame_rel f f' → 874 619 stack_of_state ge (f::fs) (fn::S) s1 → 875 stack_preserved ge ends_with_ret s1 (mk_RTLabs_ state ge (State f' fs m) (fn::S) M)620 stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (State f' fs m) (fn::S) M) 876 621  sp_stop : ∀s1,r,M. 877 622 stack_of_state ge [ ] [ ] s1 → 878 stack_preserved ge ends_with_ret s1 (mk_RTLabs_ state ge (Finalstate r) [ ] M)623 stack_preserved ge ends_with_ret s1 (mk_RTLabs_ext_state ge (Finalstate r) [ ] M) 879 624  sp_top : ∀fd,args,dst,m,r,fn,M1,M2. 880 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)625 stack_preserved ge doesnt_end_with_ret (mk_RTLabs_ext_state ge (Callstate fd args dst [ ] m) [fn] M1) (mk_RTLabs_ext_state ge (Finalstate r) [ ] M2) 881 626 . 882 627 … … 897 642 898 643 lemma stack_preserved_final : ∀ge,e,r,S,M,s. 899 ¬stack_preserved ge e (mk_RTLabs_ state ge (Finalstate r) S M) s.644 ¬stack_preserved ge e (mk_RTLabs_ext_state ge (Finalstate r) S M) s. 900 645 #ge #e #r #S #M #s % #H inversion H 901 646 [ #H184 #H185 #H186 #H188 #SOS #H189 #H190 #H191 #H192 #HA destruct … … 938 683 returning. *) 939 684 940 lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ state ge.∀cl.685 lemma stack_preserved_step : ∀ge.∀s1,s2:RTLabs_ext_state ge.∀cl. 941 686 RTLabs_classify s1 = cl → 942 687 as_execute (RTLabs_status ge) s1 s2 → … … 949 694 #ge0 #s10 #s20 #cl #CL <CL #EX inversion (eval_preserves_ext … EX) 950 695 [ #ge #f #f' #fs #m #m' * [*] #fn #S #M #M' #F #E1 #E2 #E3 #E4 destruct 951 whd in match (RTLabs_classify ?); cases ( lookup_present ???? (next_ok ?)) normalize /2/696 whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/ 952 697  #ge #f #fs #m #fd #args #f' #dst #fn * [*] #fn' #S #M #M' #F #E1 #E2 #E3 #E4 953 whd in match (RTLabs_classify ?); cases ( lookup_present ???? (next_ok ?)) normalize /2/698 whd in match (RTLabs_classify ?); cases (next_instruction f) normalize /2/ 954 699  #ge #fn #locals #next #nok #sp #fs #m #args #dst #m' #S #M #M' #E1 #E2 #E3 #E4 destruct 955 700 * #s3 #S3 #M3 #SP inversion SP … … 969 714 ] 970 715  #ge #f #fs #m #rtv #dst #m' #fn #S #M #M' #E1 #E2 #E3 #E4 destruct 971 whd in match (RTLabs_classify ?); cases ( lookup_present ???? (next_ok ?)) /2/716 whd in match (RTLabs_classify ?); cases (next_instruction f) /2/ 972 717  #ge #f #fs #rtv #dst #f' #m #S #M #M' #N #F #E1 #E2 #E3 #E4 destruct whd 973 718 cases S in M M' ⊢ %; [*] #fn #S' #M #M' @(sp_finished … F) // … … 975 720 ] qed. 976 721 977 lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ state ge.∀s2,tr.722 lemma eval_to_as_exec : ∀ge.∀s1:RTLabs_ext_state ge.∀s2,tr. 978 723 ∀EV:eval_statement ge s1 = Value … 〈tr,s2〉. 979 724 as_execute (RTLabs_status ge) s1 (next_state ge s1 s2 tr EV). … … 981 726 qed. 982 727 983 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ state ge.728 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_ext_state ge. 984 729 ∀CL : RTLabs_classify s1 = cl_call. 985 730 as_execute (RTLabs_status ge) s1 s2 → … … 1019 764 of the termination proof is respected. *) 1020 765 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) 1021 (start:RTLabs_ state ge) (full:flat_trace io_out io_in ge start)766 (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start) 1022 767 (original_terminates: will_return ge depth start full) 1023 (T:RTLabs_ state ge → Type[0]) (limit:nat) : Type[0] ≝768 (T:RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝ 1024 769 { 1025 new_state : RTLabs_ state ge;770 new_state : RTLabs_ext_state ge; 1026 771 remainder : flat_trace io_out io_in ge new_state; 1027 772 cost_labelled : well_cost_labelled_state new_state; … … 1039 784 encountering a label. *) 1040 785 record sub_trace_result (ge:genv) (depth:nat) 1041 (start:RTLabs_ state ge) (full:flat_trace io_out io_in ge start)786 (start:RTLabs_ext_state ge) (full:flat_trace io_out io_in ge start) 1042 787 (original_terminates: will_return ge depth start full) 1043 (T:trace_ends_with_ret → RTLabs_ state ge → Type[0]) (limit:nat) : Type[0] ≝788 (T:trace_ends_with_ret → RTLabs_ext_state ge → Type[0]) (limit:nat) : Type[0] ≝ 1044 789 { 1045 790 ends : trace_ends_with_ret; … … 1051 796 the size of the termination proof might need to be relaxed, too. *) 1052 797 1053 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →798 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → 1054 799 ∀r:trace_result ge d e s1 t1 TM1 T1 l1. 1055 800 will_return_end … TM1 = will_return_end … TM2 → … … 1080 825 ] qed. 1081 826 1082 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →827 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_ext_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → 1083 828 ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1. 1084 829 will_return_end … TM1 = will_return_end … TM2 → … … 1094 839 definition myge : nat → nat → Prop ≝ ge. 1095 840 1096 let rec make_label_return ge depth (s:RTLabs_ state ge)841 let rec make_label_return ge depth (s:RTLabs_ext_state ge) 1097 842 (trace: flat_trace io_out io_in ge s) 1098 843 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1135 880 1136 881 1137 and make_label_label ge depth (s:RTLabs_ state ge)882 and make_label_label ge depth (s:RTLabs_ext_state ge) 1138 883 (trace: flat_trace io_out io_in ge s) 1139 884 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1158 903 1159 904 1160 and make_any_label ge depth (s0:RTLabs_ state ge)905 and make_any_label ge depth (s0:RTLabs_ext_state ge) 1161 906 (trace: flat_trace io_out io_in ge s0) 1162 907 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1172 917 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 1173 918  S TIME ⇒ λTERMINATES_IN_TIME. 1174 match s0 return λs:RTLabs_ state ge. ∀trace:flat_trace io_out io_in ge s.919 match s0 return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. 1175 920 well_cost_labelled_state s → 1176 921 ∀TM:will_return ??? trace. 1177 922 myge ? (times 3 (will_return_length ??? trace TM)) → 1178 923 sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) 1179 with [ mk_RTLabs_ state s stk mtc0 ⇒ λtrace.924 with [ mk_RTLabs_ext_state s stk mtc0 ⇒ λtrace. 1180 925 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk. 1181 926 well_cost_labelled_state s → 1182 927 ∀TM:will_return ??? trace. 1183 928 myge ? (times 3 (will_return_length ??? trace TM)) → 1184 sub_trace_result ge depth (mk_RTLabs_ state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_state ge s stk mtc)) (will_return_length … TM) with929 sub_trace_result ge depth (mk_RTLabs_ext_state ge s stk mtc) trace TM (λends. trace_any_label (RTLabs_status ge) ends (mk_RTLabs_ext_state ge s stk mtc)) (will_return_length … TM) with 1185 930 [ ft_stop st FINAL ⇒ 1186 931 λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ 1187 932 1188 933  ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 1189 let start' ≝ mk_RTLabs_ state ge start stk mtc in934 let start' ≝ mk_RTLabs_ext_state ge start stk mtc in 1190 935 let next' ≝ next_state ? start' ?? EV in 1191 936 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with … … 1342 1087 (* We can initialise TIME with a suitably large value based on the length of the 1343 1088 termination proof. *) 1344 let rec make_label_return' ge depth (s:RTLabs_ state ge)1089 let rec make_label_return' ge depth (s:RTLabs_ext_state ge) 1345 1090 (trace: flat_trace io_out io_in ge s) 1346 1091 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1386 1131 lemma eval_successor : ∀ge,f,fs,m,tr,s'. 1387 1132 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 1388 (RTLabs_classify s' = cl_return ∧ successors ( lookup_present … (f_graph (func f)) (next f) (next_ok f)) = [ ]) ∨1389 ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors ( lookup_present … (f_graph (func f)) (next f) (next_ok f))).1133 (RTLabs_classify s' = cl_return ∧ successors (next_instruction f) = [ ]) ∨ 1134 ∃l. actual_successor s' = Some ? l ∧ Exists ? (λl0. l0 = l) (successors (next_instruction f)). 1390 1135 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' 1391 1136 whd in ⊢ (??%? → ?); 1392 generalize in ⊢ (??(?%)? → ?); cases ( lookup_present ??? next next_ok)1137 generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?) 1393 1138 [ #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // 1394 1139  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct %2 %{l} % // % // … … 1491 1236 lemma eval_steps : ∀ge,f,fs,m,tr,s'. 1492 1237 eval_statement ge (State f fs m) = Value ??? 〈tr,s'〉 → 1493 steps_for_statement ( lookup_present ?? (f_graph (func f)) (next f) (next_ok f)) =1238 steps_for_statement (next_instruction f) = 1494 1239 match s' with [ State _ _ _ ⇒ 1  Callstate _ _ _ _ _ ⇒ 2  Returnstate _ _ _ _ ⇒ 2  Finalstate _ ⇒ 1 ]. 1495 1240 #ge * #func #locals #next #next_ok #sp #dst #fs #m #tr #s' 1496 1241 whd in ⊢ (??%? → ?); 1497 generalize in ⊢ (??(?%)? → ?); cases ( lookup_present ??? next next_ok)1242 generalize in ⊢ (??(?%)? → ?); cases (next_instruction ?) 1498 1243 [ #l #LP whd in ⊢ (??%? → ?); #E destruct @refl 1499 1244  #cl #l #LP whd in ⊢ (??%? → ?); #E destruct @refl … … 1517 1262 ] qed. 1518 1263 1519 lemma bound_after_call : ∀ge.∀s,s':RTLabs_ state ge.∀n.1264 lemma bound_after_call : ∀ge.∀s,s':RTLabs_ext_state ge.∀n. 1520 1265 state_bound_on_steps_to_cost s (S n) → 1521 1266 ∀CL:RTLabs_classify s = cl_call. … … 1676 1421 use the fact that the trace is soundly labelled to achieve this. *) 1677 1422 1678 record remainder_ok (ge:genv) (s:RTLabs_ state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {1423 record remainder_ok (ge:genv) (s:RTLabs_ext_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ { 1679 1424 ro_well_cost_labelled: well_cost_labelled_state s; 1680 1425 ro_soundly_labelled: soundly_labelled_state s; … … 1683 1428 }. 1684 1429 1685 inductive finite_prefix (ge:genv) : RTLabs_ state ge → Prop ≝1686  fp_tal : ∀s,s':RTLabs_ state ge.1430 inductive finite_prefix (ge:genv) : RTLabs_ext_state ge → Prop ≝ 1431  fp_tal : ∀s,s':RTLabs_ext_state ge. 1687 1432 trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → 1688 1433 ∀t:flat_trace io_out io_in ge s'. 1689 1434 remainder_ok ge s' t → 1690 1435 finite_prefix ge s 1691  fp_tac : ∀s1,s2,s3:RTLabs_ state ge.1436  fp_tac : ∀s1,s2,s3:RTLabs_ext_state ge. 1692 1437 trace_any_call (RTLabs_status ge) s1 s2 → 1693 1438 well_cost_labelled_state s2 → … … 1698 1443 . 1699 1444 1700 definition fp_add_default : ∀ge. ∀s,s':RTLabs_ state ge.1445 definition fp_add_default : ∀ge. ∀s,s':RTLabs_ext_state ge. 1701 1446 RTLabs_classify s = cl_other → 1702 1447 finite_prefix ge s' → … … 1714 1459 ]. 1715 1460 1716 definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ state ge.1461 definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_ext_state ge. 1717 1462 as_execute (RTLabs_status ge) s s1 → 1718 1463 ∀CALL:RTLabs_classify s = cl_call. … … 1745 1490 inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). 1746 1491 1747 let rec finite_segment ge (s:RTLabs_ state ge) n trace1492 let rec finite_segment ge (s:RTLabs_ext_state ge) n trace 1748 1493 (ORACLE: termination_oracle) 1749 1494 (TRACE_OK: remainder_ok ge s trace) … … 1755 1500 [ O ⇒ λLABEL_LIMIT. ⊥ 1756 1501  S n' ⇒ 1757 match s return λs:RTLabs_ state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace'.1758 match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_ state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_state ge s ? mtc) with1502 match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with [ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace'. 1503 match trace' return λs:state.λtrace:flat_trace io_out io_in ge s. ∀mtc:Ras_Fn_Match ge s stk. remainder_ok ge (mk_RTLabs_ext_state ge s ? mtc) trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge (mk_RTLabs_ext_state ge s ? mtc) with 1759 1504 [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥ 1760 1505  ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT. 1761 let start' ≝ mk_RTLabs_ state ge start stk mtc in1506 let start' ≝ mk_RTLabs_ext_state ge start stk mtc in 1762 1507 let next' ≝ next_state ge start' next tr EV in 1763 1508 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with … … 1879 1624 *) 1880 1625 1881 let corec make_label_diverges ge (s:RTLabs_ state ge)1626 let corec make_label_diverges ge (s:RTLabs_ext_state ge) 1882 1627 (trace: flat_trace io_out io_in ge s) 1883 1628 (ORACLE: termination_oracle) … … 1890 1635 [ ex_intro n B ⇒ 1891 1636 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B 1892 return λs:RTLabs_ state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s1637 return λs:RTLabs_ext_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s 1893 1638 with 1894 1639 [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL. … … 1916 1661 ] qed. 1917 1662 1918 lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ state ge.1663 lemma after_the_initial_call_is_the_final_state : ∀ge,p.∀s1,s2,s':RTLabs_ext_state ge. 1919 1664 as_execute (RTLabs_status ge) s1 s2 → 1920 1665 make_initial_state p = OK ? s1 → … … 1947 1692 qed. 1948 1693 1949 let rec whole_structured_trace_exists ge p (s:RTLabs_ state ge)1694 let rec whole_structured_trace_exists ge p (s:RTLabs_ext_state ge) 1950 1695 (ORACLE: termination_oracle) 1951 1696 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1956 1701 ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s. 1957 1702 trace_whole_program_exists (RTLabs_status ge) s ≝ 1958 match s return λs:RTLabs_ state ge. ∀trace:flat_trace io_out io_in ge s.1703 match s return λs:RTLabs_ext_state ge. ∀trace:flat_trace io_out io_in ge s. 1959 1704 make_initial_state p = OK ? s → 1960 1705 well_cost_labelled_state s → 1961 1706 soundly_labelled_state s → 1962 1707 trace_whole_program_exists (RTLabs_status ge) s with 1963 [ mk_RTLabs_ state s0 stk mtc0 ⇒ λtrace.1708 [ mk_RTLabs_ext_state s0 stk mtc0 ⇒ λtrace. 1964 1709 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk. 1965 1710 make_initial_state p = OK state s → 1966 1711 well_cost_labelled_state s → 1967 1712 soundly_labelled_state s → 1968 trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ state ge s stk mtc) with1713 trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_ext_state ge s stk mtc) with 1969 1714 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED. 1970 1715 let IS_CALL ≝ initial_state_is_call … INITIAL in 1971 let s' ≝ mk_RTLabs_ state ge s stk mtc in1716 let s' ≝ mk_RTLabs_ext_state ge s stk mtc in 1972 1717 let next' ≝ next_state ge s' next tr EV in 1973 1718 match ORACLE ge O next trace' with … … 2014 1759 qed. 2015 1760 2016 definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ state (make_global p) ≝2017 λp,s,I. mk_RTLabs_ state (make_global p) s [init_state_is p s I] ?.1761 definition Ras_state_initial : ∀p,s. make_initial_state p = OK ? s → RTLabs_ext_state (make_global p) ≝ 1762 λp,s,I. mk_RTLabs_ext_state (make_global p) s [init_state_is p s I] ?. 2018 1763 cases (init_state_is p s I) #b 2019 1764 cases s … … 2083 1828 2084 1829 2085 lemma simplify_exec : ∀ge.∀s,s':RTLabs_ state ge.1830 lemma simplify_exec : ∀ge.∀s,s':RTLabs_ext_state ge. 2086 1831 as_execute (RTLabs_status ge) s s' → 2087 1832 ∃tr. eval_statement ge s = Value … 〈tr,s'〉. … … 2103 1848 ] qed. 2104 1849 2105 let rec deprop_as_execute ge (s,s':RTLabs_ state ge)1850 let rec deprop_as_execute ge (s,s':RTLabs_ext_state ge) 2106 1851 (X:as_execute (RTLabs_status ge) s s') 2107 1852 : Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝ … … 2132 1877 2133 1878 (* Extract a flat trace from a structured one. *) 2134 let rec flat_trace_of_label_return ge (s,s':RTLabs_ state ge)1879 let rec flat_trace_of_label_return ge (s,s':RTLabs_ext_state ge) 2135 1880 (tr:trace_label_return (RTLabs_status ge) s s') 2136 1881 on tr : … … 2143 1888 (flat_trace_of_label_return ge s2 s3 tlr) 2144 1889 ] 2145 and flat_trace_of_label_label ge ends (s,s':RTLabs_ state ge)1890 and flat_trace_of_label_label ge ends (s,s':RTLabs_ext_state ge) 2146 1891 (tr:trace_label_label (RTLabs_status ge) ends s s') 2147 1892 on tr : … … 2150 1895 [ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal 2151 1896 ] 2152 and flat_trace_of_any_label ge ends (s,s':RTLabs_ state ge)1897 and flat_trace_of_any_label ge ends (s,s':RTLabs_ext_state ge) 2153 1898 (tr:trace_any_label (RTLabs_status ge) ends s s') 2154 1899 on tr : … … 2181 1926 (* We take an extra step so that we can always return a nonempty trace to 2182 1927 satisfy the guardedness condition in the cofixpoint. *) 2183 let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ state ge) et1928 let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_ext_state ge) et 2184 1929 (tr:trace_any_call (RTLabs_status ge) s s') 2185 1930 (EX'':eval_statement ge s' = Value … 〈et,s''〉) 2186 1931 on tr : 2187 1932 partial_flat_trace io_out io_in ge s s'' ≝ 2188 match tr return λs,s':RTLabs_ state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with1933 match tr return λs,s':RTLabs_ext_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with 2189 1934 [ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX'' 2190 1935  tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''. … … 2202 1947 ] EX''. 2203 1948 2204 let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ state ge) et1949 let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_ext_state ge) et 2205 1950 (tr:trace_label_call (RTLabs_status ge) s s') 2206 1951 (EX'':eval_statement ge s' = Value … 〈et,s''〉) … … 2214 1959 to take care to satisfy the guardedness condition by witnessing the fact that 2215 1960 the partial traces are nonempty. *) 2216 let corec flat_trace_of_label_diverges ge (s:RTLabs_ state ge)1961 let corec flat_trace_of_label_diverges ge (s:RTLabs_ext_state ge) 2217 1962 (tr:trace_label_diverges (RTLabs_status ge) s) 2218 1963 : flat_trace io_out io_in ge s ≝ 2219 match tr return λs:RTLabs_ state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with1964 match tr return λs:RTLabs_ext_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with 2220 1965 [ tld_step sx sy tll tld ⇒ 2221 match sy in RTLabs_ state return λsy:RTLabs_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_state sy' stk mtc0 ⇒1966 match sy in RTLabs_ext_state return λsy:RTLabs_ext_state ge. trace_label_label (RTLabs_status ge) ? sx sy → trace_label_diverges (RTLabs_status ge) sy → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state sy' stk mtc0 ⇒ 2222 1967 λtll. 2223 match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ state ge s2 stk mtc) → flat_trace ??? s1 with1968 match flat_trace_of_label_label ge … tll return λs1,s2:state.λ_:partial_flat_trace io_out io_in ge s1 s2. ∀mtc:Ras_Fn_Match ge s2 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s2 stk mtc) → flat_trace ??? s1 with 2224 1969 [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2225  pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ state ge s3 stk mtc) tr' tld)1970  pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld) 2226 1971 ] mtc0 ] tll tld 2227 1972  tld_base s1 s2 s3 tlc EX CL tld ⇒ 2228 match s3 in RTLabs_ state return λs3:RTLabs_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_state s3' stk mtc0 ⇒1973 match s3 in RTLabs_ext_state return λs3:RTLabs_ext_state ge. as_execute (RTLabs_status ge) ? s3 → trace_label_diverges (RTLabs_status ge) s3 → flat_trace io_out io_in ge ? with [ mk_RTLabs_ext_state s3' stk mtc0 ⇒ 2229 1974 λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2230 match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ state ge s3 stk mtc) → flat_trace ??? s1 with1975 match flat_trace_of_label_call … tlc EX' return λs1,s3.λ_. ∀mtc:Ras_Fn_Match ge s3 stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s3 stk mtc) → flat_trace ??? s1 with 2231 1976 [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2232  pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ state ge s3 stk mtc) tr' tld)1977  pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tld. ft_step … EX (add_partial_flat_trace ge … (mk_RTLabs_ext_state ge s3 stk mtc) tr' tld) 2233 1978 ] mtc0 2234 1979 ] … … 2237 1982 (* Helper to keep adding the partial trace without violating the guardedness 2238 1983 condition. *) 2239 and add_partial_flat_trace ge (s:state) (s':RTLabs_ state ge)1984 and add_partial_flat_trace ge (s:state) (s':RTLabs_ext_state ge) 2240 1985 : partial_flat_trace io_out io_in ge s s' → 2241 1986 trace_label_diverges (RTLabs_status ge) s' → 2242 1987 flat_trace io_out io_in ge s ≝ 2243 match s' return λs':RTLabs_ state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_state sx stk mtc ⇒2244 λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ state ge s' ? mtc) → flat_trace io_out io_in ge s with1988 match s' return λs':RTLabs_ext_state ge. partial_flat_trace io_out io_in ge s s' → trace_label_diverges (RTLabs_status ge) s' → flat_trace io_out io_in ge s with [ mk_RTLabs_ext_state sx stk mtc ⇒ 1989 λptr. match ptr return λs,s'.λ_. ∀mtc:Ras_Fn_Match ge s' stk. trace_label_diverges (RTLabs_status ge) (mk_RTLabs_ext_state ge s' ? mtc) → flat_trace io_out io_in ge s with 2245 1990 [ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr) 2246  pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_ state ge s3 stk mtc) tr' tr)1991  pft_step s1 et s2 s3 EX tr' ⇒ λmtc,tr. ft_step … EX (add_partial_flat_trace ge s2 (mk_RTLabs_ext_state ge s3 stk mtc) tr' tr) 2247 1992 ] mtc ] 2248 1993 . … … 2279 2024 ] qed. 2280 2025 2281 let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ state ge)2026 let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge) 2282 2027 (str:trace_label_diverges (RTLabs_status ge) s) 2283 2028 (tr:flat_trace io_out io_in ge s) … … 2286 2031 qed. 2287 2032 2288 let rec flat_trace_of_whole_program ge (s:RTLabs_ state ge)2033 let rec flat_trace_of_whole_program ge (s:RTLabs_ext_state ge) 2289 2034 (tr:trace_whole_program (RTLabs_status ge) s) 2290 2035 on tr : flat_trace io_out io_in ge s ≝ 2291 match tr return λs:RTLabs_ state ge.λtr. flat_trace io_out io_in ge s with2036 match tr return λs:RTLabs_ext_state ge.λtr. flat_trace io_out io_in ge s with 2292 2037 [ twp_terminating s1 s2 sf CL EX tlr F ⇒ 2293 2038 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ … … 2300 2045 ]. 2301 2046 2302 let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ state ge)2047 let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_ext_state ge) 2303 2048 (str:trace_whole_program (RTLabs_status ge) s) 2304 2049 (tr:flat_trace io_out io_in ge s) … … 2323 2068 (* Some results to invert the classification of states *) 2324 2069 2325 lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ state ge.2070 lemma declassify_pc : ∀ge,cl. ∀P:RTLabs_pc → Prop. ∀s,s':RTLabs_ext_state ge. 2326 2071 as_execute (RTLabs_status ge) s s' → 2327 2072 RTLabs_classify s = cl → … … 2334 2079 #ge #cl #P * * 2335 2080 [ #f #fs #m * [ * ] #fn #S #M #s' #EX whd in ⊢ (??%% → ? → ?%); 2336 cases ( lookup_present ???? (next_ok f)) normalize2081 cases (next_instruction f) normalize 2337 2082 #A #B try #C try #D try #E try #F try #G try #H try #J destruct // 2338 2083  #fd #args #dst #fs #m * [*] #fn #S #M #s' #EX #CL normalize in CL; destruct // … … 2341 2086 ] qed. 2342 2087 2343 lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ state ge.2088 lemma declassify_pc' : ∀ge,cl. ∀s,s':RTLabs_ext_state ge. 2344 2089 as_execute (RTLabs_status ge) s s' → 2345 2090 RTLabs_classify s = cl → … … 2355 2100 qed. 2356 2101 2357 lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ state ge.2102 lemma declassify_state : ∀ge,cl. ∀s,s':RTLabs_ext_state ge. 2358 2103 as_execute (RTLabs_status ge) s s' → 2359 2104 RTLabs_classify s = cl → 2360 2105 match cl with 2361 [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_ state ge (Callstate fd args dst fs m) S M2362  cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ state ge (Returnstate ret dst fs m) S M2363  _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ state ge (State f fs m) S M2106 [ cl_call ⇒ ∃fd,args,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Callstate fd args dst fs m) S M 2107  cl_return ⇒ ∃ret,dst,fs,m,S,M. s = mk_RTLabs_ext_state ge (Returnstate ret dst fs m) S M 2108  _ ⇒ ∃f,fs,m,S,M. s = mk_RTLabs_ext_state ge (State f fs m) S M 2364 2109 ] . 2365 2110 #ge #cl * * [ #f #fs #m  #fd #args #dst #fs #m  #ret #dst #fs #m  #r ] … … 2367 2112 whd in CL:(??%?); 2368 2113 [ cut (cl = cl_other ∨ cl = cl_jump) 2369 [ cases ( lookup_present … (next_ok … f)) in CL;2114 [ cases (next_instruction f) in CL; 2370 2115 normalize #A try #B try #C try #D try #E try #F try #G destruct /2/ ] 2371 2116 * #E >E %{f} %{fs} %{m} %{S} %{M} % … … 2383 2128 ]. 2384 2129 #f #fs #m #cl #CL <CL whd in match (RTLabs_classify ?); 2385 cases ( lookup_present … (next_ok f)) //2130 cases (next_instruction f) // 2386 2131 qed. 2387 2132 … … 2450 2195 2451 2196 lemma graph_fn_state : ∀ge,f,fs,m,S,M,g. 2452 graph_fn ge (state_fn ge (mk_RTLabs_ state ge (State f fs m) S M)) g →2197 graph_fn ge (state_fn ge (mk_RTLabs_ext_state ge (State f fs m) S M)) g → 2453 2198 g = f_graph (func f). 2454 2199 #ge #f #fs #m * [*] #fn #S * #FFP #M #g #G … … 2459 2204 2460 2205 lemma state_fn_next : ∀ge,f,fs,m,S,M,s',tr,l. 2461 let s ≝ mk_RTLabs_ state ge (State f fs m) S M in2206 let s ≝ mk_RTLabs_ext_state ge (State f fs m) S M in 2462 2207 ∀EV:eval_statement ge s = Value … 〈tr,s'〉. 2463 2208 actual_successor s' = Some ? l → 2464 2209 state_fn ge s = state_fn ge (next_state ge s s' tr EV). 2465 2210 #ge #f #fs #m * [*] #fn #S #M #s' #tr #l #EV #AS 2466 change with (Ras_state ? (next_state ge (mk_RTLabs_ state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?);2467 inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ state ge (State f fs m) ? M) … EV))2211 change with (Ras_state ? (next_state ge (mk_RTLabs_ext_state ge (State f fs m) (fn::S) M) s' tr EV)) in AS:(??(?%)?); 2212 inversion (eval_preserves_ext … (eval_to_as_exec ge (mk_RTLabs_ext_state ge (State f fs m) ? M) … EV)) 2468 2213 [ #ge' #f' #f'' #fs' #m' #m'' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct % 2469 2214  #ge' #f' #f'' #m' #fd #args #f''' #dst #fn' #S' #M' #M'' #F #E1 #E2 #E3 #E4 destruct % … … 2487 2232 cases pre in CL AF ⊢ %; 2488 2233 * [ #f #fs #m #S #M #CL @⊥ whd in CL; whd in CL:(??%?); 2489 cases ( lookup_present ???? (next_ok f)) in CL;2234 cases (next_instruction f) in CL; 2490 2235 normalize #A try #B try #C try #D try #E try #F try #G try #H try #J destruct 2491 2236  #fd #args #dst * [2: #f' #fs ] #m * [ 1,3: * ] #fn #S #M #CL … … 2506 2251 ] qed. 2507 2252 2508 lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ state ge. ∀l.2253 lemma actual_successor_pc_label : ∀ge. ∀s:RTLabs_ext_state ge. ∀l. 2509 2254 actual_successor s = Some ? l → 2510 2255 pc_label (as_pc_of (RTLabs_status ge) s) l. … … 2588 2333 a trace_any_label. *) 2589 2334 2590 lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ state ge. ∀fl,tal.2335 lemma no_loops_in_tal : ∀ge. ∀s1,s2,s3:RTLabs_ext_state ge. ∀fl,tal. 2591 2336 soundly_labelled_state s1 → 2592 2337 RTLabs_classify s1 = cl_other → … … 2609 2354 isn't and we get a loop of successor instruction labels that breaks the 2610 2355 soundness of the cost labelling. *) 2611 cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ state ge (State f fs m) (fn::S) (conj ?? FFP M)))2356 cases (as_costed_exc (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M))) 2612 2357 [ * #H @H 2613 2358 cases (memb_exists … IN) #left * #right #E 2614 2359 @(All_split … (tal_tail_not_costed … tal CS2) … E) 2615 2360  (* Now show that the loop invalidates soundness. *) 2616 cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_ state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f))2361 cut (pc_label (as_pc_of (RTLabs_status ge) (mk_RTLabs_ext_state ge (State f fs m) (fn::S) (conj ?? FFP M))) (next f)) 2617 2362 [ %1 ] #PC1 2618 2363 cut (pc_label (as_pc_of (RTLabs_status ge) s2) l2) … … 2675 2420 whd in ⊢ (??%% → ?); #E destruct try % 2676 2421 [ cases M1 #FFP1 #M1' cases M2 >FFP1 #E1 #M2' destruct whd in ⊢ (??%%); 2422 change with (lookup_present … next2 nok1) in match (next_instruction ?); 2677 2423 cases (lookup_present … next2 nok1) 2678 2424 normalize // … … 2698 2444 #CS lapply (proj2 … (RTLabs_costed …) … CS) 2699 2445 whd in ⊢ (??%? → %); 2700 [ whd in ⊢ (? → ??%?); cases ( lookup_present … (next_ok f)) normalize2446 [ whd in ⊢ (? → ??%?); cases (next_instruction f) normalize 2701 2447 #A try #B try #C try #D try #E try #F try #G try #H try #I destruct % 2702 2448  *: #E destruct 
src/RTLabs/semantics.ma
r2475 r2499 49 49 definition build_state ≝ λf.λfs.λm.λn.λp. State (adv n f p) fs m. 50 50 51 definition next_instruction : frame → statement ≝ 52 λf. lookup_present ?? (f_graph (func f)) (next f) (next_ok f). 53 51 54 definition init_locals : list (register × typ) → register_env val ≝ 52 55 foldr ?? (λidt,en. let 〈id,ty〉 ≝ idt in add RegisterTag val en id Vundef) (empty_map ??). … … 89 92 match st return λ_. IO ??? with 90 93 [ State f fs m ⇒ 91 let s ≝ lookup_present ?? (f_graph (func f)) (next f) (next_ok f)in94 let s ≝ next_instruction f in 92 95 match s return λs. labels_present ? s → IO ??? with 93 96 [ St_skip l ⇒ λH. return 〈E0, build_state f fs m l ?〉 … … 271 274 whd in ⊢ (??%? → ?); 272 275 generalize in ⊢ (??(?%)? → ?); 273 cases ( lookup_present LabelTag statement (f_graph func) next next_ok)276 cases (next_instruction ?) 274 277 [ #l #LP whd in ⊢ (??%? → ?); #E destruct % % 275 278  #c #l #LP whd in ⊢ (??%? → ?); #E destruct % % … … 314 317 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m' 315 318 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 316 cases ( lookup_present … nok)319 cases (next_instruction ?) 317 320 (* Function call cases. *) 318 321 [ 8,9: #x #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #fd' #Efd @bind_ok #vs #Evs #E normalize in E; destruct
Note: See TracChangeset
for help on using the changeset viewer.