1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11(* 12 CSpace invariants 13*) 14 15theory CSpace_I 16imports ArchAcc_R 17begin 18 19context begin interpretation Arch . (*FIXME: arch_split*) 20 21lemma capUntypedPtr_simps [simp]: 22 "capUntypedPtr (ThreadCap r) = r" 23 "capUntypedPtr (NotificationCap r badge a b) = r" 24 "capUntypedPtr (EndpointCap r badge a b c) = r" 25 "capUntypedPtr (Zombie r bits n) = r" 26 "capUntypedPtr (ArchObjectCap x) = Arch.capUntypedPtr x" 27 "capUntypedPtr (UntypedCap d r n f) = r" 28 "capUntypedPtr (CNodeCap r n g n2) = r" 29 "capUntypedPtr (ReplyCap r m) = r" 30 "Arch.capUntypedPtr (ARM_H.ASIDPoolCap r asid) = r" 31 "Arch.capUntypedPtr (ARM_H.PageCap d r rghts sz mapdata) = r" 32 "Arch.capUntypedPtr (ARM_H.PageTableCap r mapdata2) = r" 33 "Arch.capUntypedPtr (ARM_H.PageDirectoryCap r mapdata3) = r" 34 by (auto simp: capUntypedPtr_def 35 ARM_H.capUntypedPtr_def) 36 37lemma rights_mask_map_UNIV [simp]: 38 "rights_mask_map UNIV = allRights" 39 by (simp add: rights_mask_map_def allRights_def) 40 41declare insert_UNIV[simp] 42 43lemma maskCapRights_allRights [simp]: 44 "maskCapRights allRights c = c" 45 unfolding maskCapRights_def isCap_defs allRights_def 46 ARM_H.maskCapRights_def maskVMRights_def 47 by (cases c) (simp_all add: Let_def split: arch_capability.split vmrights.split) 48 49lemma diminished_refl'[simp]: 50 "diminished' cap cap" 51 unfolding diminished'_def 52 by (rule exI[where x=allRights], simp) 53 54lemma getCTE_inv [wp]: "\<lbrace>P\<rbrace> getCTE addr \<lbrace>\<lambda>rv. P\<rbrace>" 55 by (simp add: getCTE_def) wp 56 57lemma getEndpoint_inv [wp]: 58 "\<lbrace>P\<rbrace> getEndpoint ptr \<lbrace>\<lambda>rv. P\<rbrace>" 59 by (simp add: getEndpoint_def getObject_inv loadObject_default_inv) 60 61lemma getNotification_inv [wp]: 62 "\<lbrace>P\<rbrace> getNotification ptr \<lbrace>\<lambda>rv. P\<rbrace>" 63 by (simp add: getNotification_def getObject_inv loadObject_default_inv) 64 65lemma getSlotCap_inv [wp]: "\<lbrace>P\<rbrace> getSlotCap addr \<lbrace>\<lambda>rv. P\<rbrace>" 66 by (simp add: getSlotCap_def, wp) 67 68declare resolveAddressBits.simps[simp del] 69 70lemma cap_case_CNodeCap: 71 "(case cap of CNodeCap a b c d \<Rightarrow> P 72 | _ \<Rightarrow> Q) 73 = (if isCNodeCap cap then P else Q)" 74 by (cases cap, simp_all add: isCap_simps) 75 76lemma resolveAddressBits_inv_induct: 77 shows 78 "s \<turnstile> \<lbrace>P\<rbrace> 79 resolveAddressBits cap cref depth 80 \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>\<lambda>rv. P\<rbrace>" 81proof (induct arbitrary: s rule: resolveAddressBits.induct) 82 case (1 cap fn cref depth) 83 show ?case 84 apply (subst resolveAddressBits.simps) 85 apply (simp add: Let_def split_def cap_case_CNodeCap[unfolded isCap_simps] 86 split del: if_split cong: if_cong) 87 apply (rule hoare_pre_spec_validE) 88 apply ((elim exE | wp_once spec_strengthen_postE[OF "1.hyps"])+, 89 (rule refl conjI | simp add: in_monad split del: if_split)+) 90 apply (wp | simp add: locateSlot_conv split del: if_split 91 | wp_once hoare_drop_imps)+ 92 done 93qed 94 95lemma rab_inv' [wp]: 96 "\<lbrace>P\<rbrace> resolveAddressBits cap addr depth \<lbrace>\<lambda>rv. P\<rbrace>" 97 by (rule validE_valid, rule use_specE', rule resolveAddressBits_inv_induct) 98 99lemmas rab_inv'' [wp] = rab_inv' [folded resolveAddressBits_decl_def] 100 101crunch inv [wp]: lookupCap P 102 103lemma updateObject_cte_inv: 104 "\<lbrace>P\<rbrace> updateObject (cte :: cte) ko x y n \<lbrace>\<lambda>rv. P\<rbrace>" 105 apply (simp add: updateObject_cte) 106 apply (cases ko, simp_all add: typeError_def unless_def 107 split del: if_split 108 cong: if_cong) 109 apply (wp | simp)+ 110 done 111 112definition 113 "no_mdb cte \<equiv> mdbPrev (cteMDBNode cte) = 0 \<and> mdbNext (cteMDBNode cte) = 0" 114 115lemma mdb_next_update: 116 "m (x \<mapsto> y) \<turnstile> a \<leadsto> b = 117 (if a = x then mdbNext (cteMDBNode y) = b else m \<turnstile> a \<leadsto> b)" 118 by (simp add: mdb_next_rel_def mdb_next_def) 119 120lemma neg_no_loopsI: 121 "m \<turnstile> c \<leadsto>\<^sup>+ c \<Longrightarrow> \<not> no_loops m" 122 unfolding no_loops_def by auto 123 124lemma valid_dlistEp [elim?]: 125 "\<lbrakk> valid_dlist m; m p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0; 126 \<And>cte'. \<lbrakk> m (mdbPrev (cteMDBNode cte)) = Some cte'; 127 mdbNext (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> 128 P" 129 unfolding valid_dlist_def Let_def by blast 130 131lemma valid_dlistEn [elim?]: 132 "\<lbrakk> valid_dlist m; m p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0; 133 \<And>cte'. \<lbrakk> m (mdbNext (cteMDBNode cte)) = Some cte'; 134 mdbPrev (cteMDBNode cte') = p \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> 135 P" 136 unfolding valid_dlist_def Let_def by blast 137 138lemmas valid_dlistE = valid_dlistEn valid_dlistEp 139 140lemma mdb_next_update_other: 141 "\<lbrakk> m (x \<mapsto> y) \<turnstile> a \<leadsto> b; x \<noteq> a \<rbrakk> \<Longrightarrow> m \<turnstile> a \<leadsto> b" 142 by (simp add: mdb_next_rel_def mdb_next_def) 143 144lemma mdb_trancl_update_other: 145 assumes upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y" 146 and nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p" 147 shows "m \<turnstile> x \<leadsto>\<^sup>+ y" 148 using upd nopath 149proof induct 150 case (base y) 151 152 have "m \<turnstile> x \<leadsto> y" 153 proof (rule mdb_next_update_other) 154 from base show "p \<noteq> x" by clarsimp 155 qed fact+ 156 157 thus ?case .. 158next 159 case (step y z) 160 hence ih: "m \<turnstile> x \<leadsto>\<^sup>+ y" by auto 161 162 from ih show ?case 163 proof 164 show "m \<turnstile> y \<leadsto> z" 165 proof (rule mdb_next_update_other) 166 show "p \<noteq> y" 167 proof (cases "x = p") 168 case True thus ?thesis using step.prems by simp 169 next 170 case False thus ?thesis using step.prems ih 171 by - (erule contrapos_nn, rule trancl_into_rtrancl, simp) 172 qed 173 qed fact+ 174 qed 175qed 176 177lemma next_unfold': 178 "m \<turnstile> c \<leadsto> y = (\<exists>cte. m c = Some cte \<and> mdbNext (cteMDBNode cte) = y)" 179 unfolding mdb_next_rel_def 180 by (simp add: next_unfold split: option.splits) 181 182lemma no_self_loop_next_noloop: 183 assumes no_loop: "no_loops m" 184 and lup: "m ptr = Some cte" 185 shows "mdbNext (cteMDBNode cte) \<noteq> ptr" 186proof - 187 from no_loop have "\<not> m \<turnstile> ptr \<leadsto> ptr" 188 unfolding no_loops_def 189 by - (drule spec, erule contrapos_nn, erule r_into_trancl) 190 191 thus ?thesis using lup 192 by (simp add: next_unfold') 193qed 194 195 196lemma valid_dlistI [intro?]: 197 defines "nxt \<equiv> \<lambda>cte. mdbNext (cteMDBNode cte)" 198 and "prv \<equiv> \<lambda>cte. mdbPrev (cteMDBNode cte)" 199 assumes r1: "\<And>p cte. \<lbrakk> m p = Some cte; prv cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (prv cte) = Some cte' \<and> nxt cte' = p" 200 and r2: "\<And>p cte. \<lbrakk> m p = Some cte; nxt cte \<noteq> 0 \<rbrakk> \<Longrightarrow> \<exists>cte'. m (nxt cte) = Some cte' \<and> prv cte' = p" 201 shows "valid_dlist m" 202 unfolding valid_dlist_def 203 by (auto dest: r1 r2 simp: Let_def prv_def nxt_def) 204 205lemma no_loops_tranclE: 206 assumes nl: "no_loops m" 207 and nxt: "m \<turnstile> x \<leadsto>\<^sup>+ y" 208 shows "\<not> m \<turnstile> y \<leadsto>\<^sup>* x" 209proof 210 assume "m \<turnstile> y \<leadsto>\<^sup>* x" 211 hence "m \<turnstile> x \<leadsto>\<^sup>+ x" using nxt 212 by simp 213 214 thus False using nl 215 unfolding no_loops_def by auto 216qed 217 218lemma neg_next_rtrancl_trancl: 219 "\<lbrakk> \<not> m \<turnstile> y \<leadsto>\<^sup>* r; m \<turnstile> x \<leadsto> y \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>+ r" 220 apply (erule contrapos_nn) 221 apply (drule tranclD) 222 apply (clarsimp simp: next_unfold') 223 done 224 225lemma next_trancl_split_tt: 226 assumes p1: "m \<turnstile> x \<leadsto>\<^sup>+ y" 227 and p2: "m \<turnstile> x \<leadsto>\<^sup>+ p" 228 and nm: "\<not> m \<turnstile> p \<leadsto>\<^sup>* y" 229 shows "m \<turnstile> y \<leadsto>\<^sup>* p" 230 using p2 p1 nm 231proof induct 232 case base thus ?case 233 by (clarsimp dest!: tranclD) (drule (1) next_single_value, simp) 234next 235 case (step q r) 236 237 show ?case 238 proof (cases "q = y") 239 case True thus ?thesis using step 240 by fastforce 241 next 242 case False 243 have "m \<turnstile> y \<leadsto>\<^sup>* q" 244 proof (rule step.hyps) 245 have "\<not> m \<turnstile> q \<leadsto>\<^sup>+ y" 246 by (rule neg_next_rtrancl_trancl) fact+ 247 thus "\<not> m \<turnstile> q \<leadsto>\<^sup>* y" using False 248 by (clarsimp dest!: rtranclD) 249 qed fact+ 250 thus ?thesis by (rule rtrancl_into_rtrancl) fact+ 251 qed 252qed 253 254lemma no_loops_splitat_tt: 255 assumes p1: "m \<turnstile> x \<leadsto>\<^sup>+ y" 256 and p2: "m \<turnstile> x \<leadsto>\<^sup>+ p" 257 and nl: "no_loops m" 258 and r1: "\<lbrakk> m \<turnstile> p \<leadsto>\<^sup>* y; \<not> m \<turnstile> y \<leadsto>\<^sup>+ p \<rbrakk> \<Longrightarrow> P" 259 and r2: "\<lbrakk> m \<turnstile> y \<leadsto>\<^sup>* p; \<not> m \<turnstile> p \<leadsto>\<^sup>+ y \<rbrakk> \<Longrightarrow> P" 260 shows "P" 261proof (cases "m \<turnstile> p \<leadsto>\<^sup>* y") 262 case True 263 thus ?thesis 264 proof (rule r1) 265 from nl show "\<not> m \<turnstile> y \<leadsto>\<^sup>+ p" 266 proof (rule contrapos_pn) 267 assume "m \<turnstile> y \<leadsto>\<^sup>+ p" 268 hence "m \<turnstile> p \<leadsto>\<^sup>+ p" using True by simp 269 thus "\<not> no_loops m" 270 by (rule neg_no_loopsI) 271 qed 272 qed 273next 274 case False 275 276 show ?thesis 277 proof (rule r2) 278 from False show "\<not> m \<turnstile> p \<leadsto>\<^sup>+ y" 279 by (rule contrapos_nn) (erule trancl_into_rtrancl) 280 281 show "m \<turnstile> y \<leadsto>\<^sup>* p" 282 by (rule next_trancl_split_tt) fact+ 283 qed 284qed 285 286lemma no_loops_next_selfD: 287 "\<lbrakk>no_loops m; m \<turnstile> x \<leadsto> x \<rbrakk> \<Longrightarrow> False" 288 apply (clarsimp simp: next_unfold') 289 apply (drule (1) no_self_loop_next_noloop) 290 apply simp 291 done 292 293lemma no_loops_upd_last: 294 assumes noloop: "no_loops m" 295 and nxt: "m \<turnstile> x \<leadsto>\<^sup>+ p" 296 shows "m (p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ p" 297proof - 298 from noloop nxt have xp: "x \<noteq> p" 299 by (clarsimp dest!: neg_no_loopsI) 300 301 from nxt show ?thesis using xp 302 proof (induct rule: converse_trancl_induct') 303 case (base y) 304 hence "m (p \<mapsto> cte) \<turnstile> y \<leadsto> p" using noloop 305 by (auto simp add: mdb_next_update dest!: no_loops_next_selfD) 306 thus ?case .. 307 next 308 case (step y z) 309 310 from noloop step have xp: "z \<noteq> p" 311 by (clarsimp dest!: neg_no_loopsI) 312 313 hence "m (p \<mapsto> cte) \<turnstile> y \<leadsto> z" using step 314 by (simp add: mdb_next_update) 315 316 moreover from xp have "m (p \<mapsto> cte) \<turnstile> z \<leadsto>\<^sup>+ p" using step.hyps assms 317 by (auto simp del: fun_upd_apply) 318 ultimately show ?case by (rule trancl_into_trancl2) 319 qed 320qed 321 322 323lemma no_0_neq [intro?]: 324 "\<lbrakk>m c = Some cte; no_0 m\<rbrakk> \<Longrightarrow> c \<noteq> 0" 325 by (auto simp add: no_0_def) 326 327lemma no_0_update: 328 assumes no0: "no_0 m" 329 and pnz: "p \<noteq> 0" 330 shows "no_0 (m(p \<mapsto> cte))" 331 using no0 pnz unfolding no_0_def by simp 332 333lemma has_loop_update: 334 assumes lp: "m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ c'" 335 and cn0: "c' \<noteq> 0" 336 and mnext: "mdbNext (cteMDBNode cte) = 0" 337 and mn0: "no_0 m" 338 and pn0: "p \<noteq> 0" 339 shows "m \<turnstile> c \<leadsto>\<^sup>+ c'" 340 using lp cn0 341proof induct 342 case (base y) 343 have "m \<turnstile> c \<leadsto> y" 344 proof (rule mdb_next_update_other) 345 show "p \<noteq> c" using base 346 by (clarsimp intro: contrapos_nn simp: mdb_next_update mnext) 347 qed fact+ 348 349 thus ?case .. 350next 351 case (step y z) 352 353 show ?case 354 proof 355 have "y \<noteq> 0" by (rule no_0_lhs [OF _ no_0_update]) fact+ 356 thus "m \<turnstile> c \<leadsto>\<^sup>+ y" using step by simp 357 next 358 have "z \<noteq> 0" by fact+ 359 hence "p \<noteq> y" using step.hyps mnext 360 by (clarsimp simp: mdb_next_update) 361 thus "m \<turnstile> y \<leadsto> z" 362 by (rule mdb_next_update_other [OF step.hyps(2)]) 363 qed 364qed 365 366lemma mdb_rtrancl_update_other: 367 assumes upd: "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y" 368 and nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p" 369 shows "m \<turnstile> x \<leadsto>\<^sup>* y" 370 using upd 371proof (cases rule: next_rtrancl_tranclE) 372 case eq thus ?thesis by simp 373next 374 case trancl thus ?thesis 375 by (auto intro: trancl_into_rtrancl elim: mdb_trancl_update_other [OF _ nopath]) 376qed 377 378lemma mdb_trancl_other_update: 379 assumes upd: "m \<turnstile> x \<leadsto>\<^sup>+ y" 380 and np: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p" 381 shows "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ y" 382 using upd 383proof induct 384 case (base q) 385 from np have "x \<noteq> p" by clarsimp 386 hence"m (p \<mapsto> cte) \<turnstile> x \<leadsto> q" 387 using base by (simp add: mdb_next_update del: fun_upd_apply) 388 thus ?case .. 389next 390 case (step q r) 391 392 show ?case 393 proof 394 from step.hyps(1) np have "q \<noteq> p" 395 by (auto elim!: contrapos_nn) 396 397 thus x: "m(p \<mapsto> cte) \<turnstile> q \<leadsto> r" 398 using step by (simp add: mdb_next_update del: fun_upd_apply) 399 qed fact+ 400qed 401 402lemma mdb_rtrancl_other_update: 403 assumes upd: "m \<turnstile> x \<leadsto>\<^sup>* y" 404 and nopath: "\<not> m \<turnstile> x \<leadsto>\<^sup>* p" 405 shows "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* y" 406 using upd 407proof (cases rule: next_rtrancl_tranclE) 408 case eq thus ?thesis by simp 409next 410 case trancl thus ?thesis 411 by (auto intro: trancl_into_rtrancl elim: mdb_trancl_other_update [OF _ nopath]) 412qed 413 414lemma mdb_chain_0_update: 415 assumes x: "m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0" 416 and np: "\<not> m \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* p" 417 assumes p: "p \<noteq> 0" 418 assumes 0: "no_0 m" 419 assumes n: "mdb_chain_0 m" 420 shows "mdb_chain_0 (m(p \<mapsto> cte))" 421 unfolding mdb_chain_0_def 422proof rule 423 fix x 424 assume "x \<in> dom (m(p \<mapsto> cte))" 425 hence x: "x = p \<or> x \<in> dom m" by simp 426 427 have cnxt: "m(p \<mapsto> cte) \<turnstile> mdbNext (cteMDBNode cte) \<leadsto>\<^sup>* 0" 428 by (rule mdb_rtrancl_other_update) fact+ 429 430 from x show "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>+ 0" 431 proof 432 assume xp: "x = p" 433 show ?thesis 434 proof (rule rtrancl_into_trancl2 [OF _ cnxt]) 435 show "m(p \<mapsto> cte) \<turnstile> x \<leadsto> mdbNext (cteMDBNode cte)" using xp 436 by (simp add: mdb_next_update) 437 qed 438 next 439 assume x: "x \<in> dom m" 440 441 show ?thesis 442 proof (cases "m \<turnstile> x \<leadsto>\<^sup>* p") 443 case False 444 from n have "m \<turnstile> x \<leadsto>\<^sup>+ 0" 445 unfolding mdb_chain_0_def 446 using x by auto 447 448 thus ?thesis 449 by (rule mdb_trancl_other_update) fact+ 450 next 451 case True 452 hence "m(p \<mapsto> cte) \<turnstile> x \<leadsto>\<^sup>* p" 453 proof (cases rule: next_rtrancl_tranclE) 454 case eq thus ?thesis by simp 455 next 456 case trancl 457 have "no_loops m" by (rule mdb_chain_0_no_loops) fact+ 458 thus ?thesis 459 by (rule trancl_into_rtrancl [OF no_loops_upd_last]) fact+ 460 qed 461 moreover 462 have "m(p \<mapsto> cte) \<turnstile> p \<leadsto> mdbNext (cteMDBNode cte)" by (simp add: mdb_next_update) 463 ultimately show ?thesis using cnxt by simp 464 qed 465 qed 466qed 467 468lemma mdb_chain_0_update_0: 469 assumes x: "mdbNext (cteMDBNode cte) = 0" 470 assumes p: "p \<noteq> 0" 471 assumes 0: "no_0 m" 472 assumes n: "mdb_chain_0 m" 473 shows "mdb_chain_0 (m(p \<mapsto> cte))" 474 using x 0 p 475 apply - 476 apply (rule mdb_chain_0_update [OF _ _ p 0 n]) 477 apply (auto elim: next_rtrancl_tranclE dest: no_0_lhs_trancl) 478 done 479 480lemma no_loops_0_update: 481 assumes x: "mdbNext (cteMDBNode cte) = 0" 482 assumes p: "p \<noteq> 0" 483 assumes 0: "no_0 m" 484 assumes n: "no_loops m" 485 shows "no_loops (m(p \<mapsto> cte))" 486 unfolding no_loops_def 487proof (rule, rule contrapos_pn [OF n], rule neg_no_loopsI) 488 fix c 489 assume lp: "m(p \<mapsto> cte) \<turnstile> c \<leadsto>\<^sup>+ c" 490 thus "m \<turnstile> c \<leadsto>\<^sup>+ c" 491 proof (rule has_loop_update) 492 from lp show "c \<noteq> 0" by (rule no_0_lhs_trancl [OF _ no_0_update]) fact+ 493 qed fact+ 494qed 495 496lemma valid_badges_0_update: 497 assumes nx: "mdbNext (cteMDBNode cte) = 0" 498 assumes pv: "mdbPrev (cteMDBNode cte) = 0" 499 assumes p: "m p = Some cte'" 500 assumes m: "no_mdb cte'" 501 assumes 0: "no_0 m" 502 assumes d: "valid_dlist m" 503 assumes v: "valid_badges m" 504 shows "valid_badges (m(p \<mapsto> cte))" 505proof (unfold valid_badges_def, clarify) 506 fix c c' cap cap' n n' 507 assume c: "(m(p \<mapsto> cte)) c = Some (CTE cap n)" 508 assume c': "(m(p \<mapsto> cte)) c' = Some (CTE cap' n')" 509 assume nxt: "m(p \<mapsto> cte) \<turnstile> c \<leadsto> c'" 510 assume r: "sameRegionAs cap cap'" 511 512 from p 0 have p0: "p \<noteq> 0" by (clarsimp simp: no_0_def) 513 514 from c' p0 0 515 have "c' \<noteq> 0" by (clarsimp simp: no_0_def) 516 with nx nxt 517 have cp: "c \<noteq> p" by (clarsimp simp add: mdb_next_unfold) 518 moreover 519 from pv nx nxt p p0 c d m 0 520 have "c' \<noteq> p" 521 apply clarsimp 522 apply (simp add: mdb_next_unfold split: if_split_asm) 523 apply (erule (1) valid_dlistEn, simp) 524 apply (clarsimp simp: no_mdb_def no_0_def) 525 done 526 moreover 527 with nxt c c' cp 528 have "m \<turnstile> c \<leadsto> c'" by (simp add: mdb_next_unfold) 529 ultimately 530 show "(isEndpointCap cap \<longrightarrow> 531 capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> 532 capEPBadge cap' \<noteq> 0 \<longrightarrow> 533 mdbFirstBadged n') \<and> 534 (isNotificationCap cap \<longrightarrow> 535 capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> 536 capNtfnBadge cap' \<noteq> 0 \<longrightarrow> 537 mdbFirstBadged n')" 538 using r c c' v by (fastforce simp: valid_badges_def) 539qed 540 541definition 542 "caps_no_overlap' m S \<equiv> 543 \<forall>p c n. m p = Some (CTE c n) \<longrightarrow> capRange c \<inter> S = {}" 544 545definition 546 fresh_virt_cap_class :: "capclass \<Rightarrow> cte_heap \<Rightarrow> bool" 547where 548 "fresh_virt_cap_class C m \<equiv> 549 C \<noteq> PhysicalClass \<longrightarrow> C \<notin> (capClass \<circ> cteCap) ` ran m" 550 551lemma fresh_virt_cap_class_Physical[simp]: 552 "fresh_virt_cap_class PhysicalClass = \<top>" 553 by (rule ext, simp add: fresh_virt_cap_class_def)+ 554 555lemma fresh_virt_cap_classD: 556 "\<lbrakk> m x = Some cte; fresh_virt_cap_class C m \<rbrakk> 557 \<Longrightarrow> C \<noteq> PhysicalClass \<longrightarrow> capClass (cteCap cte) \<noteq> C" 558 by (auto simp: fresh_virt_cap_class_def) 559 560lemma capRange_untyped: 561 "capRange cap' \<inter> untypedRange cap \<noteq> {} \<Longrightarrow> isUntypedCap cap" 562 by (cases cap, auto simp: isCap_simps) 563 564lemma capRange_of_untyped [simp]: 565 "capRange (UntypedCap d r n f) = untypedRange (UntypedCap d r n f)" 566 by (simp add: capRange_def isCap_simps capUntypedSize_def) 567 568lemma caps_contained_no_overlap: 569 "\<lbrakk> caps_no_overlap' m (capRange cap); caps_contained' m\<rbrakk> 570 \<Longrightarrow> caps_contained' (m(p \<mapsto> CTE cap n))" 571 apply (clarsimp simp add: caps_contained'_def) 572 apply (rule conjI) 573 apply clarsimp 574 apply (rule conjI, clarsimp dest!: capRange_untyped) 575 apply clarsimp 576 apply (simp add: caps_no_overlap'_def) 577 apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) 578 apply (frule capRange_untyped) 579 apply (clarsimp simp add: isCap_simps) 580 apply clarsimp 581 apply (simp add: caps_no_overlap'_def) 582 apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) 583 apply (frule capRange_untyped) 584 apply (clarsimp simp: isCap_simps) 585 apply blast 586 done 587 588lemma no_mdb_next: 589 "\<lbrakk> m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto> p" 590 apply clarsimp 591 apply (frule vdlist_nextD0) 592 apply clarsimp 593 apply assumption 594 apply (clarsimp simp: mdb_prev_def no_mdb_def mdb_next_unfold) 595 done 596 597lemma no_mdb_rtrancl: 598 "\<lbrakk> m p = Some cte; no_mdb cte; p \<noteq> x; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> x \<leadsto>\<^sup>* p" 599 apply (clarsimp dest!: rtranclD) 600 apply (drule tranclD2) 601 apply clarsimp 602 apply (drule (3) no_mdb_next) 603 apply fastforce 604 done 605 606lemma isNullCap [simp]: 607 "isNullCap cap = (cap = NullCap)" 608 by (simp add: isCap_simps) 609 610lemma isDomainCap [simp]: 611 "isDomainCap cap = (cap = DomainCap)" 612 by (simp add: isCap_simps) 613 614lemma isPhysicalCap[simp]: 615 "isPhysicalCap cap = (capClass cap = PhysicalClass)" 616 by (simp add: isPhysicalCap_def ARM_H.isPhysicalCap_def 617 split: capability.split arch_capability.split) 618 619definition 620 capMasterCap :: "capability \<Rightarrow> capability" 621where 622 "capMasterCap cap \<equiv> case cap of 623 EndpointCap ref bdg s r g \<Rightarrow> EndpointCap ref 0 True True True 624 | NotificationCap ref bdg s r \<Rightarrow> NotificationCap ref 0 True True 625 | CNodeCap ref bits gd gs \<Rightarrow> CNodeCap ref bits 0 0 626 | ThreadCap ref \<Rightarrow> ThreadCap ref 627 | ReplyCap ref master \<Rightarrow> ReplyCap ref True 628 | UntypedCap d ref n f \<Rightarrow> UntypedCap d ref n 0 629 | ArchObjectCap acap \<Rightarrow> ArchObjectCap (case acap of 630 PageCap d ref rghts sz mapdata \<Rightarrow> 631 PageCap d ref VMReadWrite sz None 632 | ASIDPoolCap pool asid \<Rightarrow> 633 ASIDPoolCap pool 0 634 | PageTableCap ptr data \<Rightarrow> 635 PageTableCap ptr None 636 | PageDirectoryCap ptr data \<Rightarrow> 637 PageDirectoryCap ptr None 638 | _ \<Rightarrow> acap) 639 | _ \<Rightarrow> cap" 640 641lemma capMasterCap_simps[simp]: 642 "capMasterCap (EndpointCap ref bdg s r g) = EndpointCap ref 0 True True True" 643 "capMasterCap (NotificationCap ref bdg s r) = NotificationCap ref 0 True True" 644 "capMasterCap (CNodeCap ref bits gd gs) = CNodeCap ref bits 0 0" 645 "capMasterCap (ThreadCap ref) = ThreadCap ref" 646 "capMasterCap capability.NullCap = capability.NullCap" 647 "capMasterCap capability.DomainCap = capability.DomainCap" 648 "capMasterCap (capability.IRQHandlerCap irq) = capability.IRQHandlerCap irq" 649 "capMasterCap (capability.Zombie word zombie_type n) = capability.Zombie word zombie_type n" 650 "capMasterCap (capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 word2)) = 651 capability.ArchObjectCap (arch_capability.ASIDPoolCap word1 0)" 652 "capMasterCap (capability.ArchObjectCap arch_capability.ASIDControlCap) = 653 capability.ArchObjectCap arch_capability.ASIDControlCap" 654 "capMasterCap (capability.ArchObjectCap (arch_capability.PageCap d word vmrights vmpage_size pdata)) = 655 capability.ArchObjectCap (arch_capability.PageCap d word VMReadWrite vmpage_size None)" 656 "capMasterCap (capability.ArchObjectCap (arch_capability.PageTableCap word ptdata)) = 657 capability.ArchObjectCap (arch_capability.PageTableCap word None)" 658 "capMasterCap (capability.ArchObjectCap (arch_capability.PageDirectoryCap word pddata)) = 659 capability.ArchObjectCap (arch_capability.PageDirectoryCap word None)" 660 "capMasterCap (capability.UntypedCap d word n f) = capability.UntypedCap d word n 0" 661 "capMasterCap capability.IRQControlCap = capability.IRQControlCap" 662 "capMasterCap (capability.ReplyCap word m) = capability.ReplyCap word True" 663 by (simp_all add: capMasterCap_def) 664 665lemma capMasterCap_eqDs1: 666 "capMasterCap cap = EndpointCap ref bdg s r g 667 \<Longrightarrow> bdg = 0 \<and> s \<and> r \<and> g 668 \<and> (\<exists>bdg s r g. cap = EndpointCap ref bdg s r g)" 669 "capMasterCap cap = NotificationCap ref bdg s r 670 \<Longrightarrow> bdg = 0 \<and> s \<and> r 671 \<and> (\<exists>bdg s r. cap = NotificationCap ref bdg s r)" 672 "capMasterCap cap = CNodeCap ref bits gd gs 673 \<Longrightarrow> gd = 0 \<and> gs = 0 \<and> (\<exists>gd gs. cap = CNodeCap ref bits gd gs)" 674 "capMasterCap cap = ThreadCap ref 675 \<Longrightarrow> cap = ThreadCap ref" 676 "capMasterCap cap = NullCap 677 \<Longrightarrow> cap = NullCap" 678 "capMasterCap cap = DomainCap 679 \<Longrightarrow> cap = DomainCap" 680 "capMasterCap cap = IRQControlCap 681 \<Longrightarrow> cap = IRQControlCap" 682 "capMasterCap cap = IRQHandlerCap irq 683 \<Longrightarrow> cap = IRQHandlerCap irq" 684 "capMasterCap cap = Zombie ref tp n 685 \<Longrightarrow> cap = Zombie ref tp n" 686 "capMasterCap cap = UntypedCap d ref bits 0 687 \<Longrightarrow> \<exists>f. cap = UntypedCap d ref bits f" 688 "capMasterCap cap = ReplyCap ref master 689 \<Longrightarrow> \<exists>master. cap = ReplyCap ref master" 690 "capMasterCap cap = ArchObjectCap (PageCap d ref rghts sz mapdata) 691 \<Longrightarrow> rghts = VMReadWrite \<and> mapdata = None 692 \<and> (\<exists>rghts mapdata. cap = ArchObjectCap (PageCap d ref rghts sz mapdata))" 693 "capMasterCap cap = ArchObjectCap ASIDControlCap 694 \<Longrightarrow> cap = ArchObjectCap ASIDControlCap" 695 "capMasterCap cap = ArchObjectCap (ASIDPoolCap pool asid) 696 \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = ArchObjectCap (ASIDPoolCap pool asid))" 697 "capMasterCap cap = ArchObjectCap (PageTableCap ptr data) 698 \<Longrightarrow> data = None \<and> (\<exists>data. cap = ArchObjectCap (PageTableCap ptr data))" 699 "capMasterCap cap = ArchObjectCap (PageDirectoryCap ptr data2) 700 \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = ArchObjectCap (PageDirectoryCap ptr data2))" 701 by (clarsimp simp: capMasterCap_def 702 split: capability.split_asm arch_capability.split_asm)+ 703 704lemmas capMasterCap_eqDs[dest!] = capMasterCap_eqDs1 capMasterCap_eqDs1 [OF sym] 705 706definition 707 capBadge :: "capability \<Rightarrow> word32 option" 708where 709 "capBadge cap \<equiv> if isEndpointCap cap then Some (capEPBadge cap) 710 else if isNotificationCap cap then Some (capNtfnBadge cap) 711 else None" 712 713lemma capBadge_simps[simp]: 714 "capBadge (UntypedCap d p n f) = None" 715 "capBadge (NullCap) = None" 716 "capBadge (DomainCap) = None" 717 "capBadge (EndpointCap ref badge s r w) = Some badge" 718 "capBadge (NotificationCap ref badge s r) = Some badge" 719 "capBadge (CNodeCap ref bits gd gs) = None" 720 "capBadge (ThreadCap ref) = None" 721 "capBadge (Zombie ref b n) = None" 722 "capBadge (ArchObjectCap cap) = None" 723 "capBadge (IRQControlCap) = None" 724 "capBadge (IRQHandlerCap irq) = None" 725 "capBadge (ReplyCap tcb master) = None" 726 by (simp add: capBadge_def isCap_defs)+ 727 728lemma capClass_Master: 729 "capClass (capMasterCap cap) = capClass cap" 730 by (simp add: capMasterCap_def split: capability.split arch_capability.split) 731 732lemma capRange_Master: 733 "capRange (capMasterCap cap) = capRange cap" 734 by (simp add: capMasterCap_def split: capability.split arch_capability.split, 735 simp add: capRange_def) 736 737lemma master_eqI: 738 "\<lbrakk> \<And>cap. F (capMasterCap cap) = F cap; F (capMasterCap cap) = F (capMasterCap cap') \<rbrakk> 739 \<Longrightarrow> F cap = F cap'" 740 by simp 741 742lemma isCap_Master: 743 "isZombie (capMasterCap cap) = isZombie cap" 744 "isArchObjectCap (capMasterCap cap) = isArchObjectCap cap" 745 "isThreadCap (capMasterCap cap) = isThreadCap cap" 746 "isCNodeCap (capMasterCap cap) = isCNodeCap cap" 747 "isNotificationCap (capMasterCap cap) = isNotificationCap cap" 748 "isEndpointCap (capMasterCap cap) = isEndpointCap cap" 749 "isUntypedCap (capMasterCap cap) = isUntypedCap cap" 750 "isReplyCap (capMasterCap cap) = isReplyCap cap" 751 "isIRQControlCap (capMasterCap cap) = isIRQControlCap cap" 752 "isIRQHandlerCap (capMasterCap cap) = isIRQHandlerCap cap" 753 "isNullCap (capMasterCap cap) = isNullCap cap" 754 "isDomainCap (capMasterCap cap) = isDomainCap cap" 755 "isArchPageCap (capMasterCap cap) = isArchPageCap cap" 756 by (simp add: isCap_simps capMasterCap_def 757 split: capability.split arch_capability.split)+ 758 759lemma capUntypedSize_capBits: 760 "capClass cap = PhysicalClass \<Longrightarrow> capUntypedSize cap = 2 ^ (capBits cap)" 761 apply (simp add: capUntypedSize_def objBits_simps 762 ARM_H.capUntypedSize_def 763 pteBits_def pdeBits_def 764 ptBits_def pdBits_def 765 split: capability.splits arch_capability.splits 766 zombie_type.splits) 767 apply fastforce 768 done 769 770lemma sameRegionAs_def2: 771 "sameRegionAs cap cap' = (\<lambda>cap cap'. 772 (cap = cap' 773 \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap 774 \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap) 775 \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap' 776 \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap')) 777 \<or> (capRange cap' \<noteq> {} \<and> capRange cap' \<subseteq> capRange cap 778 \<and> (isUntypedCap cap \<or> (isArchPageCap cap \<and> isArchPageCap cap'))) 779 \<or> (isIRQControlCap cap \<and> isIRQHandlerCap cap')) 780 (capMasterCap cap) (capMasterCap cap')" 781 apply (cases "isUntypedCap cap") 782 apply (clarsimp simp: sameRegionAs_def Let_def 783 isCap_Master capRange_Master capClass_Master) 784 apply (clarsimp simp: isCap_simps 785 capMasterCap_def[where cap="UntypedCap d p n f" for d p n f]) 786 apply (simp add: capRange_def capUntypedSize_capBits) 787 apply (intro impI iffI) 788 apply (clarsimp del: subsetI intro!: range_subsetI) 789 apply clarsimp 790 apply (simp add: range_subset_eq2) 791 apply (simp cong: conj_cong) 792 apply (simp add: capMasterCap_def sameRegionAs_def isArchPageCap_def 793 split: capability.split 794 split del: if_split cong: if_cong) 795 apply (simp add: ARM_H.sameRegionAs_def isCap_simps 796 split: arch_capability.split 797 split del: if_split cong: if_cong) 798 apply (clarsimp simp: capRange_def Let_def) 799 apply (simp add: range_subset_eq2 cong: conj_cong) 800 by (simp add: conj_comms) 801 802lemma sameObjectAs_def2: 803 "sameObjectAs cap cap' = (\<lambda>cap cap'. 804 (cap = cap' 805 \<and> (\<not> isNullCap cap \<and> \<not> isZombie cap 806 \<and> \<not> isUntypedCap cap) 807 \<and> (\<not> isNullCap cap' \<and> \<not> isZombie cap' 808 \<and> \<not> isUntypedCap cap') 809 \<and> (isArchPageCap cap \<longrightarrow> capRange cap \<noteq> {}) 810 \<and> (isArchPageCap cap' \<longrightarrow> capRange cap' \<noteq> {}))) 811 (capMasterCap cap) (capMasterCap cap')" 812 apply (simp add: sameObjectAs_def sameRegionAs_def2 813 isCap_simps capMasterCap_def 814 split: capability.split) 815 apply (clarsimp simp: ARM_H.sameObjectAs_def isCap_simps 816 split: arch_capability.split cong: if_cong) 817 apply (clarsimp simp: ARM_H.sameRegionAs_def isCap_simps 818 split del: if_split cong: if_cong) 819 apply (simp add: capRange_def) 820 apply fastforce 821 done 822 823lemmas sameRegionAs_def3 = 824 sameRegionAs_def2 [simplified capClass_Master capRange_Master isCap_Master] 825 826lemmas sameObjectAs_def3 = 827 sameObjectAs_def2 [simplified capClass_Master capRange_Master isCap_Master] 828 829lemma sameRegionAsE: 830 "\<lbrakk> sameRegionAs cap cap'; 831 \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; 832 \<not> isUntypedCap cap; \<not> isArchPageCap cap \<rbrakk> \<Longrightarrow> R; 833 \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isUntypedCap cap \<rbrakk> \<Longrightarrow> R; 834 \<lbrakk> capRange cap' \<noteq> {}; capRange cap' \<subseteq> capRange cap; isArchPageCap cap; 835 isArchPageCap cap' \<rbrakk> \<Longrightarrow> R; 836 \<lbrakk> isIRQControlCap cap; isIRQHandlerCap cap' \<rbrakk> \<Longrightarrow> R 837 \<rbrakk> \<Longrightarrow> R" 838 by (simp add: sameRegionAs_def3, fastforce) 839 840lemma sameObjectAsE: 841 "\<lbrakk> sameObjectAs cap cap'; 842 \<lbrakk> capMasterCap cap = capMasterCap cap'; \<not> isNullCap cap; \<not> isZombie cap; 843 \<not> isUntypedCap cap; 844 isArchPageCap cap \<Longrightarrow> capRange cap \<noteq> {} \<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 845 by (clarsimp simp add: sameObjectAs_def3) 846 847lemma sameObjectAs_sameRegionAs: 848 "sameObjectAs cap cap' \<Longrightarrow> sameRegionAs cap cap'" 849 by (clarsimp simp add: sameObjectAs_def2 sameRegionAs_def2) 850 851lemma sameObjectAs_sym: 852 "sameObjectAs c d = sameObjectAs d c" 853 by (simp add: sameObjectAs_def2 eq_commute conj_comms) 854 855lemma untypedRange_Master: 856 "untypedRange (capMasterCap cap) = untypedRange cap" 857 by (simp add: capMasterCap_def split: capability.split) 858 859lemma sameObject_untypedRange: 860 "sameObjectAs cap cap' \<Longrightarrow> untypedRange cap' = untypedRange cap" 861 apply (rule master_eqI, rule untypedRange_Master) 862 apply (clarsimp simp: sameObjectAs_def2) 863 done 864 865lemma sameObject_untypedCap: 866 "sameObjectAs cap cap' \<Longrightarrow> isUntypedCap cap' = isUntypedCap cap" 867 apply (rule master_eqI, rule isCap_Master) 868 apply (clarsimp simp: sameObjectAs_def2) 869 done 870 871lemma sameObject_capRange: 872 "sameObjectAs cap cap' \<Longrightarrow> capRange cap' = capRange cap" 873 apply (rule master_eqI, rule capRange_Master) 874 apply (clarsimp simp: sameObjectAs_def2) 875 done 876 877lemma sameRegionAs_Null [simp]: 878 "sameRegionAs c NullCap = False" 879 "sameRegionAs NullCap c = False" 880 by (simp add: sameRegionAs_def3 capRange_def isCap_simps)+ 881 882lemma isMDBParent_Null [simp]: 883 "isMDBParentOf c (CTE NullCap m) = False" 884 "isMDBParentOf (CTE NullCap m) c = False" 885 unfolding isMDBParentOf_def by (auto split: cte.splits) 886 887lemma capUntypedSize_simps [simp]: 888 "capUntypedSize (ThreadCap r) = 1 << objBits (undefined::tcb)" 889 "capUntypedSize (NotificationCap r badge a b) = 1 << objBits (undefined::Structures_H.notification)" 890 "capUntypedSize (EndpointCap r badge a b c) = 1 << objBits (undefined::endpoint)" 891 "capUntypedSize (Zombie r zs n) = 1 << (zBits zs)" 892 "capUntypedSize NullCap = 0" 893 "capUntypedSize DomainCap = 1" 894 "capUntypedSize (ArchObjectCap x) = Arch.capUntypedSize x" 895 "capUntypedSize (UntypedCap d r n f) = 1 << n" 896 "capUntypedSize (CNodeCap r n g n2) = 1 << (objBits (undefined::cte) + n)" 897 "capUntypedSize (ReplyCap r m) = 1 << objBits (undefined :: tcb)" 898 "capUntypedSize IRQControlCap = 1" 899 "capUntypedSize (IRQHandlerCap irq) = 1" 900 by (auto simp add: capUntypedSize_def isCap_simps objBits_simps 901 split: zombie_type.splits) 902 903lemma sameRegionAs_classes: 904 "\<lbrakk> sameRegionAs cap cap' \<rbrakk> \<Longrightarrow> capClass cap = capClass cap'" 905 apply (erule sameRegionAsE) 906 apply (rule master_eqI, rule capClass_Master) 907 apply simp 908 apply (simp add: capRange_def split: if_split_asm) 909 apply (clarsimp simp: isCap_simps) 910 apply (clarsimp simp: isCap_simps) 911 done 912 913lemma sameRegionAs_capRange: 914 "\<lbrakk> sameRegionAs cap cap'; 915 \<not> isUntypedCap cap; \<not> isArchPageCap cap \<rbrakk> 916 \<Longrightarrow> capRange cap = capRange cap'" 917 apply (rule master_eqI, rule capRange_Master) 918 apply (erule sameRegionAsE, simp_all) 919 apply (clarsimp simp: isCap_simps) 920 apply (simp add: capRange_def capMasterCap_def) 921 done 922 923lemma capAligned_capUntypedPtr: 924 "\<lbrakk> capAligned cap; capClass cap = PhysicalClass \<rbrakk> \<Longrightarrow> 925 capUntypedPtr cap \<in> capRange cap" 926 by (simp add: capRange_def capAligned_def is_aligned_no_overflow) 927 928lemma sameRegionAs_capRange_Int: 929 "\<lbrakk> sameRegionAs cap cap'; capClass cap = PhysicalClass \<or> capClass cap' = PhysicalClass; 930 capAligned cap; capAligned cap' \<rbrakk> 931 \<Longrightarrow> capRange cap' \<inter> capRange cap \<noteq> {}" 932 apply (frule sameRegionAs_classes, simp) 933 apply (drule(1) capAligned_capUntypedPtr)+ 934 apply (erule sameRegionAsE) 935 apply (subgoal_tac "capRange (capMasterCap cap') \<inter> capRange (capMasterCap cap) \<noteq> {}") 936 apply (simp(no_asm_use) add: capRange_Master) 937 apply (clarsimp simp: capRange_Master) 938 apply blast 939 apply blast 940 apply (clarsimp simp: isCap_simps) 941 done 942 943lemma sameRegionAs_trans: 944 "\<lbrakk> sameRegionAs a b; sameRegionAs b c \<rbrakk> \<Longrightarrow> sameRegionAs a c" 945 apply (simp add: sameRegionAs_def2, elim conjE disjE, simp_all) 946 apply (auto simp: isCap_simps) 947 apply (auto simp: capRange_def) 948 done 949 950lemma capMasterCap_maskCapRights[simp]: 951 "capMasterCap (maskCapRights msk cap) 952 = capMasterCap cap" 953 apply (cases cap; 954 simp add: maskCapRights_def Let_def isCap_simps capMasterCap_def) 955 apply (rename_tac arch_capability) 956 apply (case_tac arch_capability; 957 simp add: ARM_H.maskCapRights_def Let_def isCap_simps) 958 done 959 960lemma capBadge_maskCapRights[simp]: 961 "capBadge (maskCapRights msk cap) 962 = capBadge cap" 963 apply (cases cap; 964 simp add: maskCapRights_def Let_def isCap_simps capBadge_def) 965 apply (rename_tac arch_capability) 966 apply (case_tac arch_capability; 967 simp add: ARM_H.maskCapRights_def Let_def isCap_simps) 968 done 969 970lemma maskCapRights_region [simp]: 971 "sameRegionAs (maskCapRights R cap) cap' = sameRegionAs cap cap'" 972 by (simp add: sameRegionAs_def2) 973 974lemma sameRegionAs_mask2 [simp]: 975 "sameRegionAs cap (maskCapRights R cap') = sameRegionAs cap cap'" 976 by (simp add: sameRegionAs_def2) 977 978lemma getObject_cte_det: 979 "(r::cte,s') \<in> fst (getObject p s) \<Longrightarrow> fst (getObject p s) = {(r,s)} \<and> s' = s" 980 apply (clarsimp simp add: getObject_def bind_def get_def gets_def 981 return_def loadObject_cte split_def) 982 apply (clarsimp split: kernel_object.split_asm if_split_asm option.split_asm 983 simp: in_monad typeError_def alignError_def magnitudeCheck_def) 984 apply (simp_all add: bind_def return_def assert_opt_def split_def 985 alignCheck_def is_aligned_mask[symmetric] 986 unless_def when_def magnitudeCheck_def) 987 done 988 989lemma cte_wp_at_obj_cases': 990 "cte_wp_at' P p s = 991 (obj_at' P p s \<or> (\<exists>n \<in> dom tcb_cte_cases. obj_at' (P \<circ> (fst (the (tcb_cte_cases n)))) (p - n) s))" 992 apply (simp add: cte_wp_at_cases' obj_at'_def) 993 apply (rule iffI) 994 apply (erule disjEI 995 | clarsimp simp: objBits_simps' cte_level_bits_def projectKOs 996 | rule rev_bexI, erule domI)+ 997 apply fastforce 998 done 999 1000lemma cte_wp_at_valid_objs_valid_cap': 1001 "\<lbrakk> cte_wp_at' P p s; valid_objs' s \<rbrakk> \<Longrightarrow> \<exists>cte. P cte \<and> s \<turnstile>' (cteCap cte)" 1002 apply (simp add: cte_wp_at_obj_cases') 1003 apply (elim disjE bexE conjE) 1004 apply (drule(1) obj_at_valid_objs') 1005 apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def) 1006 apply (drule(1) obj_at_valid_objs') 1007 apply (clarsimp simp: projectKOs valid_obj'_def valid_cte'_def valid_tcb'_def) 1008 apply (fastforce dest: bspec [OF _ ranI]) 1009 done 1010 1011lemma getCTE_valid_cap: 1012 "\<lbrace>valid_objs'\<rbrace> getCTE t \<lbrace>\<lambda>cte s. s \<turnstile>' (cteCap cte) \<and> cte_at' t s\<rbrace>" 1013 apply (clarsimp simp add: getCTE_def valid_def) 1014 apply (frule in_inv_by_hoareD [OF getObject_cte_inv], clarsimp) 1015 apply (subst conj_commute) 1016 apply (subgoal_tac "cte_wp_at' ((=) a) t s") 1017 apply (rule conjI) 1018 apply (clarsimp elim!: cte_wp_at_weakenE') 1019 apply (drule(1) cte_wp_at_valid_objs_valid_cap') 1020 apply clarsimp 1021 apply (drule getObject_cte_det) 1022 apply (simp add: cte_wp_at'_def) 1023 done 1024 1025lemmas getCTE_valid_cap' [wp] = 1026 getCTE_valid_cap [THEN hoare_conjD1 [unfolded pred_conj_def]] 1027 1028lemma ctes_of_valid_cap': 1029 "\<lbrakk> ctes_of s p = Some (CTE c n); valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' c" 1030 apply (rule cte_wp_at_valid_objs_valid_cap'[where P="(=) (CTE c n)", simplified]) 1031 apply (simp add: cte_wp_at_ctes_of) 1032 apply assumption 1033 done 1034 1035lemma valid_capAligned: 1036 "valid_cap' c s \<Longrightarrow> capAligned c" 1037 by (simp add: valid_cap'_def) 1038 1039lemma capUntypedSize_range: 1040 "\<lbrakk> capAligned cap; capClass cap = PhysicalClass \<rbrakk> \<Longrightarrow> 1041 {capUntypedPtr cap .. capUntypedPtr cap + capUntypedSize cap - 1} 1042 \<subseteq> {capUntypedPtr cap .. capUntypedPtr cap + 2 ^ capBits cap - 1}" 1043 apply (rule range_subsetI) 1044 apply simp 1045 apply (clarsimp simp add: capAligned_def) 1046 apply (erule is_aligned_get_word_bits) 1047 apply (simp add: capUntypedSize_def ARM_H.capUntypedSize_def objBits_simps 1048 isCap_simps 1049 split: capability.splits arch_capability.split 1050 zombie_type.splits) 1051 apply (auto simp: is_aligned_no_overflow objBits_simps word_bits_def 1052 ptBits_def pteBits_def 1053 pdBits_def pdeBits_def) 1054 done 1055 1056lemma caps_no_overlap'_no_region: 1057 "\<lbrakk> caps_no_overlap' m (capRange cap); valid_objs' s; 1058 m = ctes_of s; s \<turnstile>' cap; fresh_virt_cap_class (capClass cap) m \<rbrakk> \<Longrightarrow> 1059 \<forall>c n p. m p = Some (CTE c n) \<longrightarrow> 1060 \<not> sameRegionAs c cap \<and> \<not> sameRegionAs cap c" 1061 apply (clarsimp simp add: caps_no_overlap'_def) 1062 apply (erule allE)+ 1063 apply (erule impE, erule exI) 1064 apply (frule (1) ctes_of_valid_cap') 1065 apply (drule valid_capAligned)+ 1066 apply (case_tac "capClass cap = PhysicalClass") 1067 apply (auto dest: sameRegionAs_capRange_Int)[1] 1068 apply (drule(1) fresh_virt_cap_classD) 1069 apply (auto dest: sameRegionAs_classes) 1070 done 1071 1072definition 1073 "initMDBNode \<equiv> MDB nullPointer nullPointer True True" 1074 1075lemma init_next [simp]: 1076 "mdbNext initMDBNode = 0" 1077 by (simp add: initMDBNode_def nullPointer_def) 1078 1079lemma init_prev [simp]: 1080 "mdbPrev initMDBNode = 0" 1081 by (simp add: initMDBNode_def nullPointer_def) 1082 1083lemma mdb_chunked_init: 1084 assumes x: "m x = Some cte" 1085 assumes no_m: "no_mdb cte" 1086 assumes no_c: "caps_no_overlap' m (capRange cap)" 1087 assumes no_v: "fresh_virt_cap_class (capClass cap) m" 1088 assumes no_0: "no_0 m" 1089 assumes dlist: "valid_dlist m" 1090 assumes chain: "mdb_chain_0 m" 1091 assumes chunked: "mdb_chunked m" 1092 assumes valid: "valid_objs' s" "m = ctes_of s" "s \<turnstile>' cap" 1093 shows "mdb_chunked (m(x \<mapsto> CTE cap initMDBNode))" 1094 unfolding mdb_chunked_def 1095proof clarify 1096 fix p p' c c' n n' 1097 define m' where "m' \<equiv> m (x \<mapsto> CTE cap initMDBNode)" 1098 assume p: "m' p = Some (CTE c n)" 1099 assume p': "m' p' = Some (CTE c' n')" 1100 assume r: "sameRegionAs c c'" 1101 assume neq: "p \<noteq> p'" 1102 1103 note no_region = caps_no_overlap'_no_region [OF no_c valid no_v] 1104 1105 from chain x no_0 1106 have chain': "mdb_chain_0 m'" 1107 unfolding m'_def 1108 apply - 1109 apply (rule mdb_chain_0_update, clarsimp) 1110 apply clarsimp 1111 apply (drule rtranclD) 1112 apply (erule disjE, clarsimp) 1113 apply clarsimp 1114 apply (drule tranclD) 1115 apply (clarsimp simp: mdb_next_unfold) 1116 apply clarsimp 1117 apply assumption 1118 apply assumption 1119 done 1120 moreover 1121 from x no_0 1122 have x0 [simp]: "x \<noteq> 0" by clarsimp 1123 with no_0 1124 have "no_0 m'" 1125 unfolding m'_def 1126 by (rule no_0_update) 1127 ultimately 1128 have nl: "no_loops m'" by (rule mdb_chain_0_no_loops) 1129 1130 from p p' r neq no_region 1131 have px: "p \<noteq> x" 1132 by (clarsimp simp: m'_def) blast 1133 moreover 1134 from p p' r neq no_region 1135 have p'x: "p' \<noteq> x" 1136 by (clarsimp simp: m'_def) blast 1137 ultimately 1138 have m: 1139 "(m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> 1140 (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m c p p') \<and> 1141 (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m c' p' p)" 1142 using chunked p p' neq r 1143 unfolding mdb_chunked_def m'_def 1144 by simp 1145 1146 from x no_m px [symmetric] dlist no_0 1147 have npx: "\<not> m \<turnstile> p \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) 1148 1149 from x no_m p'x [symmetric] dlist no_0 1150 have np'x: "\<not> m \<turnstile> p' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) 1151 1152 show "(m' \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m' \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> 1153 (m' \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m' c p p') \<and> 1154 (m' \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m' c' p' p)" 1155 proof (cases "m \<turnstile> p \<leadsto>\<^sup>+ p'") 1156 case True 1157 with m 1158 have ch: "is_chunk m c p p'" by simp 1159 1160 from True npx 1161 have "m' \<turnstile> p \<leadsto>\<^sup>+ p'" 1162 unfolding m'_def 1163 by (rule mdb_trancl_other_update) 1164 moreover 1165 with nl 1166 have "\<not> m' \<turnstile> p' \<leadsto>\<^sup>+ p" 1167 apply clarsimp 1168 apply (drule (1) trancl_trans) 1169 apply (simp add: no_loops_def) 1170 done 1171 moreover 1172 have "is_chunk m' c p p'" 1173 unfolding is_chunk_def 1174 proof clarify 1175 fix p'' 1176 assume "m' \<turnstile> p \<leadsto>\<^sup>+ p''" 1177 with npx 1178 have "m \<turnstile> p \<leadsto>\<^sup>+ p''" 1179 unfolding m'_def 1180 by - (rule mdb_trancl_update_other) 1181 moreover 1182 then 1183 have p''x: "p'' \<noteq> x" 1184 using dlist x no_m no_0 1185 apply clarsimp 1186 apply (drule tranclD2) 1187 apply clarsimp 1188 apply (frule vdlist_nextD0, simp, assumption) 1189 apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def) 1190 done 1191 moreover 1192 assume "m' \<turnstile> p'' \<leadsto>\<^sup>* p'" 1193 { 1194 moreover 1195 from x no_m p''x [symmetric] dlist no_0 1196 have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) 1197 ultimately 1198 have "m \<turnstile> p'' \<leadsto>\<^sup>* p'" 1199 unfolding m'_def 1200 by (rule mdb_rtrancl_update_other) 1201 } 1202 ultimately 1203 have "\<exists>cap'' n''. 1204 m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''" 1205 using ch 1206 by (simp add: is_chunk_def) 1207 with p''x 1208 show "\<exists>cap'' n''. 1209 m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c cap''" 1210 by (simp add: m'_def) 1211 qed 1212 ultimately 1213 show ?thesis by simp 1214 next 1215 case False 1216 with m 1217 have p'p: "m \<turnstile> p' \<leadsto>\<^sup>+ p" by simp 1218 with m 1219 have ch: "is_chunk m c' p' p" by simp 1220 from p'p np'x 1221 have "m' \<turnstile> p' \<leadsto>\<^sup>+ p" 1222 unfolding m'_def 1223 by (rule mdb_trancl_other_update) 1224 moreover 1225 with nl 1226 have "\<not> m' \<turnstile> p \<leadsto>\<^sup>+ p'" 1227 apply clarsimp 1228 apply (drule (1) trancl_trans) 1229 apply (simp add: no_loops_def) 1230 done 1231 moreover 1232 have "is_chunk m' c' p' p" 1233 unfolding is_chunk_def 1234 proof clarify 1235 fix p'' 1236 assume "m' \<turnstile> p' \<leadsto>\<^sup>+ p''" 1237 with np'x 1238 have "m \<turnstile> p' \<leadsto>\<^sup>+ p''" 1239 unfolding m'_def 1240 by - (rule mdb_trancl_update_other) 1241 moreover 1242 then 1243 have p''x: "p'' \<noteq> x" 1244 using dlist x no_m no_0 1245 apply clarsimp 1246 apply (drule tranclD2) 1247 apply clarsimp 1248 apply (frule vdlist_nextD0, simp, assumption) 1249 apply (clarsimp simp: mdb_prev_def mdb_next_unfold no_mdb_def) 1250 done 1251 moreover 1252 assume "m' \<turnstile> p'' \<leadsto>\<^sup>* p" 1253 { 1254 moreover 1255 from x no_m p''x [symmetric] dlist no_0 1256 have "\<not>m \<turnstile> p'' \<leadsto>\<^sup>* x" by (rule no_mdb_rtrancl) 1257 ultimately 1258 have "m \<turnstile> p'' \<leadsto>\<^sup>* p" 1259 unfolding m'_def 1260 by (rule mdb_rtrancl_update_other) 1261 } 1262 ultimately 1263 have "\<exists>cap'' n''. 1264 m p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''" 1265 using ch 1266 by (simp add: is_chunk_def) 1267 with p''x 1268 show "\<exists>cap'' n''. 1269 m' p'' = Some (CTE cap'' n'') \<and> sameRegionAs c' cap''" 1270 by (simp add: m'_def) 1271 qed 1272 ultimately 1273 show ?thesis by simp 1274 qed 1275qed 1276 1277lemma cte_refs_capRange: 1278 "\<lbrakk> s \<turnstile>' c; \<forall>irq. c \<noteq> IRQHandlerCap irq \<rbrakk> \<Longrightarrow> cte_refs' c x \<subseteq> capRange c" 1279 apply (cases c; simp add: capRange_def isCap_simps) 1280 apply (clarsimp dest!: valid_capAligned 1281 simp: capAligned_def objBits_simps field_simps) 1282 apply (frule tcb_cte_cases_small) 1283 apply (intro conjI) 1284 apply (erule(1) is_aligned_no_wrap') 1285 apply (rule word_plus_mono_right[where z="2^tcbBlockSizeBits - 1", simplified field_simps]) 1286 apply (drule minus_one_helper3, simp) 1287 apply (erule is_aligned_no_wrap'[where off="2^tcbBlockSizeBits - 1", simplified field_simps]) 1288 apply (drule minus_one_helper3) 1289 apply simp 1290 defer 1291 \<comment> \<open>CNodeCap\<close> 1292 apply (clarsimp simp: objBits_simps capAligned_def dest!: valid_capAligned) 1293 apply (rename_tac word1 nat1 word2 nat2 x) 1294 apply (subgoal_tac "x * 2 ^ cteSizeBits < 2 ^ (cteSizeBits + nat1)") 1295 apply (intro conjI) 1296 apply (erule(1) is_aligned_no_wrap') 1297 apply (simp add: add_diff_eq[symmetric]) 1298 apply (rule word_plus_mono_right) 1299 apply simp 1300 apply (erule is_aligned_no_wrap') 1301 apply simp 1302 apply (simp add: power_add field_simps) 1303 apply (erule word_mult_less_mono1) 1304 apply (simp add: objBits_defs) 1305 apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z]) 1306 apply simp 1307 apply (simp only: power_add) 1308 apply (simp add: word_bits_def) 1309 \<comment> \<open>Zombie\<close> 1310 apply (clarsimp simp: capAligned_def valid_cap'_def objBits_simps) 1311 apply (rename_tac word zombie_type nat x) 1312 apply (subgoal_tac "x * 2^cteSizeBits < 2 ^ zBits zombie_type") 1313 apply (intro conjI) 1314 apply (erule(1) is_aligned_no_wrap') 1315 apply (simp add: add_diff_eq[symmetric]) 1316 apply (rule word_plus_mono_right) 1317 apply simp 1318 apply (erule is_aligned_no_wrap') 1319 apply simp 1320 apply (case_tac zombie_type) 1321 apply simp 1322 apply (rule div_lt_mult) 1323 apply (simp add: objBits_defs) 1324 apply (erule order_less_le_trans) 1325 apply (simp add: word_le_nat_alt) 1326 apply (subst le_unat_uoi[where z=5]) 1327 apply simp 1328 apply simp 1329 apply (simp add: objBits_defs) 1330 apply (simp add: objBits_simps' power_add mult.commute) 1331 apply (rule word_mult_less_mono1) 1332 apply (erule order_less_le_trans) 1333 apply (simp add: word_le_nat_alt) 1334 apply (subst le_unat_uoi) 1335 apply (subst unat_power_lower) 1336 prefer 2 1337 apply assumption 1338 apply (simp add: word_bits_def) 1339 apply (simp add: word_bits_def) 1340 apply simp 1341 apply (frule power_strict_increasing [where a="2 :: nat" and n="y + z" for y z]) 1342 apply simp 1343 apply (simp only: power_add) 1344 apply (simp add: word_bits_def) 1345 done 1346 1347lemma untypedCapRange: 1348 "isUntypedCap cap \<Longrightarrow> capRange cap = untypedRange cap" 1349 by (clarsimp simp: isCap_simps) 1350 1351lemma no_direct_loop [simp]: 1352 "no_loops m \<Longrightarrow> m (mdbNext node) \<noteq> Some (CTE cap node)" 1353 by (fastforce simp: mdb_next_rel_def mdb_next_def no_loops_def) 1354 1355lemma no_loops_direct_simp: 1356 "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto> x = False" 1357 by (auto simp add: no_loops_def) 1358 1359lemma no_loops_trancl_simp: 1360 "no_loops m \<Longrightarrow> m \<turnstile> x \<leadsto>\<^sup>+ x = False" 1361 by (auto simp add: no_loops_def) 1362 1363lemma subtree_mdb_next: 1364 "m \<turnstile> a \<rightarrow> b \<Longrightarrow> m \<turnstile> a \<leadsto>\<^sup>+ b" 1365 by (erule subtree.induct) (auto simp: mdb_next_rel_def intro: trancl_into_trancl) 1366end 1367 1368context mdb_order 1369begin 1370 1371lemma no_loops: "no_loops m" 1372 using chain no_0 by (rule mdb_chain_0_no_loops) 1373 1374lemma irrefl_direct_simp [iff]: 1375 "m \<turnstile> x \<leadsto> x = False" 1376 using no_loops by (rule no_loops_direct_simp) 1377 1378lemma irrefl_trancl_simp [iff]: 1379 "m \<turnstile> x \<leadsto>\<^sup>+ x = False" 1380 using no_loops by (rule no_loops_trancl_simp) 1381 1382lemma irrefl_rtrancl: 1383 "\<lbrakk> m \<turnstile> x \<leadsto>\<^sup>* y; m \<turnstile> y \<leadsto>\<^sup>* x \<rbrakk> \<Longrightarrow> x = y" 1384 by (fastforce dest: rtranclD trancl_trans) 1385 1386lemma irrefl_subtree [iff]: 1387 "m \<turnstile> x \<rightarrow> x = False" 1388 by (clarsimp dest!: subtree_mdb_next) 1389 1390end (* of context mdb_order *) 1391 1392lemma no_loops_prev_next_0: 1393 fixes m :: cte_heap 1394 assumes src: "m src = Some (CTE src_cap src_node)" 1395 assumes no_loops: "no_loops m" 1396 assumes dlist: "valid_dlist m" 1397 shows "(mdbPrev src_node = mdbNext src_node) = 1398 (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)" 1399proof - 1400 { assume "mdbPrev src_node = mdbNext src_node" 1401 moreover 1402 assume "mdbNext src_node \<noteq> 0" 1403 ultimately 1404 obtain cte where 1405 "m (mdbNext src_node) = Some cte" 1406 "mdbNext (cteMDBNode cte) = src" 1407 using src dlist 1408 by (fastforce simp add: valid_dlist_def Let_def) 1409 hence "m \<turnstile> src \<leadsto>\<^sup>+ src" using src 1410 apply - 1411 apply (rule trancl_trans) 1412 apply (rule r_into_trancl) 1413 apply (simp add: next_unfold') 1414 apply (rule r_into_trancl) 1415 apply (simp add: next_unfold') 1416 done 1417 with no_loops 1418 have False by (simp add: no_loops_def) 1419 } 1420 thus ?thesis by auto blast 1421qed 1422 1423lemma no_loops_next_prev_0: 1424 fixes m :: cte_heap 1425 assumes "m src = Some (CTE src_cap src_node)" 1426 assumes "no_loops m" 1427 assumes "valid_dlist m" 1428 shows "(mdbNext src_node = mdbPrev src_node) = 1429 (mdbPrev src_node = 0 \<and> mdbNext src_node = 0)" 1430 apply (rule iffI) 1431 apply (drule sym) 1432 apply (simp add: no_loops_prev_next_0 [OF assms]) 1433 apply clarsimp 1434 done 1435 1436locale vmdb = mdb_next + 1437 assumes valid: "valid_mdb_ctes m" 1438 1439sublocale vmdb < mdb_order 1440 using valid 1441 by (auto simp: greater_def greater_eq_def mdb_order_def valid_mdb_ctes_def) 1442 1443context vmdb 1444begin 1445 1446declare no_0 [intro!] 1447declare no_loops [intro!] 1448 1449lemma dlist [intro!]: "valid_dlist m" 1450 using valid by (simp add: valid_mdb_ctes_def) 1451 1452lemmas m_0_simps [iff] = no_0_simps [OF no_0] 1453 1454lemma prev_next_0_p: 1455 assumes "m p = Some (CTE cap node)" 1456 shows "(mdbPrev node = mdbNext node) = 1457 (mdbPrev node = 0 \<and> mdbNext node = 0)" 1458 using assms by (rule no_loops_prev_next_0) auto 1459 1460lemma next_prev_0_p: 1461 assumes "m p = Some (CTE cap node)" 1462 shows "(mdbNext node = mdbPrev node) = 1463 (mdbPrev node = 0 \<and> mdbNext node = 0)" 1464 using assms by (rule no_loops_next_prev_0) auto 1465 1466lemmas dlistEn = valid_dlistEn [OF dlist] 1467lemmas dlistEp = valid_dlistEp [OF dlist] 1468 1469lemmas dlist_prevD = vdlist_prevD [OF _ _ dlist no_0] 1470lemmas dlist_nextD = vdlist_nextD [OF _ _ dlist no_0] 1471lemmas dlist_prevD0 = vdlist_prevD0 [OF _ _ dlist] 1472lemmas dlist_nextD0 = vdlist_nextD0 [OF _ _ dlist] 1473lemmas dlist_prev_src_unique = vdlist_prev_src_unique [OF _ _ _ dlist] 1474lemmas dlist_next_src_unique = vdlist_next_src_unique [OF _ _ _ dlist] 1475 1476lemma subtree_not_0 [simp]: 1477 "\<not>m \<turnstile> p \<rightarrow> 0" 1478 apply clarsimp 1479 apply (erule subtree.cases) 1480 apply auto 1481 done 1482 1483lemma not_0_subtree [simp]: 1484 "\<not>m \<turnstile> 0 \<rightarrow> p" 1485 apply clarsimp 1486 apply (erule subtree.induct) 1487 apply (auto simp: mdb_next_unfold) 1488 done 1489 1490lemma not_0_next [simp]: 1491 "\<not> m \<turnstile> 0 \<leadsto> p" 1492 by (clarsimp simp: mdb_next_unfold) 1493 1494lemma not_0_trancl [simp]: 1495 "\<not> m \<turnstile> 0 \<leadsto>\<^sup>+ p" 1496 by (clarsimp dest!: tranclD) 1497 1498lemma rtrancl0 [simp]: 1499 "m \<turnstile> 0 \<leadsto>\<^sup>* p = (p = 0)" 1500 by (auto dest!: rtranclD) 1501 1502lemma valid_badges: "valid_badges m" 1503 using valid by (simp add: valid_mdb_ctes_def) 1504 1505lemma nullcaps: "valid_nullcaps m" 1506 using valid by (simp add: valid_mdb_ctes_def) 1507 1508lemma 1509 caps_contained: "caps_contained' m" and 1510 chunked: "mdb_chunked m" and 1511 untyped_mdb: "untyped_mdb' m" and 1512 untyped_inc: "untyped_inc' m" and 1513 class_links: "class_links m" and 1514 irq_control: "irq_control m" 1515 using valid by (simp add: valid_mdb_ctes_def)+ 1516 1517lemma zero_next [simp]: 1518 "m \<turnstile> 0 \<leadsto> p' = False" 1519 by (clarsimp simp: mdb_next_unfold) 1520 1521end (* of context vmdb *) 1522 1523lemma no_self_loop_next: 1524 assumes vmdb: "valid_mdb_ctes m" 1525 and lup: "m ptr = Some cte" 1526 shows "mdbNext (cteMDBNode cte) \<noteq> ptr" 1527proof - 1528 from vmdb have "no_loops m" .. 1529 thus ?thesis 1530 by (rule no_self_loop_next_noloop) fact+ 1531qed 1532 1533lemma no_self_loop_prev: 1534 assumes vmdb: "valid_mdb_ctes m" 1535 and lup: "m ptr = Some cte" 1536 shows "mdbPrev (cteMDBNode cte) \<noteq> ptr" 1537proof 1538 assume prev: "mdbPrev (cteMDBNode cte) = ptr" 1539 1540 from vmdb have "no_0 m" .. 1541 with lup have "ptr \<noteq> 0" 1542 by (rule no_0_neq) 1543 1544 moreover have "mdbNext (cteMDBNode cte) \<noteq> ptr" 1545 by (rule no_self_loop_next) fact+ 1546 1547 moreover from vmdb have "valid_dlist m" .. 1548 1549 ultimately show False using lup prev 1550 by - (erule (1) valid_dlistEp, simp_all) 1551qed 1552 1553 1554locale mdb_ptr = vmdb + 1555 fixes p cap node 1556 assumes m_p [intro!]: "m p = Some (CTE cap node)" 1557begin 1558 1559lemma p_not_next [simp]: 1560 "(p = mdbNext node) = False" 1561 using valid m_p by (fastforce dest: no_self_loop_next) 1562 1563lemma p_not_prev [simp]: 1564 "(p = mdbPrev node) = False" 1565 using valid m_p by (fastforce dest: no_self_loop_prev) 1566 1567lemmas next_not_p [simp] = p_not_next [THEN x_sym] 1568lemmas prev_not_p [simp] = p_not_prev [THEN x_sym] 1569 1570lemmas prev_next_0 [simp] = prev_next_0_p [OF m_p] next_prev_0_p [OF m_p] 1571 1572lemma p_0 [simp]: "p \<noteq> 0" using m_p by clarsimp 1573 1574lemma p_nextD: 1575 assumes p': "m p' = Some (CTE cap' node')" 1576 assumes eq: "mdbNext node = mdbNext node'" 1577 shows "p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0" 1578proof (cases "mdbNext node = 0") 1579 case True thus ?thesis using eq by simp 1580next 1581 case False 1582 with eq have n': "mdbNext node' \<noteq> 0" by simp 1583 1584 have "p = p'" 1585 apply (rule dlistEn [OF m_p, simplified, OF False]) 1586 apply (simp add: eq) 1587 apply (rule dlistEn [OF p', simplified, OF n']) 1588 apply clarsimp 1589 done 1590 1591 thus ?thesis by blast 1592qed 1593 1594lemma p_next_eq: 1595 assumes "m p' = Some (CTE cap' node')" 1596 shows "(mdbNext node = mdbNext node') = 1597 (p = p' \<or> mdbNext node = 0 \<and> mdbNext node' = 0)" 1598 using assms m_p 1599 apply - 1600 apply (rule iffI) 1601 apply (erule (1) p_nextD) 1602 apply auto 1603 done 1604 1605lemma p_prevD: 1606 assumes p': "m p' = Some (CTE cap' node')" 1607 assumes eq: "mdbPrev node = mdbPrev node'" 1608 shows "p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0" 1609proof (cases "mdbPrev node = 0") 1610 case True thus ?thesis using eq by simp 1611next 1612 case False 1613 with eq have n': "mdbPrev node' \<noteq> 0" by simp 1614 1615 have "p = p'" 1616 apply (rule dlistEp [OF m_p, simplified, OF False]) 1617 apply (simp add: eq) 1618 apply (rule dlistEp [OF p', simplified, OF n']) 1619 apply clarsimp 1620 done 1621 1622 thus ?thesis by blast 1623qed 1624 1625lemma p_prev_eq: 1626 assumes "m p' = Some (CTE cap' node')" 1627 shows "(mdbPrev node = mdbPrev node') = 1628 (p = p' \<or> mdbPrev node = 0 \<and> mdbPrev node' = 0)" 1629 using assms m_p 1630 apply - 1631 apply (rule iffI) 1632 apply (erule (1) p_prevD) 1633 apply auto 1634 done 1635 1636lemmas p_prev_qe = p_prev_eq [THEN x_sym] 1637lemmas p_next_qe = p_next_eq [THEN x_sym] 1638 1639lemma m_p_prev [intro!]: 1640 "m \<turnstile> mdbPrev node \<leftarrow> p" 1641 using m_p by (clarsimp simp: mdb_prev_def) 1642 1643lemma m_p_next [intro!]: 1644 "m \<turnstile> p \<leadsto> mdbNext node" 1645 using m_p by (clarsimp simp: mdb_next_unfold) 1646 1647lemma next_p_prev: 1648 "mdbNext node \<noteq> 0 \<Longrightarrow> m \<turnstile> p \<leftarrow> mdbNext node" 1649 by (rule dlist_nextD0 [OF m_p_next]) 1650 1651lemma prev_p_next: 1652 "mdbPrev node \<noteq> 0 \<Longrightarrow> m \<turnstile> mdbPrev node \<leadsto> p" 1653 by (rule dlist_prevD0 [OF m_p_prev]) 1654 1655lemma p_next: 1656 "(m \<turnstile> p \<leadsto> p') = (p' = mdbNext node)" 1657 using m_p by (auto simp: mdb_next_unfold) 1658 1659end (* of locale mdb_ptr *) 1660 1661lemma no_mdb_not_source: 1662 "no_mdb cte \<Longrightarrow> m \<turnstile> c \<leadsto> c' \<Longrightarrow> m p = Some cte \<Longrightarrow> c = p \<longrightarrow> c' = 0" 1663 by (clarsimp simp add: mdb_next_unfold no_mdb_def) 1664 1665lemma no_mdb_not_target: 1666 "\<lbrakk> m \<turnstile> c \<leadsto> c'; m p = Some cte; no_mdb cte; valid_dlist m; no_0 m \<rbrakk> 1667 \<Longrightarrow> c' \<noteq> p" 1668 apply clarsimp 1669 apply (subgoal_tac "c \<noteq> 0") 1670 prefer 2 1671 apply (clarsimp simp: mdb_next_unfold) 1672 apply (drule (3) vdlist_nextD) 1673 apply (clarsimp simp: mdb_prev_def) 1674 apply (simp add: no_mdb_def) 1675 done 1676 1677context begin interpretation Arch . (*FIXME: arch_split*) 1678lemma valid_dlist_init: 1679 "\<lbrakk> valid_dlist m; m p = Some cte; no_mdb cte \<rbrakk> \<Longrightarrow> 1680 valid_dlist (m (p \<mapsto> CTE cap initMDBNode))" 1681 apply (simp add: initMDBNode_def Let_def nullPointer_def) 1682 apply (clarsimp simp: no_mdb_def valid_dlist_def Let_def) 1683 apply fastforce 1684 done 1685end 1686 1687lemma (in mdb_ptr) descendants_of_init': 1688 assumes n: "no_mdb (CTE cap node)" 1689 shows 1690 "descendants_of' p' (m(p \<mapsto> CTE c initMDBNode)) = 1691 descendants_of' p' m" 1692 apply (rule set_eqI) 1693 apply (simp add: descendants_of'_def) 1694 apply (rule iffI) 1695 apply (erule subtree.induct) 1696 apply (frule no_mdb_not_target [where p=p]) 1697 apply simp 1698 apply (simp add: no_mdb_def) 1699 apply (rule valid_dlist_init[OF dlist, OF m_p n]) 1700 apply (insert no_0)[1] 1701 apply (clarsimp simp: no_0_def) 1702 apply (clarsimp simp: mdb_next_unfold split: if_split_asm) 1703 apply (rule direct_parent) 1704 apply (clarsimp simp: mdb_next_unfold) 1705 apply assumption 1706 apply (clarsimp simp: parentOf_def split: if_split_asm) 1707 apply (frule no_mdb_not_target [where p=p]) 1708 apply simp 1709 apply (simp add: no_mdb_def) 1710 apply (rule valid_dlist_init[OF dlist, OF m_p n]) 1711 apply (insert no_0)[1] 1712 apply (clarsimp simp: no_0_def) 1713 apply (subgoal_tac "p' \<noteq> p") 1714 apply (erule trans_parent) 1715 apply (clarsimp simp: mdb_next_unfold split: if_split_asm) 1716 apply assumption 1717 apply (clarsimp simp: parentOf_def m_p split: if_split_asm) 1718 apply clarsimp 1719 apply (drule subtree_mdb_next)+ 1720 apply (drule tranclD)+ 1721 apply clarsimp 1722 apply (insert n)[1] 1723 apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) 1724 apply (erule subtree.induct) 1725 apply (frule no_mdb_not_target [where p=p], rule m_p, rule n) 1726 apply (rule dlist) 1727 apply (rule no_0) 1728 apply (subgoal_tac "p'\<noteq>p") 1729 prefer 2 1730 apply (insert n)[1] 1731 apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) 1732 apply (rule direct_parent) 1733 apply (clarsimp simp: mdb_next_unfold) 1734 apply assumption 1735 apply (clarsimp simp: parentOf_def) 1736 apply (frule no_mdb_not_target [where p=p], rule m_p, rule n) 1737 apply (rule dlist) 1738 apply (rule no_0) 1739 apply (subgoal_tac "c'\<noteq>p") 1740 prefer 2 1741 apply (insert n)[1] 1742 apply (clarsimp simp: mdb_next_unfold m_p no_mdb_def) 1743 apply (subgoal_tac "p'\<noteq>p") 1744 apply (erule trans_parent) 1745 apply (clarsimp simp: mdb_next_unfold) 1746 apply assumption 1747 apply (clarsimp simp: parentOf_def) 1748 apply clarsimp 1749 apply (drule subtree_mdb_next) 1750 apply (drule tranclD) 1751 apply clarsimp 1752 apply (insert n) 1753 apply (clarsimp simp: mdb_next_unfold no_mdb_def m_p) 1754 done 1755 1756lemma untyped_mdb_init: 1757 "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte; 1758 caps_no_overlap' m (capRange cap); untyped_mdb' m; 1759 valid_objs' s; s \<turnstile>' cap; 1760 m = ctes_of s\<rbrakk> 1761 \<Longrightarrow> untyped_mdb' (m(p \<mapsto> CTE cap initMDBNode))" 1762 apply (clarsimp simp add: untyped_mdb'_def) 1763 apply (rule conjI) 1764 apply clarsimp 1765 apply (simp add: caps_no_overlap'_def) 1766 apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) 1767 apply (drule (1) ctes_of_valid_cap')+ 1768 apply (drule valid_capAligned)+ 1769 apply (drule untypedCapRange)+ 1770 apply simp 1771 apply (cases cte) 1772 apply (rename_tac capability mdbnode) 1773 apply clarsimp 1774 apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") 1775 prefer 2 1776 apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def) 1777 apply (clarsimp simp: mdb_ptr.descendants_of_init') 1778 apply (simp add: caps_no_overlap'_def) 1779 apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) 1780 apply (drule (1) ctes_of_valid_cap')+ 1781 apply (drule valid_capAligned untypedCapRange)+ 1782 apply simp 1783 apply blast 1784 done 1785 1786lemma aligned_untypedRange_non_empty: 1787 "\<lbrakk>capAligned c; isUntypedCap c\<rbrakk> \<Longrightarrow> untypedRange c \<noteq> {}" 1788 apply (frule untypedCapRange) 1789 apply (drule capAligned_capUntypedPtr) 1790 apply (clarsimp simp: isCap_simps) 1791 apply blast 1792 done 1793 1794lemma untypedRange_not_emptyD: "untypedRange c' \<noteq> {} \<Longrightarrow> isUntypedCap c'" 1795 by (case_tac c'; simp add: isCap_simps) 1796 1797lemma usableRange_subseteq: 1798 "\<lbrakk>capAligned c';isUntypedCap c'\<rbrakk> \<Longrightarrow> usableUntypedRange c' \<subseteq> untypedRange c'" 1799 apply (clarsimp simp:isCap_simps capAligned_def split:if_splits) 1800 apply (erule order_trans[OF is_aligned_no_wrap']) 1801 apply (erule of_nat_power) 1802 apply (simp add:word_bits_def)+ 1803 done 1804 1805lemma untypedRange_in_capRange: "untypedRange x \<subseteq> capRange x" 1806 by (case_tac x; simp add: capRange_def) 1807 1808lemma untyped_inc_init: 1809 "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte; 1810 caps_no_overlap' m (capRange cap); 1811 valid_objs' s; s \<turnstile>' cap; 1812 m = ctes_of s\<rbrakk> 1813 \<Longrightarrow> untyped_inc' (m(p \<mapsto> CTE cap initMDBNode))" 1814 apply (clarsimp simp add: valid_mdb_ctes_def untyped_inc'_def) 1815 apply (intro conjI impI) 1816 apply clarsimp 1817 apply (simp add: caps_no_overlap'_def) 1818 apply (erule_tac x=p' in allE, erule allE, erule impE, erule exI) 1819 apply (drule (1) ctes_of_valid_cap')+ 1820 apply (drule valid_capAligned)+ 1821 apply (frule usableRange_subseteq[OF _ untypedRange_not_emptyD]) 1822 apply (drule (1) aligned_untypedRange_non_empty) 1823 apply assumption 1824 apply (frule_tac c' = c' in usableRange_subseteq) 1825 apply (drule (1) aligned_untypedRange_non_empty) 1826 apply assumption 1827 apply (drule(1) aligned_untypedRange_non_empty)+ 1828 apply (thin_tac "All P" for P) 1829 apply (subgoal_tac "untypedRange cap \<inter> untypedRange c' = {}") 1830 apply (intro conjI) 1831 apply simp 1832 apply (drule(2) set_inter_not_emptyD2) 1833 apply fastforce 1834 apply (drule(2) set_inter_not_emptyD1) 1835 apply fastforce 1836 apply (drule(2) set_inter_not_emptyD3) 1837 apply simp+ 1838 apply (rule disjoint_subset2[OF _ disjoint_subset]) 1839 apply (rule untypedRange_in_capRange)+ 1840 apply (simp add:Int_ac) 1841 apply clarsimp 1842 apply (cases cte) 1843 apply (rename_tac capability mdbnode) 1844 apply clarsimp 1845 apply (subgoal_tac "mdb_ptr (ctes_of s) p capability mdbnode") 1846 prefer 2 1847 apply (simp add: vmdb_def mdb_ptr_def mdb_ptr_axioms_def valid_mdb_ctes_def untyped_inc'_def) 1848 apply (clarsimp simp: mdb_ptr.descendants_of_init') 1849 apply (simp add: caps_no_overlap'_def) 1850 apply (erule_tac x=pa in allE, erule allE, erule impE, erule exI) 1851 apply (drule (1) ctes_of_valid_cap')+ 1852 apply (drule valid_capAligned)+ 1853 apply (frule usableRange_subseteq[OF _ untypedRange_not_emptyD]) 1854 apply (drule (1) aligned_untypedRange_non_empty) 1855 apply assumption 1856 apply (frule_tac c' = c in usableRange_subseteq) 1857 apply (drule (1) aligned_untypedRange_non_empty) 1858 apply assumption 1859 apply (drule (1) aligned_untypedRange_non_empty)+ 1860 apply (drule untypedCapRange)+ 1861 apply (thin_tac "All P" for P) 1862 apply (subgoal_tac "untypedRange cap \<inter> untypedRange c = {}") 1863 apply (intro conjI) 1864 apply simp 1865 apply (drule(2) set_inter_not_emptyD1) 1866 apply fastforce 1867 apply (drule(2) set_inter_not_emptyD2) 1868 apply fastforce 1869 apply (drule(2) set_inter_not_emptyD3) 1870 apply simp+ 1871 apply (rule disjoint_subset2[OF _ disjoint_subset]) 1872 apply (rule untypedRange_in_capRange)+ 1873 apply (simp add:Int_ac) 1874 done 1875context begin interpretation Arch . (*FIXME: arch_split*) 1876lemma valid_nullcaps_init: 1877 "\<lbrakk> valid_nullcaps m; cap \<noteq> NullCap \<rbrakk> \<Longrightarrow> valid_nullcaps (m(p \<mapsto> CTE cap initMDBNode))" 1878 by (simp add: valid_nullcaps_def initMDBNode_def nullPointer_def) 1879end 1880 1881lemma class_links_def2: 1882 "class_links m = (\<forall>p cte. m p = Some cte \<longrightarrow> mdbNext (cteMDBNode cte) \<in> dom m 1883 \<longrightarrow> capClass (cteCap cte) = capClass (cteCap (the (m (mdbNext (cteMDBNode cte))))))" 1884 by (auto simp add: class_links_def dom_def mdb_next_unfold) 1885 1886lemma class_links_init: 1887 "\<lbrakk> class_links m; no_0 m; m p = Some cte; 1888 no_mdb cte; valid_dlist m \<rbrakk> 1889 \<Longrightarrow> class_links (m(p \<mapsto> CTE cap initMDBNode))" 1890 apply (simp add: class_links_def split del: if_split) 1891 apply (erule allEI, erule allEI) 1892 apply simp 1893 apply (intro conjI impI) 1894 apply clarsimp 1895 apply (drule no_mdb_not_target[where p=p], simp) 1896 apply (simp add: no_mdb_def) 1897 apply (erule(2) valid_dlist_init) 1898 apply (clarsimp simp add: no_0_def) 1899 apply simp 1900 apply (clarsimp simp: mdb_next_unfold) 1901 apply (clarsimp simp: mdb_next_unfold) 1902 done 1903 1904lemma distinct_zombies_copyE: 1905 "\<lbrakk> distinct_zombies m; m x = Some cte; 1906 capClass (cteCap cte') = PhysicalClass 1907 \<Longrightarrow> isZombie (cteCap cte) = isZombie (cteCap cte'); 1908 \<lbrakk> capClass (cteCap cte') = PhysicalClass; isUntypedCap (cteCap cte) \<rbrakk> 1909 \<Longrightarrow> isUntypedCap (cteCap cte'); 1910 \<lbrakk> capClass (cteCap cte') = PhysicalClass; isArchPageCap (cteCap cte) \<rbrakk> 1911 \<Longrightarrow> isArchPageCap (cteCap cte'); 1912 isZombie (cteCap cte') \<Longrightarrow> x = y; 1913 capClass (cteCap cte') = PhysicalClass \<Longrightarrow> 1914 capBits (cteCap cte') = capBits (cteCap cte); 1915 capClass (cteCap cte') = PhysicalClass \<longrightarrow> capClass (cteCap cte) = PhysicalClass; 1916 capClass (cteCap cte') = PhysicalClass \<Longrightarrow> 1917 capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk> 1918 \<Longrightarrow> distinct_zombies (m (y \<mapsto> cte'))" 1919 apply (simp add: distinct_zombies_def distinct_zombie_caps_def) 1920 apply clarsimp 1921 apply (intro allI conjI impI) 1922 apply clarsimp 1923 apply (drule_tac x=y in spec) 1924 apply (drule_tac x=ptr' in spec) 1925 apply (clarsimp simp: isCap_simps) 1926 apply clarsimp 1927 apply (drule_tac x=ptr in spec) 1928 apply (drule_tac x=x in spec) 1929 apply clarsimp 1930 apply auto[1] 1931 apply clarsimp 1932 apply (drule_tac x=ptr in spec) 1933 apply (drule_tac x=ptr' in spec) 1934 apply auto[1] 1935 done 1936 1937lemmas distinct_zombies_sameE 1938 = distinct_zombies_copyE [where y=x and x=x for x, simplified, 1939 OF _ _ _ _ _] 1940context begin interpretation Arch . (*FIXME: arch_split*) 1941lemma capBits_Master: 1942 "capBits (capMasterCap cap) = capBits cap" 1943 by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split) 1944 1945lemma capUntyped_Master: 1946 "capUntypedPtr (capMasterCap cap) = capUntypedPtr cap" 1947 by (clarsimp simp: capMasterCap_def split: capability.split arch_capability.split) 1948 1949lemma distinct_zombies_copyMasterE: 1950 "\<lbrakk> distinct_zombies m; m x = Some cte; 1951 capClass (cteCap cte') = PhysicalClass 1952 \<Longrightarrow> capMasterCap (cteCap cte) = capMasterCap (cteCap cte'); 1953 isZombie (cteCap cte') \<Longrightarrow> x = y \<rbrakk> 1954 \<Longrightarrow> distinct_zombies (m (y \<mapsto> cte'))" 1955 apply (erule(1) distinct_zombies_copyE, simp_all) 1956 apply (rule master_eqI, rule isCap_Master, simp) 1957 apply (drule_tac f=isUntypedCap in arg_cong) 1958 apply (simp add: isCap_Master) 1959 apply (drule_tac f=isArchPageCap in arg_cong) 1960 apply (simp add: isCap_Master) 1961 apply (rule master_eqI, rule capBits_Master, simp) 1962 apply clarsimp 1963 apply (drule_tac f=capClass in arg_cong, simp add: capClass_Master) 1964 apply (drule_tac f=capUntypedPtr in arg_cong, simp add: capUntyped_Master) 1965 done 1966 1967lemmas distinct_zombies_sameMasterE 1968 = distinct_zombies_copyMasterE[where x=x and y=x for x, simplified, 1969 OF _ _ _] 1970 1971lemma isZombie_capClass: "isZombie cap \<Longrightarrow> capClass cap = PhysicalClass" 1972 by (clarsimp simp: isCap_simps) 1973 1974lemma distinct_zombies_unzombieE: 1975 "\<lbrakk> distinct_zombies m; m x = Some cte; 1976 isZombie (cteCap cte') \<longrightarrow> isZombie (cteCap cte); 1977 isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); 1978 isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); 1979 capClass (cteCap cte') = capClass (cteCap cte); 1980 capBits (cteCap cte') = capBits (cteCap cte); 1981 capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte) \<rbrakk> 1982 \<Longrightarrow> distinct_zombies (m(x \<mapsto> cte'))" 1983 apply (simp add: distinct_zombies_def distinct_zombie_caps_def 1984 split del: if_split) 1985 apply (erule allEI, erule allEI) 1986 apply clarsimp 1987 done 1988 1989lemma distinct_zombies_seperateE: 1990 "\<lbrakk> distinct_zombies m; 1991 \<And>y cte. m y = Some cte \<Longrightarrow> x \<noteq> y 1992 \<Longrightarrow> \<not> isUntypedCap (cteCap cte) 1993 \<Longrightarrow> \<not> isArchPageCap (cteCap cte) 1994 \<Longrightarrow> capClass (cteCap cte) = PhysicalClass 1995 \<Longrightarrow> capClass (cteCap cte') = PhysicalClass 1996 \<Longrightarrow> capUntypedPtr (cteCap cte) = capUntypedPtr (cteCap cte') 1997 \<Longrightarrow> capBits (cteCap cte) = capBits (cteCap cte') \<Longrightarrow> False \<rbrakk> 1998 \<Longrightarrow> distinct_zombies (m (x \<mapsto> cte'))" 1999 apply (simp add: distinct_zombies_def distinct_zombie_caps_def) 2000 apply (intro impI allI conjI) 2001 apply (clarsimp simp: isZombie_capClass) 2002 apply fastforce 2003 apply clarsimp 2004 apply (frule isZombie_capClass) 2005 apply (subgoal_tac "\<not> isUntypedCap (cteCap z) \<and> \<not> isArchPageCap (cteCap z)") 2006 apply fastforce 2007 apply (clarsimp simp: isCap_simps) 2008 apply clarsimp 2009 apply (erule notE[rotated], elim allE, erule mp) 2010 apply auto[1] 2011 done 2012 2013lemma distinct_zombies_seperate_if_zombiedE: 2014 "\<lbrakk> distinct_zombies m; m x = Some cte; 2015 isUntypedCap (cteCap cte) \<longrightarrow> isUntypedCap (cteCap cte'); 2016 isArchPageCap (cteCap cte) \<longrightarrow> isArchPageCap (cteCap cte'); 2017 capClass (cteCap cte') = capClass (cteCap cte); 2018 capBits (cteCap cte') = capBits (cteCap cte); 2019 capUntypedPtr (cteCap cte') = capUntypedPtr (cteCap cte); 2020 \<And>y cte''. \<lbrakk> m y = Some cte''; x \<noteq> y; 2021 isZombie (cteCap cte'); \<not> isZombie (cteCap cte); 2022 \<not> isUntypedCap (cteCap cte''); \<not> isArchPageCap (cteCap cte''); 2023 capClass (cteCap cte'') = PhysicalClass; 2024 capUntypedPtr (cteCap cte'') = capUntypedPtr (cteCap cte); 2025 capBits (cteCap cte'') = capBits (cteCap cte) 2026 \<rbrakk> \<Longrightarrow> False \<rbrakk> 2027 \<Longrightarrow> distinct_zombies (m (x \<mapsto> cte'))" 2028 apply (cases "isZombie (cteCap cte') \<and> \<not> isZombie (cteCap cte)") 2029 apply (erule distinct_zombies_seperateE) 2030 apply auto[1] 2031 apply clarsimp 2032 apply (erule(7) distinct_zombies_unzombieE) 2033 done 2034 2035lemma distinct_zombies_init: 2036 "\<lbrakk> distinct_zombies m; caps_no_overlap' m (capRange (cteCap cte)); 2037 capAligned (cteCap cte); \<forall>x cte. m x = Some cte \<longrightarrow> capAligned (cteCap cte) \<rbrakk> 2038 \<Longrightarrow> distinct_zombies (m (p \<mapsto> cte))" 2039 apply (erule distinct_zombies_seperateE) 2040 apply (rename_tac y cte') 2041 apply (clarsimp simp: caps_no_overlap'_def) 2042 apply (drule_tac x=y in spec)+ 2043 apply (case_tac cte') 2044 apply (rename_tac capability mdbnode) 2045 apply clarsimp 2046 apply (subgoal_tac "capRange capability \<noteq> capRange (cteCap cte)") 2047 apply (clarsimp simp: capRange_def) 2048 apply (drule(1) capAligned_capUntypedPtr)+ 2049 apply clarsimp 2050 done 2051 2052definition 2053 "no_irq' m \<equiv> \<forall>p cte. m p = Some cte \<longrightarrow> cteCap cte \<noteq> IRQControlCap" 2054 2055lemma no_irqD': 2056 "\<lbrakk> m p = Some (CTE IRQControlCap n); no_irq' m \<rbrakk> \<Longrightarrow> False" 2057 unfolding no_irq'_def 2058 apply (erule allE, erule allE, erule (1) impE) 2059 apply auto 2060 done 2061 2062lemma irq_control_init: 2063 assumes no_irq: "cap = IRQControlCap \<longrightarrow> no_irq' m" 2064 assumes ctrl: "irq_control m" 2065 shows "irq_control (m(p \<mapsto> CTE cap initMDBNode))" 2066 using no_irq 2067 apply (clarsimp simp: irq_control_def) 2068 apply (rule conjI) 2069 apply (clarsimp simp: initMDBNode_def) 2070 apply (erule (1) no_irqD') 2071 apply clarsimp 2072 apply (frule irq_revocable, rule ctrl) 2073 apply clarsimp 2074 apply (rule conjI) 2075 apply clarsimp 2076 apply (erule (1) no_irqD') 2077 apply clarsimp 2078 apply (erule (1) irq_controlD, rule ctrl) 2079 done 2080 2081lemma valid_mdb_ctes_init: 2082 "\<lbrakk> valid_mdb_ctes m; m p = Some cte; no_mdb cte; 2083 caps_no_overlap' m (capRange cap); s \<turnstile>' cap; 2084 valid_objs' s; m = ctes_of s; cap \<noteq> NullCap; 2085 fresh_virt_cap_class (capClass cap) (ctes_of s); 2086 cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s) \<rbrakk> \<Longrightarrow> 2087 valid_mdb_ctes (m (p \<mapsto> CTE cap initMDBNode))" 2088 apply (simp add: valid_mdb_ctes_def) 2089 apply (rule conjI, rule valid_dlist_init, simp+) 2090 apply (subgoal_tac "p \<noteq> 0") 2091 prefer 2 2092 apply (erule no_0_neq, clarsimp) 2093 apply (clarsimp simp: no_0_update) 2094 apply (rule conjI, rule mdb_chain_0_update_0, simp+) 2095 apply (rule conjI, rule valid_badges_0_update, simp+) 2096 apply (rule conjI, erule (1) caps_contained_no_overlap) 2097 apply (rule conjI, rule mdb_chunked_init, simp+) 2098 apply (rule conjI) 2099 apply (rule untyped_mdb_init, (simp add: valid_mdb_ctes_def)+) 2100 apply (rule conjI) 2101 apply (rule untyped_inc_init, (simp add: valid_mdb_ctes_def)+) 2102 apply (rule conjI) 2103 apply (erule(1) valid_nullcaps_init) 2104 apply (rule conjI, simp add: ut_revocable'_def initMDBNode_def) 2105 apply (rule conjI, erule(4) class_links_init) 2106 apply (rule conjI) 2107 apply (erule distinct_zombies_init, simp+) 2108 apply (erule valid_capAligned) 2109 apply clarsimp 2110 apply (case_tac ctea, clarsimp) 2111 apply (rule valid_capAligned, erule(1) ctes_of_valid_cap') 2112 apply (rule conjI) 2113 apply (erule (1) irq_control_init) 2114 apply (simp add: ran_def reply_masters_rvk_fb_def) 2115 apply (auto simp: initMDBNode_def)[1] 2116 done 2117 2118lemma setCTE_state_refs_of'[wp]: 2119 "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> setCTE p cte \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" 2120 unfolding setCTE_def 2121 apply (rule setObject_state_refs_of_eq) 2122 apply (clarsimp simp: updateObject_cte in_monad typeError_def 2123 in_magnitude_check objBits_simps 2124 split: kernel_object.split_asm if_split_asm) 2125 done 2126 2127lemma setCTE_valid_mdb: 2128 fixes cap 2129 defines "cte \<equiv> CTE cap initMDBNode" 2130 shows 2131 "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' no_mdb ptr s \<and> 2132 s \<turnstile>' cap \<and> valid_objs' s \<and> cap \<noteq> NullCap \<and> 2133 caps_no_overlap' (ctes_of s) (capRange cap) \<and> 2134 fresh_virt_cap_class (capClass cap) (ctes_of s) \<and> 2135 (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace> 2136 setCTE ptr cte 2137 \<lbrace>\<lambda>r. valid_mdb'\<rbrace>" 2138 apply (simp add: valid_mdb'_def setCTE_def cte_def cte_wp_at_ctes_of) 2139 apply (wp ctes_of_setObject_cte) 2140 apply (clarsimp simp del: fun_upd_apply) 2141 apply (erule(8) valid_mdb_ctes_init [OF _ _ _ _ _ _ refl]) 2142 done 2143 2144lemma setCTE_valid_objs'[wp]: 2145 "\<lbrace>valid_objs' and (valid_cap' (cteCap cte)) \<rbrace> 2146 setCTE p cte \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" 2147 unfolding setCTE_def 2148 apply (rule setObject_valid_objs') 2149 apply (clarsimp simp: prod_eq_iff lookupAround2_char1 updateObject_cte objBits_simps) 2150 apply (clarsimp simp: prod_eq_iff lookupAround2_char1 2151 updateObject_cte in_monad typeError_def 2152 valid_obj'_def valid_tcb'_def valid_cte'_def 2153 tcb_cte_cases_def 2154 split: kernel_object.split_asm if_split_asm) 2155 done 2156 2157lemma setCTE_valid_pspace: 2158 fixes cap 2159 defines "cte \<equiv> CTE cap initMDBNode" 2160 shows 2161 "\<lbrace>\<lambda>s. valid_pspace' s \<and> s \<turnstile>' cap \<and> cte_wp_at' no_mdb ptr s \<and> 2162 caps_no_overlap' (ctes_of s) (capRange cap) \<and> 2163 cap \<noteq> NullCap \<and> fresh_virt_cap_class (capClass cap) (ctes_of s) \<and> 2164 (cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace> 2165 setCTE ptr cte 2166 \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" 2167 apply (simp add: valid_pspace'_def setCTE_def cte_def) 2168 apply (rule hoare_pre) 2169 apply (wp setCTE_valid_objs'[unfolded setCTE_def] 2170 setCTE_valid_mdb[unfolded setCTE_def]) 2171 apply simp 2172 done 2173 2174lemma getCTE_cte_wp_at: 2175 "\<lbrace>\<top>\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p\<rbrace>" 2176 apply (clarsimp simp: valid_def cte_wp_at'_def getCTE_def) 2177 apply (frule state_unchanged [OF getObject_cte_inv]) 2178 apply simp 2179 apply (drule getObject_cte_det, simp) 2180 done 2181 2182lemma getCTE_cte_at: 2183 "\<lbrace>\<top>\<rbrace> getCTE c \<lbrace>\<lambda>_. cte_at' c\<rbrace>" 2184 apply (rule hoare_strengthen_post) 2185 apply (rule getCTE_cte_wp_at) 2186 apply (erule cte_wp_at_weakenE') 2187 apply simp 2188 done 2189 2190lemma getCTE_sp: 2191 "\<lbrace>P\<rbrace> getCTE p \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>c. c = rv) p and P\<rbrace>" 2192 apply (rule hoare_chain) 2193 apply (rule hoare_vcg_conj_lift) 2194 apply (rule getCTE_cte_wp_at) 2195 apply (rule getCTE_inv) 2196 apply (rule conjI, rule TrueI, assumption) 2197 apply simp 2198 done 2199 2200lemmas setCTE_ad[wp] = 2201 setObject_aligned[where 'a=cte, folded setCTE_def] 2202 setObject_distinct[where 'a=cte, folded setCTE_def] 2203lemmas setCTE_map_to_ctes = 2204 ctes_of_setObject_cte[folded setCTE_def] 2205 2206lemma getCTE_ctes_wp: 2207 "\<lbrace>\<lambda>s. \<forall>cte. ctes_of s ptr = Some cte \<longrightarrow> P cte s\<rbrace> getCTE ptr \<lbrace>P\<rbrace>" 2208 apply (rule hoare_strengthen_post, rule getCTE_sp) 2209 apply (clarsimp simp: cte_wp_at_ctes_of) 2210 done 2211 2212lemma updateMDB_valid_objs'[wp]: 2213 "\<lbrace>valid_objs'\<rbrace> updateMDB m p \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" 2214 apply (clarsimp simp add: updateMDB_def) 2215 apply (wp | simp)+ 2216 done 2217 2218lemma cte_overwrite: 2219 "cteMDBNode_update (\<lambda>x. m) (cteCap_update (\<lambda>x. c) v) = CTE c m" 2220 by (cases v, simp) 2221 2222lemma setCTE_no_0_obj' [wp]: 2223 "\<lbrace>no_0_obj'\<rbrace> setCTE p c \<lbrace>\<lambda>_. no_0_obj'\<rbrace>" 2224 by (simp add: setCTE_def) wp 2225 2226lemma insertInitCap_valid_pspace: 2227 "\<lbrace>valid_pspace' and valid_cap' cap and 2228 (\<lambda>s. caps_no_overlap' (ctes_of s) (capRange cap)) 2229 and (\<lambda>s. fresh_virt_cap_class (capClass cap) (ctes_of s)) and 2230 (\<lambda>s. cap = capability.IRQControlCap \<longrightarrow> no_irq' (ctes_of s))\<rbrace> 2231 insertInitCap ptr cap 2232 \<lbrace>\<lambda>r. valid_pspace'\<rbrace>" 2233 unfolding insertInitCap_def 2234 apply (simp add: updateCap_def valid_pspace'_def 2235 valid_mdb'_def bind_assoc 2236 split del: if_split) 2237 apply (wp setCTE_map_to_ctes getCTE_ctes_wp 2238 | simp add: updateMDB_def split del: if_split)+ 2239 apply (rule hoare_post_imp) 2240 apply (erule_tac P="pspace_aligned' s \<and> pspace_distinct' s 2241 \<and> no_0_obj' s" in conjunct2) 2242 apply (simp cong: conj_cong) 2243 apply (wp setCTE_map_to_ctes getCTE_ctes_wp)+ 2244 apply clarsimp 2245 apply (rule conjI) 2246 apply (clarsimp simp: valid_mdb_ctes_def) 2247 apply (simp add: const_def cte_overwrite nullMDBNode_def 2248 initMDBNode_def[symmetric] 2249 cong: if_cong) 2250 apply (fold fun_upd_def) 2251 apply (rule impI, rule valid_mdb_ctes_init, simp_all) 2252 apply (simp add: no_mdb_def nullPointer_def) 2253 done 2254 2255 2256declare mresults_fail[simp] 2257 2258crunch idle[wp]: get_object "valid_idle" 2259 (wp: crunch_wps simp: crunch_simps) 2260 2261lemma cte_refs_Master: 2262 "cte_refs' (capMasterCap cap) = cte_refs' cap" 2263 by (rule ext, simp add: capMasterCap_def split: capability.split) 2264end 2265 2266lemma (in vmdb) untyped_mdb': "untyped_mdb' m" 2267 using valid .. 2268 2269lemma (in vmdb) untyped_inc': "untyped_inc' m" 2270 using valid .. 2271 2272lemma diminished_capMaster: 2273 "diminished' cap cap' \<Longrightarrow> capMasterCap cap' = capMasterCap cap" 2274 by (clarsimp simp: diminished'_def) 2275 2276 2277end (* of theory *) 2278