[2839] | 1 | |
---|
| 2 | include "RTLabs/RTLabs_partial_traces.ma". |
---|
| 3 | include "common/Measurable.ma". |
---|
| 4 | include "common/stacksize.ma". |
---|
| 5 | |
---|
| 6 | definition RTLabs_stack_ident : |
---|
| 7 | genv → |
---|
| 8 | ∀s:state. |
---|
| 9 | match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → |
---|
| 10 | ident ≝ |
---|
| 11 | λge,s. |
---|
| 12 | match s return λs. match RTLabs_classify s with [ cl_call ⇒ True | _ ⇒ False ] → ident with |
---|
| 13 | [ Callstate id _ _ _ _ _ ⇒ λ_. id |
---|
| 14 | | State f fs m ⇒ λH.⊥ |
---|
| 15 | | _ ⇒ λH.⊥ |
---|
| 16 | ]. |
---|
| 17 | try @H |
---|
| 18 | whd in match (RTLabs_classify ?) in H; |
---|
| 19 | cases (next_instruction f) in H; |
---|
| 20 | normalize // |
---|
| 21 | qed. |
---|
| 22 | |
---|
| 23 | definition RTLabs_pcsys ≝ mk_preclassified_system |
---|
| 24 | RTLabs_fullexec |
---|
| 25 | (λ_.RTLabs_cost) |
---|
| 26 | (λ_.RTLabs_classify) |
---|
| 27 | RTLabs_stack_ident. |
---|
| 28 | |
---|
| 29 | definition state_at : ∀C:preclassified_system. |
---|
| 30 | ∀p:program ?? C. nat → |
---|
| 31 | res (state … C (make_global … C p)) ≝ |
---|
| 32 | λC,p,n. |
---|
| 33 | let g ≝ make_global … (pcs_exec … C) p in |
---|
| 34 | let C' ≝ pcs_to_cs C g in |
---|
| 35 | ! s0 ← make_initial_state … p; |
---|
| 36 | ! 〈prefix,s1〉 ← exec_steps n ?? (cs_exec … C') g s0; |
---|
| 37 | return s1. |
---|
| 38 | |
---|
| 39 | definition eval_ext_statement : ∀ge. RTLabs_ext_state ge → IO io_out io_in (trace × (RTLabs_ext_state ge)) ≝ |
---|
| 40 | λge,s. |
---|
| 41 | match eval_statement ge s return λx. (∀s',t. x = Value ??? 〈t,s'〉 → RTLabs_ext_state ge) → ? with |
---|
| 42 | [ Value ts ⇒ λnext. Value ??? 〈\fst ts, next (\snd ts) (\fst ts) ?〉 |
---|
| 43 | | Wrong m ⇒ λ_. Wrong ??? m |
---|
| 44 | | Interact o k ⇒ λ_. Wrong … (msg UnexpectedIO) |
---|
| 45 | ] (next_state ge s). |
---|
| 46 | // |
---|
| 47 | qed. |
---|
| 48 | |
---|
[2896] | 49 | lemma drop_exec_ext : ∀ge,s,tr,s'. |
---|
| 50 | eval_ext_statement ge s = return 〈tr,s'〉 → |
---|
| 51 | eval_statement ge s = return 〈tr,Ras_state … s'〉. |
---|
| 52 | #ge #s #tr #s' |
---|
| 53 | whd in ⊢ (??%? → ?); |
---|
| 54 | letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) |
---|
| 55 | cut (∀s',t,EV. Ras_state … (f s' t EV) = s') |
---|
| 56 | [ // ] |
---|
| 57 | generalize in match f; -f |
---|
| 58 | cases (eval_statement ge s) |
---|
| 59 | [ #o #k #n #N #E whd in E:(??%%); destruct |
---|
| 60 | | * #tr' #s'' #next #NEXT #E whd in E:(??%%); destruct >NEXT // |
---|
| 61 | | #m #n #N #E whd in E:(??%%); destruct |
---|
| 62 | ] qed. |
---|
| 63 | |
---|
| 64 | lemma as_eval_ext_statement : ∀ge,s,tr,s'. |
---|
| 65 | eval_ext_statement ge s = Value … 〈tr,s'〉 → |
---|
| 66 | as_execute (RTLabs_status ge) s s'. |
---|
| 67 | #ge #s #tr #s' #EX |
---|
| 68 | whd %{tr} %{(drop_exec_ext … EX)} |
---|
| 69 | whd in EX:(??%?); |
---|
| 70 | letin ns ≝ (next_state ge s) in EX; #EX |
---|
| 71 | change with (ns s' tr ?) in match (next_state ge s s' tr ?); |
---|
| 72 | generalize in match (drop_exec_ext ?????); |
---|
| 73 | #EX' |
---|
| 74 | generalize in match ns in EX ⊢ %; -ns >EX' #ns whd in ⊢ (??%? → %); |
---|
| 75 | #E destruct @e1 |
---|
| 76 | qed. |
---|
| 77 | |
---|
[2839] | 78 | definition RTLabs_ext_exec : trans_system io_out io_in ≝ |
---|
| 79 | mk_trans_system io_out io_in ? RTLabs_ext_state (λ_.RTLabs_is_final) eval_ext_statement. |
---|
| 80 | |
---|
| 81 | definition make_ext_initial_state : ∀p:RTLabs_program. res (RTLabs_ext_state (make_global p)) ≝ |
---|
| 82 | λp. |
---|
| 83 | let ge ≝ make_global p in |
---|
| 84 | do m ← init_mem … (λx.[Init_space x]) p; |
---|
| 85 | let main ≝ prog_main ?? p in |
---|
[2895] | 86 | do b as Eb ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol … ge main); |
---|
[2839] | 87 | do f as Ef ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr … ge b); |
---|
| 88 | let s ≝ Callstate main f (nil ?) (None ?) (nil ?) m in |
---|
| 89 | return (mk_RTLabs_ext_state (make_global p) s [b] ?). |
---|
[2895] | 90 | % [ % assumption | % ] |
---|
[2839] | 91 | qed. |
---|
| 92 | |
---|
| 93 | lemma initial_states_OK : ∀p,s. |
---|
| 94 | make_ext_initial_state p = return s → |
---|
| 95 | make_initial_state p = return (Ras_state … s). |
---|
| 96 | #p #s #E |
---|
| 97 | cases (bind_inversion ????? E) -E #m * #E1 #E |
---|
[2895] | 98 | cases (bind_as_inversion ????? E) -E #b * #Eb #E |
---|
[2839] | 99 | cases (bind_as_inversion ????? E) -E #f * #Ef #E |
---|
| 100 | whd in ⊢ (??%?); >E1 |
---|
[2895] | 101 | whd in ⊢ (??%?); >Eb |
---|
[2839] | 102 | whd in ⊢ (??%?); >Ef |
---|
| 103 | whd in E:(??%%) ⊢ (??%?); destruct |
---|
| 104 | % |
---|
| 105 | qed. |
---|
| 106 | |
---|
| 107 | lemma initial_states_OK' : ∀p,s. |
---|
| 108 | make_initial_state p = return s → |
---|
| 109 | ∃S,M. make_ext_initial_state p = return (mk_RTLabs_ext_state (make_global p) s S M). |
---|
| 110 | #p #s #E |
---|
| 111 | cases (bind_inversion ????? E) -E #m * #E1 #E |
---|
[2895] | 112 | cases (bind_inversion ????? E) -E #b * #Eb #E |
---|
[2839] | 113 | cases (bind_inversion ????? E) -E #f * #Ef #E |
---|
| 114 | whd in E:(??%%); destruct |
---|
[2895] | 115 | %{[b]} % [ % [ % assumption | % ] ] |
---|
[2839] | 116 | whd in ⊢ (??%?); >E1 |
---|
| 117 | whd in ⊢ (??%?); generalize in match (refl ??); |
---|
[2895] | 118 | >Eb in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Eb' |
---|
| 119 | whd in ⊢ (??%?); generalize in match (refl ??); |
---|
[2839] | 120 | >Ef in ⊢ (???% → ??(match % with [_⇒?|_⇒?]?)?); #Ef' % |
---|
| 121 | qed. |
---|
| 122 | |
---|
| 123 | |
---|
| 124 | definition RTLabs_ext_fullexec : fullexec io_out io_in ≝ |
---|
| 125 | mk_fullexec … RTLabs_ext_exec make_global make_ext_initial_state. |
---|
| 126 | |
---|
| 127 | definition RTLabs_ext_pcsys ≝ mk_preclassified_system |
---|
| 128 | RTLabs_ext_fullexec |
---|
| 129 | (λg,s. RTLabs_cost (Ras_state … s)) |
---|
| 130 | (λg,s. RTLabs_classify (Ras_state … s)) |
---|
| 131 | (λg,s,H. RTLabs_stack_ident g (Ras_state … s) H). |
---|
| 132 | |
---|
| 133 | lemma will_return_equiv : ∀ge,trace,depth,n,s,s',EX. |
---|
| 134 | will_return_aux (pcs_to_cs … RTLabs_pcsys ge) depth trace → |
---|
[2895] | 135 | ΣWR:will_return ge depth s (make_flat_trace ge n s trace s' EX). |
---|
| 136 | will_return_end … WR = ?. |
---|
| 137 | [2: %{s'} @ft_stop ] (* XXX replace ? above? *) |
---|
[2839] | 138 | #ge #trace0 elim trace0 |
---|
| 139 | [ #depth #n #s #s' #EX * |
---|
| 140 | | * #s1 #tr1 #tl #IH #depth #n #s #s' #EX |
---|
| 141 | lapply (exec_steps_length … EX) #E1 |
---|
| 142 | lapply (exec_steps_first … EX) #E2 |
---|
| 143 | lapply (refl ? (eval_statement ge s)) |
---|
| 144 | cases (eval_statement ge s) in ⊢ (???% → ?); |
---|
| 145 | [ #o #k destruct #EV @⊥ |
---|
| 146 | whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX; |
---|
| 147 | [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????); |
---|
| 148 | >EV #EX whd in EX:(??%%); destruct |
---|
| 149 | | #r #EX whd in EX:(??%%); destruct |
---|
| 150 | ] |
---|
| 151 | | 3: #m #EV @⊥ destruct |
---|
| 152 | whd in EX:(??%?); cases (is_final io_out io_in RTLabs_fullexec ge s1) in EX; |
---|
| 153 | [ whd in ⊢ (??%? → ?); change with (eval_statement ??) in match (step ?????); |
---|
| 154 | >EV #EX whd in EX:(??%%); destruct |
---|
| 155 | | #r #EX whd in EX:(??%%); destruct |
---|
| 156 | ] |
---|
| 157 | ] * #tr2 #s2 #EV >E1 in EX; #EX |
---|
| 158 | whd in ⊢ (?% → ?); |
---|
| 159 | lapply (refl ? (cs_classify ? s1)) |
---|
| 160 | cases (cs_classify ??) in ⊢ (???% → %); |
---|
| 161 | #CL whd in ⊢ (?% → ?); |
---|
| 162 | [ cases depth |
---|
| 163 | [ whd in ⊢ (?% → ?); cases tl in EX ⊢ %; |
---|
| 164 | [ #EX #_ |
---|
| 165 | lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
[2895] | 166 | %{(wr_base …)} |
---|
| 167 | [ destruct @CL |
---|
| 168 | | cases CFT #ctr #cs #cEV #cEX #cmake whd in ⊢ (??%?); |
---|
| 169 | whd in cEX:(??%%); destruct % |
---|
| 170 | ] |
---|
[2839] | 171 | | * #s3 #tr3 #tl3 #EX * |
---|
| 172 | ] |
---|
| 173 | | #depth' whd in ⊢ (?% → ?); #H |
---|
| 174 | lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
[2895] | 175 | cases (IH ???? (cft_EX … CFT) H) #WR' #WRe |
---|
| 176 | %{(wr_ret …)} |
---|
| 177 | [ @WR' |
---|
| 178 | | destruct @CL |
---|
| 179 | | @WRe |
---|
[2839] | 180 | ] |
---|
| 181 | ] |
---|
| 182 | | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
[2895] | 183 | cases (IH ???? (cft_EX … CFT) H) #WR' #WRe |
---|
| 184 | %{(wr_step …)} [ @WR' | %2 destruct @CL | @WRe ] |
---|
[2839] | 185 | | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
[2895] | 186 | cases (IH ???? (cft_EX … CFT) H) #WR' #WRe |
---|
| 187 | %{(wr_call …)} [ @WR' | destruct @CL | @WRe ] |
---|
[2839] | 188 | | cases (RTLabs_notail … CL) |
---|
| 189 | | #H lapply (cons_flat_trace … EX) #CFT >(cft_E … CFT) |
---|
[2895] | 190 | cases (IH ???? (cft_EX … CFT) H) #WR' #WRe |
---|
| 191 | %{(wr_step …)} [ @WR' | %1 destruct @CL | @WRe ] |
---|
[2839] | 192 | ] |
---|
| 193 | ] qed. |
---|
| 194 | |
---|
[2895] | 195 | |
---|
[2894] | 196 | lemma extend_RTLabs_eval_statement : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'. |
---|
| 197 | eval_statement ge s = return 〈tr,s'〉 → |
---|
| 198 | ∃S,M. eval_ext_statement ge s = return 〈tr,mk_RTLabs_ext_state … s' S M〉. |
---|
| 199 | #ge #s #tr #s' #EV |
---|
| 200 | whd in match (eval_ext_statement ??); |
---|
| 201 | letin f ≝ (next_state ge s) (* Is there a more natural way to generalize partial applications? *) |
---|
| 202 | cut (∀s',t,EV. Ras_state … (f s' t EV) = s') |
---|
| 203 | [ // ] |
---|
| 204 | generalize in match f; -f |
---|
| 205 | >EV #next #NEXT whd in ⊢ (??(λ_.??(λ_.??%?))); |
---|
| 206 | lapply (NEXT … (refl ??)) |
---|
| 207 | cases (next s' tr ?) #s'' #S'' #M'' #E destruct %{S''} %{M''} % |
---|
| 208 | qed. |
---|
| 209 | |
---|
[2896] | 210 | lemma intensional_state_change_State : ∀ge,cs,f,fs,m. |
---|
| 211 | intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (State f fs m) = 〈cs,[ ]〉. |
---|
| 212 | #ge #cs #f #fs #m |
---|
| 213 | whd in ⊢ (??%?); |
---|
| 214 | generalize in match (cs_callee ??); |
---|
| 215 | whd in match (cs_classify ??); cases (next_instruction f) // |
---|
| 216 | qed. |
---|
| 217 | |
---|
| 218 | lemma final_pre_S : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s'. |
---|
| 219 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 220 | match s' with [Finalstate _ ⇒ Ras_fn_stack … s = [ ] | _ ⇒ True]. |
---|
| 221 | #ge #s #tr #s' #EV |
---|
| 222 | cases (extend_RTLabs_eval_statement … EV) #S * #M #EV' |
---|
| 223 | inversion (eval_preserves_ext … (as_eval_ext_statement … EV')) |
---|
| 224 | [ 6: #ge' #r #dst #m #M1 #M2 #E1 #E2 #E3 #E4 destruct whd % |
---|
| 225 | | *: #x1 #x2 #x3 #x4 #x5 #x6 #x7 #x8 #x9 #x10 #x11 #x12 #x13 #x14 try #x15 try #x16 try #x17 try #x18 destruct // |
---|
| 226 | ] qed. |
---|
| 227 | |
---|
| 228 | lemma extend_RTLabs_step : ∀ge. ∀s:RTLabs_ext_state ge. ∀tr,s',cs. |
---|
| 229 | eval_statement ge s = Value … 〈tr,s'〉 → |
---|
| 230 | All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) cs → |
---|
| 231 | ∃S',M'. |
---|
| 232 | eval_ext_statement ge s = Value … 〈tr,mk_RTLabs_ext_state … s' S' M'〉 ∧ |
---|
| 233 | All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S' (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s')). |
---|
| 234 | #ge #s #tr #s' #cs #EV #STACK |
---|
| 235 | whd in match (eval_ext_statement ??); |
---|
| 236 | letin ns ≝ (next_state ge s) |
---|
| 237 | cut (∀s',t,EV. Ras_state … (ns s' t EV) = s' ∧ |
---|
| 238 | match s' with |
---|
| 239 | [ State _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s |
---|
| 240 | | Callstate fid _ _ _ _ _ ⇒ ∃b. symbol_for_block … ge b = Some ? fid ∧ Ras_fn_stack … (ns s' t EV) = b::(Ras_fn_stack … s) |
---|
| 241 | | Returnstate _ _ _ _ ⇒ Ras_fn_stack … (ns s' t EV) = tail … (Ras_fn_stack … s) |
---|
| 242 | | Finalstate _ ⇒ Ras_fn_stack … (ns s' t EV) = Ras_fn_stack … s |
---|
| 243 | ]) |
---|
| 244 | [ #s'' #t #EV' % [ % | |
---|
| 245 | cases s'' in EV' ⊢ %; // |
---|
| 246 | [ #fid #fn #args #ret #fs #m #EV'' |
---|
| 247 | %{(func_block_of_exec … EV'')} % |
---|
| 248 | [ cases (func_block_of_exec … EV'') #b * #FS #FFP |
---|
| 249 | @(symbol_for_block_fn … FS FFP) |
---|
| 250 | | % |
---|
| 251 | ] |
---|
| 252 | | #r #EV whd lapply (final_pre_S … EV) whd in ⊢ (% → ?); #E >E % |
---|
| 253 | ] |
---|
| 254 | ] |
---|
| 255 | ] |
---|
| 256 | generalize in match ns; -ns |
---|
| 257 | >EV #next #NEXT cases (NEXT … (refl ??)) |
---|
| 258 | lapply (refl ? (next s' tr (refl ??))) |
---|
| 259 | cases (next s' tr ?) in ⊢ (???% → ?); |
---|
| 260 | #s'' #S'' #M'' |
---|
| 261 | #Enext1 >Enext1 #Enext2 destruct #Snext %{S''} %{M''} |
---|
| 262 | % |
---|
| 263 | [ whd in ⊢ (??%%); >Enext1 % |
---|
| 264 | | cases s' in Snext ⊢ %; |
---|
| 265 | [ #f #fs #m whd in ⊢ (% → ?); #E destruct |
---|
| 266 | >intensional_state_change_State @STACK |
---|
| 267 | | #fid #fn #args #ret #fs #m whd in ⊢ (% → ?); * #b * #SYM #ES destruct |
---|
| 268 | whd in match (intensional_state_change ???); |
---|
| 269 | whd in match (cs_callee ???); |
---|
| 270 | % [ @SYM | @STACK ] |
---|
| 271 | | #rv #rr #fs #m whd in ⊢ (% → ?); #ES destruct |
---|
| 272 | whd in match (intensional_state_change ???); |
---|
| 273 | >(?:\fst ? = tail ? cs) |
---|
| 274 | [2: cases cs // ] |
---|
| 275 | @All2_tail |
---|
| 276 | @STACK |
---|
| 277 | | #r whd in ⊢ (% → ?); #E destruct |
---|
| 278 | whd in match (intensional_state_change ???); |
---|
| 279 | @STACK |
---|
| 280 | ] |
---|
| 281 | ] qed. |
---|
| 282 | |
---|
| 283 | |
---|
| 284 | lemma extend_RTLabs_exec_steps : ∀ge,n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs,cs',itrace. |
---|
[2839] | 285 | exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → |
---|
[2896] | 286 | intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs trace = 〈cs',itrace〉 → |
---|
| 287 | All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) (Ras_fn_stack … s) (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs (Ras_state … s))) → |
---|
| 288 | ∃trace',S,M. |
---|
| 289 | exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧ |
---|
| 290 | All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')). |
---|
[2839] | 291 | #ge #n0 elim n0 |
---|
[2896] | 292 | [ * #s #S #M #trace #s' #cs #cs' #itrace #E whd in E:(??%%); destruct |
---|
| 293 | #E whd in E:(??%%); destruct |
---|
| 294 | #CS %{[ ]} |
---|
| 295 | %{S} %{M} % [ % | @CS ] |
---|
| 296 | | #n #IH * #s #S #M #trace #s' #cs #cs' #itrace #EX |
---|
[2839] | 297 | cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' |
---|
[2896] | 298 | >E whd in ⊢ (??%? → ?); @pair_elim #cs1 #itrace1 #ITOT1 |
---|
| 299 | whd in ⊢ (??%? → ?); @pair_elim #cs2 #itrace2 #ITOT2 #E' destruct |
---|
| 300 | #STACK |
---|
| 301 | cases (extend_RTLabs_step ge (mk_RTLabs_ext_state ge s S M) ??? STEP STACK) |
---|
| 302 | #S' * #M' * #STEP' #STACK' |
---|
| 303 | cases (IH (mk_RTLabs_ext_state ge s1 S' M') … EX' ITOT2 STACK') |
---|
| 304 | #tl' * #S'' * #M'' * #EX'' #STACK'' |
---|
| 305 | %{(〈mk_RTLabs_ext_state … s S M,tr〉::tl')} %{S''} %{M''} |
---|
| 306 | % |
---|
| 307 | [ whd in ⊢ (??%?); |
---|
| 308 | change with (RTLabs_is_final s) in match (is_final ?????); |
---|
| 309 | change with (RTLabs_is_final s) in match (is_final ?????) in NF; |
---|
| 310 | >NF whd in ⊢ (??%?); |
---|
| 311 | change with (eval_ext_statement ??) in match (step ?????); |
---|
| 312 | >STEP' whd in ⊢ (??%?); |
---|
| 313 | >EX'' % |
---|
| 314 | | @STACK'' |
---|
| 315 | ] |
---|
[2839] | 316 | ] qed. |
---|
[2892] | 317 | |
---|
[2896] | 318 | lemma extend_initial_RTLabs_exec_steps : ∀p. let ge ≝ make_global p in ∀n. ∀s:RTLabs_ext_state ge. ∀trace,s'.∀cs',itrace. |
---|
| 319 | exec_steps n … RTLabs_fullexec ge (Ras_state … s) = return 〈trace,s'〉 → |
---|
| 320 | intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) [ ] trace = 〈cs',itrace〉 → |
---|
| 321 | make_ext_initial_state p = OK ? s → |
---|
| 322 | ∃trace',S,M. |
---|
| 323 | exec_steps n … RTLabs_ext_fullexec ge s = return 〈trace',mk_RTLabs_ext_state … s' S M〉 ∧ |
---|
| 324 | All2 ?? (λb,id. symbol_for_block ? ge b = Some ? id) S (\fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs' s')). |
---|
| 325 | #p #n #s #trace #s' #cs' #itrace #EXEC #ITOT #INIT |
---|
| 326 | @(extend_RTLabs_exec_steps … EXEC ITOT) |
---|
| 327 | cases (bind_inversion ????? INIT) -INIT #m * #E1 #INIT |
---|
| 328 | cases (bind_as_inversion ????? INIT) -INIT #b * #Eb #INIT |
---|
| 329 | cases (bind_as_inversion ????? INIT) -INIT #f * #Ef #INIT |
---|
| 330 | whd in INIT:(??%%); lapply (Ras_fn_match … s) destruct |
---|
| 331 | * * #FS #FFP #_ |
---|
| 332 | % [ >(symbol_for_block_fn … FS FFP) % | % ] |
---|
| 333 | qed. |
---|
| 334 | |
---|
[2892] | 335 | lemma label_to_return_state_labelled : ∀C,n,s,trace,s'. |
---|
| 336 | trace_is_label_to_return C trace → |
---|
| 337 | exec_steps n ?? C ? s = OK ? 〈trace,s'〉 → |
---|
| 338 | cs_labelled C s. |
---|
| 339 | #C #n #s #trace #s' |
---|
| 340 | * #tr * #s1 * #trace' * #tr' * #s2 * * #E #CS #_ destruct |
---|
| 341 | #EX >(exec_steps_first … EX) |
---|
| 342 | @CS |
---|
| 343 | qed. |
---|
| 344 | |
---|
| 345 | lemma well_cost_labelled_exec_steps : ∀n,g,s,trace,s'. |
---|
| 346 | well_cost_labelled_ge g → |
---|
| 347 | exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 → |
---|
| 348 | well_cost_labelled_state s → |
---|
| 349 | well_cost_labelled_state s'. |
---|
| 350 | #n #g elim n |
---|
| 351 | [ #s #trace #s' #_ #E whd in E:(??%%); destruct // |
---|
| 352 | | #m #IH #s #trace #s' #WCLge #EX |
---|
| 353 | cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' |
---|
| 354 | #WCLs @(IH … WCLge … EX') |
---|
| 355 | @(well_cost_labelled_state_step … STEP WCLge WCLs) |
---|
| 356 | ] qed. |
---|
[2893] | 357 | |
---|
| 358 | lemma soundly_labelled_exec_steps : ∀n,g,s,trace,s'. |
---|
| 359 | soundly_labelled_ge g → |
---|
| 360 | exec_steps n ?? RTLabs_fullexec g s = OK ? 〈trace,s'〉 → |
---|
| 361 | soundly_labelled_state s → |
---|
| 362 | soundly_labelled_state s'. |
---|
| 363 | #n #g elim n |
---|
| 364 | [ #s #trace #s' #_ #E whd in E:(??%%); destruct // |
---|
| 365 | | #m #IH #s #trace #s' #SLge #EX |
---|
| 366 | cases (exec_steps_S … EX) #NF * #tr * #s1 * #tl * * #E #STEP #EX' |
---|
| 367 | #SLs @(IH … SLge … EX') |
---|
| 368 | @(soundly_labelled_state_step … SLge STEP SLs) |
---|
| 369 | ] qed. |
---|
| 370 | |
---|
[2894] | 371 | lemma int_trace_split : ∀C,t1,t2,callstack,cs2,obs. |
---|
| 372 | intensional_trace_of_trace C callstack (t1@t2) = 〈cs2,obs〉 → |
---|
| 373 | ∃cs1,t1',t2'. |
---|
| 374 | intensional_trace_of_trace C callstack t1 = 〈cs1,t1'〉 ∧ |
---|
| 375 | intensional_trace_of_trace C cs1 t2 = 〈cs2,t2'〉 ∧ |
---|
| 376 | obs = t1'@t2'. |
---|
| 377 | #C #t1 #t2 #cs0 #cs2 #obs >int_trace_append' |
---|
| 378 | cases (intensional_trace_of_trace C cs0 t1) #cs1 #t1' |
---|
| 379 | normalize nodelta #E %{cs1} %{t1'} |
---|
| 380 | cases (intensional_trace_of_trace C cs1 t2) in E ⊢ %; #cs2 #t2' |
---|
| 381 | normalize nodelta #E destruct |
---|
| 382 | %{t2'} |
---|
| 383 | /3/ |
---|
| 384 | qed. |
---|
| 385 | |
---|
| 386 | definition cs_change : trace_ends_with_ret → ident → list ident → list ident → Prop ≝ λends,fn,cs,cs'. |
---|
| 387 | match ends with |
---|
| 388 | [ ends_with_ret ⇒ cs = cs' |
---|
| 389 | | doesnt_end_with_ret ⇒ fn::cs = cs' |
---|
| 390 | ]. |
---|
| 391 | |
---|
| 392 | lemma as_exec_eq_step : ∀ge,s1,s2,tr,s2'. |
---|
| 393 | as_execute (RTLabs_status ge) s1 s2 → |
---|
[2896] | 394 | step io_out io_in RTLabs_fullexec ge (Ras_state … s1) = Value ??? 〈tr,s2'〉 → |
---|
| 395 | Ras_state … s2 = s2'. |
---|
| 396 | #ge #s1 #s2 #tr #s2' * #tr * #EX #NX |
---|
| 397 | change with (eval_statement ge (Ras_state … s1)) in ⊢ (??%? → ?); >EX #E destruct |
---|
| 398 | % |
---|
[2894] | 399 | qed. |
---|
| 400 | |
---|
| 401 | include alias "basics/logic.ma". (* For ∧ *) |
---|
| 402 | |
---|
| 403 | let rec eq_end_tlr ge s trace' s' tlr s'' on tlr : |
---|
[2896] | 404 | exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 → |
---|
| 405 | (Ras_state … s') = s'' ≝ ? |
---|
[2894] | 406 | and eq_end_tll ge s trace' s' ends tll s'' on tll : |
---|
[2896] | 407 | exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 → |
---|
| 408 | (Ras_state … s') = s'' ≝ ? |
---|
[2894] | 409 | and eq_end_tal ge s trace' s' ends tal s'' on tal : |
---|
[2896] | 410 | exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',s''〉 → |
---|
| 411 | (Ras_state … s') = s'' ≝ ?. |
---|
[2894] | 412 | [ cases tlr |
---|
| 413 | [ #s1 #s2 #tll @eq_end_tll |
---|
| 414 | | #s1 #s2 #s3 #tll #tlr' #EX |
---|
| 415 | cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 |
---|
| 416 | <(eq_end_tll … EX1) #EX2 #E |
---|
| 417 | @(eq_end_tlr … EX2) |
---|
| 418 | ] |
---|
| 419 | | cases tll |
---|
| 420 | #ends' #s1 #s2 #tal #CS |
---|
| 421 | @eq_end_tal |
---|
| 422 | | cases tal |
---|
| 423 | [ #s1 #s2 #EX #CL #CS whd in ⊢ (??(?%?????)? → ?); #EX' |
---|
| 424 | cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' |
---|
| 425 | whd in EX':(??%%); destruct |
---|
| 426 | @(as_exec_eq_step … EX ST) |
---|
| 427 | | #s1 #s2 #EX #CL #EX' |
---|
| 428 | cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' |
---|
| 429 | whd in EX':(??%%); destruct |
---|
| 430 | @(as_exec_eq_step … EX ST) |
---|
| 431 | | #s1 #s2 #s3 #EX #CL #AF #tlr #CS #EX' |
---|
| 432 | cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' |
---|
| 433 | lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' |
---|
| 434 | @(eq_end_tlr … tlr … EX') |
---|
| 435 | | #s1 #s2 #s3 #EX #CL #tlr #EX' |
---|
| 436 | cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' |
---|
| 437 | lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' |
---|
| 438 | @(eq_end_tlr … tlr … EX') |
---|
| 439 | | #ends #s1 #s2 #s3 #s4 #EX #CL #AF #tlr #CS #tal' #EX' |
---|
| 440 | cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' |
---|
| 441 | lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' |
---|
| 442 | cases (exec_steps_split … EX') #trace1 * #trace2 * #s5 * * #EX2 #EX3 #E3 |
---|
| 443 | lapply (eq_end_tlr … tlr … EX2) #E4 <E4 in EX3; #EX3 |
---|
| 444 | @(eq_end_tal … EX3) |
---|
| 445 | | #ends #s1 #s2 #s3 #EX #tal' #CL #CS #EX' |
---|
| 446 | cases (exec_steps_S … EX') #_ * #tr * #s2' * #tl * * #E #ST #EX' |
---|
| 447 | lapply (as_exec_eq_step … EX ST) #E2 <E2 in EX'; #EX' |
---|
| 448 | @(eq_end_tal … EX') |
---|
| 449 | ] |
---|
| 450 | ] qed. |
---|
| 451 | |
---|
| 452 | definition maybe_label ≝ |
---|
| 453 | λge,s,obs. |
---|
| 454 | match as_label (RTLabs_status ge) s with |
---|
| 455 | [ None ⇒ obs |
---|
| 456 | | Some cl ⇒ (IEVcost cl)::obs |
---|
| 457 | ]. |
---|
| 458 | |
---|
| 459 | lemma definitely_maybe_label : ∀ge,s,CS,tl. |
---|
| 460 | (IEVcost (as_label_safe (RTLabs_status ge) «s,CS»))::tl = maybe_label ge s tl. |
---|
| 461 | #ge #s #CS #tl |
---|
| 462 | whd in ⊢ (???%); whd in match (as_label_safe ??); |
---|
| 463 | >(opt_to_opt_safe … CS) in ⊢ (???%); |
---|
| 464 | % |
---|
| 465 | qed. |
---|
| 466 | |
---|
| 467 | lemma only_plain_step_events_is_one_cost : ∀ge,s,tr,s'. |
---|
| 468 | eval_statement ge s = Value ??? 〈tr,s'〉 → |
---|
| 469 | (∃cl. tr = [EVcost cl] ∧ RTLabs_cost_label s = Some ? cl) ∨ |
---|
| 470 | (tr = [ ] ∧ RTLabs_cost_label s = None ?). |
---|
| 471 | #ge * |
---|
| 472 | [ #f #fs #m #tr #s' whd in ⊢ (??%? → ?); |
---|
| 473 | whd in match (RTLabs_cost_label ?); generalize in ⊢ (??(?%)? → ?); |
---|
| 474 | cases (next_instruction f) |
---|
| 475 | [ #l #LP normalize nodelta #E whd in E:(??%%); destruct %2 % % |
---|
| 476 | | #cl #l #LP #E whd in E:(??%%); destruct % %{cl} % % |
---|
| 477 | | #t #r #c #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #locals' #Eloc #E whd in E:(??%?); destruct %2 % % |
---|
| 478 | | #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 %2 % % |
---|
| 479 | | #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 %2 % % |
---|
| 480 | | #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 %2 % % |
---|
| 481 | | #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 %2 % % |
---|
| 482 | | #id #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #b #Eb @bind_ok #fd #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct %2 % % |
---|
| 483 | | #r #rs #or #l #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok * #fd #fid #Efd @bind_ok #vs #Evs #E whd in E:(??%?); destruct cases (find_funct_find_funct_ptr ?? v ? Efd) #b * #Ev' #Efn %2 % % |
---|
| 484 | | #r #l1 #l2 #LP whd in ⊢ (??%? → ?); @bind_res_value #v #Ev @bind_ok #b #Eb #E whd in E:(??%?); destruct %2 % % |
---|
| 485 | | #LP whd in ⊢ (??%? → ?); @bind_res_value #v cases (f_result ?) [ 2: * #r #t whd in ⊢ (??%? → ?); @bind_ok #v0 #Ev0 ] #E whd in E:(??%?); #E' whd in E':(??%?); destruct %2 % % |
---|
| 486 | ] |
---|
| 487 | | #vf * #fn #args #retdst #stk #m #tr #s' |
---|
| 488 | whd in ⊢ (??%? → ?); |
---|
| 489 | [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?); |
---|
| 490 | #E destruct %2 % % |
---|
| 491 | | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct %2 % % |
---|
| 492 | ] |
---|
| 493 | | #v #r * [2: #f #fs ] #m #tr #s' |
---|
| 494 | whd in ⊢ (??%? → ?); |
---|
| 495 | [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct %2 % % |
---|
| 496 | | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct %2 % % | *: normalize #a try #b destruct ] ] |
---|
| 497 | ] |
---|
| 498 | | #r #tr #s' normalize #E destruct |
---|
| 499 | ] qed. |
---|
| 500 | |
---|
| 501 | lemma RTLabs_as_label : ∀ge,s. |
---|
| 502 | RTLabs_cost_label (Ras_state … s) = as_label (RTLabs_status ge) s. |
---|
| 503 | cut (None (identifier CostTag) ≠ None ? → False) [ * /2/ ] #NONE |
---|
| 504 | #ge * * |
---|
| 505 | [ * #func #locals #next #nok #sp #r #fs #m #stk #mtc |
---|
| 506 | whd in ⊢ (???%); |
---|
| 507 | whd in match (as_pc_of ??); |
---|
| 508 | cases stk in mtc ⊢ %; [ * ] #func_block #stk' * #M1 #M2 |
---|
| 509 | whd in ⊢ (???%); >M1 whd in ⊢ (???%); |
---|
| 510 | whd in ⊢ (??%?); change with (lookup_present ?????) in match (next_instruction ?); |
---|
| 511 | >(lookup_lookup_present … nok) whd in ⊢ (??%%); |
---|
| 512 | % |
---|
| 513 | | #vf #fd #args #dst #fs #m * [*] #func #stk #mtc whd in ⊢ (??%%); % |
---|
| 514 | | #v #dst #fs #m * [2: #fn #stk] #mtc % |
---|
| 515 | | // #r #stk #mtc % |
---|
| 516 | ] qed. |
---|
| 517 | |
---|
[2839] | 518 | |
---|
| 519 | |
---|
[2894] | 520 | lemma step_cost_event : ∀ge,s,tr,s',obs. |
---|
[2896] | 521 | step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → |
---|
[2894] | 522 | maybe_label ge s obs = intensional_events_of_events tr@obs. |
---|
| 523 | #ge #s #tr #s' #obs #ST |
---|
[2896] | 524 | cases (only_plain_step_events_is_one_cost … ST) |
---|
[2894] | 525 | [ * #cl * #E1 #CS whd in ⊢ (??%?); |
---|
| 526 | <RTLabs_as_label >CS destruct % |
---|
| 527 | | * #E #CS whd in ⊢ (??%?); |
---|
| 528 | <RTLabs_as_label >CS destruct % |
---|
| 529 | ] qed. |
---|
| 530 | |
---|
[2895] | 531 | lemma really_no_label : ∀ge,s,obs. |
---|
| 532 | ¬as_costed (RTLabs_status ge) s → |
---|
| 533 | maybe_label ge s obs = obs. |
---|
| 534 | #ge #s #obs |
---|
| 535 | whd in ⊢ (?% → ??%?); |
---|
| 536 | cases (as_label ??) |
---|
| 537 | [ // |
---|
| 538 | | #l * #H @⊥ @H % #E destruct |
---|
| 539 | ] qed. |
---|
| 540 | |
---|
| 541 | |
---|
[2894] | 542 | lemma call_ret_event : ∀ge,s,tr,s',obs. |
---|
[2896] | 543 | step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → |
---|
[2894] | 544 | (as_classify (RTLabs_status ge) s = cl_call ∨ as_classify (RTLabs_status ge) s = cl_return) → |
---|
| 545 | maybe_label ge s obs = obs ∧ tr = [ ]. |
---|
| 546 | #ge * * |
---|
| 547 | [ #f #fs #m #S #M #tr #s' #obs #ST * whd in match (as_classify ??); |
---|
| 548 | cases (next_instruction f) normalize |
---|
| 549 | #A try #B try #C try #D try #E try #F try #G try #H try #I destruct |
---|
| 550 | | #fid * #fn #args #retdst #stk #m #S #M #tr #s' #obs #ST #_ |
---|
| 551 | letin s ≝ (Callstate ??????) |
---|
| 552 | cut (RTLabs_cost_label s = None ?) |
---|
| 553 | [ 1,3: // ] #CS % |
---|
| 554 | [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ] |
---|
[2896] | 555 | lapply ST |
---|
[2894] | 556 | whd in ⊢ (??%? → ?); |
---|
| 557 | [ @bind_res_value #loc #Eloc cases (alloc m O ? (*?*)) #m' #b whd in ⊢ (??%? → ?); |
---|
| 558 | #E destruct % |
---|
| 559 | | @bindIO_value #evargs #Eargs whd in ⊢ (??%? → ?); #E destruct |
---|
| 560 | ] |
---|
| 561 | | #v #r * [2: #f #fs ] #m #S #M #tr #s' #obs |
---|
| 562 | letin s ≝ (Returnstate ????) #ST #_ |
---|
| 563 | cut (RTLabs_cost_label s = None ?) |
---|
| 564 | [ 1,3: // ] #CS % |
---|
| 565 | [ 1,3: whd in ⊢ (??%?); <RTLabs_as_label >CS % ] |
---|
[2896] | 566 | lapply ST |
---|
[2894] | 567 | whd in ⊢ (??%? → ?); |
---|
| 568 | [ @bind_res_value #loc #Eloc #E whd in E:(??%?); destruct % |
---|
| 569 | | cases v [ normalize #E destruct | * [ 2: * #r normalize #E destruct % | *: normalize #a try #b destruct ] ] |
---|
| 570 | ] |
---|
| 571 | | #r #S #M #tr #s' #obs normalize #E destruct |
---|
| 572 | ] qed. |
---|
| 573 | |
---|
[2895] | 574 | lemma as_call_cs_callee : ∀ge,s,CL,CL'. |
---|
[2896] | 575 | as_call_ident (RTLabs_status ge) «s,CL» = cs_callee (pcs_to_cs RTLabs_pcsys ge) (Ras_state … s) CL'. |
---|
[2895] | 576 | #ge * #s #S #M #CL #CL' cases (rtlabs_call_inv … CL) #fn * #fd * #args * #dst * #stk * #m #E |
---|
| 577 | destruct % |
---|
| 578 | qed. |
---|
| 579 | |
---|
[2894] | 580 | lemma itot_call : ∀C,cs,s,rem,cs',trace. |
---|
| 581 | ∀CL:match cs_classify C s with [ cl_call ⇒ True | _ ⇒ False ]. |
---|
| 582 | intensional_trace_of_trace C cs (〈s,E0〉::rem) = 〈cs',trace〉 → |
---|
| 583 | ∃trace'. |
---|
| 584 | trace = (IEVcall (cs_callee C s CL))::trace' ∧ |
---|
| 585 | intensional_trace_of_trace C (cs_callee C s CL :: cs) rem = 〈cs',trace'〉. |
---|
| 586 | #C #cs #s #rem #cs' #trace #CL |
---|
[2896] | 587 | whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); |
---|
[2894] | 588 | @generalize_callee cases (cs_classify C s) in CL ⊢ %; * |
---|
| 589 | #name whd in ⊢ (??%? → ?); cases (intensional_trace_of_trace C (name I::cs) rem) |
---|
| 590 | #cs' #trace' #E whd in E:(??%?); destruct %{trace'} % % |
---|
| 591 | qed. |
---|
| 592 | |
---|
[2895] | 593 | lemma itot_step : ∀ge,cs,s,tr,s',rem,cs',obs. |
---|
| 594 | as_classifier (RTLabs_status ge) s cl_other → |
---|
[2896] | 595 | step … RTLabs_fullexec ge (Ras_state … s) = Value ??? 〈tr,s'〉 → |
---|
| 596 | intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs (〈Ras_state … s,tr〉::rem) = 〈cs',obs〉 → |
---|
[2895] | 597 | ∃obs'. |
---|
| 598 | obs = (intensional_events_of_events tr) @ obs' ∧ |
---|
[2896] | 599 | intensional_trace_of_trace (pcs_to_cs … RTLabs_pcsys ge) cs rem = 〈cs',obs'〉. |
---|
[2895] | 600 | #ge #cs #s #tr #s' #rem #cs #obs #CL #EX |
---|
[2896] | 601 | whd in ⊢ (??%? → ?); |
---|
| 602 | whd in match (intensional_state_change (pcs_to_cs RTLabs_pcsys ge) ??); |
---|
| 603 | generalize in match (cs_callee ??) in ⊢ (% → ?); |
---|
| 604 | whd in CL; change with (cs_classify (pcs_to_cs … RTLabs_pcsys ge) ?) in CL:(??%?); |
---|
[2895] | 605 | >CL #name whd in ⊢ (??%? → ?); |
---|
| 606 | cases (intensional_trace_of_trace ???) #cs'' #trace'' #E whd in E:(??%?); destruct |
---|
| 607 | %{trace''} /2/ |
---|
| 608 | qed. |
---|
[2894] | 609 | |
---|
| 610 | (* observables_trace_label_label emits the cost label for the first step of the |
---|
| 611 | enclosed tal, so we have to add that label if it exists to the front of the |
---|
| 612 | events from the structured trace *) |
---|
| 613 | let rec eq_obs_tlr ge s trace' s' tlr fn cs cs' obs on tlr : |
---|
[2896] | 614 | exec_steps (length_tlr (RTLabs_status ge) s s' tlr) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace',Ras_state … s'〉 → |
---|
| 615 | intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace' = 〈cs',obs〉 → |
---|
[2894] | 616 | pi1 … (observables_trace_label_return (RTLabs_status ge) s s' tlr fn) = obs ∧ cs = cs' ≝ ? |
---|
| 617 | and eq_obs_tll ge s trace1 s' ends tll fn cs cs' obs on tll : |
---|
[2896] | 618 | exec_steps (length_tll (RTLabs_status ge) ends s s' tll) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 → |
---|
| 619 | intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 → |
---|
[2894] | 620 | pi1 … (observables_trace_label_label (RTLabs_status ge) ends s s' tll fn) = obs ∧ cs_change ends fn cs cs' ≝ ? |
---|
| 621 | and eq_obs_tal ge s trace1 s' ends tal fn cs cs' obs on tal : |
---|
[2896] | 622 | exec_steps (length_tal (RTLabs_status ge) ends s s' tal) ?? RTLabs_fullexec ge (Ras_state … s) = OK ? 〈trace1,Ras_state … s'〉 → |
---|
| 623 | intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ge) (fn::cs) trace1 = 〈cs',obs〉 → |
---|
[2894] | 624 | maybe_label ge s (pi1 … (observables_trace_any_label (RTLabs_status ge) ends s s' tal fn)) = obs ∧ cs_change ends fn cs cs' ≝ ?. |
---|
| 625 | [ cases tlr |
---|
| 626 | [ #s1 #s2 #tll @eq_obs_tll |
---|
| 627 | | #s1 #s2 #s3 #tll #tlr #EX #ITOT |
---|
| 628 | cases (exec_steps_split … EX) #trace1 * #trace2 * #s2' * * #EX1 #EX2 #E |
---|
| 629 | >E in ITOT; #ITOT cases (int_trace_split … ITOT) #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs |
---|
| 630 | lapply (eq_end_tll … EX1) #E2 <E2 in EX1; #EX1 |
---|
| 631 | cases (eq_obs_tll … EX1 ITOT1) #ITOT1' #CS_CH whd in CS_CH; <CS_CH in ITOT2 EX2; <E2 #ITOT2 #EX2 |
---|
| 632 | cases (eq_obs_tlr … EX2 ITOT2) #E3 #E4 destruct % % |
---|
| 633 | ] |
---|
| 634 | | cases tll #ends' #s1 #s2 #tal #CS #EX #ITOT whd in ⊢ (?(??%?)?); |
---|
| 635 | whd in ⊢ (?(??(??%?)?)?) ; >(definitely_maybe_label … CS) |
---|
| 636 | @(eq_obs_tal … EX ITOT) |
---|
| 637 | | cases tal |
---|
[2895] | 638 | [ #s1 #s2 #ST #CL0 #CS #EX cases CL0 #CL |
---|
[2894] | 639 | cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX |
---|
| 640 | whd in EX:(??%?); destruct |
---|
[2896] | 641 | whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?); |
---|
| 642 | whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); |
---|
| 643 | generalize in match (cs_callee ??) in ⊢ (??%? → ?); |
---|
[2894] | 644 | whd in ⊢ (? → ? → ?(??(???%)?)?); |
---|
| 645 | >CL #call whd in ⊢ (??%? → ?); #E destruct |
---|
| 646 | % [ 1,3: @(step_cost_event … ST') | 2,4: % ] |
---|
| 647 | | #s1 #s2 #ST #CL #EX |
---|
| 648 | cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX |
---|
| 649 | whd in EX:(??%?); destruct |
---|
[2896] | 650 | whd in CL; change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ?) in CL:(??%?); |
---|
| 651 | whd in ⊢ (??%? → ?); whd in match (intensional_state_change ???); |
---|
| 652 | generalize in match (cs_callee ??) in ⊢ (??%? → ?); |
---|
[2894] | 653 | whd in ⊢ (? → ? → ?(??(???%)?)?); >CL #call whd in ⊢ (??%? → ?); #E destruct |
---|
| 654 | cases (call_ret_event … ST') |
---|
| 655 | [ #E1 #E2 >E1 >E2 % % |
---|
| 656 | | skip |
---|
| 657 | | %2 @CL |
---|
| 658 | ] |
---|
| 659 | | #s1 #s2 #s3 #ST #CL #AF #tlr #CS #EX |
---|
| 660 | cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace2 * * #E1 #ST' #EX |
---|
| 661 | whd in EX:(??%?); destruct cases (call_ret_event … ST') |
---|
| 662 | [ #E1 #E2 >E1 >E2 | skip | %1 @CL ] #ITOT |
---|
[2896] | 663 | cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ] |
---|
[2894] | 664 | #obs' * #E3 #ITOT' |
---|
| 665 | <(as_exec_eq_step … ST ST') in EX; #EX |
---|
| 666 | cases (eq_obs_tlr … EX ITOT') |
---|
| 667 | #OBS' #E4 <E4 % |
---|
[2895] | 668 | [ >E3 <OBS' whd in ⊢ (??%?); <(as_call_cs_callee … CL) % |
---|
| 669 | | % |
---|
| 670 | ] |
---|
| 671 | | #s1 #s2 #s3 #ST #CL #tlr #EX #ITOT @⊥ @(RTLabs_notail … CL) |
---|
| 672 | | #ends #s1 #s2 #s3 #s4 #ST #CL #AF #tlr #CS #tal' #EX |
---|
| 673 | cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX |
---|
| 674 | cases (call_ret_event … ST') |
---|
| 675 | [ #E2 #E3 >E2 >E3 | skip | %1 @CL ] #ITOT |
---|
[2896] | 676 | cases (itot_call … ITOT) [2: change with (cs_classify (pcs_to_cs RTLabs_pcsys ge) ? = ?) in CL; >CL % ] |
---|
[2895] | 677 | #obs' * #E4 #ITOT' |
---|
| 678 | <(as_exec_eq_step … ST ST') in EX; #EX |
---|
| 679 | cases (exec_steps_split … EX) #trace1 * #trace2 * #s2'' * * #EX1 #EX2 #E |
---|
| 680 | >E in ITOT'; #ITOT' cases (int_trace_split … ITOT') #cs1 * #t1' * #t2' * * #ITOT1 #ITOT2 #Eobs |
---|
| 681 | lapply (eq_end_tlr … EX1) #E5 <E5 in EX1; #EX1 |
---|
| 682 | cases (eq_obs_tlr … EX1 ITOT1) #ITOT1' #CS_CH <CS_CH in ITOT2 EX2; <E5 #ITOT2 #EX2 |
---|
| 683 | cases (eq_obs_tal … EX2 ITOT2) #ITOT2' #CS_CH' % |
---|
| 684 | [ >E4 whd in ⊢ (??%?); |
---|
| 685 | <(as_call_cs_callee … CL) in ITOT1' ⊢ %; #ITOT1' >ITOT1' |
---|
| 686 | >(really_no_label … CS) in ITOT2'; #ITOT2' >ITOT2' |
---|
| 687 | <Eobs % |
---|
| 688 | | @CS_CH' |
---|
| 689 | ] |
---|
| 690 | | #ends #s1 #s2 #s3 #ST #tal' #CL #CS #EX |
---|
| 691 | cases (exec_steps_S … EX) #_ * #tr * #s2' * #trace0 * * #E1 >E1 #ST' #EX |
---|
| 692 | #ITOT cases (itot_step … CL ST' ITOT) #obs' * #E >E #ITOT' |
---|
| 693 | <(as_exec_eq_step … ST ST') in EX; #EX |
---|
| 694 | cases (eq_obs_tal … EX ITOT') |
---|
| 695 | >(really_no_label … CS) #OBS' #CS_CH |
---|
| 696 | >(step_cost_event … ST') <OBS' |
---|
| 697 | % [ % | @CS_CH ] |
---|
| 698 | ] |
---|
| 699 | ] qed. |
---|
[2894] | 700 | |
---|
| 701 | |
---|
| 702 | |
---|
| 703 | |
---|
[2895] | 704 | lemma cost_state_is_in_function : ∀ge,s,S,M. |
---|
| 705 | RTLabs_cost (mk_RTLabs_ext_state ge s S M) → |
---|
| 706 | ∃fn,S',id. S = fn::S' ∧ symbol_for_block ? ge fn = Some ? id. |
---|
| 707 | #ge * |
---|
| 708 | [ #f #fs #m * [*] #fn #S' * #FFP #M #_ |
---|
| 709 | %{fn} %{S'} %{(symbol_of_function_block' … FFP)} |
---|
| 710 | % [ % | @symbol_of_function_block_ok [ >FFP % #E destruct | % ] ] |
---|
| 711 | | #fid #fn #args #ret #fs #m #S #M * |
---|
| 712 | | #rv #rr #fs #m #S #M * |
---|
| 713 | | #r #S #M * |
---|
| 714 | ] qed. |
---|
[2894] | 715 | |
---|
[2896] | 716 | lemma cost_state_intensional_state_change : ∀ge,s,cs. |
---|
| 717 | RTLabs_cost s → |
---|
| 718 | \fst (intensional_state_change (pcs_to_cs … RTLabs_pcsys ge) cs s) = cs. |
---|
| 719 | #ge * |
---|
| 720 | [ #f #fs #m #cs // |
---|
| 721 | | #fid #fn #args #ret #fs #m #cs * |
---|
| 722 | | #rv #rr #fs #m #cs * |
---|
| 723 | | #r #cs * |
---|
| 724 | ] qed. |
---|
[2895] | 725 | |
---|
[2914] | 726 | definition max_stack_of_tlr : ∀S,s1,s2. trace_label_return S s1 s2 → (ident → option nat) → ident → stacksize_info → stacksize_info ≝ |
---|
| 727 | λS,s1,s2,tlr,stack_cost,currentfn,initial. |
---|
| 728 | update_stacksize_info stack_cost initial (extract_call_ud_from_tlr S s1 s2 tlr currentfn). |
---|
[2896] | 729 | |
---|
| 730 | |
---|
[2914] | 731 | |
---|
[2839] | 732 | (* I'm not entirely certain that existentially quantifying fn is the right thing |
---|
| 733 | to do. In principle we must provide the right one to satisfy the condition |
---|
| 734 | about observables, but perhaps we ought to show how to produce it explicitly. |
---|
| 735 | *) |
---|
| 736 | |
---|
| 737 | |
---|
| 738 | theorem measurable_subtraces_are_structured : ∀p,m,n,stack_cost,max,prefix,interesting. |
---|
[2892] | 739 | well_cost_labelled_program p → |
---|
[2839] | 740 | measurable RTLabs_pcsys p m n stack_cost max → |
---|
| 741 | observables RTLabs_pcsys p m n = return 〈prefix,interesting〉 → |
---|
[2914] | 742 | let midstack ≝ measure_stack stack_cost (mk_stacksize_info 0 0) prefix in |
---|
[2839] | 743 | ∃sm,sn,fn.∃tlr:trace_label_return (RTLabs_status (make_global p)) sm sn. |
---|
| 744 | state_at RTLabs_ext_pcsys p m = return sm ∧ |
---|
[2893] | 745 | tlr_unrepeating (RTLabs_status (make_global p)) … tlr ∧ |
---|
[2914] | 746 | le (maximum (max_stack_of_tlr ??? tlr stack_cost fn midstack)) max ∧ |
---|
[2839] | 747 | pi1 … (observables_trace_label_return (RTLabs_status (make_global p)) sm sn tlr fn) = interesting. |
---|
| 748 | #p #m #n #stack_cost #max #prefix #interesting |
---|
[2892] | 749 | #WCLP cases (well_cost_labelled_make_global p WCLP) |
---|
[2839] | 750 | change with (make_global … RTLabs_fullexec p) in match (make_global p); |
---|
[2892] | 751 | #WCLge #SLge |
---|
[2839] | 752 | * #s0 * #prefix' * #s1 * #interesting' * #s2 |
---|
| 753 | letin ge ≝ (make_global … RTLabs_fullexec p) |
---|
| 754 | * * * * * #INIT #EXEC1 #EXEC2 #LABEL_TO_RETURN #RETURNS #STACK |
---|
| 755 | whd in ⊢ (??%? → ?); >INIT |
---|
| 756 | whd in ⊢ (??%? → ?); >EXEC1 |
---|
| 757 | whd in ⊢ (??%? → ?); >EXEC2 |
---|
[2896] | 758 | whd in ⊢ (??%? → ?); |
---|
| 759 | @pair_elim #cs1 #prefix1 #ITOT1 |
---|
| 760 | lapply (refl ? (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting')) |
---|
| 761 | cases (intensional_trace_of_trace (pcs_to_cs RTLabs_pcsys ?) cs1 interesting') in ⊢ (???% → %); |
---|
| 762 | #cs2 #interesting'' #ITOT2 |
---|
| 763 | #E whd in E:(??%%); destruct |
---|
[2839] | 764 | cases (initial_states_OK' … INIT) #S * #M #INIT' |
---|
[2896] | 765 | cases (extend_initial_RTLabs_exec_steps ?? (mk_RTLabs_ext_state (make_global p) s0 S M) … EXEC1 ITOT1 INIT') |
---|
| 766 | #prefix'' * #S1 * #M1 * |
---|
[2895] | 767 | lapply (label_to_return_state_labelled … LABEL_TO_RETURN EXEC2) #CS1 |
---|
| 768 | lapply (cost_state_is_in_function ge s1 S1 M1 CS1) * #fnb * #S1' * #fn * #ES1 #FN destruct |
---|
[2896] | 769 | letin s1' ≝ (mk_RTLabs_ext_state ? s1 (fnb::S1') M1) #EXEC1' #CALLSTACK1 |
---|
| 770 | cut (∃cs1'. cs1 = fn::cs1') |
---|
| 771 | [ >(cost_state_intensional_state_change … CS1) in CALLSTACK1; |
---|
| 772 | cases cs1 [ * ] #fn' #cs1' * >FN #Efn destruct #_ %{cs1'} % |
---|
| 773 | ] * #cs1' #Ecs destruct |
---|
[2895] | 774 | cases (will_return_equiv … EXEC2 RETURNS) #RETURNS' #RETURNS_END |
---|
[2839] | 775 | lapply (make_label_return' ge 0 s1' (make_flat_trace ????? EXEC2) ????) |
---|
[2895] | 776 | [ @RETURNS' |
---|
| 777 | | @CS1 |
---|
[2892] | 778 | | @(well_cost_labelled_exec_steps … EXEC1) |
---|
| 779 | [ assumption |
---|
| 780 | | @(proj1 … (well_cost_labelled_initial … INIT WCLP)) |
---|
| 781 | ] |
---|
| 782 | | @WCLge |
---|
[2895] | 783 | | * #s2' #rem #_ #tlr #LEN #STACK whd in ⊢ (% → ?); whd in ⊢ (??%? → ?); |
---|
| 784 | >RETURNS_END #E destruct |
---|
| 785 | %{s1'} %{s2'} %{fn} %{tlr} |
---|
[2893] | 786 | % [ % [ % |
---|
[2839] | 787 | [ whd in ⊢ (??%?); |
---|
| 788 | change with (make_ext_initial_state p) in match (make_initial_state ????); |
---|
| 789 | >INIT' whd in ⊢ (??%?); |
---|
| 790 | >EXEC1' % |
---|
[2893] | 791 | | @tlr_sound_unrepeating |
---|
| 792 | [ @SLge |
---|
| 793 | | @(soundly_labelled_exec_steps … EXEC1) |
---|
| 794 | [ @SLge |
---|
| 795 | | @(proj2 … (well_cost_labelled_initial … INIT WCLP)) |
---|
| 796 | ] |
---|
| 797 | ] |
---|
[2839] | 798 | ]| |
---|
[2895] | 799 | ]| cut (length_tlr … tlr = n) |
---|
| 800 | [ lapply (make_flat_trace_length ????? EXEC2) <LEN |
---|
| 801 | <plus_n_O @(λx.x) ] |
---|
| 802 | #LEN' <LEN' in EXEC2; #EXEC2 |
---|
[2896] | 803 | lapply (eq_obs_tlr ????????? EXEC2 ITOT2) |
---|
| 804 | * // |
---|
[2839] | 805 | ] |
---|
[2897] | 806 | ] |
---|
[2839] | 807 | |
---|