Changeset 2044 for src/RTLabs
 Timestamp:
 Jun 12, 2012, 10:52:37 AM (8 years ago)
 Location:
 src/RTLabs
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/RTLabs/Traces.ma
r2025 r2044 4 4 5 5 discriminator status_class. 6 7 (* We augment states with a stack of function blocks (i.e. pointers) so that we 8 can make sensible "program counters" for the abstract state definition, along 9 with a proof that we will get the correct code when we do the lookup (which 10 is done to find cost labels given a pc). 11 12 Adding them to the semantics is an alternative, more direct approach. 13 However, it makes animating the semantics extremely difficult, because it 14 is hard to avoid normalising and displaying irrelevant parts of the global 15 environment and proofs. 16 17 We use blocks rather than identifiers because the global environments go 18 19 identifier → block → definition 20 21 and we'd have to introduce backwards lookups to find identifiers for 22 function pointers. 23 *) 24 25 definition Ras_Fn_Match ≝ 26 λge,state,fn_stack. 27 match state with 28 [ State f fs m ⇒ All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) (f::fs) fn_stack 29  Callstate fd _ _ fs _ ⇒ 30 match fn_stack with 31 [ nil ⇒ False 32  cons h t ⇒ find_funct_ptr ? ge h = Some ? fd ∧ 33 All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs t 34 ] 35  Returnstate _ _ fs _ ⇒ 36 All2 … (λfr,b. find_funct_ptr ? ge b = Some ? (Internal ? (func fr))) fs fn_stack 37  Finalstate _ ⇒ fn_stack = [ ] 38 ]. 39 40 record RTLabs_state (ge:genv) : Type[0] ≝ { 41 Ras_state :> state; 42 Ras_fn_stack : list block; 43 Ras_fn_match : Ras_Fn_Match ge Ras_state Ras_fn_stack 44 }. 45 46 (* Given a plain step of the RTLabs semantics, give the next state along with 47 the shadow stack of function block numbers. Carefully defined so that the 48 coercion back to the plain state always reduces. *) 49 definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t. 50 eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝ 51 λge,s,s',t,EX. mk_RTLabs_state ge s' 52 (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) 53 ?. 54 cases s' in EX ⊢ %; 55 [ s' #f #fs #m cases s s #s #stk #mtc #EX whd in ⊢ (???%); inversion (eval_preserves … EX) 56 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct 57 whd cases stk in mtc ⊢ %; [ * ] 58 #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // 59  @M2 ] 60  #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct 61  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 62 whd cases stk in mtc ⊢ %; [ * ] 63 #hd #tl #H @H 64  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct 65  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct 66 cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 % 67 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ] 68  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 69 ] 70  s' #fd #args #dst #fs #m #EX whd in ⊢ (???%); cases (func_block_of_exec … EX) #func_block #FFP 71 whd % // func_block cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX) 72 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct 73  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct 74 cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 % 75 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ] 76  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 77  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct 78  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct 79  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 80 ] 81  s' #rtv #dst #fs #m #EX whd in ⊢ (???%); cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX) 82 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct 83  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct 84  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 85  #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct 86 cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H 87  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct 88  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 89 ] 90  #r #EX whd @refl 91 ] qed. 92 93 (* 94 definition next_state : ∀ge. ∀s:RTLabs_state ge. ∀s':state. ∀t. 95 eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge ≝ 96 λge,s,s',t. 97 match s' return λs'. eval_statement ge s = Value ??? 〈t,s'〉 → RTLabs_state ge with 98 [ State f fs m ⇒ λEX. mk_RTLabs_state ge (State f fs m) (Ras_fn_stack … s) ? 99  Callstate fd args dst fs m ⇒ λEX. mk_RTLabs_state ge (Callstate fd args dst fs m) (func_block_of_exec … EX::Ras_fn_stack … s) ? 100  Returnstate rtv dst fs m ⇒ λEX. mk_RTLabs_state ge (Returnstate rtv dst fs m) (tail … (Ras_fn_stack … s)) ? 101  Finalstate r ⇒ λEX. mk_RTLabs_state ge (Finalstate r) [ ] ? 102 ]. 103 [ cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX) 104 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct 105 whd cases stk in mtc ⊢ %; [ * ] 106 #hd #tl * #M1 #M2 % [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct // 107  @M2 ] 108  #ge' #f1 #fs1 #m1 #fd #args #f' #dst #F #b #FFP #E1 #E2 #E3 #E4 destruct 109  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 110 whd cases stk in mtc ⊢ %; [ * ] 111 #hd #tl #H @H 112  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct 113  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct 114 cases stk in mtc ⊢ %; [ * ] #hd #tl * #M1 #M2 % 115 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ] 116  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 117 ] 118  cases (func_block_of_exec … EX) #func_block #FFP 119 whd % // func_block cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX) 120 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct 121  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct 122 cases stk in mtc; [ * ] #b1 #bs * #M1 #M2 % 123 [ inversion F #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 destruct //  @M2 ] 124  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 125  #H14 #H15 #H16 #H17 #H18 #H19 #H20 #H21 #H22 #H23 #H24 destruct 126  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct 127  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 128 ] 129  cases s in EX ⊢ %; s #s #stk #mtc #EX inversion (eval_preserves … EX) 130 [ #ge' #f1 #f2 #fs' #m1 #m2 #F #E1 #E2 #E3 #E4 destruct 131  #ge' #f1 #fs1 #m1 #fd' #args' #f' #dst' #F #b #FFP #E1 #E2 #E3 #E4 destruct 132  #ge' #fn #locals #next #nok #sp #fs0 #m0 #args #dst #m' #E1 #E2 #E3 #E4 destruct 133  #ge' #f #fs' #m' #rtv' #dst' #m' #E1 #E2 #E3 #E4 destruct 134 cases stk in mtc ⊢ %; [ * ] #b #bs * #_ #H @H 135  #ge' #f0 #fs0 #rtv #dst #f' #m0 #F #E1 #E2 #E3 #E4 destruct 136  #ge' #r #dst #m0 #E1 #E2 #E3 #E4 destruct 137 ] 138  whd @refl 139 ] qed.*) 6 140 7 141 (* NB: For RTLabs we only classify branching behaviour as jumps. Other jumps … … 46 180 ]. 47 181 48 (* At the moment we don't need to talk about the program counter, so we just 49 use unit. *) 50 definition unit_deqset ≝ mk_DeqSet unit (λ_.λ_. true) ?. 51 * * % // 182 inductive RTLabs_pc : Type[0] ≝ 183  rapc_state : block → label → RTLabs_pc 184  rapc_call : block → RTLabs_pc 185  rapc_ret : option block → RTLabs_pc 186  rapc_fin : RTLabs_pc 187 . 188 189 definition block_eq : DeqSet ≝ mk_DeqSet block eq_block ?. 190 #x #y @eq_block_elim 191 [ #E destruct /2/ 192  * #NE % #E destruct cases (NE (refl ??)) 193 ] qed. 194 195 definition RTLabs_pc_eq : RTLabs_pc → RTLabs_pc → bool ≝ 196 λx,y. match x with 197 [ rapc_state b1 l1 ⇒ match y with [ rapc_state b2 l2 ⇒ eq_block b1 b2 ∧ eq_identifier … l1 l2  _ ⇒ false ] 198  rapc_call b1 ⇒ match y with [ rapc_call b2 ⇒ eq_block b1 b2  _ ⇒ false ] 199  rapc_ret b1 ⇒ match y with [ rapc_ret b2 ⇒ eq_option block_eq b1 b2  _ ⇒ false ] 200  rapc_fin ⇒ match y with [ rapc_fin ⇒ true  _ ⇒ false ] 201 ]. 202 203 definition RTLabs_deqset : DeqSet ≝ mk_DeqSet RTLabs_pc RTLabs_pc_eq ?. 204 whd in match RTLabs_pc_eq; whd in match eq_option; whd in match block_eq; 205 * [ #b1 #l1  #b1  * [2: #b1 ]  ] 206 * [ 1,5,9,13,17: #b2 #l2  2,6,10,14,18: #b2  3,7,11,15,19: * [2,4,6,8,10: #b2]  *: ] 207 normalize nodelta 208 [ 1,7,13: @eq_block_elim [ 1,3,5: #E destruct  *: * #NE ] ] 209 [ 1,4: @eq_identifier_elim [ 1,3: #E destruct  *: * #NE ] ] 210 normalize % #E destruct try (cases (NE (refl ??))) @refl 52 211 qed. 212 213 definition RTLabs_state_to_pc : ∀ge. RTLabs_state ge → RTLabs_deqset ≝ 214 λge,s. match s with [ mk_RTLabs_state s' stk mtc0 ⇒ 215 match s' return λs'. Ras_Fn_Match ? s' ? → ? with 216 [ State f fs m ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_state b (next … f) ] 217  Callstate _ _ _ _ _ ⇒ match stk return λstk. Ras_Fn_Match ?? stk → ? with [ nil ⇒ λmtc. ⊥  cons b _ ⇒ λ_. rapc_call b ] 218  Returnstate _ _ _ _ ⇒ match stk with [ nil ⇒ λ_. rapc_ret (None ?)  cons b _ ⇒ λ_. rapc_ret (Some ? b) ] 219  Finalstate _ ⇒ λmtc. rapc_fin 220 ] mtc0 ]. 221 whd in mtc; cases mtc 222 qed. 223 224 definition RTLabs_pc_to_cost_label : ∀ge. RTLabs_pc → option costlabel ≝ 225 λge,pc. 226 match pc with 227 [ rapc_state b l ⇒ 228 match find_funct_ptr … ge b with [ None ⇒ None ?  Some fd ⇒ 229 match fd with [ Internal f ⇒ match lookup ?? (f_graph f) l with [ Some s ⇒ cost_label_of s  _ ⇒ None ? ]  _ ⇒ None ? ] ] 230  _ ⇒ None ? 231 ]. 53 232 54 233 definition RTLabs_status : genv → abstract_status ≝ 55 234 λge. 56 235 mk_abstract_status 57 state58 (λs,s'. ∃t . eval_statement ge s = Value ??? 〈t,s'〉)59 unit_deqset60 ( λ_. it)236 (RTLabs_state ge) 237 (λs,s'. ∃t,EX. next_state ge s s' t EX = s') 238 RTLabs_deqset 239 (RTLabs_state_to_pc ge) 61 240 (λs,c. RTLabs_classify s = c) 62 RTLabs_cost_label241 (RTLabs_pc_to_cost_label ge) 63 242 (λs,s'. match s with 64 243 [ mk_Sig s p ⇒ … … 85 264 labelled. *) 86 265 87 lemma RTLabs_costed : ∀ge ,s.88 RTLabs_cost s = true →266 lemma RTLabs_costed : ∀ge. ∀s:RTLabs_state ge. 267 RTLabs_cost s = true ↔ 89 268 as_costed (RTLabs_status ge) s. 90 #ge * 91 [ * #func #locals #next #nok #b #r #fs #m 92 whd in ⊢ (??%? → %); whd in ⊢ (? → ?(??%?)); 93 cases (lookup_present ?? (f_graph func) ??) normalize 269 cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE 270 #ge * * 271 [ * #func #locals #next #nok #sp #r #fs #m #stk #mtc 272 whd in ⊢ (??%); whd in ⊢ (??(?(??%?))); 273 whd in match (as_pc_of ??); 274 cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2 275 whd in ⊢ (??(?(??%?))); >M1 whd in ⊢ (??(?(??%?))); 276 >(lookup_lookup_present … nok) 277 whd in ⊢ (?(??%?)(?(??%?))); 278 % cases (lookup_present ?? (f_graph func) ??) normalize 94 279 #A try #B try #C try #D try #E try #F try #G try #H try #G destruct 95 % #E' destruct 96  normalize #fd #args #r #fs #m #E destruct 97  normalize #A #B #C #D #E destruct 98  normalize #A #B destruct 99 ] qed. 100 101 lemma costed_RTLabs : ∀ge,s. 102 as_costed (RTLabs_status ge) s → 103 RTLabs_cost s = true. 104 #ge 105 cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #H 106 * 107 [ * #func #locals #next #nok #b #r #fs #m 108 whd in ⊢ (% → ??%?); whd in ⊢ (?(??%?) → ?); 109 cases (lookup_present ?? (f_graph func) ??) normalize // 110 #A try #B try #C try #D try #E try #F try #G try #I try #J cases (H ?) // 111  *: normalize #A #B try #C try #D try #E try #F cases (H ?) // 112 ] qed. 113 114 lemma RTLabs_not_cost : ∀ge,s. 280 try (% #E' destruct) 281 cases (NONE ?) assumption 282  #fd #args #dst #fs #m #stk #mtc % 283 [ #E normalize in E; destruct 284  whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??); 285 cases stk in mtc ⊢ %; [*] #fblk #fblks #mtc whd in ⊢ (?(??%?) → ?); 286 #H cases (NONE H) 287 ] 288  #v #dst #fs #m #stk #mtc % 289 [ #E normalize in E; destruct 290  whd in ⊢ (% → ?); whd in ⊢ (?(??%?) → ?); whd in match (as_pc_of ??); 291 cases stk in mtc ⊢ %; [2: #fblk #fblks ] #mtc whd in ⊢ (?(??%?) → ?); 292 #H cases (NONE H) 293 ] 294  #r #stk #mtc % 295 [ #E normalize in E; destruct 296  #E normalize in E; cases (NONE E) 297 ] 298 ] qed. 299 300 lemma RTLabs_not_cost : ∀ge. ∀s:RTLabs_state ge. 115 301 RTLabs_cost s = false → 116 302 ¬ as_costed (RTLabs_status ge) s. 117 #ge * 118 [ * #func #locals #next #nok #b #r #fs #m 119 whd in ⊢ (??%? → ?%); whd in ⊢ (? → ?(?(??%?))); 120 cases (lookup_present ?? (f_graph func) ??) normalize 121 #A try #B try #C try #D try #E try #F try #G try #H try #I destruct 122 % * #J @J @refl 123  *: normalize #A #B try #C try #D try #E try #F % * #G @G @refl 124 ] qed. 303 #ge #s #E % #C >(proj2 … (RTLabs_costed ??)) in E; // #E destruct 304 qed. 125 305 126 306 (* Before attempting to construct a structured trace, let's show that we can … … 547 727 548 728 definition well_cost_labelled_ge : genv → Prop ≝ 549 λge. ∀b,f. find_funct_ptr ??ge b = Some ? (Internal ? f) → well_cost_labelled_fn f.729 λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → well_cost_labelled_fn f. 550 730 551 731 definition well_cost_labelled_state : state → Prop ≝ … … 656 836 cases fd 657 837 [ #fn whd in ⊢ (??%? → % → ?); 658 @bind_res_value #lcl #Elcl cases (alloc ?m O (f_stacksize fn) Any)838 @bind_res_value #lcl #Elcl cases (alloc m O (f_stacksize fn) Any) 659 839 #m' #b whd in ⊢ (??%? → ?); #E' destruct 660 840 * whd in ⊢ (% → ?); * #WCL1 #WCL2 #WCL3 … … 671 851 frames never change, and that after returning from the function we preserve 672 852 the identity of the next instruction to execute. 853 854 Note: since this was first written I've introduced the shadow stack of 855 function blocks. It might be possible to replace some or all of the stack 856 preservation with that. 673 857 *) 674 858 … … 824 1008 ] qed. 825 1009 826 lemma RTLabs_after_call : ∀ge ,s1,s2,s3,tr.1010 lemma RTLabs_after_call : ∀ge.∀s1,s2,s3:RTLabs_state ge.∀tr. 827 1011 ∀CL : RTLabs_classify s1 = cl_call. 828 1012 eval_statement ge s1 = Value ??? 〈tr,s2〉 → 829 1013 stack_preserved ends_with_ret s2 s3 → 830 1014 as_after_return (RTLabs_status ge) «s1,CL» s3. 831 #ge #s1 #s2 #s3 #tr #CL #EV #S231015 #ge * #s1 #stk1 #M1 * #s2 #stk2 #M2 * #s3 #stk3 #M3 #tr #CL #EV #S23 832 1016 cases (rtlabs_call_inv … CL) #fn * #args * #dst * #stk * #m #E destruct 1017 whd 833 1018 inversion S23 834 1019 [ #H129 #H130 #H131 #H132 #H133 #H134 #H135 #H136 #H137 destruct 835  #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct 1020  #s2' #f #f' #fs #m' #N #F #S #E1 #E2 #E3 #E4 destruct whd 836 1021 inversion (eval_preserves … EV) 837 1022 [ #H139 #H140 #H141 #H142 #H143 #H144 #H145 #H146 #H147 #H148 #H149 destruct … … 870 1055 of the termination proof is respected. *) 871 1056 record trace_result (ge:genv) (depth:nat) (ends:trace_ends_with_ret) 872 (start: state) (full:flat_trace io_out io_in ge start)1057 (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start) 873 1058 (original_terminates: will_return ge depth start full) 874 (T: state → Type[0]) (limit:nat) : Type[0] ≝1059 (T:RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝ 875 1060 { 876 new_state : state;1061 new_state : RTLabs_state ge; 877 1062 remainder : flat_trace io_out io_in ge new_state; 878 1063 cost_labelled : well_cost_labelled_state new_state; … … 882 1067 [ O ⇒ will_return_end … original_terminates = ❬new_state, remainder❭ 883 1068  S d ⇒ ΣTM:will_return ge d new_state remainder. 884 limit > will_return_length … TM∧1069 gt limit (will_return_length … TM) ∧ 885 1070 will_return_end … original_terminates = will_return_end … TM 886 1071 ] … … 890 1075 encountering a label. *) 891 1076 record sub_trace_result (ge:genv) (depth:nat) 892 (start: state) (full:flat_trace io_out io_in ge start)1077 (start:RTLabs_state ge) (full:flat_trace io_out io_in ge start) 893 1078 (original_terminates: will_return ge depth start full) 894 (T:trace_ends_with_ret → state → Type[0]) (limit:nat) : Type[0] ≝1079 (T:trace_ends_with_ret → RTLabs_state ge → Type[0]) (limit:nat) : Type[0] ≝ 895 1080 { 896 1081 ends : trace_ends_with_ret; … … 902 1087 the size of the termination proof might need to be relaxed, too. *) 903 1088 904 definition replace_trace : ∀ge,d,e ,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →1089 definition replace_trace : ∀ge,d,e.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → 905 1090 ∀r:trace_result ge d e s1 t1 TM1 T1 l1. 906 1091 will_return_end … TM1 = will_return_end … TM2 → … … 931 1116 ] qed. 932 1117 933 definition replace_sub_trace : ∀ge,d ,s1,s2,t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 →1118 definition replace_sub_trace : ∀ge,d.∀s1,s2:RTLabs_state ge.∀t1,t2,TM1,TM2,T1,T2,l1,l2. l2 ≥ l1 → 934 1119 ∀r:sub_trace_result ge d s1 t1 TM1 T1 l1. 935 1120 will_return_end … TM1 = will_return_end … TM2 → … … 945 1130 definition myge : nat → nat → Prop ≝ ge. 946 1131 947 let rec make_label_return ge depth s1132 let rec make_label_return ge depth (s:RTLabs_state ge) 948 1133 (trace: flat_trace io_out io_in ge s) 949 1134 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 955 1140 on TIME : trace_result ge depth ends_with_ret s trace TERMINATES 956 1141 (trace_label_return (RTLabs_status ge) s) 957 (will_return_length … TERMINATES) ≝ 1142 (will_return_length … TERMINATES) ≝ 958 1143 959 1144 match TIME return λTIME. TIME ≥ ? → ? with … … 986 1171 987 1172 988 and make_label_label ge depth s1173 and make_label_label ge depth (s:RTLabs_state ge) 989 1174 (trace: flat_trace io_out io_in ge s) 990 1175 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1009 1194 1010 1195 1011 and make_any_label ge depth s1012 (trace: flat_trace io_out io_in ge s )1196 and make_any_label ge depth (s0:RTLabs_state ge) 1197 (trace: flat_trace io_out io_in ge s0) 1013 1198 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1014 (STATE_COSTLABELLED: well_cost_labelled_state s ) (* functions in the state *)1015 (TERMINATES: will_return ge depth s trace)1199 (STATE_COSTLABELLED: well_cost_labelled_state s0) (* functions in the state *) 1200 (TERMINATES: will_return ge depth s0 trace) 1016 1201 (TIME: nat) 1017 1202 (TERMINATES_IN_TIME: myge TIME (times 3 (will_return_length … TERMINATES))) 1018 on TIME : sub_trace_result ge depth s trace TERMINATES1019 (λends. trace_any_label (RTLabs_status ge) ends s )1203 on TIME : sub_trace_result ge depth s0 trace TERMINATES 1204 (λends. trace_any_label (RTLabs_status ge) ends s0) 1020 1205 (will_return_length … TERMINATES) ≝ 1021 1206 … … 1023 1208 [ O ⇒ λTERMINATES_IN_TIME. ⊥ 1024 1209  S TIME ⇒ λTERMINATES_IN_TIME. 1025 1026 match trace return λs,trace. well_cost_labelled_state s → 1210 match s0 return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s. 1211 well_cost_labelled_state s → 1212 ∀TM:will_return ??? trace. 1213 myge ? (times 3 (will_return_length ??? trace TM)) → 1214 sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) 1215 with [ mk_RTLabs_state s stk mtc0 ⇒ λtrace. 1216 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk. 1217 well_cost_labelled_state s → 1027 1218 ∀TM:will_return ??? trace. 1028 1219 myge ? (times 3 (will_return_length ??? trace TM)) → 1029 sub_trace_result ge depth s trace TM (λends. trace_any_label (RTLabs_status ge) ends s) (will_return_length … TM) with1220 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) with 1030 1221 [ ft_stop st FINAL ⇒ 1031 λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ 1032 1033  ft_step start tr next EV trace' ⇒ λSTATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 1034 match RTLabs_classify start return λx. RTLabs_classify start = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 1222 λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. ⊥ 1223 1224  ft_step start tr next EV trace' ⇒ λmtc,STATE_COSTLABELLED,TERMINATES,TERMINATES_IN_TIME. 1225 let start' ≝ mk_RTLabs_state ge start stk mtc in 1226 let next' ≝ next_state ? start' ?? EV in 1227 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 1035 1228 [ cl_other ⇒ λCL. 1036 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth start?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with1229 match RTLabs_cost next return λx. RTLabs_cost next = x → sub_trace_result ge depth ??? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 1037 1230 (* We're about to run into a label. *) 1038 1231 [ true ⇒ λCS. 1039 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?1232 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ? 1040 1233 doesnt_end_with_ret 1041 (mk_trace_result ge … next trace' ?1042 (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed …CS)) ??)1234 (mk_trace_result ge … next' trace' ? 1235 (tal_base_not_return (RTLabs_status ge) start' next' ?? (proj1 … (RTLabs_costed ge next') CS)) ??) 1043 1236 (* An ordinary step, keep going. *) 1044 1237  false ⇒ λCS. 1045 let r ≝ make_any_label ge depth next trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in1046 replace_sub_trace …r ?1238 let r ≝ make_any_label ge depth next' trace' ENV_COSTLABELLED ? (will_return_notfn … TERMINATES) TIME ? in 1239 replace_sub_trace ????????????? r ? 1047 1240 (tal_step_default (RTLabs_status ge) (ends … r) 1048 start next (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost …CS)) ?1241 start' next' (new_state … r) ? (new_trace … r) ? (RTLabs_not_cost ? next' CS)) ? 1049 1242 ] (refl ??) 1050 1243 1051 1244  cl_jump ⇒ λCL. 1052 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?1245 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ? 1053 1246 doesnt_end_with_ret 1054 (mk_trace_result ge … next trace' ?1055 (tal_base_not_return (RTLabs_status ge) start next???) ??)1247 (mk_trace_result ge … next' trace' ? 1248 (tal_base_not_return (RTLabs_status ge) start' next' ???) ??) 1056 1249 1057 1250  cl_call ⇒ λCL. 1058 let r ≝ make_label_return ge (S depth) next trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in1059 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with1251 let r ≝ make_label_return ge (S depth) next' trace' ENV_COSTLABELLED ?? (will_return_call … CL TERMINATES) TIME ? in 1252 match RTLabs_cost (new_state … r) return λx. RTLabs_cost (new_state … r) = x → sub_trace_result ge depth start' ?? (λends. trace_any_label (RTLabs_status ge) ends ?) (will_return_length … TERMINATES) with 1060 1253 (* We're about to run into a label, use base case for call *) 1061 1254 [ true ⇒ λCS. 1062 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?1255 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ? 1063 1256 doesnt_end_with_ret 1064 1257 (mk_trace_result ge … 1065 (tal_base_call (RTLabs_status ge) start next(new_state … r)1066 ? CL ? (new_trace … r) ( RTLabs_costed… CS)) ??)1258 (tal_base_call (RTLabs_status ge) start' next' (new_state … r) 1259 ? CL ? (new_trace … r) ((proj1 … (RTLabs_costed …)) … CS)) ??) 1067 1260 (* otherwise use step case *) 1068 1261  false ⇒ λCS. … … 1072 1265 replace_sub_trace … r' ? 1073 1266 (tal_step_call (RTLabs_status ge) (ends … r') 1074 start next(new_state … r) (new_state … r') ? CL ?1267 start' next' (new_state … r) (new_state … r') ? CL ? 1075 1268 (new_trace … r) (RTLabs_not_cost … CS) (new_trace … r')) ? 1076 1269 ] (refl ??) 1077 1270 1078 1271  cl_return ⇒ λCL. 1079 mk_sub_trace_result ge depth start ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start) ?1272 mk_sub_trace_result ge depth start' ? TERMINATES (λends. trace_any_label (RTLabs_status ge) ends start') ? 1080 1273 ends_with_ret 1081 1274 (mk_trace_result ge … 1082 next 1275 next' 1083 1276 trace' 1084 1277 ? 1085 (tal_base_return (RTLabs_status ge) start next? CL)1278 (tal_base_return (RTLabs_status ge) start' next' ? CL) 1086 1279 ? 1087 1280 ?) 1088 1281 ] (refl ? (RTLabs_classify start)) 1089 1282 1090  ft_wrong start m NF EV ⇒ λ STATE_COSTLABELLED,TERMINATES. ⊥1283  ft_wrong start m NF EV ⇒ λmtc,STATE_COSTLABELLED,TERMINATES. ⊥ 1091 1284 1092 ] STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME1285 ] mtc0 ] trace STATE_COSTLABELLED TERMINATES TERMINATES_IN_TIME 1093 1286 ] TERMINATES_IN_TIME. 1094 1287 … … 1099 1292  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #_ #EEQ // 1100 1293  @(stack_preserved_join … (stack_ok … r)) // 1101  @( costed_RTLabs ge) @(trace_label_label_label … (new_trace … r))1294  @(proj2 … (RTLabs_costed ge …)) @(trace_label_label_label … (new_trace … r)) 1102 1295  cases r #H1 #H2 #H3 #H4 #H5 * #H7 * #LT #_ 1103 1296 @(le_plus_to_le … 1) @(transitive_le … TERMINATES_IN_TIME) … … 1111 1304  @le_n 1112 1305  // 1113  @ RTLabs_costed//1306  @(proj1 … (RTLabs_costed …)) // 1114 1307  @le_S_S_to_le @TERMINATES_IN_TIME 1115 1308  @(wrl_nonzero … TERMINATES_IN_TIME) … … 1123 1316 ] 1124 1317  @(will_return_return … CL TERMINATES) 1125  /2 by stack_preserved_return/1126  %{tr} @EV1318  @(stack_preserved_return … EV) // 1319  %{tr} %{EV} @refl 1127 1320  @(well_cost_labelled_state_step … EV) // 1128 1321  whd @(will_return_notfn … TERMINATES) %2 @CL 1129  @ stack_preserved_step/2/1130  %{tr} @EV1322  @(stack_preserved_step … EV) /2/ 1323  %{tr} %{EV} % 1131 1324  %1 whd @CL 1132  @ RTLabs_costed@(well_cost_labelled_jump … EV) //1325  @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) // 1133 1326  @(well_cost_labelled_state_step … EV) // 1134 1327  whd cases (terminates ???????? r) #TMr * #LTr #EQr %{TMr} % … … 1139 1332 ] 1140 1333  @(stack_preserved_call … EV (stack_ok … r)) // 1141  %{tr} @EV1142  @ RTLabs_after_call //1334  %{tr} %{EV} % 1335  @(RTLabs_after_call … next') [2: @EV  skip  // ] 1143 1336  @(cost_labelled … r) 1144 1337  skip … … 1147 1340 cases (will_return_call … CL TERMINATES) #TM' * #LT' #_ @LT' 1148 1341  cases r #ns #rm #WS #TLR #SP * #TM * #_ #EQ <EQ 1149 cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' //1150  @ RTLabs_after_call //1151  %{tr} @EV1342 cases (will_return_call … CL TERMINATES) #TM' * #_ #EQ' @sym_eq @EQ' 1343  @(RTLabs_after_call … next') [2: @EV  skip  // ] 1344  %{tr} %{EV} % 1152 1345  @(stack_preserved_join … (stack_ok … r')) @(stack_preserved_call … EV (stack_ok … r)) // 1153 1346  @(cost_labelled … r) … … 1169 1362  whd @(will_return_notfn … TERMINATES) %1 @CL 1170 1363  @(stack_preserved_step … EV) /2/ 1171  %{tr} @EV1364  %{tr} %{EV} % 1172 1365  %2 whd @CL 1173 1366  @(well_cost_labelled_state_step … EV) // 1174 1367  cases (will_return_notfn … TERMINATES) #TM * #GT #_ @(le_S_to_le … GT) 1175  cases (will_return_notfn … TERMINATES) #TM * #_ #EQ //1368  cases (will_return_notfn … TERMINATES) #TM * #_ #EQ @sym_eq @EQ 1176 1369  @CL 1177  %{tr} @EV1370  %{tr} %{EV} % 1178 1371  @(stack_preserved_join … (stack_ok … r)) @(stack_preserved_step … EV) /2/ 1179 1372  @(well_cost_labelled_state_step … EV) // … … 1193 1386 (* We can initialise TIME with a suitably large value based on the length of the 1194 1387 termination proof. *) 1195 let rec make_label_return' ge depth s1388 let rec make_label_return' ge depth (s:RTLabs_state ge) 1196 1389 (trace: flat_trace io_out io_in ge s) 1197 1390 (ENV_COSTLABELLED: well_cost_labelled_ge ge) … … 1406 1599 ] qed. 1407 1600 1408 lemma bound_after_call : ∀ge ,s,s',n.1601 lemma bound_after_call : ∀ge.∀s,s':RTLabs_state ge.∀n. 1409 1602 state_bound_on_steps_to_cost s (S n) → 1410 1603 ∀CL:RTLabs_classify s = cl_call. … … 1412 1605 RTLabs_cost s' = false → 1413 1606 state_bound_on_steps_to_cost s' n. 1414 #ge #s #s' #n #Hinversion H1607 #ge * #s #stk #mtc * #s' #stk' #mtc' #n #H #CL whd in ⊢ (% → ?); stk stk' lapply CL CL inversion H 1415 1608 [ #f #fs #m #n' #S #E1 #E2 #_ #CL @⊥ cases (rtlabs_call_inv … CL) 1416 1609 #fn * #args * #dst * #stk * #m' #E destruct … … 1499 1692 1500 1693 definition soundly_labelled_ge : genv → Prop ≝ 1501 λge. ∀b,f. find_funct_ptr ??ge b = Some ? (Internal ? f) → soundly_labelled_fn f.1694 λge. ∀b,f. find_funct_ptr … ge b = Some ? (Internal ? f) → soundly_labelled_fn f. 1502 1695 1503 1696 definition soundly_labelled_state : state → Prop ≝ … … 1570 1763 use the fact that the trace is soundly labelled to achieve this. *) 1571 1764 1572 record remainder_ok (ge:genv) (s: state) (t:flat_trace io_out io_in ge s) : Type[0] ≝ {1765 record remainder_ok (ge:genv) (s:RTLabs_state ge) (t:flat_trace io_out io_in ge s) : Type[0] ≝ { 1573 1766 ro_well_cost_labelled: well_cost_labelled_state s; 1574 1767 ro_soundly_labelled: soundly_labelled_state s; … … 1578 1771 }. 1579 1772 1580 inductive finite_prefix (ge:genv) : state → Prop ≝1581  fp_tal : ∀s,s' .1773 inductive finite_prefix (ge:genv) : RTLabs_state ge → Prop ≝ 1774  fp_tal : ∀s,s':RTLabs_state ge. 1582 1775 trace_any_label (RTLabs_status ge) doesnt_end_with_ret s s' → 1583 1776 ∀t:flat_trace io_out io_in ge s'. 1584 1777 remainder_ok ge s' t → 1585 1778 finite_prefix ge s 1586  fp_tac : ∀s1,s2,s3 ,tr.1779  fp_tac : ∀s1,s2,s3:RTLabs_state ge. 1587 1780 trace_any_call (RTLabs_status ge) s1 s2 → 1588 1781 well_cost_labelled_state s2 → 1589 eval_statement ge s2 = Value ??? 〈tr,s3〉→1782 as_execute (RTLabs_status ge) s2 s3 → 1590 1783 ∀t:flat_trace io_out io_in ge s3. 1591 1784 remainder_ok ge s3 t → … … 1593 1786 . 1594 1787 1595 definition fp_add_default : ∀ge ,s,s'.1788 definition fp_add_default : ∀ge. ∀s,s':RTLabs_state ge. 1596 1789 RTLabs_classify s = cl_other → 1597 1790 finite_prefix ge s' → 1598 (∃t. eval_statement ge s = Value ??? 〈t,s'〉)→1791 as_execute (RTLabs_status ge) s s' → 1599 1792 RTLabs_cost s' = false → 1600 1793 finite_prefix ge s ≝ 1601 1794 λge,s,s',OTHER,fp. 1602 match fp return λs '.λ_. (∃t. eval_statement ge ? = Value ??? 〈t,s'〉) → RTLabs_cost s'= false → finite_prefix ge s with1795 match fp return λs1.λfp1:finite_prefix ge s1. as_execute (RTLabs_status ge) ? s1 → RTLabs_cost s1 = false → finite_prefix ge s with 1603 1796 [ fp_tal s' sf TAL rem rok ⇒ λEVAL, NOT_COST. fp_tal ge s sf 1604 1797 (tal_step_default (RTLabs_status ge) doesnt_end_with_ret s s' sf EVAL TAL OTHER (RTLabs_not_cost … NOT_COST)) 1605 1798 rem rok 1606  fp_tac s1 s2 s3 tr TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 tr1799  fp_tac s1 s2 s3 TAC WCL2 EV rem rok ⇒ λEVAL, NOT_COST. fp_tac ge s s2 s3 1607 1800 (tac_step_default (RTLabs_status ge) ??? EVAL TAC OTHER (RTLabs_not_cost … NOT_COST)) 1608 1801 WCL2 EV rem rok 1609 1802 ]. 1610 1803 1611 definition fp_add_terminating_call : ∀ge ,s,s1,s''.1612 (∃t. eval_statement ge s = Value ??? 〈t,s1〉)→1804 definition fp_add_terminating_call : ∀ge.∀s,s1,s'':RTLabs_state ge. 1805 as_execute (RTLabs_status ge) s s1 → 1613 1806 ∀CALL:RTLabs_classify s = cl_call. 1614 1807 finite_prefix ge s'' → … … 1618 1811 finite_prefix ge s ≝ 1619 1812 λge,s,s1,s'',EVAL,CALL,fp. 1620 match fp return λs''.λ _. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with1813 match fp return λs''.λfp:finite_prefix ge s''. trace_label_return (RTLabs_status ge) ? s'' → as_after_return (RTLabs_status ge) ? s'' → RTLabs_cost s'' = false → finite_prefix ge s with 1621 1814 [ fp_tal s'' sf TAL rem rok ⇒ λTLR,RET,NOT_COST. fp_tal ge s sf 1622 1815 (tal_step_call (RTLabs_status ge) doesnt_end_with_ret s s1 s'' sf EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAL) 1623 1816 rem rok 1624  fp_tac s'' s2 s3 tr TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 tr1817  fp_tac s'' s2 s3 TAC WCL2 EV rem rok ⇒ λTLR,RET,NOT_COST. fp_tac ge s s2 s3 1625 1818 (tac_step_call (RTLabs_status ge) s s'' s2 s1 EVAL CALL RET TLR (RTLabs_not_cost … NOT_COST) TAC) 1626 1819 WCL2 EV rem rok … … 1640 1833 inhabited (will_return ge depth s trace) ∨ ¬ inhabited (will_return ge depth s trace). 1641 1834 1642 let rec finite_segment ge sn trace1835 let rec finite_segment ge (s:RTLabs_state ge) n trace 1643 1836 (ORACLE: termination_oracle) 1644 1837 (TRACE_OK: remainder_ok ge s trace) … … 1646 1839 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1647 1840 (LABEL_LIMIT: state_bound_on_steps_to_cost s n) 1648 on n : finite_prefix ge s ≝ 1841 on n : finite_prefix ge s ≝ 1649 1842 match n return λn. state_bound_on_steps_to_cost s n → finite_prefix ge s with 1650 1843 [ O ⇒ λLABEL_LIMIT. ⊥ 1651  S n' ⇒ 1652 match trace return λs,trace. remainder_ok ge s trace → state_bound_on_steps_to_cost s (S n') → finite_prefix ge s with 1653 [ ft_stop st FINAL ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ 1654  ft_step start tr next EV trace' ⇒ λTRACE_OK,LABEL_LIMIT. 1844  S n' ⇒ 1845 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'. 1846 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) with 1847 [ ft_stop st FINAL ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥ 1848  ft_step start tr next EV trace' ⇒ λmtc,TRACE_OK,LABEL_LIMIT. 1849 let start' ≝ mk_RTLabs_state ge start stk mtc in 1850 let next' ≝ next_state ge start' next tr EV in 1655 1851 match RTLabs_classify start return λx. RTLabs_classify start = x → ? with 1656 1852 [ cl_other ⇒ λCL. … … 1658 1854 match RTLabs_cost next return λx. RTLabs_cost next = x → ? with 1659 1855 [ true ⇒ λCS. 1660 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next ?? (RTLabs_costed… CS)) trace' TRACE_OK'1856 fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ((proj1 … (RTLabs_costed ge next')) … CS)) trace' TRACE_OK' 1661 1857  false ⇒ λCS. 1662 let fs ≝ finite_segment ge next n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in1663 fp_add_default ge ??CL fs ? CS1858 let fs ≝ finite_segment ge next' n' trace' ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1859 fp_add_default ge start' next' CL fs ? CS 1664 1860 ] (refl ??) 1665 1861  cl_jump ⇒ λCL. 1666 fp_tal ge start next (tal_base_not_return (RTLabs_status ge) start next?? ?) trace' ?1862 fp_tal ge start' next' (tal_base_not_return (RTLabs_status ge) start' next' ?? ?) trace' ? 1667 1863  cl_call ⇒ λCL. 1668 match ORACLE ge O next trace' return λ_. finite_prefix ge start with1864 match ORACLE ge O next trace' return λ_. finite_prefix ge start' with 1669 1865 [ or_introl TERMINATES ⇒ 1670 1866 match TERMINATES with [ witness TERMINATES ⇒ 1671 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in1867 let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in 1672 1868 let TRACE_OK' ≝ ? in 1673 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start with1674 [ true ⇒ λCS. fp_tal ge start (new_state … tlr) (tal_base_call (RTLabs_status ge) start next (new_state … tlr) ? CL ? (new_trace … tlr) (RTLabs_costed… CS)) (remainder … tlr) TRACE_OK'1869 match RTLabs_cost (new_state … tlr) return λx. RTLabs_cost (new_state … tlr) = x → finite_prefix ge start' with 1870 [ true ⇒ λCS. fp_tal ge start' (new_state … tlr) (tal_base_call (RTLabs_status ge) start' next' (new_state … tlr) ? CL ? (new_trace … tlr) ((proj1 … (RTLabs_costed ge ?)) … CS)) (remainder … tlr) TRACE_OK' 1675 1871  false ⇒ λCS. 1676 1872 let fs ≝ finite_segment ge (new_state … tlr) n' (remainder … tlr) ORACLE TRACE_OK' ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in … … 1679 1875 ] 1680 1876  or_intror NO_TERMINATION ⇒ 1681 fp_tac ????? (tac_base (RTLabs_status ge) start CL) ? EVtrace' ?1877 fp_tac ge start' start' next' (tac_base (RTLabs_status ge) start' CL) ?? trace' ? 1682 1878 ] 1683 1879  cl_return ⇒ λCL. ⊥ 1684 1880 ] (refl ??) 1685  ft_wrong start m NF EV ⇒ λTRACE_OK,LABEL_LIMIT. ⊥ 1686 ] TRACE_OK 1881  ft_wrong start m NF EV ⇒ λmtc,TRACE_OK,LABEL_LIMIT. ⊥ 1882 ] mtc0 1883 ] trace TRACE_OK 1687 1884 ] LABEL_LIMIT. 1688 1885 [ cases (state_bound_on_steps_to_cost_zero s) /2/ … … 1690 1887  @(absurd ?? (ro_no_termination … TRACE_OK)) 1691 1888 %{0} % @wr_base // 1692  @RTLabs_costed @(well_cost_labelled_jump … EV) /2/ 1693  5,6,8,9,10,11: /3/ 1694  % [ @(well_cost_labelled_state_step … EV) /2/ 1695  @(soundly_labelled_state_step … EV) /2/ 1889  @(proj1 … (RTLabs_costed …)) @(well_cost_labelled_jump … EV) [ @(ro_well_cost_labelled … TRACE_OK)  // ] 1890  5,6,9,10,11: /3/ 1891  cases TRACE_OK #H1 #H2 #H3 #H4 #H5 1892 % [ @(well_cost_labelled_state_step … EV) // 1893  @(soundly_labelled_state_step … EV) // 1696 1894  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % @wr_step /2/ 1697  @(still_not_wrong … EV) / 2/1895  @(still_not_wrong … EV) // 1698 1896  @(not_return_to_not_final … EV) >CL % #E destruct 1699 1897 ] 1700  /2/ 1701  @(bound_after_call ge … LABEL_LIMIT CL ? CS) 1702 @(RTLabs_after_call … CL EV) @(stack_ok … tlr) 1898  @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr)) 1899  @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr)) 1900  @(bound_after_call ge start' (new_state … tlr) ? LABEL_LIMIT CL ? CS) 1901 @(RTLabs_after_call ge start' next' … EV (stack_ok … tlr)) 1703 1902  % [ /2/ 1704 1903  @(soundly_labelled_state_preserved … (stack_ok … tlr)) 1705 @(soundly_labelled_state_step … EV) /2/ 1904 @(soundly_labelled_state_step … EV) /2/ @(ro_soundly_labelled … TRACE_OK) 1706 1905  @(not_to_not … (ro_no_termination … TRACE_OK)) * #depth * #TM1 %{depth} % 1707 1906 @wr_call // … … 1709 1908 cases (terminates … tlr) // 1710 1909  @(will_return_not_wrong … TERMINATES) 1711 [ @(still_not_wrong … EV) /2/1910 [ @(still_not_wrong … EV) @(ro_not_undefined … TRACE_OK) 1712 1911  cases (terminates … tlr) // 1713 1912 ] … … 1716 1915 [ #H101 #H102 #H103 #H104 #H105 #H106 #H107 #H108 #H109 destruct 1717 1916  #s1 #f #f' #fs #m #N #F #S #E1 #E2 #E3 #E4 TERMINATES destruct @refl 1718  #s1 #r #S #E1 #E2 #E3 #E4 TERMINATES destruct 1917  #s1 #r #S #E1 #E2 #E3 #E4 TERMINATES destruct whd in S:(??%); next' s0 1719 1918 cases (rtlabs_call_inv … CL) #fd * #args * #dst * #stk * #m #E destruct 1720 1919 inversion (eval_preserves … EV) 1721 [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 TRACE_OKdestruct ]1722 #ge' #fn #locals #next #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 TRACE_OK destruct1920 [ 1,2,4,5,6: #H111 #H112 #H113 #H114 #H115 #H116 #H117 #H118 try #H119 try #H120 try #H121 try #H122 try #H123 @⊥ next destruct ] 1921 #ge' #fn #locals #nextx #nok #sp #fs #m' #args' #dst' #m'' #E1 #E2 #E3 #E4 TRACE_OK destruct 1723 1922 inversion S 1724 1923 [ #f #fs0 #m #E1 #E2 #E3 destruct  *: #H123 #H124 #H125 #H126 #H127 #H128 #H129 try #H130 destruct ] … … 1730 1929 ] 1731 1930 ] 1732  @(well_cost_labelled_state_step … EV) /2/ 1733  @(well_cost_labelled_call … EV) /2/1931  @(well_cost_labelled_state_step … EV) /2/ @(ro_well_cost_labelled … TRACE_OK) 1932  @(well_cost_labelled_call … EV) [ @(ro_well_cost_labelled … TRACE_OK)  // ] 1734 1933  /2/ 1735  % [ @(well_cost_labelled_state_step … EV) /2/ 1934  %{tr} %{EV} % 1935  cases TRACE_OK #H1 #H2 #H3 #H4 #H5 1936 % [ @(well_cost_labelled_state_step … EV) /2/ 1736 1937  @(soundly_labelled_state_step … EV) /2/ 1737 1938  @(not_to_not … NO_TERMINATION) * #depth * #TM % … … 1740 1941  @(not_return_to_not_final … EV) >CL % #E destruct 1741 1942 ] 1742  19,20,21: /2/ 1943  %2 @CL 1944  21,22: %{tr} %{EV} % 1743 1945  cases (bound_after_step … LABEL_LIMIT EV ?) 1744 1946 [ * [ #TERMINATES @⊥ @(absurd ?? (ro_no_termination … TRACE_OK)) %{0} % @wr_step [ %1 //  … … 1765 1967  // 1766 1968 ] 1767  % [ @(well_cost_labelled_state_step … EV) /2/ 1768  @(soundly_labelled_state_step … EV) /2/ 1969  cases TRACE_OK #H1 #H2 #H3 #H4 #H5 1970 % [ @(well_cost_labelled_state_step … EV) // 1971  @(soundly_labelled_state_step … EV) // 1769 1972  @(not_to_not … (ro_no_termination … TRACE_OK)) 1770 1973 * #depth * #TERM %{depth} % @wr_step /2/ … … 1784 1987 *) 1785 1988 1786 let corec make_label_diverges ge s1989 let corec make_label_diverges ge (s:RTLabs_state ge) 1787 1990 (trace: flat_trace io_out io_in ge s) 1788 1991 (ORACLE: termination_oracle) … … 1795 1998 [ ex_intro n B ⇒ 1796 1999 match finite_segment ge s n trace ORACLE TRACE_OK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED B 1797 return λs .λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s2000 return λs:RTLabs_state ge.λ_. RTLabs_cost s = true → trace_label_diverges_exists (RTLabs_status ge) s 1798 2001 with 1799 2002 [ fp_tal s s' T t tOK ⇒ λSTATEMENT_COSTLABEL. 1800 2003 let T' ≝ make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1801 tld_step (RTLabs_status ge) s s' (tll_base … T (RTLabs_costed… STATEMENT_COSTLABEL)) T'2004 tld_step' (RTLabs_status ge) s s' (tll_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) T' 1802 2005 (* 1803 2006 match make_label_diverges ge s' t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with … … 1805 2008 ex_intro ?? (tld_step (RTLabs_status ge) s s' (tll_base … T STATEMENT_COSTLABEL) T') I 1806 2009 ]*) 1807  fp_tac s s2 s3 trT WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL.2010  fp_tac s s2 s3 T WCL2 EV t tOK ⇒ λSTATEMENT_COSTLABEL. 1808 2011 let T' ≝ make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? in 1809 tld_base (RTLabs_status ge) s s2 s3 (tlc_base … T (RTLabs_costed… STATEMENT_COSTLABEL)) ?? T'2012 tld_base' (RTLabs_status ge) s s2 s3 (tlc_base … T ((proj1 … (RTLabs_costed …)) … STATEMENT_COSTLABEL)) ?? T' 1810 2013 (* 1811 2014 match make_label_diverges ge s3 t ORACLE tOK ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ? with … … 1815 2018 ] STATEMENT_COSTLABEL 1816 2019 ]. 1817 [ @( costed_RTLabs ge) @(trace_any_label_label … T)1818  %{tr}@EV2020 [ @((proj2 … (RTLabs_costed …))) @(trace_any_label_label … T) 2021  @EV 1819 2022  @(trace_any_call_call … T) 1820  @(well_cost_labelled_call … EV) // @(trace_any_call_call … T)2023  cases EV #tr * #EV' #N @(well_cost_labelled_call … EV') // @(trace_any_call_call … T) 1821 2024 ] qed. 1822 2025 … … 1852 2055 qed. 1853 2056 1854 let rec whole_structured_trace_exists ge p s 1855 (trace: flat_trace io_out io_in ge s) 2057 let rec whole_structured_trace_exists ge p (s:RTLabs_state ge) 1856 2058 (ORACLE: termination_oracle) 1857 2059 (ENV_COSTLABELLED: well_cost_labelled_ge ge) 1858 2060 (ENV_SOUNDLY_LABELLED: soundly_labelled_ge ge) 1859 : ∀INITIAL: make_initial_state p = OK ? s. 2061 : ∀trace: flat_trace io_out io_in ge s. 2062 ∀INITIAL: make_initial_state p = OK state s. 1860 2063 ∀NOT_WRONG: not_wrong ??? s trace. 1861 2064 ∀STATE_COSTLABELLED: well_cost_labelled_state s. 1862 2065 ∀STATE_SOUNDLY_LABELLED: soundly_labelled_state s. 1863 trace_whole_program_exists (RTLabs_status ge) s ≝ 1864 match trace return λs,trace. make_initial_state p = OK ? s → 2066 trace_whole_program_exists (RTLabs_status ge) s ≝ 2067 match s return λs:RTLabs_state ge. ∀trace:flat_trace io_out io_in ge s. 2068 make_initial_state p = OK ? s → 2069 not_wrong ??? s trace → 2070 well_cost_labelled_state s → 2071 soundly_labelled_state s → 2072 trace_whole_program_exists (RTLabs_status ge) s with 2073 [ mk_RTLabs_state s0 stk mtc0 ⇒ λtrace. 2074 match trace return λs,trace. ∀mtc:Ras_Fn_Match ge s stk. 2075 make_initial_state p = OK state s → 1865 2076 not_wrong ??? s trace → 1866 2077 well_cost_labelled_state s → 1867 2078 soundly_labelled_state s → 1868 trace_whole_program_exists (RTLabs_status ge) swith1869 [ ft_step s tr next EV trace' ⇒ λ INITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED.2079 trace_whole_program_exists (RTLabs_status ge) (mk_RTLabs_state ge s stk mtc) with 2080 [ ft_step s tr next EV trace' ⇒ λmtc,INITIAL,NOT_WRONG,STATE_COSTLABELLED,STATE_SOUNDLY_LABELLED. 1870 2081 let IS_CALL ≝ initial_state_is_call … INITIAL in 2082 let s' ≝ mk_RTLabs_state ge s stk mtc in 2083 let next' ≝ next_state ge s' next tr EV in 1871 2084 match ORACLE ge O next trace' with 1872 2085 [ or_introl TERMINATES ⇒ 1873 2086 match TERMINATES with 1874 2087 [ witness TERMINATES ⇒ 1875 let tlr ≝ make_label_return' ge O next trace' ENV_COSTLABELLED ?? TERMINATES in1876 twp_terminating (RTLabs_status ge) s next(new_state … tlr) IS_CALL ? (new_trace … tlr) ?2088 let tlr ≝ make_label_return' ge O next' trace' ENV_COSTLABELLED ?? TERMINATES in 2089 twp_terminating (RTLabs_status ge) s' next' (new_state … tlr) IS_CALL ? (new_trace … tlr) ? 1877 2090 ] 1878  or_intror NO_TERMINATION ⇒ 1879 twp_diverges (RTLabs_status ge) s nextIS_CALL ?1880 (make_label_diverges ge next trace' ORACLE ?2091  or_intror NO_TERMINATION ⇒ 2092 twp_diverges (RTLabs_status ge) s' next' IS_CALL ? 2093 (make_label_diverges ge next' trace' ORACLE ? 1881 2094 ENV_COSTLABELLED ENV_SOUNDLY_LABELLED ?) 1882 2095 ] 1883  ft_stop st FINAL ⇒ λ INITIAL,NOT_WRONG. ⊥1884  ft_wrong start m NF EV ⇒ λ INITIAL,NOT_WRONG. ⊥1885 ] .2096  ft_stop st FINAL ⇒ λmtc,INITIAL,NOT_WRONG. ⊥ 2097  ft_wrong start m NF EV ⇒ λmtc,INITIAL,NOT_WRONG. ⊥ 2098 ] mtc0 ]. 1886 2099 [ cases (rtlabs_call_inv … (initial_state_is_call … INITIAL)) #fn * #args * #dst * #stk * #m #E destruct 1887 2100 cases FINAL #E @E @refl 1888  %{tr} @EV2101  %{tr} %{EV} % 1889 2102  @(after_the_initial_call_is_the_final_state … INITIAL EV) 1890 2103 @(stack_ok … tlr) 1891 2104  @(well_cost_labelled_state_step … EV) // 1892 2105  @(well_cost_labelled_call … EV) // 1893  %{tr} @EV2106  %{tr} %{EV} % 1894 2107  @(well_cost_labelled_call … EV) // 1895 2108  % [ @(well_cost_labelled_state_step … EV) // … … 1929 2142 *) 1930 2143 2144 lemma simplify_exec : ∀ge.∀s,s':RTLabs_state ge. 2145 as_execute (RTLabs_status ge) s s' → 2146 ∃tr. eval_statement ge s = Value … 〈tr,s'〉. 2147 #ge #s #s' * #tr * #EX #_ %{tr} @EX 2148 qed. 2149 1931 2150 (* as_execute might be in Prop, but because the semantics is deterministic 1932 2151 we can retrieve the event trace anyway. *) 1933 let rec deprop_as_execute ge s s' 1934 (X:as_execute (RTLabs_status ge) s s') 2152 2153 let rec deprop_execute ge (s,s':state) 2154 (X:∃t. eval_statement ge s = Value … 〈t,s'〉) 1935 2155 : Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝ 1936 match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = ?with2156 match eval_statement ge s return λE. (∃t.E = ?) → Σt.E = Value … 〈t,s'〉 with 1937 2157 [ Value ts ⇒ λY. «fst … ts, ?» 1938 2158  _ ⇒ λY. ⊥ … … 1941 2161  cases Y #trP #E destruct @refl 1942 2162 ] qed. 2163 2164 let rec deprop_as_execute ge (s,s':RTLabs_state ge) 2165 (X:as_execute (RTLabs_status ge) s s') 2166 : Σtr. eval_statement ge s = Value … 〈tr,s'〉 ≝ 2167 deprop_execute ge s s' ?. 2168 cases X #tr * #EX #_ %{tr} @EX 2169 qed. 1943 2170 1944 2171 (* A nonempty finite section of a flat_trace *) … … 1964 2191 1965 2192 (* Extract a flat trace from a structured one. *) 1966 let rec flat_trace_of_label_return ge s s'2193 let rec flat_trace_of_label_return ge (s,s':RTLabs_state ge) 1967 2194 (tr:trace_label_return (RTLabs_status ge) s s') 1968 2195 on tr : … … 1975 2202 (flat_trace_of_label_return ge s2 s3 tlr) 1976 2203 ] 1977 and flat_trace_of_label_label ge ends s s'2204 and flat_trace_of_label_label ge ends (s,s':RTLabs_state ge) 1978 2205 (tr:trace_label_label (RTLabs_status ge) ends s s') 1979 2206 on tr : … … 1982 2209 [ tll_base e s1 s2 tal _ ⇒ flat_trace_of_any_label ge e s1 s2 tal 1983 2210 ] 1984 and flat_trace_of_any_label ge ends s s'2211 and flat_trace_of_any_label ge ends (s,s':RTLabs_state ge) 1985 2212 (tr:trace_any_label (RTLabs_status ge) ends s s') 1986 2213 on tr : … … 2013 2240 (* We take an extra step so that we can always return a nonempty trace to 2014 2241 satisfy the guardedness condition in the cofixpoint. *) 2015 let rec flat_trace_of_any_call ge s s' s''et2242 let rec flat_trace_of_any_call ge (s,s',s'':RTLabs_state ge) et 2016 2243 (tr:trace_any_call (RTLabs_status ge) s s') 2017 2244 (EX'':eval_statement ge s' = Value … 〈et,s''〉) 2018 2245 on tr : 2019 partial_flat_trace io_out io_in ge s s'' ≝ 2020 match tr return λs,s' .λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with2246 partial_flat_trace io_out io_in ge s s'' ≝ 2247 match tr return λs,s':RTLabs_state ge.λ_. eval_statement ge s' = ? → partial_flat_trace io_out io_in ge s s'' with 2021 2248 [ tac_base s1 CL ⇒ λEX''. pft_base … ge ??? EX'' 2022 2249  tac_step_call s1 s2 s3 s4 EX CL AR tlr CS tac ⇒ λEX''. … … 2034 2261 ] EX''. 2035 2262 2036 let rec flat_trace_of_label_call ge s s' s''et2263 let rec flat_trace_of_label_call ge (s,s',s'':RTLabs_state ge) et 2037 2264 (tr:trace_label_call (RTLabs_status ge) s s') 2038 2265 (EX'':eval_statement ge s' = Value … 〈et,s''〉) … … 2046 2273 to take care to satisfy the guardedness condition by witnessing the fact that 2047 2274 the partial traces are nonempty. *) 2048 let corec flat_trace_of_label_diverges ge s2275 let corec flat_trace_of_label_diverges ge (s:RTLabs_state ge) 2049 2276 (tr:trace_label_diverges (RTLabs_status ge) s) 2050 2277 : flat_trace io_out io_in ge s ≝ 2051 match tr with2278 match tr return λs:RTLabs_state ge.λtr:trace_label_diverges (RTLabs_status ge) s. flat_trace io_out io_in ge s with 2052 2279 [ tld_step sx sy tll tld ⇒ 2053 match flat_trace_of_label_label ge … tll with 2054 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2055  pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) 2056 ] tld 2057  tld_base s1 s2 s3 tlc EX CL tld ⇒ 2058 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2059 match flat_trace_of_label_call … tlc EX' with 2060 [ pft_base s1 tr s2 EX ⇒ λtld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2061  pft_step s1 et s2 s3 EX tr' ⇒ λtld. ft_step … EX (add_partial_flat_trace ge … tr' tld) 2062 ] tld 2063 ] 2280 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 ⇒ 2281 λtll. 2282 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 with 2283 [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2284  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) 2285 ] mtc0 ] tll tld 2286  tld_base s1 s2 s3 tlc EX CL tld ⇒ 2287 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 ⇒ 2288 λEX. match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2289 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 with 2290 [ pft_base s1 tr s2 EX ⇒ λmtc,tld. ft_step … EX (flat_trace_of_label_diverges ge ? tld) 2291  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) 2292 ] mtc0 2293 ] 2294 ] EX tld 2064 2295 ] 2065 2296 (* Helper to keep adding the partial trace without violating the guardedness 2066 2297 condition. *) 2067 and add_partial_flat_trace ge s s' 2068 (ptr:partial_flat_trace io_out io_in ge s s') 2069 (tr:trace_label_diverges (RTLabs_status ge) s') 2070 : flat_trace io_out io_in ge s ≝ 2071 match ptr with 2072 [ pft_base s tr s' EX ⇒ λtr. ft_step … EX (flat_trace_of_label_diverges ge s' tr) 2073  pft_step s1 et s2 s3 EX tr' ⇒ λtr. ft_step … EX (add_partial_flat_trace … tr' tr) 2074 ] tr 2075 . 2298 and add_partial_flat_trace ge (s:state) (s':RTLabs_state ge) 2299 : partial_flat_trace io_out io_in ge s s' → 2300 trace_label_diverges (RTLabs_status ge) s' → 2301 flat_trace io_out io_in ge s ≝ 2302 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 ⇒ 2303 λ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 with 2304 [ pft_base s tr s' EX ⇒ λmtc,tr. ft_step … EX (flat_trace_of_label_diverges ge ? tr) 2305  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) 2306 ] mtc ] 2307 . 2308 2076 2309 2077 2310 coinductive equal_flat_traces (ge:genv) : ∀s. flat_trace io_out io_in ge s → flat_trace io_out io_in ge s → Prop ≝ … … 2128 2361 ] qed. 2129 2362 2130 let corec diverging_traces_have_unique_flat_trace ge s2363 let corec diverging_traces_have_unique_flat_trace ge (s:RTLabs_state ge) 2131 2364 (str:trace_label_diverges (RTLabs_status ge) s) 2132 2365 (tr:flat_trace io_out io_in ge s) … … 2135 2368 qed. 2136 2369 2137 let rec flat_trace_of_whole_program ge s2370 let rec flat_trace_of_whole_program ge (s:RTLabs_state ge) 2138 2371 (tr:trace_whole_program (RTLabs_status ge) s) 2139 2372 on tr : flat_trace io_out io_in ge s ≝ 2140 match tr with2373 match tr return λs:RTLabs_state ge.λtr. flat_trace io_out io_in ge s with 2141 2374 [ twp_terminating s1 s2 sf CL EX tlr F ⇒ 2142 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2143 ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … sfF))2375 match deprop_as_execute ge ?? EX with [ mk_Sig tr EX' ⇒ 2376 ft_step … EX' (partial_to_flat_trace … (flat_trace_of_label_return … tlr) (ft_stop … F)) 2144 2377 ] 2145 2378  twp_diverges s1 s2 CL EX tld ⇒ … … 2149 2382 ]. 2150 2383 2151 let corec whole_traces_have_unique_flat_trace ge s2384 let corec whole_traces_have_unique_flat_trace ge (s:RTLabs_state ge) 2152 2385 (str:trace_whole_program (RTLabs_status ge) s) 2153 2386 (tr:flat_trace io_out io_in ge s) 
src/RTLabs/semantics.ma
r2025 r2044 256 256 . 257 257 258 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Prop.258 lemma bind_ok : ∀A,B,e,f,v. ∀P:B → Type[0]. 259 259 (∀a. e = OK A a → f a = OK ? v → P v) → 260 260 (match e with [ OK v ⇒ f v  Error m ⇒ Error ? m ] = OK ? v → P v). … … 305 305 ] qed. 306 306 307 (* Show that, in principle at least, we can calculate which function we called 308 on a transition. The proof is a functional inversion similar to eval_preserves, 309 above. *) 310 311 definition func_block_of_exec : ∀ge,s,t,fd,args,dst,fs,m. 312 eval_statement ge s = Value ??? 〈t,Callstate fd args dst fs m〉 → 313 Σb:block. find_funct_ptr … ge b = Some ? fd. 314 #ge * 315 [ * #func #locals #next #nok #sp #dst #fs #m #tr #fd #args #dst' #fs' #m' 316 whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); 317 cases (lookup_present … nok) 318 (* Function call cases. *) 319 [ 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 320 [ %{v} @Efd 321  cases v in Efd; 322 [ 5: * #pty #b #pc #off #Efd %{b} whd in Efd:(??(???%)?); cases (eq_offset ??) in Efd; 323 [ #E @E  #E normalize in E; destruct ] 324  *: normalize #A try #B try #C destruct 325 ] 326 ] 327 (* and everything else cannot occur, but we need to work through the 328 definition to find the resulting state to demonstrate that. *) 329  #l #LP whd in ⊢ (??%? → ?); #E destruct 330  #c #l #LP whd in ⊢ (??%? → ?); #E destruct 331  #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct 332  #t1 #t2 #op #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 333  #t1 #t2 #t' #op #r1 #r2 #r3 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v1 #Ev1 @bind_ok #v2 #Ev2 @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 334  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 335  #ch #r1 #r2 #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #v' #Ev' @bind_ok #loc #Eloc #E whd in E:(??%?); destruct 336  #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct 337  #r #ls #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev cases v [ #E whd in E:(??%?); destruct  #sz #i whd in ⊢ (??%? → ?); generalize in ⊢ (??(?%)? → ?); cases (nth_opt ?? ls) in ⊢ (∀e:???%. ??(match % with [_ ⇒ ?_ ⇒ ?]?)? → ?); [ #e #E whd in E:(??%?); destruct  #l' #e #E whd in E:(??%?); destruct ]  *: #vl #E whd in E:(??%?); destruct ] 338  #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result func) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct 339 ] 340  * #fn #args #retdst #stk #m #tr #fd' #args' #dst' #fs' #m' 341 whd in ⊢ (??%? → ?); 342 [ @bind_res_value #loc #Eloc cases (alloc m O ??) #m' #b whd in ⊢ (??%? → ?); 343 #E destruct 344  @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct 345 ] 346  #v #r * [2: #f #fs ] #m #tr #fd' #args' #dst' #fs' #m' 347 whd in ⊢ (??%? → ?); 348 [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct 349  cases v [ normalize #E destruct  * [ 2: * #r normalize #E destruct  *: normalize #a try #b destruct ] ] 350 ] 351  #r #tr #fd' #args' #dst' #fs' #m' 352 normalize #E destruct 353 ] qed. 354 307 355 308 356 lemma initial_state_is_not_final : ∀p,s.
Note: See TracChangeset
for help on using the changeset viewer.