1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory ADT_IF_Refine 12imports "InfoFlow.ADT_IF" "Refine.EmptyFail_H" 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17definition 18 kernelEntry_if 19where 20 "kernelEntry_if e tc \<equiv> do 21 t \<leftarrow> getCurThread; 22 threadSet (tcbArch_update (atcbContextSet tc)) t; 23 r \<leftarrow> handleEvent e; 24 return (r,tc) 25 od" 26 27crunch (empty_fail) empty_fail: kernelEntry_if 28 29definition prod_lift where "prod_lift R r r' \<equiv> R (fst r) (fst r') \<and> (snd r) = (snd r')" 30 31lemma kernel_entry_if_corres: 32 "corres (prod_lift (intr \<oplus> dc)) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and 33 (\<lambda>s. scheduler_action s = resume_cur_thread)) 34 (invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and 35 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 36 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) 37 (kernel_entry_if event tc) (kernelEntry_if event tc)" 38 apply (simp add: kernel_entry_if_def kernelEntry_if_def) 39 apply (rule corres_guard_imp) 40 apply (rule corres_split [OF _ gct_corres]) 41 apply (rule corres_split) 42 prefer 2 43 apply simp 44 apply (rule threadset_corresT) 45 apply (simp add: tcb_relation_def 46 arch_tcb_relation_def 47 arch_tcb_context_set_def 48 atcbContextSet_def) 49 apply (clarsimp simp: tcb_cap_cases_def) 50 apply (clarsimp simp: tcb_cte_cases_def) 51 apply (simp add: exst_same_def) 52 apply (rule corres_split [OF _ he_corres]) 53 apply (clarsimp simp: prod_lift_def) 54 apply (wp hoare_TrueI threadSet_invs_trivial thread_set_invs_trivial 55 thread_set_not_state_valid_sched thread_set_ct_running threadSet_ct_running' static_imp_wp 56 | simp add: tcb_cap_cases_def)+ 57 apply (force simp: invs_def cur_tcb_def) 58 apply force 59 done 60 61lemma kernelEntry_invs'[wp]: 62 "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and 63 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 64 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 65 kernelEntry_if e tc \<lbrace>\<lambda>_. invs'\<rbrace>" 66 apply (simp add: kernelEntry_if_def) 67 apply (wp threadSet_invs_trivial threadSet_ct_running' static_imp_wp 68 | clarsimp)+ 69 done 70 71lemma kernelEntry_valid_duplicates[wp]: 72 "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and 73 (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 74 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> 75 kernelEntry_if e tc \<lbrace>\<lambda>_. (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace>" 76 apply (simp add: kernelEntry_if_def) 77 apply (wp handleEvent_valid_duplicates' 78 threadSet_invs_trivial threadSet_ct_running' static_imp_wp 79 | clarsimp)+ 80 done 81 82 83lemma kernel_entry_if_domain_time_inv: 84 "\<lbrace> K (e \<noteq> Interrupt) and (\<lambda>s. P (domain_time s)) \<rbrace> 85 kernel_entry_if e tc 86 \<lbrace>\<lambda>_ s. P (domain_time s) \<rbrace>" 87 unfolding kernel_entry_if_def 88 by (wp handle_event_domain_time_inv) simp 89 90lemma kernel_entry_if_valid_domain_time: 91 "\<lbrace>\<lambda>s. 0 < domain_time s \<rbrace> 92 kernel_entry_if Interrupt tc 93 \<lbrace>\<lambda>_ s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread \<rbrace>" 94 unfolding kernel_entry_if_def 95 apply (rule hoare_pre) 96 apply (wp handle_interrupt_valid_domain_time 97 | clarsimp | wpc)+ 98 \<comment> \<open>strengthen post of do_machine_op; we know interrupt occurred\<close> 99 apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce) 100 apply (wp+, simp) 101 done 102 103lemma kernel_entry_if_no_preempt: 104 "\<lbrace> \<top> \<rbrace> kernel_entry_if Interrupt ctx \<lbrace>\<lambda>(interrupt,_) _. interrupt = Inr () \<rbrace>" 105 unfolding kernel_entry_if_def 106 by (wp | clarsimp intro!: validE_cases_valid)+ 107 108lemma corres_ex_abs_lift: 109 "\<lbrakk>corres r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> 110 \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>" 111 apply (clarsimp simp: corres_underlying_def valid_def ex_abs_def) 112 apply fastforce 113 done 114 115lemmas schedaction_related = sched_act_rct_related 116 117lemma kernelEntry_ex_abs[wp]: 118 "\<lbrace>invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') 119 and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) 120 and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ex_abs (einvs)\<rbrace> 121 kernelEntry_if e tc 122 \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" 123 apply (rule hoare_pre) 124 apply (rule corres_ex_abs_lift[OF kernel_entry_if_corres]) 125 apply (wp_trace kernel_entry_if_invs kernel_entry_if_valid_sched) 126 apply (clarsimp simp: ex_abs_def) 127 apply (rule_tac x=sa in exI) 128 apply (fastforce simp: ct_running_related ct_idle_related schedaction_related 129 active_from_running' active_from_running) 130 done 131 132definition 133 kernelCall_H_if 134 where 135 "kernelCall_H_if e \<equiv> 136 {(s, b, (tc,s'))|s b tc s' r. ((r,tc),s') \<in> fst (split (kernelEntry_if e) s) \<and> 137 b = (case r of Inl _ \<Rightarrow> True | Inr _ \<Rightarrow> False)}" 138 139definition 140 "ptable_rights_s' s \<equiv> ptable_rights (ksCurThread s) (absKState s)" 141 142definition 143 "ptable_lift_s' s \<equiv> ptable_lift (ksCurThread s) (absKState s)" 144 145definition 146 "ptable_attrs_s' s \<equiv> ptable_attrs (ksCurThread s) (absKState s)" 147 148definition 149 "ptable_xn_s' s \<equiv> \<lambda>addr. XNever \<in> ptable_attrs_s' s addr" 150 151definition doUserOp_if :: "user_transition_if \<Rightarrow> user_context \<Rightarrow> (kernel_state, (event option \<times> user_context)) nondet_monad" where 152 "doUserOp_if uop tc \<equiv> 153 do pr \<leftarrow> gets ptable_rights_s'; 154 pxn \<leftarrow> gets (\<lambda>s x. pr x \<noteq> {} \<and> ptable_xn_s' s x); 155 pl \<leftarrow> gets (\<lambda>s. ptable_lift_s' s |` {x. pr x \<noteq> {}}); 156 allow_read \<leftarrow> return {y. \<exists>x. pl x = Some y \<and> AllowRead \<in> pr x}; 157 allow_write \<leftarrow> return {y. \<exists>x. pl x = Some y \<and> AllowWrite \<in> pr x}; 158 t \<leftarrow> getCurThread; 159 um \<leftarrow> gets (\<lambda>s. (user_mem' s \<circ> ptrFromPAddr)); 160 dm \<leftarrow> gets (\<lambda>s. (device_mem' s \<circ> ptrFromPAddr)); 161 ds \<leftarrow> gets (device_state \<circ> ksMachineState); 162 assert (dom (um \<circ> addrFromPPtr) \<subseteq> - dom ds); 163 assert (dom (dm \<circ> addrFromPPtr) \<subseteq> dom ds); 164 es \<leftarrow> doMachineOp getExMonitor; 165 u \<leftarrow> 166 return 167 (uop t pl pr pxn 168 (tc, um |` allow_read, 169 (ds \<circ> ptrFromPAddr) |` allow_read, es)); 170 assert (u \<noteq> {}); 171 (e, tc', um',ds', es') \<leftarrow> select u; 172 doMachineOp 173 (user_memory_update 174 ((um' |` allow_write \<circ> addrFromPPtr) |` (- (dom ds)))); 175 doMachineOp 176 (device_memory_update 177 ((ds' |` allow_write \<circ> addrFromPPtr) |` dom ds)); 178 doMachineOp (setExMonitor es'); 179 return (e, tc') 180 od" 181 182lemma empty_fail_select_bind: "empty_fail (assert (S \<noteq> {}) >>= (\<lambda>_. select S))" 183 apply (clarsimp simp: empty_fail_def select_def assert_def) 184 done 185 186crunch (empty_fail) empty_fail[wp]: user_memory_update 187crunch (empty_fail) empty_fail[wp]: device_memory_update 188 189lemma getExMonitor_empty_fail[wp]: 190 "empty_fail getExMonitor" 191 by (simp add: getExMonitor_def) 192 193lemma setExMonitor_empty_fail[wp]: 194 "empty_fail (setExMonitor es)" 195 by (simp add: setExMonitor_def) 196 197lemma getExMonitor_no_fail[wp]: 198 "no_fail \<top> getExMonitor" 199 by (simp add: getExMonitor_def) 200 201lemma setExMonitor_no_fail'[wp]: 202 "no_fail \<top> (setExMonitor (x, y))" 203 by (simp add: setExMonitor_def) 204 205lemma setExMonitor_no_fail[wp]: 206 "no_fail \<top> (setExMonitor es)" 207 by (simp add: setExMonitor_def) 208 209lemma doUserOp_if_empty_fail: "empty_fail (doUserOp_if uop tc)" 210 apply (simp add: doUserOp_if_def) 211 apply wp_once 212 apply wp_once 213 apply wp_once 214 apply wp_once 215 apply wp_once 216 apply wp_once 217 apply wp_once 218 apply wp_once 219 apply wp_once 220 apply wp_once 221 apply wp_once 222 apply wp[1] 223 apply wp_once 224 apply wp[1] 225 apply wp_once 226 apply wp[1] 227 apply wp_once 228 apply wp[1] 229 apply wp_once 230 apply wp[1] 231 apply (subst bind_assoc[symmetric]) 232 apply (rule empty_fail_bind) 233 apply (rule empty_fail_select_bind) 234 apply (wp | wpc)+ 235 done 236 237 238lemma ptable_attrs_abs_state[simp]: 239 "ptable_attrs thread (abs_state s) = ptable_attrs thread s" 240 by (simp add: ptable_attrs_def abs_state_def) 241 242lemma corres_gets_same: 243 assumes equiv: "\<And>s s'. \<lbrakk>P s; Q s'; (s, s') \<in> sr\<rbrakk>\<Longrightarrow> f s = g s'" 244 and rimp : "\<And>s. P s \<Longrightarrow> R (f s) s" 245 and corres: "\<And>r. corres_underlying sr b c rr (P and (R r) and (\<lambda>s. r = f s)) Q (n r) (m r)" 246 shows "corres_underlying sr b c rr P Q 247 (do r \<leftarrow> gets f; n r od) 248 (do r \<leftarrow> gets g; m r od)" 249 apply (rule corres_guard_imp) 250 apply (rule corres_split[where r' = "(=)"]) 251 apply simp 252 apply (rule corres) 253 apply clarsimp 254 apply (rule equiv) 255 apply (wp|simp)+ 256 apply (simp add: rimp) 257 apply simp 258 done 259 260lemma corres_assert_imp_r: 261 "\<lbrakk>\<And>s. P s\<Longrightarrow> Q' ; corres_underlying state_relation a b rr P Q f (g ())\<rbrakk> 262 \<Longrightarrow> corres_underlying state_relation a b rr P Q f (assert Q' >>= g)" 263 by (force simp: corres_underlying_def assert_def return_def bind_def fail_def) 264 265lemma corres_return_same_trivial: 266 "corres_underlying sr b c (=) \<top> \<top> (return a) (return a)" 267 by simp 268 269crunch (no_fail) no_fail[wp]: device_memory_update 270 271lemma do_user_op_if_corres: 272 "corres (=) (einvs and ct_running and (\<lambda>_. \<forall>t pl pr pxn tcu. f t pl pr pxn tcu \<noteq> {})) 273 (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and 274 ct_running') 275 (do_user_op_if f tc) (doUserOp_if f tc)" 276 apply (rule corres_gen_asm) 277 apply (simp add: do_user_op_if_def doUserOp_if_def) 278 apply (rule corres_gets_same) 279 apply (clarsimp simp: ptable_rights_s_def ptable_rights_s'_def) 280 apply (subst absKState_correct, fastforce, assumption+) 281 apply (clarsimp elim!: state_relationE) 282 apply simp 283 apply (rule corres_gets_same) 284 apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def) 285 apply (subst absKState_correct, fastforce, assumption+) 286 apply (clarsimp elim!: state_relationE) 287 apply simp 288 apply (rule corres_gets_same) 289 apply (clarsimp simp: absArchState_correct curthread_relation ptable_lift_s'_def 290 ptable_lift_s_def) 291 apply (subst absKState_correct, fastforce, assumption+) 292 apply (clarsimp elim!: state_relationE) 293 apply simp 294 apply (simp add: getCurThread_def) 295 apply (rule corres_gets_same) 296 apply (simp add: curthread_relation) 297 apply simp 298 apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> - device_region s"]) 299 apply (clarsimp simp add: user_mem_relation dest!: invs_valid_stateI invs_valid_stateI') 300 apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def) 301 apply fastforce 302 apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> device_region s"]) 303 apply (clarsimp simp add: device_mem_relation dest!: invs_valid_stateI invs_valid_stateI') 304 apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def) 305 apply fastforce 306 apply (rule corres_gets_same[where R ="\<lambda>r s. dom r = device_region s"]) 307 apply (clarsimp simp: state_relation_def) 308 apply simp 309 apply (rule corres_assert_imp_r) 310 apply fastforce 311 apply (rule corres_assert_imp_r) 312 apply fastforce 313 apply (rule corres_guard_imp) 314 apply (rule corres_split[OF _ corres_machine_op,where r'="(=)"]) 315 apply clarsimp 316 apply (rule corres_split[where r'="(=)"]) 317 apply clarsimp 318 apply (rule corres_split[OF _ corres_machine_op,where r'="(=)"]) 319 apply clarsimp 320 apply (rule corres_split[OF _ corres_machine_op,where r'="(=)"]) 321 apply clarsimp 322 apply (rule corres_split[OF _ corres_machine_op, where r'="(=)"]) 323 apply (rule corres_return_same_trivial) 324 apply (wp hoare_TrueI[where P = \<top>] | simp | rule corres_underlying_trivial)+ 325 apply (clarsimp simp: user_memory_update_def) 326 apply (rule non_fail_modify) 327 apply clarsimp 328 apply (wp hoare_TrueI) 329 apply clarsimp 330 apply (wp hoare_TrueI) 331 apply (clarsimp simp: select_def corres_underlying_def) 332 apply (simp only: comp_def | wp hoare_TrueI)+ 333 apply (rule corres_underlying_trivial) 334 apply (wp hoare_TrueI)+ 335 apply clarsimp 336 apply force 337 apply force 338 done 339 340lemma dmo_getExMonitor_wp'[wp]: 341 "\<lbrace>\<lambda>s. P (exclusive_state (ksMachineState s)) s\<rbrace> 342 doMachineOp getExMonitor \<lbrace>P\<rbrace>" 343 apply(simp add: doMachineOp_def) 344 apply(wp modify_wp | wpc)+ 345 apply clarsimp 346 apply(erule use_valid) 347 apply wp 348 apply simp 349 done 350 351lemma dmo_setExMonitor_wp'[wp]: 352 "\<lbrace>\<lambda>s. P (s\<lparr>ksMachineState := ksMachineState s 353 \<lparr>exclusive_state := es\<rparr>\<rparr>)\<rbrace> 354 doMachineOp (setExMonitor es) \<lbrace>\<lambda>_. P\<rbrace>" 355 apply(simp add: doMachineOp_def) 356 apply(wp modify_wp | wpc)+ 357 apply clarsimp 358 apply(erule use_valid) 359 apply wp 360 apply simp 361 done 362 363lemma valid_state'_exclusive_state_update[iff]: 364 "valid_state' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = valid_state' s" 365 by (simp add: valid_state'_def valid_machine_state'_def) 366 367lemma invs'_exclusive_state_update[iff]: 368 "invs' (s\<lparr>ksMachineState := ksMachineState s\<lparr>exclusive_state := es\<rparr>\<rparr>) = invs' s" 369 by (simp add: invs'_def) 370 371lemma doUserOp_if_invs'[wp]: 372 "\<lbrace>invs' and 373 (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and 374 ct_running' and ex_abs (einvs)\<rbrace> 375 doUserOp_if f tc 376 \<lbrace>\<lambda>_. invs'\<rbrace>" 377 apply (simp add: doUserOp_if_def split_def ex_abs_def) 378 apply (wp device_update_invs' dmo_setExMonitor_wp' dmo_invs' | simp)+ 379 apply (clarsimp simp add: no_irq_modify user_memory_update_def) 380 apply wpsimp 381 apply (wp doMachineOp_ct_running' select_wp)+ 382 apply (clarsimp simp: user_memory_update_def simpler_modify_def 383 restrict_map_def 384 split: option.splits) 385 apply (drule ptable_rights_imp_UserData[rotated 2], auto simp: ptable_rights_s'_def ptable_lift_s'_def) 386 done 387 388lemma doUserOp_valid_duplicates[wp]: 389 "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> doUserOp_if f tc 390 \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" 391 apply (simp add: doUserOp_if_def split_def) 392 apply (wp dmo_setExMonitor_wp' dmo_invs' select_wp | simp)+ 393 done 394 395lemma doUserOp_if_schedact[wp]: 396 "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> 397 doUserOp_if f tc 398 \<lbrace>\<lambda>r s. P (ksSchedulerAction s)\<rbrace>" 399 apply (simp add: doUserOp_if_def) 400 apply (wp select_wp | wpc | simp)+ 401 done 402 403lemma doUserOp_if_st_tcb_at[wp]: 404 "\<lbrace>st_tcb_at' st t\<rbrace> 405 doUserOp_if f tc 406 \<lbrace>\<lambda>_. st_tcb_at' st t\<rbrace>" 407 apply (simp add: doUserOp_if_def) 408 apply (wp select_wp | wpc | simp)+ 409 done 410 411lemma doUserOp_if_cur_thread[wp]: 412 "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> doUserOp_if f tc 413 \<lbrace>\<lambda>r s. P (ksCurThread s)\<rbrace>" 414 apply (simp add: doUserOp_if_def) 415 apply (wp select_wp | wpc | simp)+ 416 done 417 418 419lemma doUserOp_if_ct_in_state[wp]: 420 "\<lbrace>ct_in_state' st\<rbrace> 421 doUserOp_if f tc 422 \<lbrace>\<lambda>_. ct_in_state' st\<rbrace>" 423 apply (rule hoare_pre) 424 apply (rule ct_in_state_thread_state_lift') 425 apply (wp | simp)+ 426 done 427 428 429lemma corres_ex_abs_lift': 430 "\<lbrakk>corres_underlying state_relation False False r S P' f f'; \<lbrace>P\<rbrace> f \<lbrace>\<lambda>_. Q\<rbrace>\<rbrakk> \<Longrightarrow> 431 \<lbrace>ex_abs (P and S) and P'\<rbrace> f' \<lbrace>\<lambda>_. ex_abs Q\<rbrace>" 432 apply (clarsimp simp: corres_underlying_def valid_def ex_abs_def) 433 apply fastforce 434 done 435 436lemma gct_corres': "corres_underlying state_relation nf nf' (=) \<top> \<top> (gets cur_thread) getCurThread" 437 by (simp add: getCurThread_def curthread_relation) 438 439lemma user_mem_corres': 440 "corres_underlying state_relation nf nf' (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))" 441 by (clarsimp simp add: gets_def get_def return_def bind_def 442 invs_def invs'_def 443 corres_underlying_def user_mem_relation) 444 445lemma corres_machine_op': 446 assumes P: "corres_underlying Id nf nf' r P Q x x'" 447 shows "corres_underlying state_relation nf nf' r (P \<circ> machine_state) (Q \<circ> ksMachineState) 448 (do_machine_op x) (doMachineOp x')" 449 apply (rule corres_submonad3 450 [OF submonad_do_machine_op submonad_doMachineOp _ _ _ _ P]) 451 apply (simp_all add: state_relation_def swp_def) 452 done 453 454lemma corres_assert': 455 "corres_underlying sr nf False dc \<top> \<top> (assert P) (assert P)" 456 by (clarsimp simp: corres_underlying_def assert_def return_def fail_def) 457 458lemma do_user_op_if_corres': 459 "corres_underlying state_relation nf False (=) (einvs and ct_running) 460 (invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and 461 ct_running') 462 (do_user_op_if f tc) (doUserOp_if f tc)" 463 apply (simp add: do_user_op_if_def doUserOp_if_def) 464 apply (rule corres_gets_same) 465 apply (clarsimp simp: ptable_rights_s_def ptable_rights_s'_def) 466 apply (subst absKState_correct, fastforce, assumption+) 467 apply (clarsimp elim!: state_relationE) 468 apply simp 469 apply (rule corres_gets_same) 470 apply (clarsimp simp: ptable_attrs_s'_def ptable_attrs_s_def ptable_xn_s'_def ptable_xn_s_def) 471 apply (subst absKState_correct, fastforce, assumption+) 472 apply (clarsimp elim!: state_relationE) 473 apply simp 474 apply (rule corres_gets_same) 475 apply (clarsimp simp: absArchState_correct curthread_relation ptable_lift_s'_def 476 ptable_lift_s_def) 477 apply (subst absKState_correct, fastforce, assumption+) 478 apply (clarsimp elim!: state_relationE) 479 apply simp 480 apply (simp add: getCurThread_def) 481 apply (rule corres_gets_same) 482 apply (simp add: curthread_relation) 483 apply simp 484 apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> - device_region s"]) 485 apply (clarsimp simp add: user_mem_relation dest!: invs_valid_stateI invs_valid_stateI') 486 apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def) 487 apply fastforce 488 apply (rule corres_gets_same[where R ="\<lambda>r s. dom (r \<circ> addrFromPPtr) \<subseteq> device_region s"]) 489 apply (clarsimp simp add: device_mem_relation dest!: invs_valid_stateI invs_valid_stateI') 490 apply (clarsimp simp: invs_def valid_state_def pspace_respects_device_region_def dom_def) 491 apply (rule corres_gets_same[where R ="\<lambda>r s. dom r = device_region s"]) 492 apply (clarsimp simp: state_relation_def) 493 apply simp 494 apply (rule corres_assert_imp_r) 495 apply fastforce 496 apply (rule corres_assert_imp_r) 497 apply fastforce 498 apply (rule corres_guard_imp) 499 apply (rule corres_split[OF _ corres_machine_op',where r'="(=)"]) 500 apply simp 501 apply (rule corres_split[where r'="dc"]) 502 apply simp 503 apply (rule corres_split[where r'="(=)"]) 504 apply clarsimp 505 apply (rule corres_split[OF _ corres_machine_op',where r'="(=)"]) 506 apply simp 507 apply (rule corres_split[OF _ corres_machine_op', where r'="(=)"]) 508 apply simp 509 apply (rule corres_split[OF _ corres_machine_op', where r'="(=)"]) 510 apply (rule corres_return_same_trivial) 511 apply (wp hoare_TrueI[where P = \<top>] | simp | rule corres_underlying_trivial)+ 512 apply (clarsimp simp: select_def corres_underlying_def) 513 apply (simp only: comp_def | wp hoare_TrueI)+ 514 apply (rule corres_assert') 515 apply (wp hoare_TrueI[where P = \<top>] | simp | rule corres_underlying_trivial)+ 516 apply clarsimp 517 apply force 518 apply force 519 done 520 521lemma doUserOp_if_ex_abs[wp]: 522 "\<lbrace>invs' and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and ex_abs (einvs)\<rbrace> 523 doUserOp_if f tc 524\<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" 525 apply (rule hoare_pre) 526 apply (rule corres_ex_abs_lift'[OF do_user_op_if_corres']) 527 apply (rule_tac Q="\<lambda>a . (invs and ct_running) and valid_list and valid_sched" in hoare_strengthen_post) 528 apply (wp do_user_op_if_invs) 529 apply clarsimp 530 apply (clarsimp simp: ex_abs_def) 531 apply (rule_tac x=sa in exI) 532 apply (clarsimp simp: active_from_running ct_running_related 533 schedaction_related)+ 534 done 535 536 537 538definition 539 doUserOp_H_if 540 where 541 "doUserOp_H_if uop \<equiv> {(s,e,(tc,s'))| s e tc s'. ((e,tc),s') \<in> fst (split (doUserOp_if uop) s)}" 542 543definition checkActiveIRQ_if :: "(MachineTypes.register \<Rightarrow> 32 word) \<Rightarrow> (10 word option \<times> (MachineTypes.register \<Rightarrow> 32 word)) kernel" where 544"checkActiveIRQ_if tc \<equiv> 545do 546 irq \<leftarrow> doMachineOp (getActiveIRQ False); 547 return (irq, tc) 548od" 549 550crunch (empty_fail) empty_fail: checkActiveIRQ_if 551 552 553lemma getActiveIRQ_nf: "no_fail (\<lambda>_. True) (getActiveIRQ in_kernel)" 554 apply (simp add: getActiveIRQ_def) 555 apply (rule no_fail_pre) 556 apply (rule non_fail_gets non_fail_modify 557 no_fail_return | rule no_fail_bind | simp 558 | intro impI conjI)+ 559 apply (wp del: no_irq | simp)+ 560 done 561 562lemma dmo_getActiveIRQ_corres: "corres (=) \<top> \<top> (do_machine_op (getActiveIRQ in_kernel)) 563 (doMachineOp (getActiveIRQ in_kernel'))" 564 apply (rule SubMonad_R.corres_machine_op) 565 apply (rule corres_Id) 566 apply (simp add: getActiveIRQ_def non_kernel_IRQs_def) 567 apply simp 568 apply (rule getActiveIRQ_nf) 569 done 570 571lemma check_active_irq_if_corres: 572 "corres (=) \<top> \<top> (check_active_irq_if tc) (checkActiveIRQ_if tc)" 573 apply (simp add: checkActiveIRQ_if_def check_active_irq_if_def) 574 apply (rule corres_underlying_split[where r'="(=)"]) 575 apply (rule dmo_getActiveIRQ_corres) 576 apply wp+ 577 apply clarsimp 578 done 579 580lemma dmo'_getActiveIRQ_wp: 581 "\<lbrace>\<lambda>s. P (irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s))) (s\<lparr>ksMachineState := (ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>)\<rparr>)\<rbrace> doMachineOp (getActiveIRQ in_kernel)\<lbrace>P\<rbrace>" 582 apply(simp add: doMachineOp_def getActiveIRQ_def non_kernel_IRQs_def) 583 apply(wp modify_wp | wpc)+ 584 apply clarsimp 585 apply(erule use_valid) 586 apply (wp modify_wp) 587 apply(auto simp: irq_at_def) 588 done 589 590lemma checkActiveIRQ_if_wp: 591 "\<lbrace>\<lambda>s. P ((irq_at (irq_state (ksMachineState s) + 1) (irq_masks (ksMachineState s))),tc) 592 (s\<lparr>ksMachineState := (ksMachineState s\<lparr>irq_state := irq_state (ksMachineState s) + 1\<rparr>)\<rparr>)\<rbrace> checkActiveIRQ_if tc \<lbrace>P\<rbrace>" 593 apply(simp add: checkActiveIRQ_if_def | wp dmo'_getActiveIRQ_wp)+ 594 done 595 596lemma checkActiveIRQ_invs'[wp]: "\<lbrace>invs'\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. invs'\<rbrace>" 597 apply (wp checkActiveIRQ_if_wp) 598 apply simp 599 done 600 601lemma checkActiveIRQ_ct_in_state[wp]: "\<lbrace>ct_in_state' st\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ct_in_state' st\<rbrace>" 602 apply (wp checkActiveIRQ_if_wp) 603 apply simp 604 done 605 606lemma checkActiveIRQ_schedact[wp]: "\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>r s. P (ksSchedulerAction s)\<rbrace>" 607 apply (wp checkActiveIRQ_if_wp) 608 apply simp 609 done 610 611lemma checkActiveIRQ_vs_valid_duplicates'[wp]: "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>r s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" 612 apply (wp checkActiveIRQ_if_wp) 613 apply simp 614 done 615 616 617lemma checkActiveIRQ_ex_abs[wp]: "\<lbrace>ex_abs (einvs)\<rbrace> checkActiveIRQ_if tc \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" 618 apply (rule hoare_pre) 619 apply (rule corres_ex_abs_lift[OF check_active_irq_if_corres]) 620 apply (rule check_active_irq_if_wp) 621 apply (clarsimp simp: ex_abs_def) 622 done 623 624definition 625 checkActiveIRQ_H_if 626 where 627 "checkActiveIRQ_H_if \<equiv> {((tc, s), irq, (tc', s')). ((irq, tc'), s') \<in> fst (checkActiveIRQ_if tc s)}" 628 629definition 630 handlePreemption_if :: "(MachineTypes.register \<Rightarrow> 32 word) \<Rightarrow> (MachineTypes.register \<Rightarrow> 32 word) kernel" where 631 "handlePreemption_if tc \<equiv> do 632 irq \<leftarrow> doMachineOp (getActiveIRQ False); 633 when (irq \<noteq> None) $ handleInterrupt (the irq); 634 return tc 635 od" 636 637crunch (empty_fail) empty_fail: handlePreemption_if 638 639lemma handle_preemption_if_corres: 640 "corres (=) (einvs) 641 (invs') 642 (handle_preemption_if tc) (handlePreemption_if tc)" 643 apply (simp add: handlePreemption_if_def handle_preemption_if_def) 644 apply (rule corres_guard_imp) 645 apply (rule corres_split[where r'="(=)"]) 646 apply (rule corres_split[where r'="dc"]) 647 apply simp 648 apply (rule corres_when) 649 apply simp 650 apply simp 651 apply (rule handle_interrupt_corres) 652 apply (rule hoare_post_taut[where P=\<top>])+ 653 apply (rule dmo_getActiveIRQ_corres) 654 apply (rule dmo_getActiveIRQ_wp) 655 apply (rule dmo'_getActiveIRQ_wp) 656 apply clarsimp+ 657 apply (clarsimp simp: invs'_def valid_state'_def irq_at_def invs_def 658 Let_def valid_irq_states'_def) 659 done 660 661lemma handlePreemption_invs'[wp]: 662 "\<lbrace>invs'\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. invs'\<rbrace>" 663 apply (simp add: handlePreemption_if_def) 664 apply (wp dmo'_getActiveIRQ_wp) 665 apply clarsimp 666 done 667 668lemma handlePreemption_if_valid_duplicates[wp]: 669 "\<lbrace>\<lambda>s. vs_valid_duplicates' (ksPSpace s)\<rbrace> handlePreemption_if tc 670 \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" 671 apply (simp add: handlePreemption_if_def) 672 apply (wp dmo'_getActiveIRQ_wp) 673 apply clarsimp 674 done 675 676lemma handlePreemption_ex_abs[wp]: 677 "\<lbrace>invs' and ex_abs (einvs)\<rbrace> handlePreemption_if tc \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" 678 apply (rule hoare_pre) 679 apply (rule corres_ex_abs_lift[OF handle_preemption_if_corres]) 680 apply (wp handle_preemption_if_invs) 681 apply (auto simp: ex_abs_def non_kernel_IRQs_def) 682 done 683 684lemma handle_preemption_if_valid_domain_time: 685 "\<lbrace>\<lambda>s. 0 < domain_time s \<rbrace> 686 handle_preemption_if tc 687 \<lbrace>\<lambda>r s. domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread \<rbrace>" 688 unfolding handle_preemption_if_def 689 apply (rule hoare_pre) 690 apply (wp handle_interrupt_valid_domain_time) 691 apply (rule_tac Q="\<lambda>_ s. 0 < domain_time s" in hoare_post_imp, fastforce) 692 apply (wp, simp) 693 done 694 695definition 696 handlePreemption_H_if 697 where 698 "handlePreemption_H_if \<equiv> 699 {(s, u, s'). s' \<in> fst (split handlePreemption_if s)}" 700 701definition 702 schedule'_if :: "(MachineTypes.register \<Rightarrow> 32 word) \<Rightarrow> (MachineTypes.register \<Rightarrow> 32 word) kernel" where 703 "schedule'_if tc \<equiv> do 704 schedule; 705 activateThread; 706 return tc 707 od" 708 709crunch (empty_fail) empty_fail: schedule'_if 710 711 712lemma schedule_if_corres: 713 "corres (=) (invs and valid_sched and valid_list) 714 (invs') 715 (schedule_if tc) (schedule'_if tc)" 716 apply (simp add: schedule_if_def schedule'_if_def) 717 apply (rule corres_guard_imp) 718 apply (rule corres_split[where r'="dc"]) 719 apply (rule corres_split[where r'="dc"]) 720 apply simp 721 apply (rule activate_corres) 722 apply (rule hoare_post_taut[where P=\<top>])+ 723 apply (rule schedule_corres) 724 apply (wp schedule_invs')+ 725 apply clarsimp+ 726 done 727 728lemma schedule_if'_invs'_post: 729 "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs' and (ct_running' or ct_idle')\<rbrace>" 730 apply (simp add: schedule'_if_def) 731 apply (wp activate_invs' schedule_invs' schedule_sch_act_simple | simp)+ 732 done 733 734lemma schedule_if'_invs'[wp]: 735 "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. invs'\<rbrace>" 736 apply (rule hoare_post_imp[OF _ schedule_if'_invs'_post]) 737 apply simp 738 done 739 740lemma schedule_if'_ct_running_or_idle[wp]: 741 "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>r s. ct_running' s \<or> ct_idle' s\<rbrace>" 742 apply (rule hoare_post_imp[OF _ schedule_if'_invs'_post]) 743 apply simp 744 done 745 746 747lemma schedule_if'_rct[wp]: 748 "\<lbrace>invs'\<rbrace> schedule'_if tc \<lbrace>\<lambda>r s. ksSchedulerAction s = ResumeCurrentThread\<rbrace>" 749 apply (simp add: schedule'_if_def) 750 apply (wp activate_sch_act schedule_sch) 751 done 752 753 754lemma scheduler_if'_valid_duplicates[wp]: 755 "\<lbrace>invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))\<rbrace> schedule'_if tc 756 \<lbrace>\<lambda>_ s. vs_valid_duplicates' (ksPSpace s)\<rbrace>" 757 apply (simp add: schedule'_if_def) 758 apply (wp | simp)+ 759 done 760 761lemma schedule_if_domain_time_left: 762 "\<lbrace>\<lambda>s. valid_domain_list s \<and> (domain_time s = 0 \<longrightarrow> scheduler_action s = choose_new_thread) \<rbrace> 763 schedule_if tc 764 \<lbrace>\<lambda>rv s. 0 < domain_time s \<rbrace>" 765 unfolding schedule_if_def schedule_det_ext_ext_def schedule_switch_thread_fastfail_def 766 supply ethread_get_wp[wp del] 767 supply if_split[split del] 768 apply (rule hoare_pre) 769 apply (wpsimp simp: ethread_get_when_def wp: gts_wp 770 | wp hoare_drop_imp[where f="ethread_get a b" for a b] 771 hoare_drop_imp[where f="tcb_sched_action a b" for a b])+ 772 apply (auto split: if_split) 773 done 774 775lemma scheduler'_if_ex_abs[wp]: 776 "\<lbrace>invs' and ex_abs (einvs)\<rbrace> schedule'_if tc \<lbrace>\<lambda>_. ex_abs (einvs)\<rbrace>" 777 apply (rule hoare_pre) 778 apply (rule corres_ex_abs_lift[OF schedule_if_corres]) 779 apply wp 780 apply (auto simp: ex_abs_def) 781 done 782 783definition 784 schedule'_H_if 785 where 786 "schedule'_H_if \<equiv> 787 {(s, e, s'). s' \<in> fst (split schedule'_if s)}" 788 789definition 790 kernelExit_if 791 where 792 "kernelExit_if tc \<equiv> do 793 t' \<leftarrow> getCurThread; 794 threadGet (atcbContextGet o tcbArch) t' 795 od" 796 797crunch (empty_fail) empty_fail: kernelExit_if 798 799lemma kernel_exit_if_corres: 800 "corres (=) (invs) 801 (invs') 802 (kernel_exit_if tc) (kernelExit_if tc)" 803 apply (simp add: kernel_exit_if_def kernelExit_if_def) 804 apply (rule corres_guard_imp) 805 apply (rule corres_split[where r'="(=)"]) 806 apply simp 807 apply (rule threadget_corres) 808 apply (clarsimp simp: tcb_relation_def arch_tcb_relation_def 809 arch_tcb_context_get_def atcbContextGet_def) 810 apply (rule gct_corres) 811 apply wp+ 812 apply clarsimp+ 813 done 814 815lemma kernelExit_inv[wp]: 816 "\<lbrace>P\<rbrace> kernelExit_if tc \<lbrace>\<lambda>_. P\<rbrace>" 817 apply (simp add: kernelExit_if_def) 818 apply wp 819 done 820 821 822definition 823 kernelExit_H_if 824 where 825 "kernelExit_H_if \<equiv> 826 {(s, m, s'). s' \<in> fst (split kernelExit_if s) \<and> 827 m = (if ct_running' (snd s') then InUserMode else InIdleMode)}" 828 829definition full_invs_if' where 830 "full_invs_if' \<equiv> 831 {s. invs' (internal_state_if s) \<and> ex_abs (einvs) (internal_state_if s) 832 \<and> vs_valid_duplicates' (ksPSpace (internal_state_if s)) 833 \<and> (snd s \<noteq> KernelSchedule True \<longrightarrow> ksDomainTime (internal_state_if s) > 0) 834 \<and> (ksDomainTime (internal_state_if s) = 0 835 \<longrightarrow> ksSchedulerAction (internal_state_if s) = ChooseNewThread) 836 \<and> valid_domain_list' (internal_state_if s) 837 \<and> (case (snd s) 838 of (KernelEntry e) \<Rightarrow> 839 (e \<noteq> Interrupt \<longrightarrow> ct_running' (internal_state_if s) \<and> 840 ksDomainTime (internal_state_if s) \<noteq> 0) \<and> 841 (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> 842 ksSchedulerAction (internal_state_if s) = ResumeCurrentThread 843 | KernelExit \<Rightarrow> 844 (ct_running' (internal_state_if s) \<or> ct_idle' (internal_state_if s)) \<and> 845 ksSchedulerAction (internal_state_if s) = ResumeCurrentThread \<and> 846 ksDomainTime (internal_state_if s) \<noteq> 0 847 | InUserMode \<Rightarrow> 848 ct_running' (internal_state_if s) \<and> 849 ksSchedulerAction (internal_state_if s) = ResumeCurrentThread 850 | InIdleMode \<Rightarrow> 851 ct_idle' (internal_state_if s) \<and> 852 ksSchedulerAction (internal_state_if s) = ResumeCurrentThread 853 | _ \<Rightarrow> True) }" 854 855definition has_srel_state where 856"has_srel_state srel P \<equiv> {s. \<exists>s'. (s,s') \<in> srel \<and> s' \<in> P}" 857 858definition lift_fst_rel where 859 "lift_fst_rel srel \<equiv> {(r,r'). snd r = snd r' \<and> (fst r, fst r') \<in> srel}" 860 861(*Includes serializability*) 862definition step_corres where 863 "step_corres nf srel mode G G' \<equiv> 864 \<lambda>mabs mconc. \<forall>(s,s')\<in>srel. (s',mode) \<in> G' \<and> (s,mode) \<in> G \<longrightarrow> 865 ((nf \<longrightarrow> (\<exists>e' t'. (s',e',t') \<in> mconc)) \<and> 866 (\<forall>e' t'. (s',e',t') \<in> mconc \<longrightarrow> 867 (\<exists>e t. (s,e,t) \<in> mabs \<and> (t,t') \<in> srel \<and> e = e')))" 868 869 870definition lift_snd_rel where 871 "lift_snd_rel srel \<equiv> {(r,r'). fst r = fst r' \<and> (snd r, snd r') \<in> srel}" 872 873definition preserves where 874"preserves mode mode' P f \<equiv> \<forall>(s,e,s') \<in> f. (s,mode) \<in> P \<longrightarrow> (s',mode') \<in> P" 875 876(*Special case for KernelExit*) 877definition preserves' where 878"preserves' mode P f \<equiv> \<forall>(s,e,s') \<in> f. (s,mode) \<in> P \<longrightarrow> (s',e) \<in> P" 879 880lemma preservesE: 881 assumes preserves: "preserves mode mode' P f" 882 assumes inf: "(s,e,s') \<in> f" 883 assumes P: "(s,mode) \<in> P" 884 assumes a: "(s',mode') \<in> P \<Longrightarrow> Q" 885 shows "Q" 886 apply (rule a) 887 apply (insert preserves inf P) 888 apply (clarsimp simp: preserves_def) 889 apply fastforce 890 done 891 892lemma preserves'E: 893 assumes preserves: "preserves' mode P f" 894 assumes inf: "(s,e,s') \<in> f" 895 assumes P: "(s,mode) \<in> P" 896 assumes a: "(s',e) \<in> P \<Longrightarrow> Q" 897 shows "Q" 898 apply (rule a) 899 apply (insert preserves inf P) 900 apply (clarsimp simp: preserves'_def) 901 apply fastforce 902 done 903 904lemma step_corres_bothE: 905 assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc" 906 assumes preserves: "preserves mode mode' invs_conc f_conc" 907 assumes a: "(s, s') \<in> srel" 908 assumes e: "(s, mode) \<in> invs_abs" 909 assumes b: "(s', mode) \<in> invs_conc" 910 assumes c: "(s', e, t') \<in> f_conc" 911 assumes d: "\<And>t. 912 (s, e, t) \<in> f_abs \<Longrightarrow> 913 (t,mode') \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> 914 (t, t') \<in> srel \<Longrightarrow> P" 915 shows "P" 916 apply (insert corres a b c e) 917 apply (clarsimp simp: step_corres_def) 918 apply (drule_tac x="(s,s')" in bspec,clarsimp+) 919 apply (drule_tac x=e in spec) 920 apply (drule_tac x="t'" in spec) 921 apply simp 922 apply clarsimp 923 apply (rule_tac t=t in d,simp+) 924 apply (clarsimp simp: has_srel_state_def lift_fst_rel_def) 925 apply (rule preservesE[OF preserves],assumption+) 926 apply fastforce+ 927 done 928 929lemma step_corres_both'E: 930 assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc" 931 assumes preserves: "preserves' mode invs_conc f_conc" 932 assumes a: "(s, s') \<in> srel" 933 assumes e: "(s, mode) \<in> invs_abs" 934 assumes b: "(s', mode) \<in> invs_conc" 935 assumes c: "(s', e, t') \<in> f_conc" 936 assumes d: "\<And>t. 937 (s, e, t) \<in> f_abs \<Longrightarrow> 938 (t,e) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> 939 (t, t') \<in> srel \<Longrightarrow> P" 940 shows "P" 941 apply (insert corres a b c e) 942 apply (clarsimp simp: step_corres_def) 943 apply (drule_tac x="(s,s')" in bspec,clarsimp+) 944 apply (drule_tac x=e in spec) 945 apply (drule_tac x="t'" in spec) 946 apply simp 947 apply clarsimp 948 apply (rule_tac t=t in d,simp+) 949 apply (clarsimp simp: has_srel_state_def lift_fst_rel_def) 950 apply (rule preserves'E[OF preserves],assumption+) 951 apply fastforce+ 952 done 953 954lemma step_corresE: 955 assumes corres: "step_corres nf srel mode invs_abs invs_conc f_abs f_conc" 956 assumes a: "(s, s') \<in> srel" 957 assumes e: "(s, mode) \<in> invs_abs" 958 assumes b: "(s', mode) \<in> invs_conc" 959 assumes c: "(s', e, t') \<in> f_conc" 960 assumes d: "\<And>t. 961 (s, e, t) \<in> f_abs \<Longrightarrow> 962 (t, t') \<in> srel \<Longrightarrow> P" 963 shows "P" 964 apply (insert corres a b c e) 965 apply (clarsimp simp: step_corres_def) 966 apply (drule_tac x="(s,s')" in bspec,clarsimp+) 967 apply (drule_tac x=e in spec) 968 apply (drule_tac x=t' in spec) 969 apply clarsimp 970 apply (rule d) 971 apply simp+ 972 done 973end 974 975locale global_automaton_invs = 976 fixes check_active_irq 977 fixes do_user_op 978 fixes kernel_call 979 fixes handle_preemption 980 fixes schedule 981 fixes kernel_exit 982 fixes invs :: "('a global_sys_state) set" 983 fixes ADT :: "(('a global_sys_state),'o, unit) data_type" 984 fixes extras :: "'a global_sys_state set" 985 assumes step_adt: "Step ADT = 986 (\<lambda>u. (global_automaton_if check_active_irq do_user_op kernel_call handle_preemption schedule kernel_exit) \<inter> {(s,s'). s' \<in> extras})" 987 assumes check_active_irq_invs: "preserves InUserMode InUserMode invs check_active_irq" 988 assumes check_active_irq_idle_invs: "preserves InIdleMode InIdleMode invs check_active_irq" 989 assumes check_active_irq_invs_entry: "preserves InUserMode (KernelEntry Interrupt) invs check_active_irq" 990 assumes check_active_irq_idle_invs_entry: "preserves InIdleMode (KernelEntry Interrupt) invs check_active_irq" 991 992 assumes do_user_op_invs: "preserves InUserMode InUserMode invs do_user_op" 993 assumes do_user_op_invs_entry: "preserves InUserMode (KernelEntry e) invs do_user_op" 994 assumes kernel_call_invs: "e \<noteq> Interrupt \<Longrightarrow> preserves (KernelEntry e) KernelPreempted invs (kernel_call e)" 995 assumes kernel_call_invs_sched: "preserves (KernelEntry e) (KernelSchedule (e = Interrupt)) invs (kernel_call e)" 996 assumes handle_preemption_invs: "preserves KernelPreempted (KernelSchedule True) invs handle_preemption" 997 assumes schedule_invs: "preserves (KernelSchedule b) KernelExit invs schedule" 998 assumes kernel_exit_invs: "preserves' KernelExit invs kernel_exit" 999 assumes init_invs: "(Init ADT) s \<subseteq> invs" 1000 assumes init_extras: "(Init ADT) s \<subseteq> extras" 1001 begin 1002 1003 lemma ADT_extras: "ADT \<Turnstile> extras" 1004 apply (rule invariantI) 1005 apply (clarsimp simp: init_extras) 1006 apply (clarsimp simp: step_adt) 1007 done 1008 1009 lemma ADT_invs: "ADT \<Turnstile> invs" 1010 apply (rule invariantI) 1011 apply (intro allI) 1012 apply (rule init_invs) 1013 apply (clarsimp simp: step_adt global_automaton_if_def) 1014 apply (elim disjE exE conjE,simp_all) 1015apply (rule preservesE[OF kernel_call_invs]) 1016 apply (rule preservesE[OF kernel_call_invs],assumption+) 1017 apply (rule preservesE[OF kernel_call_invs_sched],assumption+) 1018 apply (rule preservesE[OF handle_preemption_invs],assumption+) 1019 apply (rule preservesE[OF schedule_invs],assumption+) 1020 apply (rule preserves'E[OF kernel_exit_invs],assumption+) 1021 apply (rule preservesE[OF check_active_irq_invs],assumption+) 1022 apply (rule preservesE[OF do_user_op_invs_entry],assumption+) 1023 apply (rule preservesE[OF check_active_irq_invs],assumption+) 1024 apply (rule preservesE[OF do_user_op_invs],assumption+) 1025 apply (rule preservesE[OF check_active_irq_invs_entry],assumption+) 1026 apply (rule preservesE[OF check_active_irq_idle_invs_entry],assumption+) 1027 apply (rule preservesE[OF check_active_irq_idle_invs],assumption+) 1028 done 1029end 1030 1031 1032lemma invariant_holds_inter: "A \<Turnstile> I \<Longrightarrow> A \<Turnstile> S \<Longrightarrow> A \<Turnstile> (I \<inter> S)" 1033 apply (clarsimp simp: invariant_holds_def) 1034 apply blast 1035 done 1036 1037lemma preserves_lift_ret: "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>) 1038 \<Longrightarrow> 1039 preserves mode mode' P 1040 {((tc, s), irq, tc', s'). 1041 ((irq, tc'), s') \<in> fst (f tc s)}" 1042 apply (clarsimp simp: preserves_def valid_def) 1043 apply fastforce 1044 done 1045 1046lemma preserves_lift: "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),mode') \<in> P\<rbrace>) 1047 \<Longrightarrow> 1048 preserves mode mode' P 1049 {((tc, s), irq, tc', s'). 1050 (tc', s') \<in> fst (f tc s)}" 1051 apply (clarsimp simp: preserves_def valid_def) 1052 done 1053 1054 1055lemma preserves_lift':"(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f uop tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>) 1056 \<Longrightarrow> 1057 preserves mode mode' P 1058 {((a, b), e, tc, s') |a b e tc s'. 1059 ((e, tc), s') \<in> fst (f uop a b)}" 1060 apply (clarsimp simp: preserves_def valid_def) 1061 apply fastforce 1062 done 1063 1064lemma preserves_lift'': 1065 "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f e tc \<lbrace>\<lambda>tc' s'. ((snd tc',s'),mode') \<in> P\<rbrace>) \<Longrightarrow> 1066 preserves mode mode' P 1067 {((a, b), ba, tc, s') |a b ba tc s'. 1068 \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and> ba = (r \<noteq> Inr ())}" 1069 apply (clarsimp simp: preserves_def valid_def) 1070 apply fastforce 1071 done 1072 1073lemma preserves_lift''': "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),mode') \<in> P\<rbrace>) 1074 \<Longrightarrow> 1075 preserves mode mode' P 1076 {(s, u, s'). s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)}" 1077 apply (clarsimp simp: preserves_def valid_def) 1078 done 1079 1080 1081lemma preserves'_lift: 1082 "(\<And>tc. \<lbrace>\<lambda>s. ((tc,s),mode) \<in> P\<rbrace> f tc \<lbrace>\<lambda>tc' s'. ((tc',s'),y s') \<in> P\<rbrace>) 1083 \<Longrightarrow> 1084 preserves' mode P 1085 {(s, m, s'). 1086 s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and> 1087 m = (y (snd s'))}" 1088 apply (clarsimp simp: preserves'_def valid_def) 1089 apply fastforce 1090 done 1091 1092lemmas preserves_lifts = preserves_lift_ret preserves_lift preserves_lift' 1093 preserves_lift'' preserves_lift''' preserves'_lift 1094 1095 1096 1097 1098defs step_restrict_def: 1099 "step_restrict \<equiv> \<lambda>s. s \<in> has_srel_state (lift_fst_rel (lift_snd_rel state_relation)) full_invs_if'" 1100 1101context begin interpretation Arch . 1102lemma abstract_invs: 1103 "global_automaton_invs check_active_irq_A_if (do_user_op_A_if uop) 1104 kernel_call_A_if kernel_handle_preemption_if 1105 kernel_schedule_if kernel_exit_A_if 1106 (full_invs_if) (ADT_A_if uop) {s. step_restrict s}" 1107 supply conj_cong[cong] 1108 apply (unfold_locales) 1109 apply (simp add: ADT_A_if_def) 1110 apply (simp_all add: check_active_irq_A_if_def do_user_op_A_if_def 1111 kernel_call_A_if_def kernel_handle_preemption_if_def 1112 kernel_schedule_if_def kernel_exit_A_if_def split del: if_split)[12] 1113 apply (rule preserves_lifts | 1114 wp check_active_irq_if_wp do_user_op_if_invs 1115 | clarsimp simp add: full_invs_if_def)+ 1116 apply (rule_tac Q="\<lambda>r s'. (invs and ct_running) s' \<and> 1117 valid_list s' \<and> 1118 valid_sched s' \<and> scheduler_action s' = resume_cur_thread \<and> 1119 valid_domain_list s' \<and> 1120 (domain_time s' = 0 \<longrightarrow> scheduler_action s' = choose_new_thread)" in hoare_post_imp) 1121 apply (clarsimp) 1122 apply (wp do_user_op_if_invs hoare_vcg_imp_lift) 1123 apply clarsimp+ 1124 apply (rule preserves_lifts) 1125 apply (simp add: full_invs_if_def) 1126 apply (rule_tac Q="\<lambda>r s'. (invs and ct_running) s' \<and> 1127 valid_list s' \<and> 1128 valid_domain_list s' \<and> 1129 domain_time s' \<noteq> 0 \<and> 1130 valid_sched s' \<and> scheduler_action s' = resume_cur_thread" in hoare_post_imp) 1131 apply (clarsimp simp: active_from_running) 1132 apply (wp do_user_op_if_invs kernel_entry_if_invs kernel_entry_if_valid_sched ; clarsimp) 1133 (* KernelEntry \<rightarrow> KernelPreempted *) 1134 apply (rule preserves_lifts, simp add: full_invs_if_def) 1135 subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched 1136 kernel_entry_if_domain_time_inv 1137 ; clarsimp simp: active_from_running) 1138 1139 (* KernelEntry \<rightarrow> KernelSchedule (e = Interrupt) *) 1140 apply (rule preserves_lifts, simp add: full_invs_if_def) 1141 apply (case_tac "e = Interrupt") 1142 subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched kernel_entry_if_valid_domain_time 1143 | clarsimp simp: active_from_running)+ 1144 apply (clarsimp simp: conj_left_commute) 1145 subgoal by (wp kernel_entry_if_invs kernel_entry_if_valid_sched kernel_entry_if_domain_time_inv 1146 ; clarsimp simp: active_from_running) 1147 (* KernelPreempted \<rightarrow> KernelSchedule True *) 1148 apply (rule preserves_lifts, simp add: full_invs_if_def) 1149 subgoal for tc 1150 apply (rule hoare_pre) 1151 apply (wp handle_preemption_if_invs) 1152 apply (wp handle_preemption_if_valid_domain_time) 1153 apply (clarsimp simp: non_kernel_IRQs_def) 1154 done 1155 (* KernelSchedule \<rightarrow> KernelExit *) 1156 apply (rule preserves_lifts, simp add: full_invs_if_def) 1157 subgoal by (rule hoare_pre, wp schedule_if_domain_time_left, fastforce) 1158 (* KernelExit \<rightarrow> InUserMode \<or> InIdleMode *) 1159 apply (rule preserves_lifts, simp add: full_invs_if_def) 1160 subgoal by (clarsimp cong: conj_cong | wp)+ 1161 apply (fastforce simp: full_invs_if_def ADT_A_if_def step_restrict_def)+ 1162 done 1163end 1164 1165definition ADT_H_if where 1166"ADT_H_if uop \<equiv> \<lparr>Init = \<lambda>s. ({user_context_of s} \<times> {s'. absKState s' = (internal_state_if s)}) \<times> {sys_mode_of s} \<inter> full_invs_if', 1167 Fin = \<lambda>((uc,s),m). ((uc, absKState s),m), 1168 Step = (\<lambda>u. global_automaton_if 1169 checkActiveIRQ_H_if (doUserOp_H_if uop) 1170 kernelCall_H_if handlePreemption_H_if 1171 schedule'_H_if kernelExit_H_if)\<rparr>" 1172 1173crunch ksDomainTime_inv[wp]: doUserOp_if "(\<lambda>s. P (ksDomainTime s))" 1174 (wp: select_wp) 1175 1176crunch ksDomSchedule_inv[wp]: doUserOp_if "(\<lambda>s. P (ksDomSchedule s))" 1177 (wp: select_wp) 1178 1179crunch ksDomainTime_inv[wp]: checkActiveIRQ_if "\<lambda>s. P (ksDomainTime s)" 1180 1181crunch ksDomSchedule_inv[wp]: 1182 kernelEntry_if, handlePreemption_if, checkActiveIRQ_if, schedule'_if 1183 "\<lambda>s. P (ksDomSchedule s)" 1184 1185lemma kernelEntry_if_ksDomainTime_inv: 1186 "\<lbrace> K (e \<noteq> Interrupt) and (\<lambda>s. P (ksDomainTime s)) \<rbrace> 1187 kernelEntry_if e tc 1188 \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>" 1189 unfolding kernelEntry_if_def 1190 by (wp handleEvent_ksDomainTime_inv) simp 1191 1192lemma kernelEntry_if_valid_domain_time: 1193 "\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace> 1194 kernelEntry_if Interrupt tc 1195 \<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread \<rbrace>" 1196 unfolding kernelEntry_if_def 1197 apply (clarsimp simp: handleEvent_def) 1198 apply (rule hoare_pre) 1199 apply (wp handleInterrupt_valid_domain_time | wpc | clarsimp)+ 1200 apply (rule hoare_false_imp) \<comment> \<open>debugPrint\<close> 1201 apply (wp handleInterrupt_valid_domain_time hoare_vcg_all_lift hoare_drop_imps | simp)+ 1202 done 1203 1204lemma handlePreemption_if_valid_domain_time: 1205 "\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace> 1206 handlePreemption_if tc 1207 \<lbrace>\<lambda>r s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread \<rbrace>" 1208 unfolding handlePreemption_if_def 1209 apply (rule hoare_pre) 1210 apply (wp handleInterrupt_valid_domain_time) 1211 apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, fastforce) 1212 apply (wp, simp) 1213 done 1214 1215lemma schedule'_if_domain_time_left: 1216 "\<lbrace>\<lambda>s. valid_domain_list' s \<and> (ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace> 1217 schedule'_if tc 1218 \<lbrace>\<lambda>rv s. 0 < ksDomainTime s \<rbrace>" 1219 unfolding schedule'_if_def 1220 apply (rule hoare_pre) 1221 apply wp 1222 apply (rule hoare_post_imp[OF _ schedule_domain_time_left']) 1223 apply clarsimp+ 1224 done 1225 1226lemma kernelEntry_if_no_preempt: 1227 "\<lbrace> \<top> \<rbrace> kernelEntry_if Interrupt ctx \<lbrace>\<lambda>(interrupt,_) _. interrupt = Inr () \<rbrace>" 1228 unfolding kernelEntry_if_def handleEvent_def 1229 by (wp | clarsimp intro!: validE_cases_valid)+ 1230 1231lemma haskell_invs: 1232 "global_automaton_invs checkActiveIRQ_H_if (doUserOp_H_if uop) 1233 kernelCall_H_if handlePreemption_H_if 1234 schedule'_H_if kernelExit_H_if full_invs_if' (ADT_H_if uop) UNIV" 1235 supply conj_cong[cong] 1236 apply (unfold_locales) 1237 apply (simp add: ADT_H_if_def) 1238 apply (simp_all add: checkActiveIRQ_H_if_def doUserOp_H_if_def 1239 kernelCall_H_if_def handlePreemption_H_if_def 1240 schedule'_H_if_def kernelExit_H_if_def split del: if_split)[12] 1241 apply (rule preserves_lifts | wp | simp add: full_invs_if'_def 1242 | wp_once hoare_vcg_disj_lift)+ 1243 apply (wp | wp_once hoare_vcg_disj_lift hoare_drop_imps)+ 1244 apply simp 1245 apply (rule preserves_lifts) 1246 apply (simp add: full_invs_if'_def) 1247 apply (wp kernelEntry_if_ksDomainTime_inv ; simp) 1248 1249 subgoal for e 1250 apply (rule preserves_lifts, simp add: full_invs_if'_def) 1251 apply wp 1252 apply (case_tac "e = Interrupt") 1253 apply clarsimp 1254 apply (wp kernelEntry_if_valid_domain_time ; simp) 1255 apply clarsimp 1256 apply (wp kernelEntry_if_ksDomainTime_inv ; simp) 1257 apply fastforce+ 1258 done 1259 subgoal 1260 apply (rule preserves_lifts, simp add: full_invs_if'_def) 1261 apply (rule hoare_pre) 1262 apply (wp handlePreemption_if_valid_domain_time ; simp) 1263 apply fastforce 1264 done 1265 subgoal 1266 apply (rule preserves_lifts, simp add: full_invs_if'_def) 1267 apply (rule hoare_pre) 1268 apply (wp schedule'_if_domain_time_left) 1269 apply fastforce 1270 done 1271 subgoal by (rule preserves_lifts, simp add: full_invs_if'_def) 1272 (wp, fastforce) 1273 apply (clarsimp simp: ADT_H_if_def)+ 1274 done 1275 1276lemma step_corres_exE: 1277 assumes step: "step_corres nf srel mode invs_abs invs_conc f f'" 1278 assumes nf: "nf" 1279 assumes invsC: "(s',mode) \<in> invs_conc" 1280 assumes invsA: "(s,mode) \<in> invs_abs" 1281 assumes srel: "(s,s') \<in> srel" 1282 assumes ex: "\<And>e t' t. (s',e,t') \<in> f' \<Longrightarrow> (s,e,t) \<in> f \<Longrightarrow> (t,t') \<in> srel \<Longrightarrow> P" 1283 shows P 1284 apply (insert step invsC invsA srel nf) 1285 apply (clarsimp simp: step_corres_def) 1286 apply (drule_tac x="(s,s')" in bspec,clarsimp+) 1287 apply (drule_tac x=e' in spec) 1288 apply (drule_tac x=t' in spec) 1289 apply clarsimp 1290 apply (rule ex) 1291 apply assumption+ 1292 done 1293 1294 1295 1296locale global_automata_refine = 1297abs : global_automaton_invs check_active_irq_abs do_user_op_abs 1298 kernel_call_abs handle_preemption_abs 1299 schedule_abs kernel_exit_abs invs_abs 1300 ADT_abs extras_abs + 1301conc: global_automaton_invs check_active_irq_conc do_user_op_conc 1302 kernel_call_conc handle_preemption_conc 1303 schedule_conc kernel_exit_conc invs_conc 1304 ADT_conc "UNIV" 1305for check_active_irq_abs and 1306 do_user_op_abs and 1307 kernel_call_abs and handle_preemption_abs and 1308 schedule_abs and kernel_exit_abs and invs_abs and 1309 ADT_abs :: "(('a global_sys_state),'o, unit) data_type" and extras_abs and 1310 check_active_irq_conc and 1311 do_user_op_conc and 1312 kernel_call_conc and handle_preemption_conc and 1313 schedule_conc and kernel_exit_conc and 1314 invs_conc and 1315 ADT_conc :: "(('c global_sys_state),'o, unit) data_type" + 1316 fixes srel :: "((user_context \<times> 'a) \<times> (user_context \<times> 'c)) set" 1317 fixes nf :: "bool" 1318 assumes extras_abs_intro: "has_srel_state (lift_fst_rel srel) invs_conc \<subseteq> extras_abs" 1319 assumes srel_Fin: "(s,s') \<in> srel \<Longrightarrow> (s,mode) \<in> invs_abs \<Longrightarrow> (s',mode) \<in> invs_conc \<Longrightarrow> (Fin (ADT_conc)) (s',mode) = (Fin (ADT_abs)) (s,mode)" 1320 assumes init_refinement: "((Init (ADT_conc)) a) \<subseteq> lift_fst_rel srel `` ((Init (ADT_abs)) a)" 1321 assumes corres_check_active_irq: "step_corres nf srel InUserMode (invs_abs) invs_conc check_active_irq_abs check_active_irq_conc" 1322 assumes corres_check_active_irq_idle: "step_corres nf srel InIdleMode (invs_abs) invs_conc check_active_irq_abs check_active_irq_conc" 1323 assumes corres_do_user_op: "step_corres nf srel InUserMode (invs_abs) invs_conc (do_user_op_abs) (do_user_op_conc)" 1324 assumes corres_kernel_call: "step_corres nf srel (KernelEntry e) (invs_abs) invs_conc (kernel_call_abs e) (kernel_call_conc e)" 1325 assumes corres_handle_preemption: "step_corres nf srel KernelPreempted (invs_abs) invs_conc handle_preemption_abs handle_preemption_conc" 1326 assumes corres_schedule: "step_corres nf srel (KernelSchedule b) (invs_abs) invs_conc schedule_abs schedule_conc" 1327 assumes corres_kernel_exit: "step_corres nf srel KernelExit (invs_abs) invs_conc kernel_exit_abs kernel_exit_conc" 1328 assumes kernel_call_no_preempt: 1329 "\<And>s s' b. (s, b, s') \<in> kernel_call_abs Interrupt \<Longrightarrow> b = False" 1330 1331 begin 1332 1333 1334lemma extras_inter'[dest!]: "(t,mode) \<in> has_srel_state (lift_fst_rel srel) invs_conc \<Longrightarrow> (t,mode) \<in> extras_abs" 1335 apply (rule set_mp) 1336 apply (rule extras_abs_intro) 1337 apply simp 1338 done 1339 1340 1341 lemma fw_sim_abs_conc: 1342 "LI (ADT_abs) 1343 (ADT_conc) 1344 (lift_fst_rel srel) 1345 (invs_abs \<times> invs_conc)" 1346 apply (unfold LI_def ) 1347 apply (intro conjI allI) 1348 apply (rule init_refinement) 1349 apply (clarsimp simp: rel_semi_def relcomp_unfold lift_fst_rel_def 1350 abs.step_adt conc.step_adt) 1351 apply (clarsimp simp: global_automaton_if_def) 1352 apply (elim disjE exE conjE,simp_all) 1353 apply (rule step_corres_bothE[OF corres_kernel_call conc.kernel_call_invs],assumption+,auto)[1] 1354 apply (rule step_corres_bothE[OF corres_kernel_call conc.kernel_call_invs_sched],assumption+,auto)[1] 1355 apply (rule step_corres_bothE[OF corres_handle_preemption conc.handle_preemption_invs],assumption+,auto)[1] 1356 apply (rule step_corres_bothE[OF corres_schedule conc.schedule_invs],assumption+,auto)[1] 1357 apply (rule step_corres_both'E[OF corres_kernel_exit conc.kernel_exit_invs],assumption+,auto)[1] 1358 apply (rule preservesE[OF conc.check_active_irq_invs],assumption+) 1359 apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs],assumption+,clarsimp) 1360 apply (rule preservesE[OF abs.check_active_irq_invs],assumption+) 1361 apply (rule_tac s'="(ac,be)" in step_corres_bothE[OF corres_do_user_op conc.do_user_op_invs_entry],assumption+,auto)[1] 1362 apply (rule preservesE[OF conc.check_active_irq_invs],assumption+) 1363 apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs],assumption+,clarsimp) 1364 apply (rule preservesE[OF abs.check_active_irq_invs],assumption+) 1365 apply (rule_tac s'="(ac,be)" in step_corres_bothE[OF corres_do_user_op conc.do_user_op_invs],assumption+,auto)[1] 1366 apply (rule step_corres_bothE[OF corres_check_active_irq conc.check_active_irq_invs_entry],assumption+,auto)[1] 1367 apply (rule step_corres_bothE[OF corres_check_active_irq_idle conc.check_active_irq_idle_invs_entry],assumption+,auto)[1] 1368 apply (rule preservesE[OF conc.check_active_irq_idle_invs],assumption+) 1369 apply (rule step_corres_bothE[OF corres_check_active_irq_idle conc.check_active_irq_idle_invs],assumption+,auto)[1] 1370 apply (fastforce intro!: srel_Fin simp: lift_fst_rel_def) 1371 done 1372 1373 lemma fw_simulates: "ADT_conc \<sqsubseteq>\<^sub>F ADT_abs" 1374 apply (rule L_invariantI) 1375 apply (rule abs.ADT_invs) 1376 apply (rule conc.ADT_invs) 1377 apply (rule fw_sim_abs_conc) 1378 done 1379 1380 lemma refinement: "ADT_conc \<sqsubseteq> ADT_abs" 1381 apply (rule sim_imp_refines[OF fw_simulates]) 1382 done 1383 1384 lemma conc_serial: 1385 assumes uop_sane: "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow> 1386 e \<noteq> Some Interrupt" 1387 assumes no_fail: "nf" 1388 shows 1389 "serial_system (ADT_conc) {s'. \<exists>s. (s,s') \<in> (lift_fst_rel srel) \<and> s \<in> invs_abs \<and> s' \<in> invs_conc}" 1390 apply (insert no_fail) 1391 apply (unfold_locales) 1392 apply (rule fw_inv_transport) 1393 apply (rule abs.ADT_invs) 1394 apply (rule conc.ADT_invs) 1395 apply (rule fw_sim_abs_conc) 1396 apply (clarsimp simp: conc.step_adt global_automaton_if_def lift_fst_rel_def) 1397 apply (case_tac ba,simp_all) 1398 apply (rule step_corres_exE[OF corres_check_active_irq],assumption+) 1399 apply (rule preservesE[OF conc.check_active_irq_invs],assumption+) 1400 apply (rule preservesE[OF abs.check_active_irq_invs],assumption+) 1401 apply (rule_tac s=t and s'=t' in step_corres_exE[OF corres_do_user_op],assumption+) 1402 apply (rule_tac s=t and s'=t' in step_corresE[OF corres_do_user_op],assumption+) 1403 apply clarsimp 1404 apply (case_tac e) 1405 apply (case_tac ea) 1406 apply fastforce 1407 apply simp 1408 apply (frule uop_sane) 1409 apply fastforce 1410 apply (case_tac ea) 1411 apply fastforce 1412 apply fastforce 1413 apply (rule step_corres_exE[OF corres_check_active_irq_idle],assumption+) 1414 apply (case_tac e) 1415 apply fastforce 1416 apply fastforce 1417 apply clarsimp 1418 apply (rule step_corres_exE[OF corres_kernel_call],assumption+) 1419 apply (case_tac e ; fastforce dest: kernel_call_no_preempt) 1420 apply (rule step_corres_exE[OF corres_handle_preemption],assumption+) 1421 apply fastforce 1422 apply (rule step_corres_exE[OF corres_schedule],assumption+) 1423 apply fastforce 1424 apply (rule step_corres_exE[OF corres_kernel_exit],assumption+) 1425 apply fastforce 1426 done 1427 1428lemma abs_serial: 1429 assumes constrained_B: "\<And>s. s \<in> invs_abs \<inter> extras_abs \<Longrightarrow> 1430 \<exists>s'. s' \<in> invs_conc \<and> (s, s') \<in> lift_fst_rel srel" 1431 assumes uop_sane: "\<And>s e t. (s,e,t) \<in> do_user_op_conc \<Longrightarrow> 1432 e \<noteq> Some Interrupt" 1433 assumes no_fail: "nf" 1434 shows 1435 "serial_system (ADT_abs) (invs_abs \<inter> extras_abs)" 1436 apply (rule serial_system.fw_sim_serial) 1437 apply (rule conc_serial) 1438 apply (rule uop_sane,simp) 1439 apply (rule no_fail) 1440 apply (rule fw_sim_abs_conc) 1441 apply (rule invariant_holds_inter) 1442 apply (rule abs.ADT_invs) 1443 apply (rule abs.ADT_extras) 1444 apply clarsimp 1445 apply simp 1446 apply (frule constrained_B) 1447 apply (clarsimp simp: lift_fst_rel_def) 1448 apply auto 1449 done 1450 1451 1452end 1453 1454(*Unused*) 1455 lemma Init_Fin_ADT_H: "s' \<in> full_invs_if' \<Longrightarrow> s' \<in> Init (ADT_H_if uop) (Fin (ADT_H_if uop) s')" 1456 apply (clarsimp simp: ADT_H_if_def) 1457 apply (case_tac s') 1458 apply simp 1459 apply (case_tac a) 1460 apply simp 1461 done 1462 1463(*Unused*) 1464 lemma Fin_Init_ADT_H: "s' \<in> (Init (ADT_H_if uop) s) \<Longrightarrow> s' \<in> full_invs_if' \<Longrightarrow> s \<in> Fin (ADT_H_if uop) ` Init (ADT_H_if uop) s" 1465 apply (clarsimp simp: ADT_H_if_def) 1466 apply (case_tac s) 1467 apply simp 1468 apply clarsimp 1469 apply (simp add: image_def) 1470 apply (rule_tac x="((a,b),baa)" in bexI) 1471 apply clarsimp 1472 apply clarsimp 1473 done 1474 1475 1476lemma 1477 step_corres_lift: 1478 "(\<And>tc. corres_underlying srel False nf (=) 1479 (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc)) \<Longrightarrow> 1480 (\<And>tc. nf \<Longrightarrow> empty_fail (f' tc)) \<Longrightarrow> 1481 step_corres nf (lift_snd_rel srel) mode P 1482 P' 1483 {((tc, s), irq, tc', s'). 1484 ((irq, tc'), s') \<in> fst (f tc s)} 1485 {((tc, s), irq, tc', s'). 1486 ((irq, tc'), s') \<in> fst (f' tc s)}" 1487 apply (clarsimp simp: corres_underlying_def step_corres_def 1488 lift_snd_rel_def empty_fail_def) 1489 apply fastforce 1490 done 1491 1492lemma step_corres_lift': 1493 "(\<And>tc. corres_underlying srel False nf (=) 1494 (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f u tc) (f' u tc)) \<Longrightarrow> 1495 (\<And>tc. nf \<Longrightarrow> empty_fail (f' u tc)) \<Longrightarrow> 1496 step_corres nf (lift_snd_rel srel) mode 1497 P P' 1498 {((a, b), e, tc, s') |a b e tc s'. 1499 ((e, tc), s') \<in> fst (f u a b)} 1500 {((a, b), e, tc, s') |a b e tc s'. 1501 ((e, tc), s') \<in> fst (f' u a b)}" 1502 apply (clarsimp simp: corres_underlying_def step_corres_def 1503 lift_snd_rel_def empty_fail_def) 1504 apply fastforce 1505 done 1506 1507 1508lemma step_corres_lift'': 1509 "(\<And>tc. corres_underlying srel False nf (\<lambda>r r'. ((fst r) = Inr ()) = ((fst r') = Inr ()) \<and> (snd r) = (snd r')) 1510 (\<lambda>s. ((tc,s),mode) \<in> P) (\<lambda>s'. ((tc,s'),mode) \<in> P') (f e tc) (f' e tc)) \<Longrightarrow> 1511 (\<And>tc. nf \<Longrightarrow> empty_fail (f' e tc)) \<Longrightarrow> 1512 step_corres nf (lift_snd_rel srel) mode 1513 P P' 1514 {((a, b), ba, tc, s') |a b ba tc s'. 1515 \<exists>r. ((r, tc), s') \<in> fst (f e a b) \<and> 1516 ba = (r \<noteq> Inr ())} 1517 {((a, b), ba, tc, s') |a b ba tc s'. 1518 \<exists>r. ((r, tc), s') \<in> fst (f' e a b) \<and> 1519 ba = (r \<noteq> Inr ())}" 1520 apply (clarsimp simp: corres_underlying_def step_corres_def 1521 lift_snd_rel_def empty_fail_def) 1522 apply fastforce 1523 done 1524 1525lemma step_corres_lift''': 1526 "(\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P) 1527 (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc)) \<Longrightarrow> 1528 (\<And>tc. nf \<Longrightarrow> empty_fail (f' tc)) \<Longrightarrow> 1529 step_corres nf (lift_snd_rel srel) mode 1530 P P' 1531 {(s, u, s'). 1532 s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa)} 1533 {(s, u, s'). 1534 s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa)}" 1535 apply (clarsimp simp: corres_underlying_def step_corres_def 1536 lift_snd_rel_def empty_fail_def) 1537 apply fastforce 1538 done 1539 1540lemma step_corres_lift'''': 1541 "(\<And>tc. corres_underlying srel False nf (=) (\<lambda>s. ((tc,s),mode) \<in> P) 1542 (\<lambda>s'. ((tc,s'),mode) \<in> P') (f tc) (f' tc)) \<Longrightarrow> 1543 (\<And>tc. nf \<Longrightarrow> empty_fail (f' tc)) \<Longrightarrow> 1544 (\<And>tc s s'. (s,s') \<in> srel \<Longrightarrow> S' s' \<Longrightarrow> S s \<Longrightarrow> y s = y' s') \<Longrightarrow> 1545 (\<And>tc. \<lbrace>\<lambda>s'. ((tc,s'),mode) \<in> P'\<rbrace> (f' tc) \<lbrace>\<lambda>_. S'\<rbrace>) \<Longrightarrow> 1546 (\<And>tc. \<lbrace>\<lambda>s'. ((tc,s'),mode) \<in> P\<rbrace> (f tc) \<lbrace>\<lambda>_. S\<rbrace>) \<Longrightarrow> 1547 step_corres nf (lift_snd_rel srel) mode P 1548 P' 1549 {(s, m, s'). 1550 s' \<in> fst (case s of (x, xa) \<Rightarrow> f x xa) \<and> 1551 m = (y (snd s'))} 1552 {(s, m, s'). 1553 s' \<in> fst (case s of (x, xa) \<Rightarrow> f' x xa) \<and> 1554 m = (y' (snd s'))}" 1555 apply (clarsimp simp: corres_underlying_def step_corres_def 1556 lift_snd_rel_def empty_fail_def) 1557 apply (clarsimp simp: valid_def) 1558 apply (drule_tac x=a in meta_spec)+ 1559 apply fastforce 1560 done 1561 1562 1563lemmas step_corres_lifts = step_corres_lift step_corres_lift' 1564 step_corres_lift'' step_corres_lift''' 1565 step_corres_lift'''' 1566 1567 1568lemma st_tcb_at_coerce_haskell: "\<lbrakk>st_tcb_at P t a; (a, c) \<in> state_relation; tcb_at' t c\<rbrakk> 1569\<Longrightarrow> st_tcb_at' (\<lambda>st'. \<exists>st. thread_state_relation st st' \<and> P st) t c" 1570 apply (clarsimp simp: state_relation_def 1571 pspace_relation_def 1572 obj_at_def st_tcb_at'_def 1573 1574 st_tcb_at_def) 1575 apply (drule_tac x=t in bspec) 1576 apply fastforce 1577 apply clarsimp 1578 apply (simp add: other_obj_relation_def) 1579 apply clarsimp 1580 apply (clarsimp simp: obj_at'_def) 1581 apply (simp add: projectKO_eq) 1582 apply (case_tac "ko",simp_all) 1583 apply (simp add: project_inject) 1584 apply (rule_tac x="tcb_state tcb" in exI) 1585 apply simp 1586 apply (simp add: tcb_relation_def) 1587 done 1588 1589 1590lemma ct_running'_related: "\<lbrakk>(a, c) \<in> state_relation; invs' c; ct_running a\<rbrakk> \<Longrightarrow> ct_running' c" 1591 apply (clarsimp simp: ct_in_state_def ct_in_state'_def 1592 curthread_relation) 1593 apply (frule(1) st_tcb_at_coerce_haskell) 1594 apply (simp add: invs'_def cur_tcb'_def curthread_relation) 1595 apply (erule pred_tcb'_weakenE) 1596 apply (case_tac st, simp_all)[1] 1597 done 1598 1599lemma ct_idle'_related: "\<lbrakk>(a, c) \<in> state_relation; invs' c; ct_idle a\<rbrakk> \<Longrightarrow> ct_idle' c" 1600 apply (clarsimp simp: ct_in_state_def ct_in_state'_def 1601 curthread_relation) 1602 apply (frule(1) st_tcb_at_coerce_haskell) 1603 apply (simp add: invs'_def cur_tcb'_def curthread_relation) 1604 apply (erule pred_tcb'_weakenE) 1605 apply (case_tac st, simp_all)[1] 1606 done 1607 1608lemma invs_machine_state: 1609 "invs s \<Longrightarrow> valid_machine_state s" 1610 by (clarsimp simp: invs_def valid_state_def) 1611 1612(* FIXME MOVE to where sched_act_rct_related *) 1613lemma sched_act_cnt_related: 1614 "\<lbrakk> (a, c) \<in> state_relation; ksSchedulerAction c = ChooseNewThread \<rbrakk> 1615 \<Longrightarrow> scheduler_action a = choose_new_thread" 1616 by (case_tac "scheduler_action a", simp_all add: state_relation_def) 1617 1618 1619lemma haskell_to_abs: "uop_nonempty uop \<Longrightarrow> global_automata_refine 1620 check_active_irq_A_if (do_user_op_A_if uop) 1621 kernel_call_A_if kernel_handle_preemption_if 1622 kernel_schedule_if kernel_exit_A_if 1623 full_invs_if (ADT_A_if uop) {s. step_restrict s} 1624 checkActiveIRQ_H_if (doUserOp_H_if uop) 1625 kernelCall_H_if handlePreemption_H_if 1626 schedule'_H_if kernelExit_H_if 1627 full_invs_if' (ADT_H_if uop) (lift_snd_rel state_relation) True" 1628 apply (simp add: global_automata_refine_def) 1629 apply (intro conjI) 1630 apply (rule abstract_invs) 1631 apply (rule haskell_invs) 1632 apply (unfold_locales) 1633 apply (simp add: step_restrict_def) 1634 apply (simp add: ADT_H_if_def ADT_A_if_def) 1635 apply (clarsimp simp add: lift_snd_rel_def full_invs_if_def full_invs_if'_def) 1636 apply (frule valid_device_abs_state_eq[OF invs_machine_state]) 1637 apply (frule absKState_correct[rotated]) 1638 apply simp+ 1639 apply (simp add: ADT_H_if_def ADT_A_if_def lift_fst_rel_def) 1640 apply (clarsimp simp: lift_snd_rel_def) 1641 apply (subgoal_tac "((a, absKState bb), ba) \<in> full_invs_if \<and> (absKState bb, bb) \<in> state_relation") 1642 apply (fastforce simp: step_restrict_def has_srel_state_def 1643 lift_fst_rel_def lift_snd_rel_def) 1644 apply (simp add: full_invs_if'_def) 1645 apply (clarsimp simp: ex_abs_def) 1646 apply (frule(1) absKState_correct[rotated],simp+) 1647 apply (simp add: full_invs_if_def) 1648 apply (frule valid_device_abs_state_eq[OF invs_machine_state]) 1649 apply (case_tac ba; clarsimp simp: domain_time_rel_eq domain_list_rel_eq) 1650 apply (fastforce simp: active_from_running ct_running_related ct_idle_related schedaction_related)+ 1651 apply (simp add: sched_act_cnt_related) 1652 apply (fastforce simp: active_from_running ct_running_related ct_idle_related schedaction_related)+ 1653 apply (simp add: check_active_irq_A_if_def checkActiveIRQ_H_if_def) 1654 apply (rule step_corres_lifts) 1655 apply (rule corres_guard_imp) 1656 apply (rule check_active_irq_if_corres,simp+) 1657 apply (rule checkActiveIRQ_if_empty_fail) 1658 apply (simp add: check_active_irq_A_if_def checkActiveIRQ_H_if_def) 1659 apply (rule step_corres_lifts) 1660 apply (rule corres_guard_imp) 1661 apply (rule check_active_irq_if_corres,simp+) 1662 apply (rule checkActiveIRQ_if_empty_fail) 1663 apply (simp add: do_user_op_A_if_def doUserOp_H_if_def) 1664 apply (rule step_corres_lifts) 1665 apply (rule corres_guard_imp) 1666 apply (rule do_user_op_if_corres) 1667 apply (fastforce simp: full_invs_if_def uop_nonempty_def) 1668 apply (simp add: full_invs_if'_def uop_nonempty_def) 1669 apply (rule doUserOp_if_empty_fail) 1670 apply (simp add: kernelCall_H_if_def kernel_call_A_if_def) 1671 apply (rule step_corres_lifts) 1672 apply (rule corres_rel_imp) 1673 apply (rule corres_guard_imp) 1674 apply (rule kernel_entry_if_corres) 1675 apply clarsimp 1676 apply ((clarsimp simp: full_invs_if_def full_invs_if'_def)+)[2] 1677 apply (fastforce simp: prod_lift_def) 1678 apply (rule kernelEntry_if_empty_fail) 1679 apply (simp add: kernel_handle_preemption_if_def handlePreemption_H_if_def) 1680 apply (rule step_corres_lifts) 1681 apply (rule corres_guard_imp) 1682 apply (rule handle_preemption_if_corres) 1683 apply (simp add: full_invs_if_def) 1684 apply (simp add: full_invs_if'_def) 1685 apply (rule handlePreemption_if_empty_fail) 1686 apply (simp add: kernel_schedule_if_def schedule'_H_if_def) 1687 apply (rule step_corres_lifts) 1688 apply (rule corres_guard_imp) 1689 apply (rule schedule_if_corres) 1690 apply (simp add: full_invs_if_def) 1691 apply (simp add: full_invs_if'_def) 1692 apply (rule schedule'_if_empty_fail) 1693 apply (simp add: kernel_exit_A_if_def kernelExit_H_if_def split del: if_split) 1694 apply (rule_tac S="\<top>" and S'="invs'" in step_corres_lifts(5)) 1695 apply (rule corres_guard_imp) 1696 apply (rule kernel_exit_if_corres) 1697 apply ((simp add: full_invs_if_def full_invs_if'_def)+)[2] 1698 apply (rule kernelExit_if_empty_fail) 1699 apply clarsimp 1700 apply (clarsimp simp: ct_running'_related ct_running_related) 1701 apply wp 1702 apply (clarsimp simp: full_invs_if'_def) 1703 apply wp 1704 apply (clarsimp simp: kernel_call_A_if_def) 1705 apply (drule use_valid[OF _ kernel_entry_if_no_preempt]; simp) 1706 done 1707 1708lemma doUserOp_if_no_interrupt: "\<lbrace>K(uop_sane uop)\<rbrace> doUserOp_if uop tc \<lbrace>\<lambda>r s. (fst r) \<noteq> Some Interrupt\<rbrace>" 1709 apply (simp add: doUserOp_if_def del: split_paired_All) 1710 apply (wp select_wp | wpc)+ 1711 apply (clarsimp simp: uop_sane_def simp del: split_paired_All) 1712 done 1713 1714lemma ADT_A_if_Init_Fin_serial: "uop_sane uop \<Longrightarrow> 1715 Init_Fin_serial (ADT_A_if uop) s0 (full_invs_if \<inter> {s. step_restrict s})" 1716 apply (simp add: Init_Fin_serial_def) 1717 apply (rule conjI) 1718 apply (rule global_automata_refine.abs_serial[OF haskell_to_abs]) 1719 apply (simp add: uop_sane_def uop_nonempty_def) 1720 apply (fastforce simp: step_restrict_def has_srel_state_def) 1721 apply (clarsimp simp add: doUserOp_H_if_def) 1722 apply (frule use_valid[OF _ doUserOp_if_no_interrupt]) 1723 apply simp+ 1724 apply (unfold_locales) 1725 apply (clarsimp simp: ADT_A_if_def)+ 1726 done 1727 1728lemma ADT_A_if_enabled: 1729 "uop_sane uop \<Longrightarrow> enabled_system (ADT_A_if uop) s0" 1730 apply (rule Init_Fin_serial.enabled) 1731 apply (rule ADT_A_if_Init_Fin_serial) 1732 apply simp 1733 done 1734 1735lemma (in valid_initial_state_noenabled) uop_nonempty: 1736 "uop_nonempty utf" 1737 apply (simp add: uop_nonempty_def utf_non_empty) 1738 done 1739 1740lemma (in valid_initial_state_noenabled) uop_sane: 1741 "uop_sane utf" 1742 apply (simp add: uop_sane_def utf_non_empty) 1743 apply (cut_tac utf_non_interrupt) 1744 apply blast 1745 done 1746 1747sublocale valid_initial_state_noenabled \<subseteq> valid_initial_state 1748 apply (unfold_locales) 1749 using ADT_A_if_enabled[of utf s0, OF uop_sane] 1750 apply (fastforce simp: enabled_system_def s0_def) 1751 using ADT_A_if_Init_Fin_serial[OF uop_sane, of s0] 1752 apply (simp only: Init_Fin_serial_def serial_system_def Init_Fin_serial_axioms_def s0_def)+ 1753 done 1754 1755end 1756