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 Syscall_S 12imports Separation 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17lemma syscall_bisim: 18 assumes bs: 19 "bisim (fr \<oplus> r_flt_rel) P P' m_flt m_flt'" 20 "\<And>flt flt'. fr flt flt' \<Longrightarrow> 21 bisim r (P_flt flt) (P'_flt flt') (h_flt flt) (h_flt' flt')" 22 "\<And>rv rv'. r_flt_rel rv rv' \<Longrightarrow> 23 bisim (ser \<oplus> r_err_rel rv rv') 24 (P_no_flt rv) (P'_no_flt rv') 25 (m_err rv) (m_err' rv')" 26 "\<And>rv rv' err err'. \<lbrakk>r_flt_rel rv rv'; ser err err'\<rbrakk> 27 \<Longrightarrow> bisim r (P_err rv err) 28 (P'_err rv' err') (h_err err) (h_err' err')" 29 "\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk> 30 \<Longrightarrow> bisim (f \<oplus> r) 31 (P_no_err rvf rve) (P'_no_err rvf' rve') 32 (m_fin rve) (m_fin' rve')" 33 assumes wp: "\<And>rv. \<lbrace>Q_no_flt rv\<rbrace> m_err rv \<lbrace>P_no_err rv\<rbrace>, \<lbrace>P_err rv\<rbrace>" 34 "\<And>rv'. \<lbrace>Q'_no_flt rv'\<rbrace> m_err' rv' \<lbrace>P'_no_err rv'\<rbrace>,\<lbrace>P'_err rv'\<rbrace>" 35 "\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>" 36 "\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>" 37 38 shows "bisim (f \<oplus> r) (P and Q) (P' and Q') 39 (syscall m_flt h_flt m_err h_err m_fin) 40 (syscall m_flt' h_flt' m_err' h_err' m_fin')" 41 apply (simp add: syscall_def liftE_bindE) 42 apply (rule bisim_split_bind_case_sum) 43 apply (rule bs) 44 apply simp 45 apply (rule bs) 46 apply simp 47 apply (simp add: liftE_bindE) 48 apply (rule bisim_split_bind_case_sum) 49 apply (erule bs) 50 apply simp 51 apply (erule bs) 52 apply simp 53 apply (erule(1) bs) 54 apply (rule wp)+ 55 done 56 57lemma dc_refl: "dc r r" by simp 58 59 60lemma bisim_catch_faults_r: 61 assumes bs: "\<And>x. bisim_underlying sr r P (P' x) a (m x)" 62 and flt: "\<lbrace>S\<rbrace> b \<lbrace>\<lambda>_ _. False\<rbrace>, \<lbrace>P'\<rbrace>" 63 and pure: "\<And>s. \<lbrace>S' and (=) s\<rbrace> b \<lbrace>\<lambda>_. (=) s\<rbrace>" 64 and db: "not_empty Pd b" 65 shows "bisim_underlying sr r P (S and S' and Pd) a (b <catch> m)" 66 unfolding catch_def 67 apply (rule bisim_symb_exec_r [OF _ flt [unfolded validE_def] pure db] ) 68 apply (case_tac x) 69 apply simp 70 apply (rule bs) 71 apply simp 72 apply (rule bisim_underlyingI, simp_all)[1] 73 done 74 75lemma bisim_validE_R: 76 assumes ac: "bisim_underlying (=) (dc \<oplus> (=)) P P' a a'" 77 and rl: "\<lbrace>Q\<rbrace> a \<lbrace>S\<rbrace>, -" 78 shows "\<lbrace>P and P' and Q\<rbrace> a' \<lbrace>S\<rbrace>, -" 79 using ac rl 80 unfolding bisim_underlying_def valid_def validE_def validE_R_def 81 by (fastforce simp: split_def split: sum.splits) 82 83lemma bisim_validE_R2: 84 assumes ac: "bisim_underlying (=) (=) P P' a a'" 85 and rl: "\<lbrace>Q\<rbrace> a' \<lbrace>S\<rbrace>, -" 86 shows "\<lbrace>P and P' and Q\<rbrace> a \<lbrace>S\<rbrace>, -" 87 using ac rl 88 unfolding bisim_underlying_def valid_def validE_def validE_R_def 89 by (fastforce simp: split_def split: sum.splits) 90 91 92lemma bisim_rab: 93 "bisim (dc \<oplus> (=)) \<top> (\<lambda>s. separate_cnode_cap (caps_of_state s) cap \<and> valid_cap cap s) 94 (doE 95 _ \<leftarrow> whenE (length cref < word_bits) (throwError undefined); 96 case cap of 97 CNodeCap p bits guard \<Rightarrow> if guard \<le> cref then 98 returnOk ((p, take bits (drop (length guard) cref)), drop (bits + length guard) cref) 99 else 100 (throwError undefined) 101 | _ \<Rightarrow> throwError undefined 102 odE) 103 (resolve_address_bits (cap, cref))" 104 unfolding resolve_address_bits_def 105 apply (cases "length cref < word_bits") 106 apply (auto intro!: bisim_underlyingI 107 elim!: separate_cnode_capE 108 simp: whenE_def in_monad Bex_def in_bindE word_bits_def in_get_cap_cte_wp_at cte_wp_at_caps_of_state 109 simp del: add_is_0 split: if_split_asm)[1] 110 apply simp 111 apply (rule bisim_underlyingI) 112 apply (clarsimp ) 113 apply (erule separate_cnode_capE) 114 apply (fastforce simp: word_bits_def in_monad ) 115 apply (case_tac "\<not> guard \<le> cref") 116 apply (clarsimp simp: in_monad Bex_def) 117 apply (drule (2) valid_sep_cap_not_cnode [where cref = cref]) 118 apply simp 119 apply (fastforce simp: in_monad Bex_def in_bindE word_bits_def in_get_cap_cte_wp_at cte_wp_at_caps_of_state whenE_def 120 simp del: add_is_0 split: if_split_asm) 121 apply clarsimp 122 apply (erule separate_cnode_capE) 123 apply (fastforce simp: word_bits_def in_monad) 124 apply (drule (2) valid_sep_cap_not_cnode [where cref = cref]) 125 apply simp 126 apply (fastforce simp: in_monad Bex_def in_bindE word_bits_def in_get_cap_cte_wp_at cte_wp_at_caps_of_state whenE_def 127 simp del: add_is_0 split: if_split_asm) 128 done 129 130 131lemma lsft_sep: 132 "\<lbrace>separate_state and valid_objs\<rbrace> lookup_slot_for_thread tcb cptr \<lbrace>\<lambda>rv s. \<forall>cap. caps_of_state s (fst rv) = Some cap \<longrightarrow> separate_cap cap\<rbrace>, -" 133 unfolding lookup_slot_for_thread_def 134 apply wp 135 apply (rule bisim_validE_R) 136 apply (rule bisim_rab) 137 apply (wpc | wp whenE_throwError_wp)+ 138 apply (fastforce elim: separate_cnode_capE dest: separate_state_get_tcbD objs_valid_tcb_ctable) 139 done 140 141lemma get_cap_wp': 142 "\<lbrace>\<lambda>s. \<forall>cap. caps_of_state s p = Some cap \<longrightarrow> Q cap s\<rbrace> get_cap p \<lbrace>Q\<rbrace>" 143 apply (wp get_cap_wp) 144 apply (simp add: cte_wp_at_caps_of_state) 145 done 146 147lemma lc_sep [wp]: 148 "\<lbrace>separate_state and valid_objs \<rbrace> lookup_cap tcb cptr \<lbrace>\<lambda>cap _. separate_cap cap\<rbrace>, -" 149 unfolding lookup_cap_def 150 apply (simp add: split_def) 151 apply (rule hoare_pre) 152 apply (wp get_cap_wp' lsft_sep) 153 apply simp 154 done 155 156 157lemma not_empty_thread_get [wp]: 158 "not_empty (tcb_at p) (thread_get f p)" 159 unfolding thread_get_def 160 apply (rule not_empty_guard_imp) 161 apply (simp add: gets_the_def bind_assoc) 162 apply (wp ) 163 apply (simp add: tcb_at_def) 164 done 165 166lemma not_empty_throwError [wp]: 167 "not_empty \<top> (throwError e)" 168 unfolding not_empty_def throwError_def by (fastforce simp: return_def) 169 170lemma not_empty_cap_fault_on_failure [wp]: 171 assumes d: "not_empty P m" 172 shows "not_empty P (cap_fault_on_failure a b m)" 173 unfolding cap_fault_on_failure_def 174 apply (simp add: handleE_def handleE'_def) 175 apply (rule not_empty_guard_imp) 176 apply (wp d | wpc | simp)+ 177 done 178 179lemma not_empty_splitE [wp_split]: 180 assumes da: "not_empty Pa a" 181 and db: "\<And>x. not_empty (Pb x) (b x)" 182 and v: "\<lbrace>Pb'\<rbrace> a \<lbrace>Pb\<rbrace>, -" 183 shows "not_empty (Pa and Pb') (a >>=E b)" 184 using v 185 apply (clarsimp simp: bindE_def validE_R_def validE_def) 186 apply (rule not_empty_split [OF da]) 187 apply (rule not_empty_lift [OF db]) 188 apply (erule hoare_post_imp [rotated]) 189 apply (clarsimp split: sum.splits) 190 done 191 192lemma not_empty_whenE_throwError [wp]: 193 "not_empty \<top> (whenE P (throwError e))" 194 by (simp add: whenE_def throwError_def return_def not_empty_def returnOk_def) 195 196lemma not_empty_returnOk [wp]: 197 "not_empty \<top> (returnOk v)" 198 by (simp add: return_def not_empty_def returnOk_def) 199 200lemma not_empty_if [wp_split]: 201 "\<lbrakk> not_empty Pt m; not_empty Pf m' \<rbrakk> \<Longrightarrow> not_empty (\<lambda>s. (b \<longrightarrow> Pt s) \<and> ( \<not> b \<longrightarrow> Pf s)) (if b then m else m')" 202 by clarsimp 203 204lemma not_empty_lsft: 205 shows "not_empty (tcb_at t and valid_objs and separate_state) (lookup_slot_for_thread t cptr)" 206 unfolding lookup_slot_for_thread_def 207 apply (simp add: gets_the_def bind_assoc) 208 apply (rule not_empty_guard_imp) 209 apply (wp bisim_not_empty [OF bisim_rab] | wpc)+ 210 apply (fastforce simp: tcb_at_def elim: separate_cnode_capE dest: separate_state_get_tcbD objs_valid_tcb_ctable) 211 done 212 213lemma not_empty_get_cap [wp]: 214 "not_empty (cte_at p) (get_cap p)" 215 unfolding not_empty_def 216 by (clarsimp simp: cte_at_def) 217 218lemma not_empty_lc: 219 shows "not_empty (tcb_at t and valid_objs and separate_state) (lookup_cap t cptr)" 220 unfolding lookup_cap_def 221 apply (simp add: split_def) 222 apply (rule not_empty_guard_imp) 223 apply (wp not_empty_lsft) 224 apply simp 225 done 226 227lemma not_empty_get [wp]: 228 "not_empty \<top> get" 229 unfolding not_empty_def get_def by simp 230 231lemma not_empty_put [wp]: 232 "not_empty \<top> (put s)" 233 unfolding not_empty_def put_def by simp 234 235lemma not_empty_set_object [wp]: 236 "not_empty \<top> (set_object p v)" 237 unfolding set_object_def 238 apply simp 239 apply (rule not_empty_guard_imp) 240 apply wp 241 apply simp 242 done 243 244lemma not_empty_assert_opt [wp]: 245 "not_empty (\<lambda>_. v \<noteq> None) (assert_opt v)" 246 unfolding not_empty_def assert_opt_def 247 by (clarsimp simp: return_def) 248 249lemma not_empty_thread_set [wp]: 250 "not_empty (tcb_at p) (thread_set f p)" 251 unfolding thread_set_def 252 apply (simp add: gets_the_def bind_assoc) 253 apply (rule not_empty_guard_imp) 254 apply wp 255 apply (simp add: tcb_at_def) 256 done 257 258lemma not_empty_False: 259 "not_empty (\<lambda>_. False) m" 260 unfolding not_empty_def by simp 261 262lemma not_empty_gen_asm: 263 assumes ne: "P \<Longrightarrow> not_empty R m" 264 shows "not_empty (R and (\<lambda>_. P)) m" 265 using ne unfolding not_empty_def by auto 266 267lemmas bisim_refl' = bisim_refl [where P = \<top> and P' = \<top> and R = "(=)", OF refl] 268 269lemma send_fault_ipc_bisim: 270 "bisim (=) \<top> (tcb_at tcb and valid_objs and separate_state) 271 (set_thread_state tcb Inactive) (send_fault_ipc tcb flt' <catch> handle_double_fault tcb flt')" 272 unfolding send_fault_ipc_def 273 apply (rule bisim_guard_imp) 274 apply (rule bisim_catch_faults_r [where S = "separate_state and valid_objs"]) 275 apply (clarsimp simp: handle_double_fault_def) 276 apply (rule bisim_refl') 277 apply (simp add: Let_def) 278 apply (rule hoare_vcg_seqE) 279 apply (rule hoare_vcg_seqE) 280 apply wpc 281 apply wp+ 282 apply simp 283 apply (rule hoare_post_imp_R [OF lc_sep]) 284 apply (clarsimp simp: separate_cap_def) 285 apply (wp | simp add: Let_def)+ 286 apply (rule_tac P = "separate_cap handler_cap" in hoare_gen_asmE') 287 apply (erule separate_capE, simp_all)[1] 288 apply (wp | simp)+ 289 apply clarsimp 290 apply assumption 291 \<comment> \<open>det_ont\<close> 292 apply (simp add: Let_def cong: cap.case_cong) 293 apply (wp not_empty_lc) 294 apply (rule_tac P = "separate_cap xa" in not_empty_gen_asm) 295 apply (erule separate_capE, simp_all)[1] 296 apply wpsimp+ 297 done 298 299lemma handle_fault_bisim: 300 "bisim (=) \<top> (separate_state and tcb_at tcb and valid_objs) (handle_fault tcb flt) (Ipc_A.handle_fault tcb flt')" 301 unfolding handle_fault_def Ipc_A.handle_fault_def 302 apply (rule bisim_guard_imp) 303 apply (rule bisim_symb_exec_r [where Pe = \<top>]) 304 apply simp 305 apply (rule send_fault_ipc_bisim) 306 apply (wpsimp simp: gets_the_def tcb_at_def)+ 307 done 308 309lemmas bisim_throwError_dc = bisim_throwError [where f = dc, OF dc_refl] 310 311lemma bisim_returnOk: 312 "R a b \<Longrightarrow> bisim (f \<oplus> R) \<top> \<top> (returnOk a) (returnOk b)" 313 apply (simp add: returnOk_def) 314 apply (rule bisim_return) 315 apply simp 316 done 317 318lemma bisim_liftME_same: 319 assumes bs: "bisim (f \<oplus> (=)) P P' m m'" 320 shows "bisim (f \<oplus> (=)) P P' (liftME g m) (liftME g m')" 321 unfolding liftME_def 322 apply (rule bisim_guard_imp) 323 apply (rule bisim_splitE [OF bs]) 324 apply simp 325 apply (rule bisim_returnOk) 326 apply simp 327 apply wp 328 apply simp+ 329 done 330 331lemma bisim_split_if: 332 "\<lbrakk> P \<Longrightarrow> bisim R Pt Pt' a a'; \<not> P \<Longrightarrow> bisim R Pf Pf' b b' \<rbrakk> \<Longrightarrow> 333 bisim R (\<lambda>s. (P \<longrightarrow> Pt s) \<and> (\<not> P \<longrightarrow> Pf s)) (\<lambda>s. (P \<longrightarrow> Pt' s) \<and> (\<not> P \<longrightarrow> Pf' s)) 334 (if P then a else b) (if P then a' else b')" 335 by simp 336 337lemma bisim_reflE: 338 "bisim ((=) \<oplus> (=)) \<top> \<top> a a" 339 apply (rule bisim_underlyingI) 340 apply (case_tac r, fastforce+)[1] 341 apply (case_tac r', fastforce+)[1] 342 done 343 344lemma bisim_reflE_dc: 345 "bisim (dc \<oplus> (=)) \<top> \<top> a a" 346 apply (rule bisim_underlyingI) 347 apply (case_tac r, fastforce+)[1] 348 apply (case_tac r', fastforce+)[1] 349 done 350 351lemma decode_invocation_bisim: 352 "bisim ((=) \<oplus> (=)) \<top> (K (separate_cap cap)) 353 (decode_invocation a b c d cap f) (Decode_A.decode_invocation a b c d cap f)" 354 unfolding decode_invocation_def Decode_A.decode_invocation_def 355 apply (rule bisim_guard_imp) 356 apply (rule bisim_separate_cap_cases [where cap = cap]) 357 apply (simp split del: if_split) 358 apply (rule bisim_throwError, simp) 359 apply (simp split del: if_split) 360 apply (rule bisim_reflE) 361 apply (fastforce intro!: bisim_throwError bisim_returnOk simp: AllowRecv_def AllowSend_def) 362 apply simp 363 done 364 365abbreviation 366 "separate_inv c \<equiv> \<exists>ptr badge. c = InvokeNotification ptr badge" 367 368lemma perform_invocation_bisim: 369 "bisim (dc \<oplus> (=)) \<top> (\<top> and K (separate_inv c)) 370 (perform_invocation a b c) (Syscall_A.perform_invocation a b c)" 371 apply (rule bisim_gen_asm_r) 372 apply clarsimp 373 apply (rule bisim_reflE_dc) 374 done 375 376lemmas bisim_split_reflE_eq = bisim_split_reflE [where R = "(=)" and f = "(=)", OF _ _ _ refl refl] 377lemmas bisim_split_reflE_dc = bisim_split_reflE [where R = "(=)" and f = "dc", OF _ _ _ dc_refl refl] 378 379lemma decode_separate_inv: 380 "\<lbrace>\<top> and K ((\<forall>c \<in> set f. separate_cap (fst c)) \<and> (separate_cap cap))\<rbrace> Decode_A.decode_invocation a b c d cap f \<lbrace>\<lambda>rv s. separate_inv rv\<rbrace>, -" 381 unfolding Decode_A.decode_invocation_def 382 apply (rule hoare_gen_asmE) 383 apply clarify 384 apply (erule separate_capE, simp_all split del: if_split) 385 apply (rule hoare_pre, (wp | simp add: comp_def)+)[1] 386 apply (rule hoare_pre) 387 apply (wp | simp)+ 388done 389 390lemma lcas_sep [wp]: 391 "\<lbrace>separate_state and valid_objs\<rbrace> lookup_cap_and_slot t v \<lbrace>\<lambda>rv s. separate_cap (fst rv)\<rbrace>, -" 392 apply (simp add: lookup_cap_and_slot_def split_def bind_assoc) 393 apply (rule hoare_pre) 394 apply (wp lsft_sep get_cap_wp'|simp)+ 395 done 396 397lemma lec_separate_caps: 398 "\<lbrace>separate_state and valid_objs\<rbrace> lookup_extra_caps t buffer ra \<lbrace>\<lambda>rv s. (\<forall>c\<in>set rv. separate_cap (fst c))\<rbrace>, -" 399 unfolding lookup_extra_caps_def 400 apply (wp mapME_set | simp)+ 401 done 402 403lemma handle_invocation_bisim: 404 "bisim (dc \<oplus> (=)) \<top> (separate_state and valid_objs and cur_tcb) (handle_invocation c b) (Syscall_A.handle_invocation c b)" 405 unfolding handle_invocation_def Syscall_A.handle_invocation_def 406 apply (simp add: split_def) 407 apply (rule bisim_guard_imp) 408 apply (rule bisim_split_reflE_dc)+ 409 apply (rule syscall_bisim) 410 apply (rule bisim_split_reflE_dc [where Q = "\<lambda>_. \<top>" and Q' = "\<lambda>_. \<top>"])+ 411 apply (rule bisim_reflE_dc) 412 apply wp+ 413 apply (rule bisim_when [OF _ refl]) 414 apply (rule handle_fault_bisim) 415 apply simp 416 apply (rule bisim_split_reflE_eq) 417 apply simp 418 apply (rule decode_invocation_bisim) 419 apply wp+ 420 apply (simp, rule bisim_refl') 421 apply simp 422 apply (rule bisim_split_reflE_dc) 423 apply (rule bisim_splitE_req) 424 apply (rule perform_invocation_bisim) 425 apply simp 426 apply (rule bisim_refl') 427 apply (wp | simp)+ 428 apply (rule decode_separate_inv) 429 apply (wp lec_separate_caps | simp add: cur_tcb_def)+ 430 done 431 432lemma bisim_split_catch: 433 assumes bm: "bisim (f' \<oplus> r) Pn Pn' m m'" 434 and bc: "\<And>x x'. f' x x' \<Longrightarrow> bisim r (Pf x) (Pf' x') (c x) (c' x')" 435 and v1: "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>Pf\<rbrace>" 436 and v2: "\<lbrace>P'\<rbrace> m' \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>Pf'\<rbrace>" 437 shows "bisim r (Pn and P) (Pn' and P') (m <catch> c) (m' <catch> c')" 438 unfolding catch_def 439 apply (rule bisim_split [where Q = "\<lambda>r s. case_sum (\<lambda>l. Pf l s) (\<lambda>_. True) r" and Q' = "\<lambda>r s. case_sum (\<lambda>l. Pf' l s) (\<lambda>_. True) r", OF bm, folded validE_def]) 440 apply (case_tac ra) 441 apply clarsimp 442 apply (erule bc) 443 apply clarsimp 444 apply (rule bisim_return') 445 apply simp 446 apply (rule v1) 447 apply (rule v2) 448 done 449 450lemma rel_sum_comb_eq: 451 "((=) \<oplus> (=)) = (=)" 452 apply (rule ext, rule ext) 453 apply (case_tac x) 454 apply auto 455 done 456 457lemma bisim_split_catch_req: 458 assumes bm: "bisim ((=) \<oplus> (=)) Pn Pn' m m'" 459 and bc: "\<And>x. bisim (=) (Pf x) (Pf' x) (c x) (c' x)" 460 and v1: "\<lbrace>P\<rbrace> m \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>\<lambda>r. Pf r and Pf' r\<rbrace>" 461 shows "bisim (=) (Pn and P) Pn' (m <catch> c) (m' <catch> c')" 462 unfolding catch_def 463 apply (rule bisim_split_req [where Q = "\<lambda>r s. case_sum (\<lambda>l. Pf l s) (\<lambda>_. True) r" and Q' = "\<lambda>r s. case_sum (\<lambda>l. Pf' l s) (\<lambda>_. True) r"]) 464 apply (rule bm [simplified rel_sum_comb_eq]) 465 apply (case_tac r) 466 apply clarsimp 467 apply (rule bc) 468 apply clarsimp 469 apply (rule bisim_return') 470 apply simp 471 apply (rule hoare_post_imp [OF _ v1 [unfolded validE_def]]) 472 apply (clarsimp split: sum.split_asm) 473 done 474 475lemma bisim_injection: 476 assumes x: "t = injection_handler fn" 477 assumes y: "t' = injection_handler fn'" 478 assumes z: "\<And>ft ft'. f' ft ft' \<Longrightarrow> f (fn ft) (fn' ft')" 479 shows "bisim (f' \<oplus> r) P P' m m' 480 \<Longrightarrow> bisim (f \<oplus> r) P P' (t m) (t' m')" 481 apply (simp add: injection_handler_def handleE'_def x y) 482 apply (rule bisim_guard_imp) 483 apply (erule bisim_split) 484 apply (case_tac ra, clarsimp+)[1] 485 apply (rule bisim_throwError) 486 apply (simp add: z) 487 apply clarsimp 488 apply (rule bisim_return) 489 apply wpsimp+ 490 done 491 492lemma separate_state_cdt [simp]: 493 "separate_state (s\<lparr>cdt := x\<rparr>) = separate_state s" 494 unfolding separate_state_def 495 by (simp add: get_tcb_def) 496 497lemma separate_state_original [simp]: 498 "separate_state (s\<lparr>is_original_cap := x\<rparr>) = separate_state s" 499 unfolding separate_state_def 500 by (simp add: get_tcb_def) 501 502lemma separate_cap_NullCap [simp]: "separate_cap NullCap" by (simp add: separate_cap_def) 503 504lemma set_cap_NullCap_separate_state [wp]: 505 "\<lbrace>separate_state\<rbrace> set_cap NullCap cptr \<lbrace>\<lambda>_. separate_state\<rbrace>" 506 unfolding separate_state_def separate_tcb_def separate_cnode_cap_def 507 apply (simp add: tcb_at_typ) 508 apply (rule hoare_pre) 509 apply wps 510 apply (wp set_cap_typ_at hoare_vcg_all_lift) 511 apply (clarsimp simp: separate_cap_def) 512 apply (drule spec, drule (1) mp) 513 apply (clarsimp split: cap.splits option.splits) 514 done 515 516lemma separate_state_pres: 517 assumes rl: "(\<And>P t p. \<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>)" 518 shows "\<lbrace>separate_state\<rbrace> f \<lbrace>\<lambda>_. separate_state\<rbrace>" 519 unfolding separate_state_def[abs_def] 520 apply (simp add: tcb_at_typ) 521 apply (wp hoare_vcg_all_lift rl) 522 done 523 524lemma separate_state_pres': 525 assumes rl: "(\<And>P t p. \<lbrace>\<lambda>s. P (typ_at t p s)\<rbrace> f \<lbrace>\<lambda>_ s. P (typ_at t p s)\<rbrace>)" 526 "(\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>)" 527 shows "\<lbrace>separate_state\<rbrace> f \<lbrace>\<lambda>_. separate_state\<rbrace>" 528 apply (rule separate_state_pres) 529 apply (rule hoare_pre) 530 apply (wps rl) 531 apply wp 532 apply simp 533 done 534 535lemma separate_state_more_update[simp]: 536 "separate_state (trans_state f s) = 537 separate_state s" 538 by (simp add: separate_state_def) 539 540lemma cap_delete_one_sep [wp]: 541 "\<lbrace>separate_state\<rbrace> cap_delete_one cptr \<lbrace>\<lambda>_. separate_state\<rbrace>" 542 unfolding cap_delete_one_def 543 apply (simp add: unless_when) 544 apply (wp get_cap_wp') 545 apply (simp add: empty_slot_def post_cap_deletion_def) 546 apply (wp | simp)+ 547 (* ugh *) 548 apply (rule separate_state_pres) 549 apply (rule hoare_pre) 550 apply (wps set_cdt_typ_at) 551 apply (wp) 552 apply assumption 553 apply (wp get_cap_inv hoare_drop_imps)+ 554 apply (simp add: conj_comms) 555 apply (rule separate_state_pres) 556 apply (rule hoare_pre) 557 apply (wps) 558 apply wp 559 apply simp 560 apply (wp get_cap_wp')+ 561 apply simp 562 done 563 564lemma bisim_caller_cap: 565 assumes bs: "bisim R P P' a (f NullCap)" 566 shows "bisim R P (P' and tcb_at p and separate_state) a (get_cap (p, tcb_cnode_index 3) >>= f)" 567 apply (rule bisim_guard_imp) 568 apply (rule bisim_symb_exec_r [where Pe = \<top>]) 569 apply (rule_tac F = "rv = NullCap" in bisim_gen_asm_r) 570 apply simp 571 apply (rule bs) 572 apply (wp get_cap_wp')+ 573 apply fastforce 574 apply wp 575 apply simp 576 apply (clarsimp simp: cte_wp_at_caps_of_state tcb_at_def 577 caps_of_state_tcb_cap_cases dom_tcb_cap_cases 578 cong: conj_cong) 579 apply (drule (1) separate_state_get_tcbD) 580 apply simp 581 done 582 583lemma delete_caller_cap_bisim: 584 "bisim (=) \<top> (tcb_at r and separate_state) (return ()) (delete_caller_cap r)" 585 unfolding delete_caller_cap_def 586 apply (rule bisim_guard_imp) 587 apply (simp add: cap_delete_one_def unless_when) 588 apply (rule bisim_caller_cap) 589 apply (simp add: when_def) 590 apply (rule bisim_refl') 591 apply simp_all 592 done 593 594lemma bisim_guard_imp_both: 595 "\<lbrakk> bisim r P P' m m'; \<And>s. R s \<Longrightarrow> P s \<and> P' s \<rbrakk> \<Longrightarrow> bisim r \<top> R m m'" 596 unfolding bisim_underlying_def by auto 597 598lemma handle_recv_bisim: 599 "bisim (=) \<top> (separate_state and cur_tcb and valid_objs) (handle_recv is_blocking) (Syscall_A.handle_recv is_blocking)" 600 unfolding handle_recv_def Syscall_A.handle_recv_def 601 apply (simp add: Let_def) 602 apply (rule bisim_guard_imp_both) 603 apply (rule bisim_split_refl) 604 apply (rule bisim_split_refl) 605 apply (rule bisim_split_catch_req) 606 apply (simp add: cap_fault_injection) 607 apply (rule bisim_injection [OF refl refl, where f' = "(=)"]) 608 apply simp 609 apply (rule bisim_split_reflE) 610 apply (rule_tac cap = rb in bisim_separate_cap_cases) 611 apply (simp, rule bisim_throwError, rule refl)+ 612 apply (simp split del: if_split) 613 apply (rule bisim_refl [where P = \<top> and P' = \<top>]) 614 apply (case_tac rc, simp_all)[1] 615 apply (wp get_cap_wp' lsft_sep | simp add: lookup_cap_def split_def del: hoare_True_E_R)+ 616 apply (rule handle_fault_bisim) 617 apply (wp get_simple_ko_wp | wpc | simp)+ 618 apply (rule_tac Q' = "\<lambda>_. separate_state and valid_objs and tcb_at r" in hoare_post_imp_R) 619 prefer 2 620 apply simp 621 apply (wp | simp add: cur_tcb_def)+ 622 done 623 624lemma handle_reply_bisim: 625 "bisim (=) \<top> (separate_state and cur_tcb) (return ()) Syscall_A.handle_reply" 626 unfolding Syscall_A.handle_reply_def 627 apply (rule bisim_guard_imp_both) 628 apply (rule bisim_symb_exec_r [where Pe = \<top>]) 629 apply (rule bisim_caller_cap) 630 apply simp 631 apply (rule bisim_return) 632 apply simp 633 apply (wp | simp add: cur_tcb_def)+ 634 done 635 636lemma handle_event_bisim: 637 "bisim (dc \<oplus> (=)) \<top> (separate_state and cur_tcb and valid_objs) (handle_event ev) (Syscall_A.handle_event ev)" 638 apply (cases ev; simp add: handle_send_def Syscall_A.handle_send_def 639 handle_call_def Syscall_A.handle_call_def 640 handle_reply_def 641 cong: syscall.case_cong) 642 643 apply (rename_tac syscall) 644 apply (case_tac syscall, simp_all)[1] 645 646 apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp) 647 apply (rule bisim_guard_imp_both) 648 apply (rule bisim_symb_exec_r_bs) 649 apply (rule handle_reply_bisim) 650 apply (rule handle_recv_bisim) 651 apply simp 652 653 apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp) 654 apply (rule bisim_guard_imp_both, rule handle_invocation_bisim, simp) 655 apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp) 656 apply (rule bisim_guard_imp_both, rule handle_reply_bisim, simp) 657 658 apply (simp add: handle_yield_def Syscall_A.handle_yield_def) 659 apply (rule bisim_guard_imp_both, rule bisim_refl', simp) 660 661 apply (rule bisim_guard_imp_both, rule handle_recv_bisim, simp) 662 663 apply (rule bisim_split_refl) 664 apply (rule handle_fault_bisim) 665 apply wp+ 666 apply (simp add: cur_tcb_def) 667 668 apply (rule bisim_split_refl) 669 apply (rule handle_fault_bisim) 670 apply wp+ 671 apply (simp add: cur_tcb_def) 672 673 apply (rule bisim_refl) 674 apply simp 675 676 apply (rename_tac vmfault_type) 677 apply (rule bisim_guard_imp_both) 678 apply (rule bisim_split_refl) 679 apply (rule bisim_split_catch_req) 680 apply (rule bisim_reflE) 681 apply (rule handle_fault_bisim) 682 apply wp 683 apply (case_tac vmfault_type, simp_all)[1] 684 apply (wp separate_state_pres) 685 apply (rule hoare_pre, wps, wp, simp) 686 apply wp 687 apply (rule hoare_pre, wps, wp, simp) 688 apply simp 689 690 apply (wp separate_state_pres)+ 691 apply (rule hoare_pre, wps, wp+, simp) 692 apply wpsimp+ 693 apply (simp add: cur_tcb_def) 694 695 apply (rule bisim_refl, simp) 696 done 697 698lemma call_kernel_bisim: 699 "bisim (=) \<top> (separate_state and cur_tcb and valid_objs) (call_kernel ev) (Syscall_A.call_kernel ev)" 700 unfolding call_kernel_def Syscall_A.call_kernel_def 701 apply (rule bisim_guard_imp_both) 702 apply simp 703 apply (rule bisim_split) 704 apply (rule bisim_split_handle) 705 apply (rule handle_event_bisim) 706 apply simp 707 apply (rule bisim_refl') 708 apply wp+ 709 apply (rule bisim_refl') 710 apply wpsimp+ 711 done 712 713 714lemma as_user_separate_state [wp]: 715 "\<lbrace>separate_state\<rbrace> as_user t f \<lbrace>\<lambda>_. separate_state\<rbrace>" 716 by (wp separate_state_pres') 717 718lemma activate_thread_separate_state [wp]: 719 "\<lbrace>separate_state\<rbrace> activate_thread \<lbrace>\<lambda>_. separate_state\<rbrace>" 720 unfolding activate_thread_def 721 by (wp separate_state_pres' | wpc | simp add: arch_activate_idle_thread_def | strengthen imp_consequent)+ 722 723lemma schedule_separate_state [wp]: 724 "\<lbrace>separate_state\<rbrace> schedule :: (unit,unit) s_monad \<lbrace>\<lambda>_. separate_state\<rbrace>" 725 apply (simp add: schedule_def switch_to_thread_def arch_switch_to_thread_def switch_to_idle_thread_def arch_switch_to_idle_thread_def allActiveTCBs_def) 726 apply (wp select_inv separate_state_pres' alternative_valid | wpc | simp add: arch_activate_idle_thread_def | strengthen imp_consequent)+ 727 done 728 729lemma set_message_info_sep_pres [wp]: 730 "\<lbrace>\<lambda>s. P (typ_at t p s) (caps_of_state s)\<rbrace> 731 set_message_info a b 732 \<lbrace>\<lambda>_ s. P (typ_at t p s) (caps_of_state s)\<rbrace>" 733 apply (rule hoare_pre) 734 apply (wp | wpc | wps | simp )+ 735 done 736 737lemma set_mrs_separate_state [wp]: 738 "\<lbrace>separate_state\<rbrace> set_mrs a b c \<lbrace>\<lambda>_. separate_state\<rbrace>" 739 apply (rule separate_state_pres) 740 apply (rule hoare_pre) 741 apply (wp | wpc | wps | simp )+ 742 done 743 744lemma send_signal_separate_state [wp]: 745 "\<lbrace>separate_state\<rbrace> send_signal a b \<lbrace>\<lambda>_. separate_state\<rbrace>" 746 unfolding send_signal_def cancel_ipc_def 747 apply (rule separate_state_pres) 748 apply (rule hoare_pre) 749 apply (wp gts_wp get_simple_ko_wp hoare_pre_cont[where a = "reply_cancel_ipc x" for x] 750 | wpc | wps 751 | simp add: update_waiting_ntfn_def)+ 752 apply (clarsimp) 753 apply (simp add: receive_blocked_def) 754 apply (case_tac st; clarsimp) 755 apply (clarsimp simp add: pred_tcb_at_def obj_at_def) 756 done 757 758lemma dmo_separate_state [wp]: 759 "\<lbrace>separate_state\<rbrace> do_machine_op f \<lbrace>\<lambda>_. separate_state\<rbrace>" 760 by (rule separate_state_pres, rule hoare_pre, wps, wp, simp) 761 762lemma handle_interrupt_separate_state [wp]: 763 "\<lbrace>separate_state\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_. separate_state\<rbrace>" 764 unfolding handle_interrupt_def 765 apply (rule hoare_pre) 766 apply (wp | wpc | wps | simp add: handle_reserved_irq_def | strengthen imp_consequent)+ 767 done 768 769lemma decode_invocation_separate_state [wp]: 770 "\<lbrace> separate_state \<rbrace> 771 Decode_SA.decode_invocation param_a param_b param_c param_d param_e param_f 772 \<lbrace> \<lambda>_. separate_state \<rbrace>" 773 unfolding decode_invocation_def by wpsimp 774 775lemma separate_state_machine_state: 776 "separate_state (s\<lparr>machine_state := ms\<rparr>) = separate_state s" 777 unfolding separate_state_def by simp 778 779crunch separate_state [wp]: set_thread_state, set_simple_ko "separate_state" 780 (wp: separate_state_pres' crunch_wps simp: crunch_simps) 781 782crunch separate_state [wp]: "Syscall_SA.handle_event" "separate_state" 783 (wp: crunch_wps syscall_valid 784 simp: crunch_simps separate_state_machine_state 785 ignore: syscall) 786 787lemma call_kernel_separate_state: 788 "\<lbrace>separate_state and cur_tcb and valid_objs\<rbrace> Syscall_A.call_kernel ev :: (unit,unit) s_monad \<lbrace>\<lambda>_. separate_state\<rbrace>" 789 apply (rule hoare_pre) 790 apply (rule bisim_valid) 791 apply (rule call_kernel_bisim) 792 apply (simp add: call_kernel_def) 793 apply (wp | wpc | wps | simp | strengthen imp_consequent)+ 794 done 795 796end 797 798end 799