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 11theory Finalise_R 12imports 13 IpcCancel_R 14 InterruptAcc_R 15 Retype_R 16begin 17context begin interpretation Arch . (*FIXME: arch_split*) 18 19declare doUnbindNotification_def[simp] 20 21text {* Properties about empty_slot/emptySlot *} 22 23lemma case_Null_If: 24 "(case c of NullCap \<Rightarrow> a | _ \<Rightarrow> b) = (if c = NullCap then a else b)" 25 by (case_tac c, simp_all) 26 27crunch aligned'[wp]: emptySlot pspace_aligned' (simp: case_Null_If) 28crunch distinct'[wp]: emptySlot pspace_distinct' (simp: case_Null_If) 29 30lemma updateCap_cte_wp_at_cases: 31 "\<lbrace>\<lambda>s. (ptr = ptr' \<longrightarrow> cte_wp_at' (P \<circ> cteCap_update (K cap)) ptr' s) \<and> (ptr \<noteq> ptr' \<longrightarrow> cte_wp_at' P ptr' s)\<rbrace> 32 updateCap ptr cap 33 \<lbrace>\<lambda>rv. cte_wp_at' P ptr'\<rbrace>" 34 apply (clarsimp simp: valid_def) 35 apply (drule updateCap_stuff) 36 apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def) 37 done 38 39crunch cte_wp_at'[wp]: postCapDeletion, updateTrackedFreeIndex "cte_wp_at' P p" 40 41lemma updateFreeIndex_cte_wp_at: 42 "\<lbrace>\<lambda>s. cte_at' p s \<and> P (cte_wp_at' (if p = p' then P' 43 o (cteCap_update (capFreeIndex_update (K idx))) else P') p' s)\<rbrace> 44 updateFreeIndex p idx 45 \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p' s)\<rbrace>" 46 apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def 47 split del: if_split) 48 apply (rule hoare_pre) 49 apply (wp updateCap_cte_wp_at' getSlotCap_wp) 50 apply (clarsimp simp: cte_wp_at_ctes_of) 51 apply (cases "p' = p", simp_all) 52 apply (case_tac cte, simp) 53 done 54 55lemma emptySlot_cte_wp_cap_other: 56 "\<lbrace>(\<lambda>s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s) and K (p \<noteq> p')\<rbrace> 57 emptySlot p' opt 58 \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. P (cteCap c)) p s\<rbrace>" 59 apply (rule hoare_gen_asm) 60 apply (simp add: emptySlot_def clearUntypedFreeIndex_def getSlotCap_def) 61 apply (rule hoare_pre) 62 apply (wp updateMDB_weak_cte_wp_at updateCap_cte_wp_at_cases 63 updateFreeIndex_cte_wp_at getCTE_wp' hoare_vcg_all_lift 64 | simp add: | wpc 65 | wp_once hoare_drop_imps)+ 66 done 67 68crunch typ_at'[wp]: emptySlot "\<lambda>s. P (typ_at' T p s)" 69lemmas clearUntypedFreeIndex_typ_ats[wp] 70 = typ_at_lifts[OF clearUntypedFreeIndex_typ_at'] 71 72crunch tcb_at'[wp]: postCapDeletion "tcb_at' t" 73crunch ct[wp]: emptySlot "\<lambda>s. P (ksCurThread s)" 74crunch cur_tcb'[wp]: clearUntypedFreeIndex "cur_tcb'" 75 (ignore: setObject wp: cur_tcb_lift) 76 77crunch ksRQ[wp]: emptySlot "\<lambda>s. P (ksReadyQueues s)" 78crunch ksRQL1[wp]: emptySlot "\<lambda>s. P (ksReadyQueuesL1Bitmap s)" 79crunch ksRQL2[wp]: emptySlot "\<lambda>s. P (ksReadyQueuesL2Bitmap s)" 80crunch obj_at'[wp]: postCapDeletion "obj_at' P p" 81 82lemmas postCapDeletion_valid_queues[wp] = 83 valid_queues_lift [OF postCapDeletion_obj_at' 84 postCapDeletion_pred_tcb_at' 85 postCapDeletion_ksRQ] 86 87crunch inQ[wp]: clearUntypedFreeIndex "\<lambda>s. P (obj_at' (inQ d p) t s)" 88crunch tcbDomain[wp]: clearUntypedFreeIndex "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t" 89crunch tcbPriority[wp]: clearUntypedFreeIndex "obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t" 90 91lemma emptySlot_queues [wp]: 92 "\<lbrace>Invariants_H.valid_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" 93 unfolding emptySlot_def 94 by (wp | wpcw | wp valid_queues_lift | simp)+ 95 96crunch nosch[wp]: emptySlot "\<lambda>s. P (ksSchedulerAction s)" 97crunch ksCurDomain[wp]: emptySlot "\<lambda>s. P (ksCurDomain s)" 98 99lemma emptySlot_sch_act_wf [wp]: 100 "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> 101 emptySlot sl opt 102 \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 103 apply (simp add: emptySlot_def case_Null_If) 104 apply (wp sch_act_wf_lift tcb_in_cur_domain'_lift | wpcw | simp)+ 105 done 106 107lemma updateCap_valid_objs' [wp]: 108 "\<lbrace>valid_objs' and valid_cap' cap\<rbrace> 109 updateCap ptr cap \<lbrace>\<lambda>r. valid_objs'\<rbrace>" 110 unfolding updateCap_def 111 by (wp setCTE_valid_objs getCTE_wp) (clarsimp dest!: cte_at_cte_wp_atD) 112 113lemma updateFreeIndex_valid_objs' [wp]: 114 "\<lbrace>valid_objs'\<rbrace> clearUntypedFreeIndex ptr \<lbrace>\<lambda>r. valid_objs'\<rbrace>" 115 apply (simp add: clearUntypedFreeIndex_def getSlotCap_def) 116 apply (wp getCTE_wp' | wpc | simp add: updateTrackedFreeIndex_def)+ 117 done 118 119crunch valid_objs'[wp]: emptySlot "valid_objs'" 120 121crunch state_refs_of'[wp]: setInterruptState "\<lambda>s. P (state_refs_of' s)" 122 (simp: state_refs_of'_pspaceI) 123crunch state_refs_of'[wp]: emptySlot "\<lambda>s. P (state_refs_of' s)" 124 (wp: crunch_wps) 125 126lemma mdb_chunked2D: 127 "\<lbrakk> mdb_chunked m; m \<turnstile> p \<leadsto> p'; m \<turnstile> p' \<leadsto> p''; 128 m p = Some (CTE cap nd); m p'' = Some (CTE cap'' nd''); 129 sameRegionAs cap cap''; p \<noteq> p'' \<rbrakk> 130 \<Longrightarrow> \<exists>cap' nd'. m p' = Some (CTE cap' nd') \<and> sameRegionAs cap cap'" 131 apply (subgoal_tac "\<exists>cap' nd'. m p' = Some (CTE cap' nd')") 132 apply (clarsimp simp add: mdb_chunked_def) 133 apply (drule spec[where x=p]) 134 apply (drule spec[where x=p'']) 135 apply clarsimp 136 apply (drule mp, erule trancl_into_trancl2) 137 apply (erule trancl.intros(1)) 138 apply (simp add: is_chunk_def) 139 apply (drule spec, drule mp, erule trancl.intros(1)) 140 apply (drule mp, rule trancl_into_rtrancl) 141 apply (erule trancl.intros(1)) 142 apply clarsimp 143 apply (clarsimp simp: mdb_next_unfold) 144 apply (case_tac z, simp) 145 done 146 147lemma nullPointer_eq_0_simp[simp]: 148 "(nullPointer = 0) = True" 149 "(0 = nullPointer) = True" 150 by (simp add: nullPointer_def)+ 151 152lemma capRange_Null [simp]: 153 "capRange NullCap = {}" 154 by (simp add: capRange_def) 155 156lemma no_0_no_0_lhs_trancl [simp]: 157 "no_0 m \<Longrightarrow> \<not> m \<turnstile> 0 \<leadsto>\<^sup>+ x" 158 by (rule, drule tranclD, clarsimp simp: next_unfold') 159 160lemma no_0_no_0_lhs_rtrancl [simp]: 161 "\<lbrakk> no_0 m; x \<noteq> 0 \<rbrakk> \<Longrightarrow> \<not> m \<turnstile> 0 \<leadsto>\<^sup>* x" 162 by (clarsimp dest!: rtranclD) 163 164end 165locale mdb_empty = 166 mdb_ptr?: mdb_ptr m _ _ slot s_cap s_node 167 for m slot s_cap s_node + 168 169 fixes n 170 defines "n \<equiv> 171 modify_map 172 (modify_map 173 (modify_map 174 (modify_map m (mdbPrev s_node) 175 (cteMDBNode_update (mdbNext_update (%_. (mdbNext s_node))))) 176 (mdbNext s_node) 177 (cteMDBNode_update 178 (\<lambda>mdb. mdbFirstBadged_update (%_. (mdbFirstBadged mdb \<or> mdbFirstBadged s_node)) 179 (mdbPrev_update (%_. (mdbPrev s_node)) mdb)))) 180 slot (cteCap_update (%_. capability.NullCap))) 181 slot (cteMDBNode_update (const nullMDBNode))" 182begin 183interpretation Arch . (*FIXME: arch_split*) 184 185lemmas m_slot_prev = m_p_prev 186lemmas m_slot_next = m_p_next 187lemmas prev_slot_next = prev_p_next 188lemmas next_slot_prev = next_p_prev 189 190lemma n_revokable: 191 "n p = Some (CTE cap node) \<Longrightarrow> 192 (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> 193 (if p = slot 194 then \<not> mdbRevocable node 195 else mdbRevocable node = mdbRevocable node'))" 196 by (auto simp add: n_def modify_map_if nullMDBNode_def split: if_split_asm) 197 198lemma m_revokable: 199 "m p = Some (CTE cap node) \<Longrightarrow> 200 (\<exists>cap' node'. n p = Some (CTE cap' node') \<and> 201 (if p = slot 202 then \<not> mdbRevocable node' 203 else mdbRevocable node' = mdbRevocable node))" 204 apply (clarsimp simp add: n_def modify_map_if nullMDBNode_def split: if_split_asm) 205 apply (cases "p=slot", simp) 206 apply (cases "p=mdbNext s_node", simp) 207 apply (cases "p=mdbPrev s_node", simp) 208 apply clarsimp 209 apply simp 210 apply (cases "p=mdbPrev s_node", simp) 211 apply simp 212 done 213 214lemma no_0_n: 215 "no_0 n" 216 using no_0 by (simp add: n_def) 217 218lemma n_next: 219 "n p = Some (CTE cap node) \<Longrightarrow> 220 (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> 221 (if p = slot 222 then mdbNext node = 0 223 else if p = mdbPrev s_node 224 then mdbNext node = mdbNext s_node 225 else mdbNext node = mdbNext node'))" 226 apply (subgoal_tac "p \<noteq> 0") 227 prefer 2 228 apply (insert no_0_n)[1] 229 apply clarsimp 230 apply (cases "p = slot") 231 apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 232 apply (cases "p = mdbPrev s_node") 233 apply (auto simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 234 done 235 236lemma n_prev: 237 "n p = Some (CTE cap node) \<Longrightarrow> 238 (\<exists>cap' node'. m p = Some (CTE cap' node') \<and> 239 (if p = slot 240 then mdbPrev node = 0 241 else if p = mdbNext s_node 242 then mdbPrev node = mdbPrev s_node 243 else mdbPrev node = mdbPrev node'))" 244 apply (subgoal_tac "p \<noteq> 0") 245 prefer 2 246 apply (insert no_0_n)[1] 247 apply clarsimp 248 apply (cases "p = slot") 249 apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 250 apply (cases "p = mdbNext s_node") 251 apply (auto simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 252 done 253 254lemma n_cap: 255 "n p = Some (CTE cap node) \<Longrightarrow> 256 \<exists>cap' node'. m p = Some (CTE cap' node') \<and> 257 (if p = slot 258 then cap = NullCap 259 else cap' = cap)" 260 apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 261 apply (cases node) 262 apply auto 263 done 264 265lemma m_cap: 266 "m p = Some (CTE cap node) \<Longrightarrow> 267 \<exists>cap' node'. n p = Some (CTE cap' node') \<and> 268 (if p = slot 269 then cap' = NullCap 270 else cap' = cap)" 271 apply (clarsimp simp: n_def modify_map_cases initMDBNode_def) 272 apply (cases node) 273 apply clarsimp 274 apply (cases "p=slot", simp) 275 apply clarsimp 276 apply (cases "mdbNext s_node = p", simp) 277 apply fastforce 278 apply simp 279 apply (cases "mdbPrev s_node = p", simp) 280 apply fastforce 281 done 282 283lemma n_badged: 284 "n p = Some (CTE cap node) \<Longrightarrow> 285 \<exists>cap' node'. m p = Some (CTE cap' node') \<and> 286 (if p = slot 287 then \<not> mdbFirstBadged node 288 else if p = mdbNext s_node 289 then mdbFirstBadged node = (mdbFirstBadged node' \<or> mdbFirstBadged s_node) 290 else mdbFirstBadged node = mdbFirstBadged node')" 291 apply (subgoal_tac "p \<noteq> 0") 292 prefer 2 293 apply (insert no_0_n)[1] 294 apply clarsimp 295 apply (cases "p = slot") 296 apply (clarsimp simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 297 apply (cases "p = mdbNext s_node") 298 apply (auto simp: n_def modify_map_if nullMDBNode_def split: if_split_asm) 299 done 300 301lemma m_badged: 302 "m p = Some (CTE cap node) \<Longrightarrow> 303 \<exists>cap' node'. n p = Some (CTE cap' node') \<and> 304 (if p = slot 305 then \<not> mdbFirstBadged node' 306 else if p = mdbNext s_node 307 then mdbFirstBadged node' = (mdbFirstBadged node \<or> mdbFirstBadged s_node) 308 else mdbFirstBadged node' = mdbFirstBadged node)" 309 apply (subgoal_tac "p \<noteq> 0") 310 prefer 2 311 apply (insert no_0_n)[1] 312 apply clarsimp 313 apply (cases "p = slot") 314 apply (clarsimp simp: n_def modify_map_if nullMDBNode_def split: if_split_asm) 315 apply (cases "p = mdbNext s_node") 316 apply (clarsimp simp: n_def modify_map_if nullMDBNode_def split: if_split_asm) 317 apply clarsimp 318 apply (cases "p = mdbPrev s_node") 319 apply (auto simp: n_def modify_map_if initMDBNode_def split: if_split_asm) 320 done 321 322lemmas slot = m_p 323 324lemma m_next: 325 "m p = Some (CTE cap node) \<Longrightarrow> 326 \<exists>cap' node'. n p = Some (CTE cap' node') \<and> 327 (if p = slot 328 then mdbNext node' = 0 329 else if p = mdbPrev s_node 330 then mdbNext node' = mdbNext s_node 331 else mdbNext node' = mdbNext node)" 332 apply (subgoal_tac "p \<noteq> 0") 333 prefer 2 334 apply clarsimp 335 apply (cases "p = slot") 336 apply (clarsimp simp: n_def modify_map_if) 337 apply (cases "p = mdbPrev s_node") 338 apply (simp add: n_def modify_map_if) 339 apply simp 340 apply (simp add: n_def modify_map_if) 341 apply (cases "mdbNext s_node = p") 342 apply fastforce 343 apply fastforce 344 done 345 346lemma m_prev: 347 "m p = Some (CTE cap node) \<Longrightarrow> 348 \<exists>cap' node'. n p = Some (CTE cap' node') \<and> 349 (if p = slot 350 then mdbPrev node' = 0 351 else if p = mdbNext s_node 352 then mdbPrev node' = mdbPrev s_node 353 else mdbPrev node' = mdbPrev node)" 354 apply (subgoal_tac "p \<noteq> 0") 355 prefer 2 356 apply clarsimp 357 apply (cases "p = slot") 358 apply (clarsimp simp: n_def modify_map_if) 359 apply (cases "p = mdbPrev s_node") 360 apply (simp add: n_def modify_map_if) 361 apply simp 362 apply (simp add: n_def modify_map_if) 363 apply (cases "mdbNext s_node = p") 364 apply fastforce 365 apply fastforce 366 done 367 368lemma n_nextD: 369 "n \<turnstile> p \<leadsto> p' \<Longrightarrow> 370 if p = slot then p' = 0 371 else if p = mdbPrev s_node 372 then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node 373 else m \<turnstile> p \<leadsto> p'" 374 apply (clarsimp simp: mdb_next_unfold split del: if_split cong: if_cong) 375 apply (case_tac z) 376 apply (clarsimp split del: if_split) 377 apply (drule n_next) 378 apply (elim exE conjE) 379 apply (simp split: if_split_asm) 380 apply (frule dlist_prevD [OF m_slot_prev]) 381 apply (clarsimp simp: mdb_next_unfold) 382 done 383 384lemma n_next_eq: 385 "n \<turnstile> p \<leadsto> p' = 386 (if p = slot then p' = 0 387 else if p = mdbPrev s_node 388 then m \<turnstile> p \<leadsto> slot \<and> p' = mdbNext s_node 389 else m \<turnstile> p \<leadsto> p')" 390 apply (rule iffI) 391 apply (erule n_nextD) 392 apply (clarsimp simp: mdb_next_unfold split: if_split_asm) 393 apply (simp add: n_def modify_map_if slot) 394 apply hypsubst_thin 395 apply (case_tac z) 396 apply simp 397 apply (drule m_next) 398 apply clarsimp 399 apply (case_tac z) 400 apply simp 401 apply (drule m_next) 402 apply clarsimp 403 done 404 405lemma n_prev_eq: 406 "n \<turnstile> p \<leftarrow> p' = 407 (if p' = slot then p = 0 408 else if p' = mdbNext s_node 409 then m \<turnstile> slot \<leftarrow> p' \<and> p = mdbPrev s_node 410 else m \<turnstile> p \<leftarrow> p')" 411 apply (rule iffI) 412 apply (clarsimp simp: mdb_prev_def split del: if_split cong: if_cong) 413 apply (case_tac z) 414 apply (clarsimp split del: if_split) 415 apply (drule n_prev) 416 apply (elim exE conjE) 417 apply (simp split: if_split_asm) 418 apply (frule dlist_nextD [OF m_slot_next]) 419 apply (clarsimp simp: mdb_prev_def) 420 apply (clarsimp simp: mdb_prev_def split: if_split_asm) 421 apply (simp add: n_def modify_map_if slot) 422 apply hypsubst_thin 423 apply (case_tac z) 424 apply clarsimp 425 apply (drule m_prev) 426 apply clarsimp 427 apply (case_tac z) 428 apply simp 429 apply (drule m_prev) 430 apply clarsimp 431 done 432 433lemma valid_dlist_n: 434 "valid_dlist n" using dlist 435 apply (clarsimp simp: valid_dlist_def2 [OF no_0_n]) 436 apply (simp add: n_next_eq n_prev_eq m_slot_next m_slot_prev cong: if_cong) 437 apply (rule conjI, clarsimp) 438 apply (rule conjI, clarsimp simp: next_slot_prev prev_slot_next) 439 apply (fastforce dest!: dlist_prev_src_unique) 440 apply clarsimp 441 apply (rule conjI, clarsimp) 442 apply (clarsimp simp: valid_dlist_def2 [OF no_0]) 443 apply (case_tac "mdbNext s_node = 0") 444 apply simp 445 apply (subgoal_tac "m \<turnstile> slot \<leadsto> c'") 446 prefer 2 447 apply fastforce 448 apply (clarsimp simp: mdb_next_unfold slot) 449 apply (frule next_slot_prev) 450 apply (drule (1) dlist_prev_src_unique, simp) 451 apply simp 452 apply clarsimp 453 apply (rule conjI, clarsimp) 454 apply (fastforce dest: dlist_next_src_unique) 455 apply clarsimp 456 apply (rule conjI, clarsimp) 457 apply (clarsimp simp: valid_dlist_def2 [OF no_0]) 458 apply (clarsimp simp: mdb_prev_def slot) 459 apply (clarsimp simp: valid_dlist_def2 [OF no_0]) 460 done 461 462lemma caps_contained_n: 463 "caps_contained' n" 464 using valid 465 apply (clarsimp simp: valid_mdb_ctes_def caps_contained'_def) 466 apply (drule n_cap)+ 467 apply (clarsimp split: if_split_asm) 468 apply (erule disjE, clarsimp) 469 apply clarsimp 470 apply fastforce 471 done 472 473lemma chunked: 474 "mdb_chunked m" 475 using valid by (simp add: valid_mdb_ctes_def) 476 477lemma valid_badges: 478 "valid_badges m" 479 using valid .. 480 481lemma valid_badges_n: 482 "valid_badges n" 483proof - 484 from valid_badges 485 show ?thesis 486 apply (simp add: valid_badges_def2) 487 apply clarsimp 488 apply (drule_tac p=p in n_cap) 489 apply (frule n_cap) 490 apply (drule n_badged) 491 apply (clarsimp simp: n_next_eq) 492 apply (case_tac "p=slot", simp) 493 apply clarsimp 494 apply (case_tac "p'=slot", simp) 495 apply clarsimp 496 apply (case_tac "p = mdbPrev s_node") 497 apply clarsimp 498 apply (insert slot)[1] 499 (* using mdb_chunked to show cap in between is same as on either side *) 500 apply (subgoal_tac "capMasterCap s_cap = capMasterCap cap'") 501 prefer 2 502 apply (thin_tac "\<forall>p. P p" for P) 503 apply (drule mdb_chunked2D[OF chunked]) 504 apply (fastforce simp: mdb_next_unfold) 505 apply assumption+ 506 apply (simp add: sameRegionAs_def3) 507 apply (intro disjI1) 508 apply (fastforce simp:isCap_simps capMasterCap_def split:capability.splits) 509 apply clarsimp 510 apply clarsimp 511 apply (erule sameRegionAsE, auto simp: isCap_simps capMasterCap_def split:capability.splits)[1] 512 (* instantiating known valid_badges on both sides to transitively 513 give the link we need *) 514 apply (frule_tac x="mdbPrev s_node" in spec) 515 apply simp 516 apply (drule spec, drule spec, drule spec, 517 drule(1) mp, drule(1) mp) 518 apply simp 519 apply (drule_tac x=slot in spec) 520 apply (drule_tac x="mdbNext s_node" in spec) 521 apply simp 522 apply (drule mp, simp(no_asm) add: mdb_next_unfold) 523 apply simp 524 apply (cases "capBadge s_cap", simp_all)[1] 525 apply clarsimp 526 apply (case_tac "p' = mdbNext s_node") 527 apply clarsimp 528 apply (frule vdlist_next_src_unique[where y=slot]) 529 apply (simp add: mdb_next_unfold slot) 530 apply clarsimp 531 apply (rule dlist) 532 apply clarsimp 533 apply clarsimp 534 apply fastforce 535 done 536qed 537 538lemma p_not_slot: 539 assumes "n \<turnstile> p \<rightarrow> p'" 540 shows "p \<noteq> slot" 541 using assms 542 by induct (auto simp: mdb_next_unfold n_def modify_map_if) 543 544lemma to_slot_eq [simp]: 545 "m \<turnstile> p \<leadsto> slot = (p = mdbPrev s_node \<and> p \<noteq> 0)" 546 apply (rule iffI) 547 apply (frule dlist_nextD0, simp) 548 apply (clarsimp simp: mdb_prev_def slot mdb_next_unfold) 549 apply (clarsimp intro!: prev_slot_next) 550 done 551 552lemma n_parent_of: 553 "\<lbrakk> n \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot \<rbrakk> \<Longrightarrow> m \<turnstile> p parentOf p'" 554 apply (clarsimp simp: parentOf_def) 555 apply (case_tac cte, case_tac cte') 556 apply clarsimp 557 apply (frule_tac p=p in n_cap) 558 apply (frule_tac p=p in n_badged) 559 apply (drule_tac p=p in n_revokable) 560 apply (clarsimp) 561 apply (frule_tac p=p' in n_cap) 562 apply (frule_tac p=p' in n_badged) 563 apply (drule_tac p=p' in n_revokable) 564 apply (clarsimp split: if_split_asm; 565 clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong) 566 done 567 568lemma m_parent_of: 569 "\<lbrakk> m \<turnstile> p parentOf p'; p \<noteq> slot; p' \<noteq> slot; p\<noteq>p'; p'\<noteq>mdbNext s_node \<rbrakk> \<Longrightarrow> n \<turnstile> p parentOf p'" 570 apply (clarsimp simp add: parentOf_def) 571 apply (case_tac cte, case_tac cte') 572 apply clarsimp 573 apply (frule_tac p=p in m_cap) 574 apply (frule_tac p=p in m_badged) 575 apply (drule_tac p=p in m_revokable) 576 apply clarsimp 577 apply (frule_tac p=p' in m_cap) 578 apply (frule_tac p=p' in m_badged) 579 apply (drule_tac p=p' in m_revokable) 580 apply clarsimp 581 apply (simp split: if_split_asm; 582 clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong) 583 done 584 585lemma m_parent_of_next: 586 "\<lbrakk> m \<turnstile> p parentOf mdbNext s_node; m \<turnstile> p parentOf slot; p \<noteq> slot; p\<noteq>mdbNext s_node \<rbrakk> 587 \<Longrightarrow> n \<turnstile> p parentOf mdbNext s_node" 588 using slot 589 apply (clarsimp simp add: parentOf_def) 590 apply (case_tac cte'a, case_tac cte) 591 apply clarsimp 592 apply (frule_tac p=p in m_cap) 593 apply (frule_tac p=p in m_badged) 594 apply (drule_tac p=p in m_revokable) 595 apply (frule_tac p="mdbNext s_node" in m_cap) 596 apply (frule_tac p="mdbNext s_node" in m_badged) 597 apply (drule_tac p="mdbNext s_node" in m_revokable) 598 apply (frule_tac p="slot" in m_cap) 599 apply (frule_tac p="slot" in m_badged) 600 apply (drule_tac p="slot" in m_revokable) 601 apply (clarsimp simp: isMDBParentOf_def isCap_simps split: if_split_asm cong: if_cong) 602 done 603 604lemma parency_n: 605 assumes "n \<turnstile> p \<rightarrow> p'" 606 shows "m \<turnstile> p \<rightarrow> p' \<and> p \<noteq> slot \<and> p' \<noteq> slot" 607using assms 608proof induct 609 case (direct_parent c') 610 moreover 611 hence "p \<noteq> slot" 612 by (clarsimp simp: n_next_eq) 613 moreover 614 from direct_parent 615 have "c' \<noteq> slot" 616 by (clarsimp simp add: n_next_eq split: if_split_asm) 617 ultimately 618 show ?case 619 apply simp 620 apply (simp add: n_next_eq split: if_split_asm) 621 prefer 2 622 apply (erule (1) subtree.direct_parent) 623 apply (erule (2) n_parent_of) 624 apply clarsimp 625 apply (frule n_parent_of, simp, simp) 626 apply (rule subtree.trans_parent[OF _ m_slot_next], simp_all) 627 apply (rule subtree.direct_parent) 628 apply (erule prev_slot_next) 629 apply simp 630 apply (clarsimp simp: parentOf_def slot) 631 apply (case_tac cte'a) 632 apply (case_tac ctea) 633 apply clarsimp 634 apply (frule(2) mdb_chunked2D [OF chunked prev_slot_next m_slot_next]) 635 apply (clarsimp simp: isMDBParentOf_CTE) 636 apply simp 637 apply (simp add: slot) 638 apply (clarsimp simp add: isMDBParentOf_CTE) 639 apply (insert valid_badges) 640 apply (simp add: valid_badges_def2) 641 apply (drule spec[where x=slot]) 642 apply (drule spec[where x="mdbNext s_node"]) 643 apply (simp add: slot m_slot_next) 644 apply (insert valid_badges) 645 apply (simp add: valid_badges_def2) 646 apply (drule spec[where x="mdbPrev s_node"]) 647 apply (drule spec[where x=slot]) 648 apply (simp add: slot prev_slot_next) 649 apply (case_tac cte, case_tac cte') 650 apply (rename_tac cap'' node'') 651 apply (clarsimp simp: isMDBParentOf_CTE) 652 apply (frule n_cap, drule n_badged) 653 apply (frule n_cap, drule n_badged) 654 apply clarsimp 655 apply (case_tac cap'', simp_all add: isCap_simps)[1] 656 apply (clarsimp simp: sameRegionAs_def3 isCap_simps) 657 apply (clarsimp simp: sameRegionAs_def3 isCap_simps) 658 done 659next 660 case (trans_parent c c') 661 moreover 662 hence "p \<noteq> slot" 663 by (clarsimp simp: n_next_eq) 664 moreover 665 from trans_parent 666 have "c' \<noteq> slot" 667 by (clarsimp simp add: n_next_eq split: if_split_asm) 668 ultimately 669 show ?case 670 apply clarsimp 671 apply (simp add: n_next_eq split: if_split_asm) 672 prefer 2 673 apply (erule (2) subtree.trans_parent) 674 apply (erule n_parent_of, simp, simp) 675 apply clarsimp 676 apply (rule subtree.trans_parent) 677 apply (rule subtree.trans_parent, assumption) 678 apply (rule prev_slot_next) 679 apply clarsimp 680 apply clarsimp 681 apply (frule n_parent_of, simp, simp) 682 apply (clarsimp simp: parentOf_def slot) 683 apply (case_tac cte'a) 684 apply (rename_tac cap node) 685 apply (case_tac ctea) 686 apply clarsimp 687 apply (subgoal_tac "sameRegionAs cap s_cap") 688 prefer 2 689 apply (insert chunked)[1] 690 apply (simp add: mdb_chunked_def) 691 apply (erule_tac x="p" in allE) 692 apply (erule_tac x="mdbNext s_node" in allE) 693 apply simp 694 apply (drule isMDBParent_sameRegion)+ 695 apply clarsimp 696 apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ slot") 697 prefer 2 698 apply (rule trancl_trans) 699 apply (erule subtree_mdb_next) 700 apply (rule r_into_trancl) 701 apply (rule prev_slot_next) 702 apply clarsimp 703 apply (subgoal_tac "m \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node") 704 prefer 2 705 apply (erule trancl_trans) 706 apply fastforce 707 apply simp 708 apply (erule impE) 709 apply clarsimp 710 apply clarsimp 711 apply (thin_tac "s \<longrightarrow> t" for s t) 712 apply (simp add: is_chunk_def) 713 apply (erule_tac x=slot in allE) 714 apply (erule impE, fastforce) 715 apply (erule impE, fastforce) 716 apply (clarsimp simp: slot) 717 apply (clarsimp simp: isMDBParentOf_CTE) 718 apply (insert valid_badges, simp add: valid_badges_def2) 719 apply (drule spec[where x=slot], drule spec[where x="mdbNext s_node"]) 720 apply (simp add: slot m_slot_next) 721 apply (case_tac cte, case_tac cte') 722 apply (rename_tac cap'' node'') 723 apply (clarsimp simp: isMDBParentOf_CTE) 724 apply (frule n_cap, drule n_badged) 725 apply (frule n_cap, drule n_badged) 726 apply (clarsimp split: if_split_asm) 727 apply (drule subtree_mdb_next) 728 apply (drule no_loops_tranclE[OF no_loops]) 729 apply (erule notE, rule trancl_into_rtrancl) 730 apply (rule trancl.intros(2)[OF _ m_slot_next]) 731 apply (rule trancl.intros(1), rule prev_slot_next) 732 apply simp 733 apply (case_tac cap'', simp_all add: isCap_simps)[1] 734 apply (clarsimp simp: sameRegionAs_def3 isCap_simps) 735 apply (clarsimp simp: sameRegionAs_def3 isCap_simps) 736 apply (rule m_slot_next) 737 apply simp 738 apply (erule n_parent_of, simp, simp) 739 done 740qed 741 742lemma parency_m: 743 assumes "m \<turnstile> p \<rightarrow> p'" 744 shows "p \<noteq> slot \<longrightarrow> (if p' \<noteq> slot then n \<turnstile> p \<rightarrow> p' else m \<turnstile> p \<rightarrow> mdbNext s_node \<longrightarrow> n \<turnstile> p \<rightarrow> mdbNext s_node)" 745using assms 746proof induct 747 case (direct_parent c) 748 thus ?case 749 apply clarsimp 750 apply (rule conjI) 751 apply clarsimp 752 apply (rule subtree.direct_parent) 753 apply (simp add: n_next_eq) 754 apply clarsimp 755 apply (subgoal_tac "mdbPrev s_node \<noteq> 0") 756 prefer 2 757 apply (clarsimp simp: mdb_next_unfold) 758 apply (drule prev_slot_next) 759 apply (clarsimp simp: mdb_next_unfold) 760 apply assumption 761 apply (erule m_parent_of, simp, simp) 762 apply clarsimp 763 apply clarsimp 764 apply (drule dlist_next_src_unique) 765 apply fastforce 766 apply clarsimp 767 apply simp 768 apply clarsimp 769 apply (rule subtree.direct_parent) 770 apply (simp add: n_next_eq) 771 apply (drule subtree_parent) 772 apply (clarsimp simp: parentOf_def) 773 apply (drule subtree_parent) 774 apply (erule (1) m_parent_of_next) 775 apply clarsimp 776 apply clarsimp 777 done 778next 779 case (trans_parent c c') 780 thus ?case 781 apply clarsimp 782 apply (rule conjI) 783 apply clarsimp 784 apply (cases "c=slot") 785 apply simp 786 apply (erule impE) 787 apply (erule subtree.trans_parent) 788 apply fastforce 789 apply (clarsimp simp: slot mdb_next_unfold) 790 apply (clarsimp simp: slot mdb_next_unfold) 791 apply (clarsimp simp: slot mdb_next_unfold) 792 apply clarsimp 793 apply (erule subtree.trans_parent) 794 apply (simp add: n_next_eq) 795 apply clarsimp 796 apply (subgoal_tac "mdbPrev s_node \<noteq> 0") 797 prefer 2 798 apply (clarsimp simp: mdb_next_unfold) 799 apply (drule prev_slot_next) 800 apply (clarsimp simp: mdb_next_unfold) 801 apply assumption 802 apply (erule m_parent_of, simp, simp) 803 apply clarsimp 804 apply (drule subtree_mdb_next) 805 apply (drule trancl_trans) 806 apply (erule r_into_trancl) 807 apply simp 808 apply clarsimp 809 apply (drule dlist_next_src_unique) 810 apply fastforce 811 apply clarsimp 812 apply simp 813 apply clarsimp 814 apply (erule subtree.trans_parent) 815 apply (simp add: n_next_eq) 816 apply clarsimp 817 apply (rule m_parent_of_next, erule subtree_parent, assumption, assumption) 818 apply clarsimp 819 done 820qed 821 822lemma parency: 823 "n \<turnstile> p \<rightarrow> p' = (p \<noteq> slot \<and> p' \<noteq> slot \<and> m \<turnstile> p \<rightarrow> p')" 824 by (auto dest!: parency_n parency_m) 825 826lemma descendants: 827 "descendants_of' p n = 828 (if p = slot then {} else descendants_of' p m - {slot})" 829 by (auto simp add: parency descendants_of'_def) 830 831lemma n_tranclD: 832 "n \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> p' \<noteq> slot" 833 apply (erule trancl_induct) 834 apply (clarsimp simp add: n_next_eq split: if_split_asm) 835 apply (rule mdb_chain_0D) 836 apply (rule chain) 837 apply (clarsimp simp: slot) 838 apply (blast intro: trancl_trans prev_slot_next) 839 apply fastforce 840 apply (clarsimp simp: n_next_eq split: if_split_asm) 841 apply (erule trancl_trans) 842 apply (blast intro: trancl_trans prev_slot_next) 843 apply (fastforce intro: trancl_trans) 844 done 845 846lemma m_tranclD: 847 "m \<turnstile> p \<leadsto>\<^sup>+ p' \<Longrightarrow> 848 if p = slot then n \<turnstile> mdbNext s_node \<leadsto>\<^sup>* p' 849 else if p' = slot then n \<turnstile> p \<leadsto>\<^sup>+ mdbNext s_node 850 else n \<turnstile> p \<leadsto>\<^sup>+ p'" 851 using no_0_n 852 apply - 853 apply (erule trancl_induct) 854 apply clarsimp 855 apply (rule conjI) 856 apply clarsimp 857 apply (rule r_into_trancl) 858 apply (clarsimp simp: n_next_eq) 859 apply clarsimp 860 apply (rule conjI) 861 apply (insert m_slot_next)[1] 862 apply (clarsimp simp: mdb_next_unfold) 863 apply clarsimp 864 apply (rule r_into_trancl) 865 apply (clarsimp simp: n_next_eq) 866 apply (rule context_conjI) 867 apply (clarsimp simp: mdb_next_unfold) 868 apply (drule prev_slot_next) 869 apply (clarsimp simp: mdb_next_unfold) 870 apply clarsimp 871 apply (rule conjI) 872 apply clarsimp 873 apply (rule conjI) 874 apply clarsimp 875 apply (drule prev_slot_next) 876 apply (drule trancl_trans, erule r_into_trancl) 877 apply simp 878 apply clarsimp 879 apply (erule trancl_trans) 880 apply (rule r_into_trancl) 881 apply (simp add: n_next_eq) 882 apply clarsimp 883 apply (rule conjI) 884 apply clarsimp 885 apply (erule rtrancl_trans) 886 apply (rule r_into_rtrancl) 887 apply (simp add: n_next_eq) 888 apply (rule conjI) 889 apply clarsimp 890 apply (rule context_conjI) 891 apply (clarsimp simp: mdb_next_unfold) 892 apply (drule prev_slot_next) 893 apply (clarsimp simp: mdb_next_unfold) 894 apply clarsimp 895 apply clarsimp 896 apply (simp split: if_split_asm) 897 apply (clarsimp simp: mdb_next_unfold slot) 898 apply (erule trancl_trans) 899 apply (rule r_into_trancl) 900 apply (clarsimp simp add: n_next_eq) 901 apply (rule context_conjI) 902 apply (clarsimp simp: mdb_next_unfold) 903 apply (drule prev_slot_next) 904 apply (clarsimp simp: mdb_next_unfold) 905 done 906 907lemma n_trancl_eq: 908 "n \<turnstile> p \<leadsto>\<^sup>+ p' = (m \<turnstile> p \<leadsto>\<^sup>+ p' \<and> (p = slot \<longrightarrow> p' = 0) \<and> p' \<noteq> slot)" 909 using no_0_n 910 apply - 911 apply (rule iffI) 912 apply (frule n_tranclD) 913 apply clarsimp 914 apply (drule tranclD) 915 apply (clarsimp simp: n_next_eq) 916 apply (simp add: rtrancl_eq_or_trancl) 917 apply clarsimp 918 apply (drule m_tranclD) 919 apply (simp split: if_split_asm) 920 apply (rule r_into_trancl) 921 apply (simp add: n_next_eq) 922 done 923 924lemma n_rtrancl_eq: 925 "n \<turnstile> p \<leadsto>\<^sup>* p' = 926 (m \<turnstile> p \<leadsto>\<^sup>* p' \<and> 927 (p = slot \<longrightarrow> p' = 0 \<or> p' = slot) \<and> 928 (p' = slot \<longrightarrow> p = slot))" 929 by (auto simp: rtrancl_eq_or_trancl n_trancl_eq) 930 931lemma mdb_chain_0_n: 932 "mdb_chain_0 n" 933 using chain 934 apply (clarsimp simp: mdb_chain_0_def) 935 apply (drule bspec) 936 apply (fastforce simp: n_def modify_map_if split: if_split_asm) 937 apply (simp add: n_trancl_eq) 938 done 939 940lemma mdb_chunked_n: 941 "mdb_chunked n" 942 using chunked 943 apply (clarsimp simp: mdb_chunked_def) 944 apply (drule n_cap)+ 945 apply (clarsimp split: if_split_asm) 946 apply (case_tac "p=slot", clarsimp) 947 apply clarsimp 948 apply (erule_tac x=p in allE) 949 apply (erule_tac x=p' in allE) 950 apply (clarsimp simp: is_chunk_def) 951 apply (simp add: n_trancl_eq n_rtrancl_eq) 952 apply (rule conjI) 953 apply clarsimp 954 apply (erule_tac x=p'' in allE) 955 apply clarsimp 956 apply (drule_tac p=p'' in m_cap) 957 apply clarsimp 958 apply clarsimp 959 apply (erule_tac x=p'' in allE) 960 apply clarsimp 961 apply (drule_tac p=p'' in m_cap) 962 apply clarsimp 963 done 964 965lemma untyped_mdb_n: 966 "untyped_mdb' n" 967 using untyped_mdb 968 apply (simp add: untyped_mdb'_def descendants_of'_def parency) 969 apply clarsimp 970 apply (drule n_cap)+ 971 apply (clarsimp split: if_split_asm) 972 apply (case_tac "p=slot", simp) 973 apply clarsimp 974 done 975 976lemma untyped_inc_n: 977 "untyped_inc' n" 978 using untyped_inc 979 apply (simp add: untyped_inc'_def descendants_of'_def parency) 980 apply clarsimp 981 apply (drule n_cap)+ 982 apply (clarsimp split: if_split_asm) 983 apply (case_tac "p=slot", simp) 984 apply clarsimp 985 apply (erule_tac x=p in allE) 986 apply (erule_tac x=p' in allE) 987 apply simp 988 done 989 990lemmas vn_prev [dest!] = valid_nullcaps_prev [OF _ slot no_0 dlist nullcaps] 991lemmas vn_next [dest!] = valid_nullcaps_next [OF _ slot no_0 dlist nullcaps] 992 993lemma nullcaps_n: "valid_nullcaps n" 994proof - 995 from valid have "valid_nullcaps m" .. 996 thus ?thesis 997 apply (clarsimp simp: valid_nullcaps_def nullMDBNode_def nullPointer_def) 998 apply (frule n_cap) 999 apply (frule n_next) 1000 apply (frule n_badged) 1001 apply (frule n_revokable) 1002 apply (drule n_prev) 1003 apply (case_tac n) 1004 apply (insert slot) 1005 apply (fastforce split: if_split_asm) 1006 done 1007qed 1008 1009lemma ut_rev_n: "ut_revocable' n" 1010 apply(insert valid) 1011 apply(clarsimp simp: ut_revocable'_def) 1012 apply(frule n_cap) 1013 apply(drule n_revokable) 1014 apply(clarsimp simp: isCap_simps split: if_split_asm) 1015 apply(simp add: valid_mdb_ctes_def ut_revocable'_def) 1016 done 1017 1018lemma class_links_n: "class_links n" 1019 using valid slot 1020 apply (clarsimp simp: valid_mdb_ctes_def class_links_def) 1021 apply (case_tac cte, case_tac cte') 1022 apply (drule n_nextD) 1023 apply (clarsimp simp: split: if_split_asm) 1024 apply (simp add: no_0_n) 1025 apply (drule n_cap)+ 1026 apply clarsimp 1027 apply (frule spec[where x=slot], 1028 drule spec[where x="mdbNext s_node"], 1029 simp, simp add: m_slot_next) 1030 apply (drule spec[where x="mdbPrev s_node"], 1031 drule spec[where x=slot], simp) 1032 apply (drule n_cap)+ 1033 apply clarsimp 1034 apply (fastforce split: if_split_asm) 1035 done 1036 1037lemma distinct_zombies_m: "distinct_zombies m" 1038 using valid by (simp add: valid_mdb_ctes_def) 1039 1040lemma distinct_zombies_n[simp]: 1041 "distinct_zombies n" 1042 using distinct_zombies_m 1043 apply (simp add: n_def distinct_zombies_nonCTE_modify_map) 1044 apply (subst modify_map_apply[where p=slot]) 1045 apply (simp add: modify_map_def slot) 1046 apply simp 1047 apply (rule distinct_zombies_sameMasterE) 1048 apply (simp add: distinct_zombies_nonCTE_modify_map) 1049 apply (simp add: modify_map_def slot) 1050 apply simp 1051 done 1052 1053lemma irq_control_n [simp]: "irq_control n" 1054 using slot 1055 apply (clarsimp simp: irq_control_def) 1056 apply (frule n_revokable) 1057 apply (drule n_cap) 1058 apply (clarsimp split: if_split_asm) 1059 apply (frule irq_revocable, rule irq_control) 1060 apply clarsimp 1061 apply (drule n_cap) 1062 apply (clarsimp simp: if_split_asm) 1063 apply (erule (1) irq_controlD, rule irq_control) 1064 done 1065 1066lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m" 1067 using valid by auto 1068 1069lemma reply_masters_rvk_fb_n [simp]: "reply_masters_rvk_fb n" 1070 using reply_masters_rvk_fb_m 1071 apply (simp add: reply_masters_rvk_fb_def n_def 1072 ball_ran_modify_map_eq 1073 modify_map_comp[symmetric]) 1074 apply (subst ball_ran_modify_map_eq) 1075 apply (frule bspec, rule ranI, rule slot) 1076 apply (simp add: nullMDBNode_def isCap_simps modify_map_def 1077 slot) 1078 apply (subst ball_ran_modify_map_eq) 1079 apply (clarsimp simp add: modify_map_def) 1080 apply fastforce 1081 apply (simp add: ball_ran_modify_map_eq) 1082 done 1083 1084lemma vmdb_n: "valid_mdb_ctes n" 1085 by (simp add: valid_mdb_ctes_def valid_dlist_n 1086 no_0_n mdb_chain_0_n valid_badges_n 1087 caps_contained_n mdb_chunked_n 1088 untyped_mdb_n untyped_inc_n 1089 nullcaps_n ut_rev_n class_links_n) 1090 1091end 1092 1093context begin interpretation Arch . 1094crunch ctes_of[wp]: postCapDeletion, clearUntypedFreeIndex "\<lambda>s. P (ctes_of s)" 1095 1096lemma emptySlot_mdb [wp]: 1097 "\<lbrace>valid_mdb'\<rbrace> 1098 emptySlot sl opt 1099 \<lbrace>\<lambda>_. valid_mdb'\<rbrace>" 1100 unfolding emptySlot_def 1101 apply (simp only: case_Null_If valid_mdb'_def) 1102 apply (wp updateCap_ctes_of_wp getCTE_wp' 1103 opt_return_pres_lift | simp add: cte_wp_at_ctes_of)+ 1104 apply (clarsimp) 1105 apply (case_tac cte) 1106 apply (rename_tac cap node) 1107 apply (simp) 1108 apply (subgoal_tac "mdb_empty (ctes_of s) sl cap node") 1109 prefer 2 1110 apply (rule mdb_empty.intro) 1111 apply (rule mdb_ptr.intro) 1112 apply (rule vmdb.intro) 1113 apply (simp add: valid_mdb_ctes_def) 1114 apply (rule mdb_ptr_axioms.intro) 1115 apply (simp add: cte_wp_at_ctes_of) 1116 apply (rule conjI, clarsimp simp: valid_mdb_ctes_def) 1117 apply (erule mdb_empty.vmdb_n[unfolded const_def]) 1118 done 1119end 1120 1121lemma if_live_then_nonz_cap'_def2: 1122 "if_live_then_nonz_cap' = (\<lambda>s. \<forall>ptr. ko_wp_at' live' ptr s 1123 \<longrightarrow> (\<exists>p zr. (option_map zobj_refs' o cteCaps_of s) p = Some zr \<and> ptr \<in> zr))" 1124 by (fastforce intro!: ext 1125 simp: if_live_then_nonz_cap'_def ex_nonz_cap_to'_def 1126 cte_wp_at_ctes_of cteCaps_of_def) 1127 1128lemma updateMDB_ko_wp_at_live[wp]: 1129 "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> 1130 updateMDB p m 1131 \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>" 1132 unfolding updateMDB_def Let_def 1133 apply (rule hoare_pre, wp) 1134 apply simp 1135 done 1136 1137lemma updateCap_ko_wp_at_live[wp]: 1138 "\<lbrace>\<lambda>s. P (ko_wp_at' live' p' s)\<rbrace> 1139 updateCap p cap 1140 \<lbrace>\<lambda>rv s. P (ko_wp_at' live' p' s)\<rbrace>" 1141 unfolding updateCap_def 1142 by wp 1143 1144primrec 1145 threadCapRefs :: "capability \<Rightarrow> word32 set" 1146where 1147 "threadCapRefs (ThreadCap r) = {r}" 1148| "threadCapRefs (ReplyCap t m) = {}" 1149| "threadCapRefs NullCap = {}" 1150| "threadCapRefs (UntypedCap d r n i) = {}" 1151| "threadCapRefs (EndpointCap r badge x y z) = {}" 1152| "threadCapRefs (NotificationCap r badge x y) = {}" 1153| "threadCapRefs (CNodeCap r b g gsz) = {}" 1154| "threadCapRefs (Zombie r b n) = {}" 1155| "threadCapRefs (ArchObjectCap ac) = {}" 1156| "threadCapRefs (IRQHandlerCap irq) = {}" 1157| "threadCapRefs (IRQControlCap) = {}" 1158| "threadCapRefs (DomainCap) = {}" 1159 1160lemma threadCapRefs_def2: 1161 "threadCapRefs cap = (case cap of ThreadCap r \<Rightarrow> {r} | _ \<Rightarrow> {})" 1162 by (simp split: capability.split) 1163 1164definition 1165 "isFinal cap p m \<equiv> 1166 \<not>isUntypedCap cap \<and> 1167 (\<forall>p' c. m p' = Some c \<longrightarrow> 1168 p \<noteq> p' \<longrightarrow> \<not>isUntypedCap c \<longrightarrow> 1169 \<not> sameObjectAs cap c)" 1170 1171lemma not_FinalE: 1172 "\<lbrakk> \<not> isFinal cap sl cps; isUntypedCap cap \<Longrightarrow> P; 1173 \<And>p c. \<lbrakk> cps p = Some c; p \<noteq> sl; \<not> isUntypedCap c; sameObjectAs cap c \<rbrakk> \<Longrightarrow> P 1174 \<rbrakk> \<Longrightarrow> P" 1175 by (fastforce simp: isFinal_def) 1176 1177definition 1178 "removeable' sl \<equiv> \<lambda>s cap. 1179 (\<exists>p. p \<noteq> sl \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap cap) p s) 1180 \<or> ((\<forall>p \<in> cte_refs' cap (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = NullCap) p s) 1181 \<and> (\<forall>p \<in> zobj_refs' cap. ko_wp_at' (Not \<circ> live') p s) 1182 \<and> (\<forall>t \<in> threadCapRefs cap. \<forall>p. t \<notin> set (ksReadyQueues s p)))" 1183 1184lemma not_Final_removeable: 1185 "\<not> isFinal cap sl (cteCaps_of s) 1186 \<Longrightarrow> removeable' sl s cap" 1187 apply (erule not_FinalE) 1188 apply (clarsimp simp: removeable'_def isCap_simps) 1189 apply (clarsimp simp: cteCaps_of_def sameObjectAs_def2 removeable'_def 1190 cte_wp_at_ctes_of) 1191 apply fastforce 1192 done 1193 1194context begin interpretation Arch . 1195crunch ko_wp_at'[wp]: postCapDeletion "\<lambda>s. P (ko_wp_at' P' p s)" 1196crunch cteCaps_of[wp]: postCapDeletion "\<lambda>s. P (cteCaps_of s)" 1197 (simp: cteCaps_of_def o_def) 1198end 1199 1200crunch ko_at_live[wp]: clearUntypedFreeIndex "\<lambda>s. P (ko_wp_at' live' ptr s)" 1201 1202lemma clearUntypedFreeIndex_cteCaps_of[wp]: 1203 "\<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> 1204 clearUntypedFreeIndex sl \<lbrace>\<lambda>y s. P (cteCaps_of s)\<rbrace>" 1205 by (simp add: cteCaps_of_def, wp) 1206 1207lemma emptySlot_iflive'[wp]: 1208 "\<lbrace>\<lambda>s. if_live_then_nonz_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace> 1209 emptySlot sl opt 1210 \<lbrace>\<lambda>rv. if_live_then_nonz_cap'\<rbrace>" 1211 apply (simp add: emptySlot_def case_Null_If if_live_then_nonz_cap'_def2 1212 del: comp_apply) 1213 apply (rule hoare_pre) 1214 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift 1215 getCTE_wp opt_return_pres_lift 1216 clearUntypedFreeIndex_ctes_of 1217 clearUntypedFreeIndex_cteCaps_of 1218 hoare_vcg_ex_lift 1219 | wp_once hoare_vcg_imp_lift 1220 | simp add: cte_wp_at_ctes_of del: comp_apply)+ 1221 apply (clarsimp simp: modify_map_same 1222 imp_conjR[symmetric]) 1223 apply (drule spec, drule(1) mp) 1224 apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def split: if_split_asm) 1225 apply (case_tac "p \<noteq> sl") 1226 apply blast 1227 apply (simp add: removeable'_def cteCaps_of_def) 1228 apply (erule disjE) 1229 apply (clarsimp simp: cte_wp_at_ctes_of modify_map_def 1230 dest!: capMaster_same_refs) 1231 apply fastforce 1232 apply clarsimp 1233 apply (drule(1) bspec) 1234 apply (clarsimp simp: ko_wp_at'_def) 1235 done 1236 1237crunch irq_node'[wp]: doMachineOp "\<lambda>s. P (irq_node' s)" 1238 1239lemma setIRQState_irq_node'[wp]: 1240 "\<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> setIRQState state irq \<lbrace>\<lambda>_ s. P (irq_node' s)\<rbrace>" 1241 apply (simp add: setIRQState_def setInterruptState_def getInterruptState_def) 1242 apply wp 1243 apply simp 1244 done 1245 1246context begin interpretation Arch . 1247crunch irq_node'[wp]: emptySlot "\<lambda>s. P (irq_node' s)" 1248end 1249 1250lemma emptySlot_ifunsafe'[wp]: 1251 "\<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace> 1252 emptySlot sl opt 1253 \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" 1254 apply (simp add: ifunsafe'_def3) 1255 apply (rule hoare_pre, rule hoare_use_eq_irq_node'[OF emptySlot_irq_node']) 1256 apply (simp add: emptySlot_def case_Null_If) 1257 apply (wp opt_return_pres_lift | simp add: o_def)+ 1258 apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of)+ 1259 apply (clarsimp simp: tree_cte_cteCap_eq[unfolded o_def] 1260 modify_map_same 1261 modify_map_comp[symmetric] 1262 split: option.split_asm if_split_asm 1263 dest!: modify_map_K_D) 1264 apply (clarsimp simp: modify_map_def) 1265 apply (drule_tac x=cref in spec, clarsimp) 1266 apply (case_tac "cref' \<noteq> sl") 1267 apply (rule_tac x=cref' in exI) 1268 apply (clarsimp simp: modify_map_def) 1269 apply (simp add: removeable'_def) 1270 apply (erule disjE) 1271 apply (clarsimp simp: modify_map_def) 1272 apply (subst(asm) tree_cte_cteCap_eq[unfolded o_def]) 1273 apply (clarsimp split: option.split_asm dest!: capMaster_same_refs) 1274 apply fastforce 1275 apply clarsimp 1276 apply (drule(1) bspec) 1277 apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) 1278 done 1279 1280lemma ex_nonz_cap_to'_def2: 1281 "ex_nonz_cap_to' p = (\<lambda>s. \<exists>p' c. cteCaps_of s p' = Some c \<and> p \<in> zobj_refs' c)" 1282 by (fastforce simp: ex_nonz_cap_to'_def cte_wp_at_ctes_of cteCaps_of_def 1283 intro!: ext) 1284 1285lemma ctes_of_valid'[elim]: 1286 "\<lbrakk>ctes_of s p = Some cte; valid_objs' s\<rbrakk> \<Longrightarrow> s \<turnstile>' cteCap cte" 1287 by (cases cte, simp) (rule ctes_of_valid_cap') 1288 1289crunch ksrq[wp]: postCapDeletion "\<lambda>s. P (ksReadyQueues s)" 1290 1291crunch valid_idle'[wp]: setInterruptState "valid_idle'" 1292 (simp: valid_idle'_def) 1293 1294context begin interpretation Arch . 1295crunch valid_idle'[wp]: emptySlot "valid_idle'" 1296 1297crunch ksArch[wp]: emptySlot "\<lambda>s. P (ksArchState s)" 1298crunch ksIdle[wp]: emptySlot "\<lambda>s. P (ksIdleThread s)" 1299crunch gsMaxObjectSize[wp]: emptySlot "\<lambda>s. P (gsMaxObjectSize s)" 1300end 1301 1302lemma emptySlot_cteCaps_of: 1303 "\<lbrace>\<lambda>s. P (cteCaps_of s(p \<mapsto> NullCap))\<rbrace> 1304 emptySlot p opt 1305 \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" 1306 apply (simp add: emptySlot_def case_Null_If) 1307 apply (wp opt_return_pres_lift getCTE_cteCap_wp 1308 clearUntypedFreeIndex_cteCaps_of) 1309 apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of) 1310 apply (auto elim!: rsubst[where P=P] 1311 simp: modify_map_def fun_upd_def[symmetric] o_def 1312 fun_upd_idem cteCaps_of_def 1313 split: option.splits) 1314 done 1315 1316lemma emptySlot_valid_global_refs[wp]: 1317 "\<lbrace>valid_global_refs' and cte_at' sl\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_global_refs'\<rbrace>" 1318 apply (simp add: valid_global_refs'_def global_refs'_def) 1319 apply (rule hoare_pre) 1320 apply (rule hoare_use_eq_irq_node' [OF emptySlot_irq_node']) 1321 apply (rule hoare_use_eq [where f=ksArchState, OF emptySlot_ksArch]) 1322 apply (rule hoare_use_eq [where f=ksIdleThread, OF emptySlot_ksIdle]) 1323 apply (rule hoare_use_eq [where f=gsMaxObjectSize], wp) 1324 apply (simp add: valid_refs'_cteCaps valid_cap_sizes_cteCaps) 1325 apply (rule emptySlot_cteCaps_of) 1326 apply (clarsimp simp: cte_wp_at_ctes_of) 1327 apply (frule(1) cte_at_valid_cap_sizes_0) 1328 apply (clarsimp simp: valid_refs'_cteCaps valid_cap_sizes_cteCaps ball_ran_eq) 1329 done 1330 1331lemmas doMachineOp_irq_handlers[wp] 1332 = valid_irq_handlers_lift'' [OF doMachineOp_ctes doMachineOp_ksInterruptState] 1333 1334lemma deletedIRQHandler_irq_handlers'[wp]: 1335 "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (IRQHandlerCap irq \<notin> ran (cteCaps_of s))\<rbrace> 1336 deletedIRQHandler irq 1337 \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" 1338 apply (simp add: deletedIRQHandler_def setIRQState_def setInterruptState_def getInterruptState_def) 1339 apply wp 1340 apply (clarsimp simp: valid_irq_handlers'_def irq_issued'_def ran_def cteCaps_of_def) 1341 done 1342 1343context begin interpretation Arch . 1344 1345lemma postCapDeletion_irq_handlers'[wp]: 1346 "\<lbrace>\<lambda>s. valid_irq_handlers' s \<and> (cap \<noteq> NullCap \<longrightarrow> cap \<notin> ran (cteCaps_of s))\<rbrace> 1347 postCapDeletion cap 1348 \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" 1349 by (wpsimp simp: Retype_H.postCapDeletion_def ARM_H.postCapDeletion_def) 1350 1351end 1352 1353crunch ksInterruptState[wp]: clearUntypedFreeIndex "\<lambda>s. P (ksInterruptState s)" 1354 1355lemma emptySlot_valid_irq_handlers'[wp]: 1356 "\<lbrace>\<lambda>s. valid_irq_handlers' s 1357 \<and> (\<forall>sl'. info \<noteq> NullCap \<longrightarrow> sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)\<rbrace> 1358 emptySlot sl info 1359 \<lbrace>\<lambda>rv. valid_irq_handlers'\<rbrace>" 1360 apply (simp add: emptySlot_def case_Null_If) 1361 apply (wp | wpc)+ 1362 apply (unfold valid_irq_handlers'_def irq_issued'_def) 1363 apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of 1364 | wps clearUntypedFreeIndex_ksInterruptState)+ 1365 apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of ran_def modify_map_def 1366 split: option.split) 1367 apply auto 1368 done 1369 1370declare setIRQState_irq_states' [wp] 1371 1372context begin interpretation Arch . 1373crunch irq_states' [wp]: emptySlot valid_irq_states' 1374 1375crunch no_0_obj' [wp]: emptySlot no_0_obj' 1376 (wp: crunch_wps) 1377 1378crunch valid_queues'[wp]: setInterruptState "valid_queues'" 1379 (simp: valid_queues'_def) 1380 1381crunch valid_queues'[wp]: emptySlot "valid_queues'" 1382 1383crunch pde_mappings'[wp]: emptySlot "valid_pde_mappings'" 1384end 1385 1386lemma deletedIRQHandler_irqs_masked'[wp]: 1387 "\<lbrace>irqs_masked'\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. irqs_masked'\<rbrace>" 1388 apply (simp add: deletedIRQHandler_def setIRQState_def getInterruptState_def setInterruptState_def) 1389 apply (wp dmo_maskInterrupt) 1390 apply (simp add: irqs_masked'_def) 1391 done 1392 1393context begin interpretation Arch . (*FIXME: arch_split*) 1394crunch irqs_masked'[wp]: emptySlot "irqs_masked'" 1395 1396lemma setIRQState_umm: 1397 "\<lbrace>\<lambda>s. P (underlying_memory (ksMachineState s))\<rbrace> 1398 setIRQState irqState irq 1399 \<lbrace>\<lambda>_ s. P (underlying_memory (ksMachineState s))\<rbrace>" 1400 by (simp add: setIRQState_def maskInterrupt_def 1401 setInterruptState_def getInterruptState_def 1402 | wp dmo_lift')+ 1403 1404crunch umm[wp]: emptySlot "\<lambda>s. P (underlying_memory (ksMachineState s))" 1405 (wp: setIRQState_umm) 1406 1407lemma emptySlot_vms'[wp]: 1408 "\<lbrace>valid_machine_state'\<rbrace> emptySlot slot irq \<lbrace>\<lambda>_. valid_machine_state'\<rbrace>" 1409 by (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) 1410 (wp hoare_vcg_all_lift hoare_vcg_disj_lift) 1411 1412crunch pspace_domain_valid[wp]: emptySlot "pspace_domain_valid" 1413 1414lemma ct_not_inQ_ksInterruptState_update[simp]: 1415 "ct_not_inQ (s\<lparr>ksInterruptState := v\<rparr>) = ct_not_inQ s" 1416 by (simp add: ct_not_inQ_def) 1417 1418crunch nosch[wp]: emptySlot "\<lambda>s. P (ksSchedulerAction s)" 1419crunch ct[wp]: emptySlot "\<lambda>s. P (ksCurThread s)" 1420crunch ksCurDomain[wp]: emptySlot "\<lambda>s. P (ksCurDomain s)" 1421crunch ksDomSchedule[wp]: emptySlot "\<lambda>s. P (ksDomSchedule s)" 1422crunch ksDomScheduleIdx[wp]: emptySlot "\<lambda>s. P (ksDomScheduleIdx s)" 1423 1424lemma deletedIRQHandler_ct_not_inQ[wp]: 1425 "\<lbrace>ct_not_inQ\<rbrace> deletedIRQHandler irq \<lbrace>\<lambda>_. ct_not_inQ\<rbrace>" 1426 apply (rule ct_not_inQ_lift [OF deletedIRQHandler_nosch]) 1427 apply (rule hoare_weaken_pre) 1428 apply (wps deletedIRQHandler_ct) 1429 apply (simp add: deletedIRQHandler_def setIRQState_def) 1430 apply (wp) 1431 apply (simp add: comp_def) 1432 done 1433 1434crunch ct_not_inQ[wp]: emptySlot "ct_not_inQ" 1435 1436crunch tcbDomain[wp]: emptySlot "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t" 1437 1438lemma emptySlot_ct_idle_or_in_cur_domain'[wp]: 1439 "\<lbrace>ct_idle_or_in_cur_domain'\<rbrace> emptySlot sl opt \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" 1440apply (wp ct_idle_or_in_cur_domain'_lift2 tcb_in_cur_domain'_lift | simp)+ 1441done 1442 1443crunch gsUntypedZeroRanges[wp]: postCapDeletion "\<lambda>s. P (gsUntypedZeroRanges s)" 1444 (wp: crunch_wps simp: crunch_simps) 1445 1446lemma untypedZeroRange_modify_map_isUntypedCap: 1447 "m sl = Some v \<Longrightarrow> \<not> isUntypedCap v \<Longrightarrow> \<not> isUntypedCap (f v) 1448 \<Longrightarrow> (untypedZeroRange \<circ>\<^sub>m modify_map m sl f) = (untypedZeroRange \<circ>\<^sub>m m)" 1449 by (simp add: modify_map_def map_comp_def fun_eq_iff untypedZeroRange_def) 1450 1451lemma emptySlot_untyped_ranges[wp]: 1452 "\<lbrace>untyped_ranges_zero' and valid_objs' and valid_mdb'\<rbrace> 1453 emptySlot sl opt \<lbrace>\<lambda>rv. untyped_ranges_zero'\<rbrace>" 1454 apply (simp add: emptySlot_def case_Null_If) 1455 apply (rule hoare_pre) 1456 apply (rule hoare_seq_ext) 1457 apply (rule untyped_ranges_zero_lift) 1458 apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of 1459 | wpc | simp add: clearUntypedFreeIndex_def updateTrackedFreeIndex_def 1460 getSlotCap_def 1461 split: option.split)+ 1462 apply (clarsimp simp: modify_map_comp[symmetric] modify_map_same) 1463 apply (case_tac "\<not> isUntypedCap (the (cteCaps_of s sl))") 1464 apply (case_tac "the (cteCaps_of s sl)", 1465 simp_all add: untyped_ranges_zero_inv_def 1466 untypedZeroRange_modify_map_isUntypedCap isCap_simps)[1] 1467 apply (clarsimp simp: isCap_simps untypedZeroRange_def modify_map_def) 1468 apply (strengthen untyped_ranges_zero_fun_upd[mk_strg I E]) 1469 apply simp 1470 apply (simp add: untypedZeroRange_def isCap_simps) 1471 done 1472 1473lemma emptySlot_invs'[wp]: 1474 "\<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s 1475 \<and> (\<forall>sl'. info \<noteq> NullCap \<longrightarrow> sl' \<noteq> sl \<longrightarrow> cteCaps_of s sl' \<noteq> Some info)\<rbrace> 1476 emptySlot sl info 1477 \<lbrace>\<lambda>rv. invs'\<rbrace>" 1478 apply (simp add: invs'_def valid_state'_def valid_pspace'_def) 1479 apply (rule hoare_pre) 1480 apply (wp valid_arch_state_lift' valid_irq_node_lift cur_tcb_lift) 1481 apply (clarsimp simp: cte_wp_at_ctes_of) 1482 done 1483 1484lemma deleted_irq_corres: 1485 "corres dc \<top> \<top> 1486 (deleted_irq_handler irq) 1487 (deletedIRQHandler irq)" 1488 apply (simp add: deleted_irq_handler_def deletedIRQHandler_def) 1489 apply (rule set_irq_state_corres) 1490 apply (simp add: irq_state_relation_def) 1491 done 1492 1493lemma arch_post_cap_deletion_corres: 1494 "acap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (arch_post_cap_deletion cap) (ARM_H.postCapDeletion cap')" 1495 by (corressimp simp: arch_post_cap_deletion_def ARM_H.postCapDeletion_def) 1496 1497lemma post_cap_deletion_corres: 1498 "cap_relation cap cap' \<Longrightarrow> corres dc \<top> \<top> (post_cap_deletion cap) (postCapDeletion cap')" 1499 apply (cases cap; clarsimp simp: post_cap_deletion_def Retype_H.postCapDeletion_def) 1500 apply (corressimp corres: deleted_irq_corres) 1501 by (corressimp corres: arch_post_cap_deletion_corres) 1502 1503lemma exec_update_cdt_list: 1504 "\<lbrakk>\<exists>x\<in>fst (g r (s\<lparr>cdt_list := (f (cdt_list s))\<rparr>)). P x\<rbrakk> 1505\<Longrightarrow> \<exists>x\<in>fst (((update_cdt_list f) >>= g) (s::det_state)). P x" 1506 apply (clarsimp simp: update_cdt_list_def set_cdt_list_def exec_gets exec_get put_def bind_assoc) 1507 apply (clarsimp simp: bind_def) 1508 apply (erule bexI) 1509 apply simp 1510 done 1511 1512lemma set_cap_trans_state: 1513 "((),s') \<in> fst (set_cap c p s) \<Longrightarrow> ((),trans_state f s') \<in> fst (set_cap c p (trans_state f s))" 1514 apply (cases p) 1515 apply (clarsimp simp add: set_cap_def in_monad get_object_def) 1516 apply (case_tac y) 1517 apply (auto simp add: in_monad set_object_def split: if_split_asm) 1518 done 1519 1520lemma clearUntypedFreeIndex_corres_noop: 1521 "corres dc \<top> (cte_at' (cte_map slot)) 1522 (return ()) (clearUntypedFreeIndex (cte_map slot))" 1523 apply (simp add: clearUntypedFreeIndex_def) 1524 apply (rule corres_guard_imp) 1525 apply (rule corres_bind_return2) 1526 apply (rule corres_symb_exec_r_conj[where P'="cte_at' (cte_map slot)"]) 1527 apply (rule corres_trivial, simp) 1528 apply (wp getCTE_wp' | wpc 1529 | simp add: updateTrackedFreeIndex_def getSlotCap_def)+ 1530 apply (clarsimp simp: state_relation_def) 1531 apply (rule no_fail_pre) 1532 apply (wp no_fail_getSlotCap getCTE_wp' 1533 | wpc | simp add: updateTrackedFreeIndex_def getSlotCap_def)+ 1534 done 1535 1536lemma clearUntypedFreeIndex_valid_pspace'[wp]: 1537 "\<lbrace>valid_pspace'\<rbrace> clearUntypedFreeIndex slot \<lbrace>\<lambda>rv. valid_pspace'\<rbrace>" 1538 apply (simp add: valid_pspace'_def) 1539 apply (rule hoare_pre) 1540 apply (wp | simp add: valid_mdb'_def)+ 1541 done 1542 1543lemma empty_slot_corres: 1544 "cap_relation info info' \<Longrightarrow> corres dc (einvs and cte_at slot) (invs' and cte_at' (cte_map slot)) 1545 (empty_slot slot info) (emptySlot (cte_map slot) info')" 1546 unfolding emptySlot_def empty_slot_def 1547 apply (simp add: case_Null_If) 1548 apply (rule corres_guard_imp) 1549 apply (rule corres_split_noop_rhs[OF _ clearUntypedFreeIndex_corres_noop]) 1550 apply (rule_tac R="\<lambda>cap. einvs and cte_wp_at ((=) cap) slot" and 1551 R'="\<lambda>cte. valid_pspace' and cte_wp_at' ((=) cte) (cte_map slot)" in 1552 corres_split [OF _ get_cap_corres]) 1553 defer 1554 apply (wp get_cap_wp getCTE_wp')+ 1555 apply (simp add: cte_wp_at_ctes_of) 1556 apply (wp hoare_vcg_imp_lift clearUntypedFreeIndex_valid_pspace') 1557 apply fastforce 1558 apply (fastforce simp: cte_wp_at_ctes_of) 1559 apply simp 1560 apply (rule conjI, clarsimp) 1561 defer 1562 apply clarsimp 1563 apply (rule conjI, clarsimp) 1564 apply clarsimp 1565 apply (simp only: bind_assoc[symmetric]) 1566 apply (rule corres_split'[where r'=dc, OF _ post_cap_deletion_corres]) 1567 defer 1568 apply wpsimp+ 1569 apply (rule corres_no_failI) 1570 apply (rule no_fail_pre, wp static_imp_wp) 1571 apply (clarsimp simp: cte_wp_at_ctes_of valid_pspace'_def) 1572 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) 1573 apply (rule conjI, clarsimp) 1574 apply (erule (2) valid_dlistEp) 1575 apply simp 1576 apply clarsimp 1577 apply (erule (2) valid_dlistEn) 1578 apply simp 1579 apply (clarsimp simp: in_monad bind_assoc exec_gets) 1580 apply (subgoal_tac "mdb_empty_abs a") 1581 prefer 2 1582 apply (rule mdb_empty_abs.intro) 1583 apply (rule vmdb_abs.intro) 1584 apply fastforce 1585 apply (frule mdb_empty_abs'.intro) 1586 apply (simp add: mdb_empty_abs'.empty_slot_ext_det_def2 update_cdt_list_def set_cdt_list_def exec_gets set_cdt_def bind_assoc exec_get exec_put set_original_def modify_def del: fun_upd_apply | subst bind_def, simp, simp add: mdb_empty_abs'.empty_slot_ext_det_def2)+ 1587 apply (simp add: put_def) 1588 apply (simp add: exec_gets exec_get exec_put del: fun_upd_apply | subst bind_def)+ 1589 apply (clarsimp simp: state_relation_def) 1590 apply (drule updateMDB_the_lot, fastforce simp: pspace_relations_def, fastforce, fastforce) 1591 apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def 1592 valid_mdb'_def valid_mdb_ctes_def) 1593 apply (elim conjE) 1594 apply (drule (4) updateMDB_the_lot, elim conjE) 1595 apply clarsimp 1596 apply (drule_tac s'=s''a and c=cap.NullCap in set_cap_not_quite_corres) 1597 subgoal by simp 1598 subgoal by simp 1599 subgoal by simp 1600 subgoal by fastforce 1601 subgoal by fastforce 1602 subgoal by fastforce 1603 subgoal by fastforce 1604 subgoal by fastforce 1605 apply fastforce 1606 subgoal by fastforce 1607 subgoal by fastforce 1608 subgoal by fastforce 1609 apply (erule cte_wp_at_weakenE, rule TrueI) 1610 apply assumption 1611 subgoal by simp 1612 subgoal by simp 1613 subgoal by simp 1614 subgoal by simp 1615 apply (rule refl) 1616 apply clarsimp 1617 apply (drule updateCap_stuff, elim conjE, erule (1) impE) 1618 apply clarsimp 1619 apply (drule updateMDB_the_lot, force simp: pspace_relations_def, assumption+, simp) 1620 apply (rule bexI) 1621 prefer 2 1622 apply (simp only: trans_state_update[symmetric]) 1623 apply (rule set_cap_trans_state) 1624 apply (rule set_cap_revokable_update) 1625 apply (erule set_cap_cdt_update) 1626 apply clarsimp 1627 apply (thin_tac "ctes_of t = s" for t s)+ 1628 apply (thin_tac "ksMachineState t = p" for t p)+ 1629 apply (thin_tac "ksCurThread t = p" for t p)+ 1630 apply (thin_tac "ksReadyQueues t = p" for t p)+ 1631 apply (thin_tac "ksSchedulerAction t = p" for t p)+ 1632 apply (clarsimp simp: cte_wp_at_ctes_of) 1633 apply (case_tac rv') 1634 apply (rename_tac s_cap s_node) 1635 apply (subgoal_tac "cte_at slot a") 1636 prefer 2 1637 apply (fastforce elim: cte_wp_at_weakenE) 1638 apply (subgoal_tac "mdb_empty (ctes_of b) (cte_map slot) s_cap s_node") 1639 prefer 2 1640 apply (rule mdb_empty.intro) 1641 apply (rule mdb_ptr.intro) 1642 apply (rule vmdb.intro) 1643 subgoal by (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def) 1644 apply (rule mdb_ptr_axioms.intro) 1645 subgoal by simp 1646 apply (clarsimp simp: ghost_relation_typ_at set_cap_a_type_inv) 1647 apply (simp add: pspace_relations_def) 1648 apply (rule conjI) 1649 apply (clarsimp simp: data_at_def ghost_relation_typ_at set_cap_a_type_inv) 1650 apply (rule conjI) 1651 prefer 2 1652 apply (rule conjI) 1653 apply (clarsimp simp: cdt_list_relation_def) 1654 apply(frule invs_valid_pspace, frule invs_mdb) 1655 apply(subgoal_tac "no_mloop (cdt a) \<and> finite_depth (cdt a)") 1656 prefer 2 1657 subgoal by(simp add: finite_depth valid_mdb_def) 1658 apply(subgoal_tac "valid_mdb_ctes (ctes_of b)") 1659 prefer 2 1660 subgoal by(simp add: mdb_empty_def mdb_ptr_def vmdb_def) 1661 apply(clarsimp simp: valid_pspace_def) 1662 1663 apply(case_tac "cdt a slot") 1664 apply(simp add: next_slot_eq[OF mdb_empty_abs'.next_slot_no_parent]) 1665 apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a)") 1666 subgoal by (simp) 1667 apply(clarsimp) 1668 apply(frule(1) mdb_empty.n_next) 1669 apply(clarsimp) 1670 apply(erule_tac x=aa in allE, erule_tac x=bb in allE) 1671 apply(simp split: if_split_asm) 1672 apply(drule cte_map_inj_eq) 1673 apply(drule cte_at_next_slot) 1674 apply(assumption)+ 1675 apply(simp) 1676 apply(subgoal_tac "(ab, bc) = slot") 1677 prefer 2 1678 apply(drule_tac cte="CTE s_cap s_node" in valid_mdbD2') 1679 subgoal by (clarsimp simp: valid_mdb_ctes_def no_0_def) 1680 subgoal by (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) 1681 apply(clarsimp) 1682 apply(rule cte_map_inj_eq) 1683 apply(assumption) 1684 apply(drule(3) cte_at_next_slot', assumption) 1685 apply(assumption)+ 1686 apply(simp) 1687 apply(drule_tac p="(aa, bb)" in no_parent_not_next_slot) 1688 apply(assumption)+ 1689 apply(clarsimp) 1690 1691 apply(simp add: next_slot_eq[OF mdb_empty_abs'.next_slot] split del: if_split) 1692 apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a)") 1693 subgoal by (simp) 1694 apply(case_tac "(aa, bb) = slot", simp) 1695 apply(case_tac "next_slot (aa, bb) (cdt_list a) (cdt a) = Some slot") 1696 apply(simp) 1697 apply(case_tac "next_slot ac (cdt_list a) (cdt a)", simp) 1698 apply(simp) 1699 apply(frule(1) mdb_empty.n_next) 1700 apply(clarsimp) 1701 apply(erule_tac x=aa in allE', erule_tac x=bb in allE) 1702 apply(erule_tac x=ac in allE, erule_tac x=bd in allE) 1703 apply(clarsimp split: if_split_asm) 1704 apply(drule(1) no_self_loop_next) 1705 apply(simp) 1706 apply(drule_tac cte="CTE cap' node'" in valid_mdbD1') 1707 apply(fastforce simp: valid_mdb_ctes_def no_0_def) 1708 subgoal by (simp add: valid_mdb'_def) 1709 apply(clarsimp) 1710 apply(simp) 1711 apply(frule(1) mdb_empty.n_next) 1712 apply(erule_tac x=aa in allE, erule_tac x=bb in allE) 1713 apply(clarsimp split: if_split_asm) 1714 apply(drule(1) no_self_loop_prev) 1715 apply(clarsimp) 1716 apply(drule_tac cte="CTE s_cap s_node" in valid_mdbD2') 1717 apply(clarsimp simp: valid_mdb_ctes_def no_0_def) 1718 apply clarify 1719 apply(clarsimp) 1720 apply(drule cte_map_inj_eq) 1721 apply(drule(3) cte_at_next_slot') 1722 apply(assumption)+ 1723 apply(simp) 1724 apply(erule disjE) 1725 apply(drule cte_map_inj_eq) 1726 apply(drule(3) cte_at_next_slot) 1727 apply(assumption)+ 1728 apply(simp) 1729 subgoal by (simp) 1730 apply (simp add: revokable_relation_def) 1731 apply (clarsimp simp: in_set_cap_cte_at) 1732 apply (rule conjI) 1733 apply clarsimp 1734 apply (drule(1) mdb_empty.n_revokable) 1735 subgoal by clarsimp 1736 apply clarsimp 1737 apply (drule (1) mdb_empty.n_revokable) 1738 apply (subgoal_tac "null_filter (caps_of_state a) (aa,bb) \<noteq> None") 1739 prefer 2 1740 apply (drule set_cap_caps_of_state_monad) 1741 subgoal by (force simp: null_filter_def) 1742 apply clarsimp 1743 apply (subgoal_tac "cte_at (aa, bb) a") 1744 prefer 2 1745 apply (drule null_filter_caps_of_stateD, erule cte_wp_cte_at) 1746 apply (drule (2) cte_map_inj_ps, fastforce) 1747 subgoal by simp 1748 apply (clarsimp simp add: cdt_relation_def) 1749 apply (subst mdb_empty_abs.descendants, assumption) 1750 apply (subst mdb_empty.descendants, assumption) 1751 apply clarsimp 1752 apply (frule_tac p="(aa, bb)" in in_set_cap_cte_at) 1753 apply clarsimp 1754 apply (frule (2) cte_map_inj_ps, fastforce) 1755 apply simp 1756 apply (case_tac "slot \<in> descendants_of (aa,bb) (cdt a)") 1757 apply (subst inj_on_image_set_diff) 1758 apply (rule inj_on_descendants_cte_map) 1759 apply fastforce 1760 apply fastforce 1761 apply fastforce 1762 apply fastforce 1763 apply fastforce 1764 subgoal by simp 1765 subgoal by simp 1766 apply simp 1767 apply (subgoal_tac "cte_map slot \<notin> descendants_of' (cte_map (aa,bb)) (ctes_of b)") 1768 subgoal by simp 1769 apply (erule_tac x=aa in allE, erule allE, erule (1) impE) 1770 apply (drule_tac s="cte_map ` u" for u in sym) 1771 apply clarsimp 1772 apply (drule cte_map_inj_eq, assumption) 1773 apply (erule descendants_of_cte_at, fastforce) 1774 apply fastforce 1775 apply fastforce 1776 apply fastforce 1777 apply simp 1778 done 1779 1780 1781 1782text {* Some facts about is_final_cap/isFinalCapability *} 1783 1784lemma isFinalCapability_inv: 1785 "\<lbrace>P\<rbrace> isFinalCapability cap \<lbrace>\<lambda>_. P\<rbrace>" 1786 apply (simp add: isFinalCapability_def Let_def 1787 split del: if_split cong: if_cong) 1788 apply (rule hoare_pre, wp) 1789 apply (rule hoare_post_imp [where Q="\<lambda>s. P"], simp) 1790 apply wp 1791 apply simp 1792 done 1793 1794definition 1795 final_matters' :: "capability \<Rightarrow> bool" 1796where 1797 "final_matters' cap \<equiv> case cap of 1798 EndpointCap ref bdg s r g \<Rightarrow> True 1799 | NotificationCap ref bdg s r \<Rightarrow> True 1800 | ThreadCap ref \<Rightarrow> True 1801 | CNodeCap ref bits gd gs \<Rightarrow> True 1802 | Zombie ptr zb n \<Rightarrow> True 1803 | IRQHandlerCap irq \<Rightarrow> True 1804 | ArchObjectCap acap \<Rightarrow> (case acap of 1805 PageCap d ref rghts sz mapdata \<Rightarrow> False 1806 | ASIDControlCap \<Rightarrow> False 1807 | _ \<Rightarrow> True) 1808 | _ \<Rightarrow> False" 1809 1810lemma final_matters_Master: 1811 "final_matters' (capMasterCap cap) = final_matters' cap" 1812 by (simp add: capMasterCap_def split: capability.split arch_capability.split, 1813 simp add: final_matters'_def) 1814 1815lemma final_matters_sameRegion_sameObject: 1816 "final_matters' cap \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'" 1817 apply (rule iffI) 1818 apply (erule sameRegionAsE) 1819 apply (simp add: sameObjectAs_def3) 1820 apply (clarsimp simp: isCap_simps sameObjectAs_sameRegionAs final_matters'_def 1821 split:capability.splits arch_capability.splits)+ 1822 done 1823 1824lemma final_matters_sameRegion_sameObject2: 1825 "\<lbrakk> final_matters' cap'; \<not> isUntypedCap cap; \<not> isIRQHandlerCap cap' \<rbrakk> 1826 \<Longrightarrow> sameRegionAs cap cap' = sameObjectAs cap cap'" 1827 apply (rule iffI) 1828 apply (erule sameRegionAsE) 1829 apply (simp add: sameObjectAs_def3) 1830 apply (fastforce simp: isCap_simps final_matters'_def) 1831 apply simp 1832 apply (clarsimp simp: final_matters'_def isCap_simps) 1833 apply (clarsimp simp: final_matters'_def isCap_simps) 1834 apply (erule sameObjectAs_sameRegionAs) 1835 done 1836 1837lemma notFinal_prev_or_next: 1838 "\<lbrakk> \<not> isFinal cap x (cteCaps_of s); mdb_chunked (ctes_of s); 1839 valid_dlist (ctes_of s); no_0 (ctes_of s); 1840 ctes_of s x = Some (CTE cap node); final_matters' cap \<rbrakk> 1841 \<Longrightarrow> (\<exists>cap' node'. ctes_of s (mdbPrev node) = Some (CTE cap' node') 1842 \<and> sameObjectAs cap cap') 1843 \<or> (\<exists>cap' node'. ctes_of s (mdbNext node) = Some (CTE cap' node') 1844 \<and> sameObjectAs cap cap')" 1845 apply (erule not_FinalE) 1846 apply (clarsimp simp: isCap_simps final_matters'_def) 1847 apply (clarsimp simp: mdb_chunked_def cte_wp_at_ctes_of cteCaps_of_def 1848 del: disjCI) 1849 apply (erule_tac x=x in allE, erule_tac x=p in allE) 1850 apply simp 1851 apply (case_tac z, simp add: sameObjectAs_sameRegionAs) 1852 apply (elim conjE disjE, simp_all add: is_chunk_def) 1853 apply (rule disjI2) 1854 apply (drule tranclD) 1855 apply (clarsimp simp: mdb_next_unfold) 1856 apply (drule spec[where x="mdbNext node"]) 1857 apply simp 1858 apply (drule mp[where P="ctes_of s \<turnstile> x \<leadsto>\<^sup>+ mdbNext node"]) 1859 apply (rule trancl.intros(1), simp add: mdb_next_unfold) 1860 apply clarsimp 1861 apply (drule rtranclD) 1862 apply (erule disjE, clarsimp+) 1863 apply (drule tranclD) 1864 apply (clarsimp simp: mdb_next_unfold final_matters_sameRegion_sameObject) 1865 apply (rule disjI1) 1866 apply clarsimp 1867 apply (drule tranclD2) 1868 apply clarsimp 1869 apply (frule vdlist_nextD0) 1870 apply clarsimp 1871 apply assumption 1872 apply (clarsimp simp: mdb_prev_def) 1873 apply (drule rtranclD) 1874 apply (erule disjE, clarsimp+) 1875 apply (drule spec, drule(1) mp) 1876 apply (drule mp, rule trancl_into_rtrancl, erule trancl.intros(1)) 1877 apply clarsimp 1878 apply (drule iffD1 [OF final_matters_sameRegion_sameObject, rotated]) 1879 apply (subst final_matters_Master[symmetric]) 1880 apply (subst(asm) final_matters_Master[symmetric]) 1881 apply (clarsimp simp: sameObjectAs_def3) 1882 apply (clarsimp simp: sameObjectAs_def3) 1883 done 1884 1885lemma isFinal: 1886 "\<lbrace>\<lambda>s. valid_mdb' s \<and> cte_wp_at' ((=) cte) x s 1887 \<and> final_matters' (cteCap cte) 1888 \<and> Q (isFinal (cteCap cte) x (cteCaps_of s)) s\<rbrace> 1889 isFinalCapability cte 1890 \<lbrace>Q\<rbrace>" 1891 unfolding isFinalCapability_def 1892 apply (cases cte) 1893 apply (rename_tac cap node) 1894 apply (unfold Let_def) 1895 apply (simp only: if_False) 1896 apply (wp getCTE_wp') 1897 apply (cases "mdbPrev (cteMDBNode cte) = nullPointer") 1898 apply simp 1899 apply (clarsimp simp: valid_mdb_ctes_def valid_mdb'_def 1900 cte_wp_at_ctes_of) 1901 apply (rule conjI, clarsimp simp: nullPointer_def) 1902 apply (erule rsubst[where P="\<lambda>x. Q x s" for s], simp) 1903 apply (rule classical) 1904 apply (drule(5) notFinal_prev_or_next) 1905 apply clarsimp 1906 apply (clarsimp simp: nullPointer_def) 1907 apply (erule rsubst[where P="\<lambda>x. Q x s" for s]) 1908 apply (rule sym, rule iffI) 1909 apply (rule classical) 1910 apply (drule(5) notFinal_prev_or_next) 1911 apply clarsimp 1912 apply clarsimp 1913 apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) 1914 apply (case_tac cte) 1915 apply clarsimp 1916 apply (clarsimp simp add: isFinal_def) 1917 apply (erule_tac x="mdbNext node" in allE) 1918 apply simp 1919 apply (erule impE) 1920 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) 1921 apply (drule (1) mdb_chain_0_no_loops) 1922 apply simp 1923 apply (clarsimp simp: sameObjectAs_def3 isCap_simps) 1924 apply simp 1925 apply (clarsimp simp: cte_wp_at_ctes_of 1926 valid_mdb_ctes_def valid_mdb'_def) 1927 apply (case_tac cte) 1928 apply clarsimp 1929 apply (rule conjI) 1930 apply clarsimp 1931 apply (erule rsubst[where P="\<lambda>x. Q x s" for s]) 1932 apply clarsimp 1933 apply (clarsimp simp: isFinal_def cteCaps_of_def) 1934 apply (erule_tac x="mdbPrev node" in allE) 1935 apply simp 1936 apply (erule impE) 1937 apply clarsimp 1938 apply (drule (1) mdb_chain_0_no_loops) 1939 apply (subgoal_tac "ctes_of s (mdbNext node) = Some (CTE cap node)") 1940 apply clarsimp 1941 apply (erule (1) valid_dlistEp) 1942 apply clarsimp 1943 apply (case_tac cte') 1944 apply clarsimp 1945 apply (clarsimp simp add: sameObjectAs_def3 isCap_simps) 1946 apply clarsimp 1947 apply (rule conjI) 1948 apply clarsimp 1949 apply (erule rsubst[where P="\<lambda>x. Q x s" for s], simp) 1950 apply (rule classical, drule(5) notFinal_prev_or_next) 1951 apply (clarsimp simp: sameObjectAs_sym nullPointer_def) 1952 apply (clarsimp simp: nullPointer_def) 1953 apply (erule rsubst[where P="\<lambda>x. Q x s" for s]) 1954 apply (rule sym, rule iffI) 1955 apply (rule classical, drule(5) notFinal_prev_or_next) 1956 apply (clarsimp simp: sameObjectAs_sym) 1957 apply auto[1] 1958 apply (clarsimp simp: isFinal_def cteCaps_of_def) 1959 apply (case_tac cte) 1960 apply (erule_tac x="mdbNext node" in allE) 1961 apply simp 1962 apply (erule impE) 1963 apply clarsimp 1964 apply (drule (1) mdb_chain_0_no_loops) 1965 apply simp 1966 apply clarsimp 1967 apply (clarsimp simp: isCap_simps sameObjectAs_def3) 1968 done 1969end 1970 1971lemma (in vmdb) isFinal_no_subtree: 1972 "\<lbrakk> m \<turnstile> sl \<rightarrow> p; isFinal cap sl (option_map cteCap o m); 1973 m sl = Some (CTE cap n); final_matters' cap \<rbrakk> \<Longrightarrow> False" 1974 apply (erule subtree.induct) 1975 apply (case_tac "c'=sl", simp) 1976 apply (clarsimp simp: isFinal_def parentOf_def mdb_next_unfold cteCaps_of_def) 1977 apply (erule_tac x="mdbNext n" in allE) 1978 apply simp 1979 apply (clarsimp simp: isMDBParentOf_CTE final_matters_sameRegion_sameObject) 1980 apply (clarsimp simp: isCap_simps sameObjectAs_def3) 1981 apply clarsimp 1982 done 1983 1984lemma isFinal_no_descendants: 1985 "\<lbrakk> isFinal cap sl (cteCaps_of s); ctes_of s sl = Some (CTE cap n); 1986 valid_mdb' s; final_matters' cap \<rbrakk> 1987 \<Longrightarrow> descendants_of' sl (ctes_of s) = {}" 1988 apply (clarsimp simp add: descendants_of'_def cteCaps_of_def) 1989 apply (erule(3) vmdb.isFinal_no_subtree[rotated]) 1990 apply unfold_locales[1] 1991 apply (simp add: valid_mdb'_def) 1992 done 1993 1994lemma (in vmdb) isFinal_untypedParent: 1995 assumes x: "m slot = Some cte" "isFinal (cteCap cte) slot (option_map cteCap o m)" 1996 "final_matters' (cteCap cte) \<and> \<not> isIRQHandlerCap (cteCap cte)" 1997 shows 1998 "m \<turnstile> x \<rightarrow> slot \<Longrightarrow> 1999 (\<exists>cte'. m x = Some cte' \<and> isUntypedCap (cteCap cte') \<and> RetypeDecls_H.sameRegionAs (cteCap cte') (cteCap cte))" 2000 apply (cases "x=slot", simp) 2001 apply (insert x) 2002 apply (frule subtree_mdb_next) 2003 apply (drule subtree_parent) 2004 apply (drule tranclD) 2005 apply clarsimp 2006 apply (clarsimp simp: mdb_next_unfold parentOf_def isFinal_def) 2007 apply (case_tac cte') 2008 apply (rename_tac c' n') 2009 apply (cases cte) 2010 apply (rename_tac c n) 2011 apply simp 2012 apply (erule_tac x=x in allE) 2013 apply clarsimp 2014 apply (drule isMDBParent_sameRegion) 2015 apply simp 2016 apply (rule classical, simp) 2017 apply (simp add: final_matters_sameRegion_sameObject2 2018 sameObjectAs_sym) 2019 done 2020 2021lemma isFinal2: 2022 "\<lbrace>\<lambda>s. cte_wp_at' ((=) cte) sl s \<and> valid_mdb' s\<rbrace> 2023 isFinalCapability cte 2024 \<lbrace>\<lambda>rv s. rv \<and> final_matters' (cteCap cte) \<longrightarrow> 2025 isFinal (cteCap cte) sl (cteCaps_of s)\<rbrace>" 2026 apply (cases "final_matters' (cteCap cte)") 2027 apply simp 2028 apply (wp isFinal[where x=sl]) 2029 apply simp 2030 apply (simp|wp)+ 2031 done 2032 2033context begin interpretation Arch . (*FIXME: arch_split*) 2034 2035lemma no_fail_isFinalCapability [wp]: 2036 "no_fail (valid_mdb' and cte_wp_at' ((=) cte) p) (isFinalCapability cte)" 2037 apply (simp add: isFinalCapability_def) 2038 apply (clarsimp simp: Let_def split del: if_split) 2039 apply (rule no_fail_pre, wp getCTE_wp') 2040 apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def cte_wp_at_ctes_of nullPointer_def) 2041 apply (rule conjI) 2042 apply clarsimp 2043 apply (erule (2) valid_dlistEp) 2044 apply simp 2045 apply clarsimp 2046 apply (rule conjI) 2047 apply (erule (2) valid_dlistEn) 2048 apply simp 2049 apply clarsimp 2050 apply (rule valid_dlistEn, assumption+) 2051 apply (erule (2) valid_dlistEp) 2052 apply simp 2053 done 2054 2055lemma corres_gets_lift: 2056 assumes inv: "\<And>P. \<lbrace>P\<rbrace> g \<lbrace>\<lambda>_. P\<rbrace>" 2057 assumes res: "\<lbrace>Q'\<rbrace> g \<lbrace>\<lambda>r s. r = g' s\<rbrace>" 2058 assumes Q: "\<And>s. Q s \<Longrightarrow> Q' s" 2059 assumes nf: "no_fail Q g" 2060 shows "corres r P Q f (gets g') \<Longrightarrow> corres r P Q f g" 2061 apply (clarsimp simp add: corres_underlying_def simpler_gets_def) 2062 apply (drule (1) bspec) 2063 apply (rule conjI) 2064 apply clarsimp 2065 apply (rule bexI) 2066 prefer 2 2067 apply assumption 2068 apply simp 2069 apply (frule in_inv_by_hoareD [OF inv]) 2070 apply simp 2071 apply (drule use_valid, rule res) 2072 apply (erule Q) 2073 apply simp 2074 apply (insert nf) 2075 apply (clarsimp simp: no_fail_def) 2076 done 2077 2078lemma obj_refs_Master: 2079 "\<lbrakk> cap_relation cap cap'; P cap \<rbrakk> 2080 \<Longrightarrow> obj_refs cap = 2081 (if capClass (capMasterCap cap') = PhysicalClass 2082 \<and> \<not> isUntypedCap (capMasterCap cap') 2083 then {capUntypedPtr (capMasterCap cap')} else {})" 2084 by (clarsimp simp: isCap_simps 2085 split: cap_relation_split_asm arch_cap.split_asm) 2086 2087lemma final_cap_corres': 2088 "final_matters' (cteCap cte) \<Longrightarrow> 2089 corres (=) (invs and cte_wp_at ((=) cap) ptr) 2090 (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) 2091 (is_final_cap cap) (isFinalCapability cte)" 2092 apply (rule corres_gets_lift) 2093 apply (rule isFinalCapability_inv) 2094 apply (rule isFinal[where x="cte_map ptr"]) 2095 apply clarsimp 2096 apply (rule conjI, clarsimp) 2097 apply (rule refl) 2098 apply (rule no_fail_pre, wp, fastforce) 2099 apply (simp add: is_final_cap_def) 2100 apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def state_relation_def) 2101 apply (frule (1) pspace_relation_ctes_ofI) 2102 apply fastforce 2103 apply fastforce 2104 apply clarsimp 2105 apply (rule iffI) 2106 apply (simp add: is_final_cap'_def2 isFinal_def) 2107 apply clarsimp 2108 apply (subgoal_tac "obj_refs cap \<noteq> {} \<or> cap_irqs cap \<noteq> {} \<or> arch_gen_refs cap \<noteq> {}") 2109 prefer 2 2110 apply (erule_tac x=a in allE) 2111 apply (erule_tac x=b in allE) 2112 apply (clarsimp simp: cte_wp_at_def gen_obj_refs_Int) 2113 apply (subgoal_tac "ptr = (a,b)") 2114 prefer 2 2115 apply (erule_tac x="fst ptr" in allE) 2116 apply (erule_tac x="snd ptr" in allE) 2117 apply (clarsimp simp: cte_wp_at_def gen_obj_refs_Int) 2118 apply clarsimp 2119 apply (rule context_conjI) 2120 apply (clarsimp simp: isCap_simps) 2121 apply (cases cap, auto)[1] 2122 apply clarsimp 2123 apply (drule_tac x=p' in pspace_relation_cte_wp_atI, assumption) 2124 apply fastforce 2125 apply clarsimp 2126 apply (erule_tac x=aa in allE) 2127 apply (erule_tac x=ba in allE) 2128 apply (clarsimp simp: cte_wp_at_caps_of_state) 2129 apply (clarsimp simp: sameObjectAs_def3 obj_refs_Master cap_irqs_relation_Master 2130 arch_gen_refs_relation_Master gen_obj_refs_Int 2131 cong: if_cong 2132 split: capability.split_asm) 2133 apply (clarsimp simp: isFinal_def is_final_cap'_def3) 2134 apply (rule_tac x="fst ptr" in exI) 2135 apply (rule_tac x="snd ptr" in exI) 2136 apply (rule conjI) 2137 apply (clarsimp simp: cte_wp_at_def final_matters'_def 2138 gen_obj_refs_Int 2139 split: cap_relation_split_asm arch_cap.split_asm) 2140 apply clarsimp 2141 apply (drule_tac p="(a,b)" in cte_wp_at_eqD) 2142 apply clarsimp 2143 apply (frule_tac slot="(a,b)" in pspace_relation_ctes_ofI, assumption) 2144 apply fastforce 2145 apply fastforce 2146 apply clarsimp 2147 apply (frule_tac p="(a,b)" in cte_wp_valid_cap, fastforce) 2148 apply (erule_tac x="cte_map (a,b)" in allE) 2149 apply simp 2150 apply (erule impCE, simp, drule cte_map_inj_eq) 2151 apply (erule cte_wp_at_weakenE, rule TrueI) 2152 apply (erule cte_wp_at_weakenE, rule TrueI) 2153 apply fastforce 2154 apply fastforce 2155 apply (erule invs_distinct) 2156 apply simp 2157 apply (frule_tac p=ptr in cte_wp_valid_cap, fastforce) 2158 apply (clarsimp simp: cte_wp_at_def gen_obj_refs_Int) 2159 apply (rule conjI) 2160 apply (rule classical) 2161 apply (frule(1) zombies_finalD2[OF _ _ _ invs_zombies], 2162 simp?, clarsimp, assumption+) 2163 subgoal by (clarsimp simp: sameObjectAs_def3 isCap_simps valid_cap_def 2164 obj_at_def is_obj_defs a_type_def final_matters'_def 2165 split: cap.split_asm arch_cap.split_asm 2166 option.split_asm if_split_asm, 2167 simp_all add: is_cap_defs) 2168 apply (rule classical) 2169 by (clarsimp simp: cap_irqs_def cap_irq_opt_def sameObjectAs_def3 isCap_simps arch_gen_obj_refs_def 2170 split: cap.split_asm) 2171 2172lemma final_cap_corres: 2173 "corres (\<lambda>rv rv'. final_matters' (cteCap cte) \<longrightarrow> rv = rv') 2174 (invs and cte_wp_at ((=) cap) ptr) 2175 (invs' and cte_wp_at' ((=) cte) (cte_map ptr)) 2176 (is_final_cap cap) (isFinalCapability cte)" 2177 apply (cases "final_matters' (cteCap cte)") 2178 apply simp 2179 apply (erule final_cap_corres') 2180 apply (subst bind_return[symmetric], 2181 rule corres_symb_exec_r) 2182 apply (rule corres_no_failI) 2183 apply wp 2184 apply (clarsimp simp: in_monad is_final_cap_def simpler_gets_def) 2185 apply (wp isFinalCapability_inv)+ 2186 apply fastforce 2187 done 2188 2189text {* Facts about finalise_cap/finaliseCap and 2190 cap_delete_one/cteDelete in no particular order *} 2191 2192 2193definition 2194 finaliseCapTrue_standin_simple_def: 2195 "finaliseCapTrue_standin cap fin \<equiv> finaliseCap cap fin True" 2196 2197context 2198begin 2199 2200declare if_cong [cong] 2201 2202lemmas finaliseCapTrue_standin_def 2203 = finaliseCapTrue_standin_simple_def 2204 [unfolded finaliseCap_def, simplified] 2205 2206lemmas cteDeleteOne_def' 2207 = eq_reflection [OF cteDeleteOne_def] 2208lemmas cteDeleteOne_def 2209 = cteDeleteOne_def'[folded finaliseCapTrue_standin_simple_def] 2210 2211crunch typ_at'[wp]: cteDeleteOne, suspend, prepareThreadDelete "\<lambda>s. P (typ_at' T p s)" 2212 (wp: crunch_wps getObject_inv loadObject_default_inv 2213 simp: crunch_simps unless_def o_def 2214 ignore: getObject) 2215 2216end 2217 2218lemmas cancelAllIPC_typs[wp] = typ_at_lifts [OF cancelAllIPC_typ_at'] 2219lemmas cancelAllSignals_typs[wp] = typ_at_lifts [OF cancelAllSignals_typ_at'] 2220lemmas suspend_typs[wp] = typ_at_lifts [OF suspend_typ_at'] 2221 2222definition 2223 arch_cap_has_cleanup' :: "arch_capability \<Rightarrow> bool" 2224where 2225 "arch_cap_has_cleanup' acap \<equiv> False" 2226 2227definition 2228 cap_has_cleanup' :: "capability \<Rightarrow> bool" 2229where 2230 "cap_has_cleanup' cap \<equiv> case cap of 2231 IRQHandlerCap _ \<Rightarrow> True 2232 | ArchObjectCap acap \<Rightarrow> arch_cap_has_cleanup' acap 2233 | _ \<Rightarrow> False" 2234 2235lemmas cap_has_cleanup'_simps[simp] = cap_has_cleanup'_def[split_simps capability.split] 2236 2237lemma finaliseCap_cases[wp]: 2238 "\<lbrace>\<top>\<rbrace> 2239 finaliseCap cap final flag 2240 \<lbrace>\<lambda>rv s. fst rv = NullCap \<and> (snd rv \<noteq> NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd rv = cap) 2241 \<or> 2242 isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = NullCap 2243 \<and> capUntypedPtr (fst rv) = capUntypedPtr cap 2244 \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace>" 2245 apply (simp add: finaliseCap_def ARM_H.finaliseCap_def Let_def 2246 getThreadCSpaceRoot 2247 cong: if_cong split del: if_split) 2248 apply (rule hoare_pre) 2249 apply ((wp | simp add: isCap_simps split del: if_split 2250 | wpc 2251 | simp only: valid_NullCap fst_conv snd_conv)+)[1] 2252 apply (simp only: simp_thms fst_conv snd_conv option.simps if_cancel 2253 o_def) 2254 apply (intro allI impI conjI TrueI) 2255 apply (auto simp add: isCap_simps cap_has_cleanup'_def) 2256 done 2257 2258crunch aligned'[wp]: finaliseCap "pspace_aligned'" 2259 (simp: crunch_simps assertE_def unless_def o_def 2260 ignore: getObject setObject forM ignoreFailure 2261 wp: getObject_inv loadObject_default_inv crunch_wps) 2262 2263crunch distinct'[wp]: finaliseCap "pspace_distinct'" 2264 (ignore: getObject setObject forM ignoreFailure 2265 simp: crunch_simps assertE_def unless_def o_def 2266 wp: getObject_inv loadObject_default_inv crunch_wps) 2267 2268crunch typ_at'[wp]: finaliseCap "\<lambda>s. P (typ_at' T p s)" 2269 (simp: crunch_simps assertE_def ignore: getObject setObject 2270 wp: getObject_inv loadObject_default_inv crunch_wps) 2271lemmas finaliseCap_typ_ats[wp] = typ_at_lifts[OF finaliseCap_typ_at'] 2272 2273crunch it'[wp]: finaliseCap "\<lambda>s. P (ksIdleThread s)" 2274 (ignore: getObject setObject forM ignoreFailure maskInterrupt 2275 wp: mapM_x_wp_inv mapM_wp' hoare_drop_imps getObject_inv loadObject_default_inv 2276 simp: crunch_simps o_def) 2277 2278crunch vs_lookup[wp]: flush_space "\<lambda>s. P (vs_lookup s)" 2279 (wp: crunch_wps) 2280 2281declare doUnbindNotification_def[simp] 2282 2283lemma ntfn_q_refs_of'_mult: 2284 "ntfn_q_refs_of' ntfn = (case ntfn of Structures_H.WaitingNtfn q \<Rightarrow> set q | _ \<Rightarrow> {}) \<times> {NTFNSignal}" 2285 by (cases ntfn, simp_all) 2286 2287lemma tcb_st_not_Bound: 2288 "(p, NTFNBound) \<notin> tcb_st_refs_of' ts" 2289 "(p, TCBBound) \<notin> tcb_st_refs_of' ts" 2290 by (auto simp: tcb_st_refs_of'_def split: Structures_H.thread_state.split) 2291 2292lemma unbindNotification_invs[wp]: 2293 "\<lbrace>invs'\<rbrace> unbindNotification tcb \<lbrace>\<lambda>rv. invs'\<rbrace>" 2294 apply (simp add: unbindNotification_def invs'_def valid_state'_def) 2295 apply (rule hoare_seq_ext[OF _ gbn_sp']) 2296 apply (case_tac ntfnPtr, clarsimp, wp, clarsimp) 2297 apply clarsimp 2298 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 2299 apply (rule hoare_pre) 2300 apply (wp sbn'_valid_pspace'_inv sbn_sch_act' sbn_valid_queues valid_irq_node_lift 2301 irqs_masked_lift setBoundNotification_ct_not_inQ 2302 untyped_ranges_zero_lift | clarsimp simp: cteCaps_of_def o_def)+ 2303 apply (rule conjI) 2304 apply (clarsimp elim!: obj_atE' 2305 simp: projectKOs 2306 dest!: pred_tcb_at') 2307 apply (clarsimp simp: pred_tcb_at' conj_comms) 2308 apply (frule bound_tcb_ex_cap'', clarsimp+) 2309 apply (frule(1) sym_refs_bound_tcb_atD') 2310 apply (frule(1) sym_refs_obj_atD') 2311 apply (clarsimp simp: refs_of_rev') 2312 apply normalise_obj_at' 2313 apply (subst delta_sym_refs, assumption) 2314 apply (auto split: if_split_asm)[1] 2315 apply (auto simp: tcb_st_not_Bound ntfn_q_refs_of'_mult split: if_split_asm)[1] 2316 apply (frule obj_at_valid_objs', clarsimp+) 2317 apply (simp add: valid_ntfn'_def valid_obj'_def projectKOs 2318 split: ntfn.splits) 2319 apply (erule if_live_then_nonz_capE') 2320 apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) 2321 done 2322 2323lemma ntfn_bound_tcb_at': 2324 "\<lbrakk>sym_refs (state_refs_of' s); valid_objs' s; ko_at' ntfn ntfnptr s; 2325 ntfnBoundTCB ntfn = Some tcbptr; P (Some ntfnptr)\<rbrakk> 2326 \<Longrightarrow> bound_tcb_at' P tcbptr s" 2327 apply (drule_tac x=ntfnptr in sym_refsD[rotated]) 2328 apply (clarsimp simp: obj_at'_def projectKOs) 2329 apply (fastforce simp: state_refs_of'_def) 2330 apply (auto simp: pred_tcb_at'_def obj_at'_def valid_obj'_def valid_ntfn'_def 2331 state_refs_of'_def refs_of_rev' projectKOs 2332 simp del: refs_of_simps 2333 elim!: valid_objsE 2334 split: option.splits if_split_asm) 2335 done 2336 2337 2338lemma unbindMaybeNotification_invs[wp]: 2339 "\<lbrace>invs'\<rbrace> unbindMaybeNotification ntfnptr \<lbrace>\<lambda>rv. invs'\<rbrace>" 2340 apply (simp add: unbindMaybeNotification_def invs'_def valid_state'_def) 2341 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 2342 apply (rule hoare_pre) 2343 apply (wp sbn'_valid_pspace'_inv sbn_sch_act' sbn_valid_queues valid_irq_node_lift 2344 irqs_masked_lift setBoundNotification_ct_not_inQ 2345 untyped_ranges_zero_lift 2346 | wpc | clarsimp simp: cteCaps_of_def o_def)+ 2347 apply safe[1] 2348 defer 3 2349 defer 7 2350 apply (fold_subgoals (prefix))[8] 2351 subgoal premises prems using prems by (auto simp: pred_tcb_at' valid_pspace'_def projectKOs valid_obj'_def valid_ntfn'_def 2352 ko_wp_at'_def 2353 elim!: obj_atE' valid_objsE' if_live_then_nonz_capE' 2354 split: option.splits ntfn.splits) 2355 apply (rule delta_sym_refs, assumption) 2356 apply (fold_subgoals (prefix))[2] 2357 subgoal premises prems using prems by (fastforce simp: symreftype_inverse' ntfn_q_refs_of'_def 2358 split: ntfn.splits if_split_asm 2359 dest!: ko_at_state_refs_ofD')+ 2360 apply (rule delta_sym_refs, assumption) 2361 apply (clarsimp split: if_split_asm) 2362 apply (frule ko_at_state_refs_ofD', simp) 2363 apply (clarsimp split: if_split_asm) 2364 apply (frule_tac P="(=) (Some ntfnptr)" in ntfn_bound_tcb_at', simp_all add: valid_pspace'_def)[1] 2365 subgoal by (fastforce simp: ntfn_q_refs_of'_def state_refs_of'_def tcb_ntfn_is_bound'_def 2366 tcb_st_refs_of'_def 2367 dest!: bound_tcb_at_state_refs_ofD' 2368 split: ntfn.splits thread_state.splits) 2369 apply (frule ko_at_state_refs_ofD', simp) 2370 done 2371 2372(* Ugh, required to be able to split out the abstract invs *) 2373lemma finaliseCap_True_invs[wp]: 2374 "\<lbrace>invs'\<rbrace> finaliseCap cap final True \<lbrace>\<lambda>rv. invs'\<rbrace>" 2375 apply (simp add: finaliseCap_def Let_def) 2376 apply safe 2377 apply (wp irqs_masked_lift| simp | wpc)+ 2378 done 2379 2380crunch invs'[wp]: flushSpace "invs'" (ignore: doMachineOp) 2381 2382lemma ct_not_inQ_ksArchState_update[simp]: 2383 "ct_not_inQ (s\<lparr>ksArchState := v\<rparr>) = ct_not_inQ s" 2384 by (simp add: ct_not_inQ_def) 2385 2386lemma invs_asid_update_strg': 2387 "invs' s \<and> tab = armKSASIDTable (ksArchState s) \<longrightarrow> 2388 invs' (s\<lparr>ksArchState := armKSASIDTable_update 2389 (\<lambda>_. tab (asid := None)) (ksArchState s)\<rparr>)" 2390 apply (simp add: invs'_def) 2391 apply (simp add: valid_state'_def) 2392 apply (simp add: valid_global_refs'_def global_refs'_def valid_arch_state'_def valid_asid_table'_def valid_machine_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 2393 apply (auto simp add: ran_def split: if_split_asm) 2394 done 2395 2396lemma invalidateASIDEntry_invs' [wp]: 2397 "\<lbrace>invs'\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. invs'\<rbrace>" 2398 apply (simp add: invalidateASIDEntry_def invalidateASID_def 2399 invalidateHWASIDEntry_def bind_assoc) 2400 apply (wp loadHWASID_wp | simp)+ 2401 apply (clarsimp simp: fun_upd_def[symmetric]) 2402 apply (rule conjI) 2403 apply (clarsimp simp: invs'_def valid_state'_def) 2404 apply (rule conjI) 2405 apply (simp add: valid_global_refs'_def 2406 global_refs'_def) 2407 apply (simp add: valid_arch_state'_def ran_def 2408 valid_asid_table'_def is_inv_None_upd 2409 valid_machine_state'_def 2410 comp_upd_simp fun_upd_def[symmetric] 2411 inj_on_fun_upd_elsewhere 2412 valid_asid_map'_def 2413 ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 2414 subgoal by (auto elim!: subset_inj_on) 2415 apply (clarsimp simp: invs'_def valid_state'_def) 2416 apply (rule conjI) 2417 apply (simp add: valid_global_refs'_def 2418 global_refs'_def) 2419 apply (rule conjI) 2420 apply (simp add: valid_arch_state'_def ran_def 2421 valid_asid_table'_def None_upd_eq 2422 fun_upd_def[symmetric] comp_upd_simp) 2423 apply (simp add: valid_machine_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 2424 done 2425 2426lemma deleteASIDPool_invs[wp]: 2427 "\<lbrace>invs'\<rbrace> deleteASIDPool asid pool \<lbrace>\<lambda>rv. invs'\<rbrace>" 2428 apply (simp add: deleteASIDPool_def) 2429 apply wp 2430 apply (simp del: fun_upd_apply) 2431 apply (strengthen invs_asid_update_strg') 2432 apply (wp mapM_wp' getObject_inv loadObject_default_inv 2433 | simp)+ 2434 done 2435 2436lemma invalidateASIDEntry_valid_ap' [wp]: 2437 "\<lbrace>valid_asid_pool' p\<rbrace> invalidateASIDEntry asid \<lbrace>\<lambda>r. valid_asid_pool' p\<rbrace>" 2438 apply (simp add: invalidateASIDEntry_def invalidateASID_def 2439 invalidateHWASIDEntry_def bind_assoc) 2440 apply (wp loadHWASID_wp | simp)+ 2441 apply (case_tac p) 2442 apply (clarsimp simp del: fun_upd_apply) 2443 done 2444 2445lemmas flushSpace_typ_ats' [wp] = typ_at_lifts [OF flushSpace_typ_at'] 2446 2447lemma deleteASID_invs'[wp]: 2448 "\<lbrace>invs'\<rbrace> deleteASID asid pd \<lbrace>\<lambda>rv. invs'\<rbrace>" 2449 apply (simp add: deleteASID_def cong: option.case_cong) 2450 apply (rule hoare_pre) 2451 apply (wp | wpc)+ 2452 apply (rule_tac Q="\<lambda>rv. valid_obj' (injectKO rv) and invs'" 2453 in hoare_post_imp) 2454 apply (clarsimp split: if_split_asm del: subsetI) 2455 apply (simp add: fun_upd_def[symmetric] valid_obj'_def) 2456 apply (case_tac r, simp) 2457 apply (subst inv_f_f, rule inj_onI, simp)+ 2458 apply (rule conjI) 2459 apply clarsimp 2460 apply (drule subsetD, blast) 2461 apply clarsimp 2462 apply (auto dest!: ran_del_subset)[1] 2463 apply (wp getObject_valid_obj getObject_inv loadObject_default_inv 2464 | simp add: objBits_simps archObjSize_def pageBits_def)+ 2465 apply clarsimp 2466 done 2467 2468lemma arch_finaliseCap_invs[wp]: 2469 "\<lbrace>invs' and valid_cap' (ArchObjectCap cap)\<rbrace> 2470 Arch.finaliseCap cap fin 2471 \<lbrace>\<lambda>rv. invs'\<rbrace>" 2472 unfolding ARM_H.finaliseCap_def 2473 apply clarsimp 2474 apply (safe ; wpsimp) 2475 done 2476 2477lemma arch_finaliseCap_removeable[wp]: 2478 "\<lbrace>\<lambda>s. s \<turnstile>' ArchObjectCap cap \<and> invs' s 2479 \<and> (final \<and> final_matters' (ArchObjectCap cap) 2480 \<longrightarrow> isFinal (ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> 2481 Arch.finaliseCap cap final 2482 \<lbrace>\<lambda>rv s. isNullCap (fst rv) \<and> removeable' slot s (ArchObjectCap cap) \<and> isNullCap (snd rv)\<rbrace>" 2483 apply (simp add: ARM_H.finaliseCap_def 2484 removeable'_def) 2485 apply (safe ; wpsimp) 2486 done 2487 2488lemma isZombie_Null: 2489 "\<not> isZombie NullCap" 2490 by (simp add: isCap_simps) 2491 2492lemma prepares_delete_helper'': 2493 assumes x: "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>rv. ko_wp_at' (Not \<circ> live') p\<rbrace>" 2494 shows "\<lbrace>P and K ((\<forall>x. cte_refs' cap x = {}) 2495 \<and> zobj_refs' cap = {p} 2496 \<and> threadCapRefs cap = {})\<rbrace> 2497 f \<lbrace>\<lambda>rv s. removeable' sl s cap\<rbrace>" 2498 apply (rule hoare_gen_asm) 2499 apply (rule hoare_strengthen_post [OF x]) 2500 apply (clarsimp simp: removeable'_def) 2501 done 2502 2503lemma ctes_of_cteCaps_of_lift: 2504 "\<lbrakk> \<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace> \<rbrakk> 2505 \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s)\<rbrace> f \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" 2506 by (wp | simp add: cteCaps_of_def)+ 2507 2508crunch ctes_of[wp]: finaliseCapTrue_standin, unbindNotification "\<lambda>s. P (ctes_of s)" 2509 (wp: crunch_wps getObject_inv loadObject_default_inv simp: crunch_simps ignore: getObject) 2510 2511lemma cteDeleteOne_cteCaps_of: 2512 "\<lbrace>\<lambda>s. (cte_wp_at' (\<lambda>cte. \<exists>final. finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow> 2513 P (cteCaps_of s(p \<mapsto> NullCap)))\<rbrace> 2514 cteDeleteOne p 2515 \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" 2516 apply (simp add: cteDeleteOne_def unless_def split_def) 2517 apply (rule hoare_seq_ext [OF _ getCTE_sp]) 2518 apply (case_tac "\<forall>final. finaliseCap (cteCap cte) final True = fail") 2519 apply (simp add: finaliseCapTrue_standin_simple_def) 2520 apply wp 2521 apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def 2522 finaliseCap_def isCap_simps) 2523 apply (drule_tac x=s in fun_cong) 2524 apply (simp add: return_def fail_def) 2525 apply (wp emptySlot_cteCaps_of) 2526 apply (simp add: cteCaps_of_def) 2527 apply (wp_once hoare_drop_imps) 2528 apply (wp isFinalCapability_inv getCTE_wp')+ 2529 apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of) 2530 apply (auto simp: fun_upd_idem fun_upd_def[symmetric] o_def) 2531 done 2532 2533lemma cteDeleteOne_isFinal: 2534 "\<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s)\<rbrace> 2535 cteDeleteOne p 2536 \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace>" 2537 apply (wp cteDeleteOne_cteCaps_of) 2538 apply (clarsimp simp: isFinal_def sameObjectAs_def2) 2539 done 2540 2541lemmas setEndpoint_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF set_ep_ctes_of] 2542lemmas setNotification_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF set_ntfn_ctes_of] 2543lemmas setQueue_cteCaps_of[wp] = ctes_of_cteCaps_of_lift [OF setQueue_ctes_of] 2544lemmas threadSet_cteCaps_of = ctes_of_cteCaps_of_lift [OF threadSet_ctes_of] 2545 2546crunch isFinal: suspend, prepareThreadDelete "\<lambda>s. isFinal cap slot (cteCaps_of s)" 2547 (ignore: setObject getObject threadSet 2548 wp: threadSet_cteCaps_of crunch_wps 2549 simp: crunch_simps unless_def o_def) 2550 2551lemma isThreadCap_threadCapRefs_tcbptr: 2552 "isThreadCap cap \<Longrightarrow> threadCapRefs cap = {capTCBPtr cap}" 2553 by (clarsimp simp: isCap_simps) 2554 2555lemma isArchObjectCap_Cap_capCap: 2556 "isArchObjectCap cap \<Longrightarrow> ArchObjectCap (capCap cap) = cap" 2557 by (clarsimp simp: isCap_simps) 2558 2559lemma cteDeleteOne_deletes[wp]: 2560 "\<lbrace>\<top>\<rbrace> cteDeleteOne p \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>c. cteCap c = NullCap) p s\<rbrace>" 2561 apply (subst tree_cte_cteCap_eq[unfolded o_def]) 2562 apply (wp cteDeleteOne_cteCaps_of) 2563 apply clarsimp 2564 done 2565 2566crunch irq_node'[wp]: finaliseCap "\<lambda>s. P (irq_node' s)" 2567 (wp: mapM_x_wp crunch_wps getObject_inv loadObject_default_inv 2568 updateObject_default_inv setObject_ksInterrupt 2569 ignore: getObject setObject 2570 simp: crunch_simps unless_def o_def) 2571 2572lemma deletingIRQHandler_removeable': 2573 "\<lbrace>invs' and (\<lambda>s. isFinal (IRQHandlerCap irq) slot (cteCaps_of s)) 2574 and K (cap = IRQHandlerCap irq)\<rbrace> 2575 deletingIRQHandler irq 2576 \<lbrace>\<lambda>rv s. removeable' slot s cap\<rbrace>" 2577 apply (rule hoare_gen_asm) 2578 apply (simp add: deletingIRQHandler_def getIRQSlot_def locateSlot_conv 2579 getInterruptState_def getSlotCap_def) 2580 apply (simp add: removeable'_def tree_cte_cteCap_eq[unfolded o_def]) 2581 apply (subst tree_cte_cteCap_eq[unfolded o_def])+ 2582 apply (wp hoare_use_eq_irq_node' [OF cteDeleteOne_irq_node' cteDeleteOne_cteCaps_of] 2583 getCTE_wp') 2584 apply (clarsimp simp: cte_level_bits_def ucast_nat_def split: option.split_asm) 2585 done 2586 2587lemma finaliseCap_cte_refs: 2588 "\<lbrace>\<lambda>s. s \<turnstile>' cap\<rbrace> 2589 finaliseCap cap final flag 2590 \<lbrace>\<lambda>rv s. fst rv \<noteq> NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace>" 2591 apply (simp add: finaliseCap_def Let_def getThreadCSpaceRoot 2592 ARM_H.finaliseCap_def 2593 cong: if_cong split del: if_split) 2594 apply (rule hoare_pre) 2595 apply (wp | wpc | simp only: o_def)+ 2596 apply (frule valid_capAligned) 2597 apply (cases cap, simp_all add: isCap_simps) 2598 apply (clarsimp simp: tcb_cte_cases_def word_count_from_top objBits_defs) 2599 apply clarsimp 2600 apply (rule ext, simp) 2601 apply (rule image_cong [OF _ refl]) 2602 apply (fastforce simp: capAligned_def objBits_simps shiftL_nat) 2603 done 2604 2605lemma deletingIRQHandler_final: 2606 "\<lbrace>\<lambda>s. isFinal cap slot (cteCaps_of s) 2607 \<and> (\<forall>final. finaliseCap cap final True = fail)\<rbrace> 2608 deletingIRQHandler irq 2609 \<lbrace>\<lambda>rv s. isFinal cap slot (cteCaps_of s)\<rbrace>" 2610 apply (simp add: deletingIRQHandler_def isFinal_def getIRQSlot_def 2611 getInterruptState_def locateSlot_conv getSlotCap_def) 2612 apply (wp cteDeleteOne_cteCaps_of getCTE_wp') 2613 apply (auto simp: sameObjectAs_def3) 2614 done 2615 2616declare suspend_unqueued [wp] 2617 2618lemma unbindNotification_valid_objs'_helper: 2619 "valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbBoundNotification_update (\<lambda>_. None) tcb) s " 2620 by (clarsimp simp: valid_bound_ntfn'_def valid_tcb'_def tcb_cte_cases_def 2621 split: option.splits ntfn.splits) 2622 2623lemma unbindNotification_valid_objs'_helper': 2624 "valid_ntfn' tcb s \<longrightarrow> valid_ntfn' (ntfnBoundTCB_update (\<lambda>_. None) tcb) s " 2625 by (clarsimp simp: valid_bound_tcb'_def valid_ntfn'_def 2626 split: option.splits ntfn.splits) 2627 2628lemma typ_at'_valid_tcb'_lift: 2629 assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" 2630 shows "\<lbrace>\<lambda>s. valid_tcb' tcb s\<rbrace> f \<lbrace>\<lambda>rv s. valid_tcb' tcb s\<rbrace>" 2631 including no_pre 2632 apply (simp add: valid_tcb'_def) 2633 apply (case_tac "tcbState tcb", simp_all add: valid_tcb_state'_def split_def valid_bound_ntfn'_def) 2634 apply (wp hoare_vcg_const_Ball_lift typ_at_lifts[OF P] 2635 | case_tac "tcbBoundNotification tcb", simp_all)+ 2636 done 2637 2638lemmas setNotification_valid_tcb' = typ_at'_valid_tcb'_lift [OF setNotification_typ_at'] 2639 2640lemma unbindNotification_valid_objs'[wp]: 2641 "\<lbrace>valid_objs'\<rbrace> 2642 unbindNotification t 2643 \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" 2644 apply (simp add: unbindNotification_def) 2645 apply (rule hoare_pre) 2646 apply (wp threadSet_valid_objs' gbn_wp' set_ntfn_valid_objs' hoare_vcg_all_lift 2647 setNotification_valid_tcb' getNotification_wp 2648 | wpc | clarsimp simp: setBoundNotification_def unbindNotification_valid_objs'_helper)+ 2649 apply (clarsimp elim!: obj_atE' simp: projectKOs) 2650 apply (rule valid_objsE', assumption+) 2651 apply (clarsimp simp: valid_obj'_def unbindNotification_valid_objs'_helper') 2652 done 2653 2654lemma unbindMaybeNotification_valid_objs'[wp]: 2655 "\<lbrace>valid_objs'\<rbrace> 2656 unbindMaybeNotification t 2657 \<lbrace>\<lambda>rv. valid_objs'\<rbrace>" 2658 apply (simp add: unbindMaybeNotification_def) 2659 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 2660 apply (rule hoare_pre) 2661 apply (wp threadSet_valid_objs' gbn_wp' set_ntfn_valid_objs' hoare_vcg_all_lift 2662 setNotification_valid_tcb' getNotification_wp 2663 | wpc | clarsimp simp: setBoundNotification_def unbindNotification_valid_objs'_helper)+ 2664 apply (clarsimp elim!: obj_atE' simp: projectKOs) 2665 apply (rule valid_objsE', assumption+) 2666 apply (clarsimp simp: valid_obj'_def unbindNotification_valid_objs'_helper') 2667 done 2668 2669lemma unbindNotification_sch_act_wf[wp]: 2670 "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> unbindNotification t 2671 \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 2672 apply (simp add: unbindNotification_def) 2673 apply (rule hoare_pre) 2674 apply (wp sbn_sch_act' | wpc | simp)+ 2675 done 2676 2677lemma unbindMaybeNotification_sch_act_wf[wp]: 2678 "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> unbindMaybeNotification t 2679 \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 2680 apply (simp add: unbindMaybeNotification_def) 2681 apply (rule hoare_pre) 2682 apply (wp sbn_sch_act' | wpc | simp)+ 2683 done 2684 2685lemma valid_cong: 2686 "\<lbrakk> \<And>s. P s = P' s; \<And>s. P' s \<Longrightarrow> f s = f' s; 2687 \<And>rv s' s. \<lbrakk> (rv, s') \<in> fst (f' s); P' s \<rbrakk> \<Longrightarrow> Q rv s' = Q' rv s' \<rbrakk> 2688 \<Longrightarrow> \<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace> = \<lbrace>P'\<rbrace> f' \<lbrace>Q'\<rbrace>" 2689 by (clarsimp simp add: valid_def, blast) 2690 2691lemma sym_refs_ntfn_bound_eq: "sym_refs (state_refs_of' s) 2692 \<Longrightarrow> obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = Some t) x s 2693 = bound_tcb_at' (\<lambda>st. st = Some x) t s" 2694 apply (rule iffI) 2695 apply (drule (1) sym_refs_obj_atD') 2696 apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs 2697 refs_of_rev') 2698 apply (drule(1) sym_refs_bound_tcb_atD') 2699 apply (clarsimp simp: obj_at'_def projectKOs ko_wp_at'_def refs_of_rev') 2700 done 2701 2702lemma unbindNotification_obj_at'_boundedness: 2703 "\<lbrace>obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = Some t \<or> ntfnBoundTCB ntfn = None) x 2704 and sym_refs o state_refs_of'\<rbrace> 2705 unbindNotification t 2706 \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) x s\<rbrace>" 2707 apply (simp add: unbindNotification_def) 2708 apply (rule hoare_seq_ext[OF _ gbn_sp']) 2709 apply (case_tac ntfnPtr) 2710 apply (wp | simp)+ 2711 apply clarsimp 2712 apply (frule sym_refs_ntfn_bound_eq[where t=t and x=x]) 2713 apply (clarsimp simp: obj_at'_def pred_tcb_at'_def) 2714 apply simp 2715 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 2716 apply (simp add: setBoundNotification_def threadSet_def setNotification_def) 2717 apply (wp obj_at_setObject2) 2718 apply (clarsimp simp: updateObject_default_def in_monad) 2719 apply wp 2720 apply (simp add: obj_at'_real_def cong: valid_cong) 2721 apply (wp setObject_ko_wp_at, (simp add: objBits_simps')+) 2722 apply clarsimp 2723 apply (frule sym_refs_ntfn_bound_eq[where t=t and x=x]) 2724 apply (clarsimp simp: pred_tcb_at'_def obj_at'_def ko_wp_at'_def projectKOs) 2725 done 2726 2727lemma unbindMaybeNotification_obj_at'_bound: 2728 "\<lbrace>\<top>\<rbrace> 2729 unbindMaybeNotification r 2730 \<lbrace>\<lambda>_ s. obj_at' (\<lambda>ntfn. ntfnBoundTCB ntfn = None) r s\<rbrace>" 2731 apply (simp add: unbindMaybeNotification_def) 2732 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 2733 apply (rule hoare_pre) 2734 apply (wp obj_at_setObject2 2735 | wpc 2736 | simp add: setBoundNotification_def threadSet_def updateObject_default_def in_monad projectKOs)+ 2737 apply (simp add: setNotification_def obj_at'_real_def cong: valid_cong) 2738 apply (wp setObject_ko_wp_at, (simp add: objBits_simps')+) 2739 apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs) 2740 done 2741 2742crunch isFinal[wp]: unbindNotification, unbindMaybeNotification "\<lambda>s. isFinal cap slot (cteCaps_of s)" 2743 (wp: sts_bound_tcb_at' threadSet_cteCaps_of crunch_wps getObject_inv 2744 loadObject_default_inv 2745 ignore: getObject setObject threadSet) 2746 2747crunch bound_tcb_at'[wp]: cancelSignal, cancelAllIPC "bound_tcb_at' P t" 2748 (wp: sts_bound_tcb_at' threadSet_cteCaps_of crunch_wps getObject_inv 2749 loadObject_default_inv 2750 ignore: getObject setObject threadSet) 2751 2752lemma finaliseCapTrue_standin_bound_tcb_at': 2753 "\<lbrace>\<lambda>s. bound_tcb_at' P t s \<and> (\<exists>tt b. cap = ReplyCap tt b) \<rbrace> finaliseCapTrue_standin cap final \<lbrace>\<lambda>_. bound_tcb_at' P t\<rbrace>" 2754 apply (case_tac cap, simp_all add:finaliseCapTrue_standin_def) 2755 apply (clarsimp simp: isNotificationCap_def) 2756 apply (wp, clarsimp) 2757 done 2758 2759lemma capDeleteOne_bound_tcb_at': 2760 "\<lbrace>bound_tcb_at' P tptr and cte_wp_at' (isReplyCap \<circ> cteCap) callerCap\<rbrace> 2761 cteDeleteOne callerCap \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>" 2762 apply (simp add: cteDeleteOne_def unless_def) 2763 apply (rule hoare_pre) 2764 apply (wp finaliseCapTrue_standin_bound_tcb_at' hoare_vcg_all_lift 2765 hoare_vcg_if_lift2 getCTE_cteCap_wp 2766 | wpc | simp | wp_once hoare_drop_imp)+ 2767 apply (clarsimp simp: cteCaps_of_def projectKOs isReplyCap_def cte_wp_at_ctes_of 2768 split: option.splits) 2769 apply (case_tac "cteCap cte", simp_all) 2770 done 2771 2772lemma cancelIPC_bound_tcb_at'[wp]: 2773 "\<lbrace>bound_tcb_at' P tptr\<rbrace> cancelIPC t \<lbrace>\<lambda>rv. bound_tcb_at' P tptr\<rbrace>" 2774 apply (simp add: cancelIPC_def Let_def) 2775 apply (rule hoare_seq_ext[OF _ gts_sp']) 2776 apply (case_tac "state", simp_all) 2777 defer 2 2778 apply (rule hoare_pre) 2779 apply ((wp sts_bound_tcb_at' getEndpoint_wp | wpc | simp)+)[8] 2780 apply (simp add: getThreadReplySlot_def locateSlot_conv liftM_def) 2781 apply (rule hoare_pre) 2782 apply (wp capDeleteOne_bound_tcb_at' getCTE_ctes_of) 2783 apply (rule_tac Q="\<lambda>_. bound_tcb_at' P tptr" in hoare_post_imp) 2784 apply (clarsimp simp: capHasProperty_def cte_wp_at_ctes_of) 2785 apply (wp threadSet_pred_tcb_no_state | simp)+ 2786 done 2787 2788crunch bound_tcb_at'[wp]: suspend, prepareThreadDelete "bound_tcb_at' P t" 2789 (wp: sts_bound_tcb_at' cancelIPC_bound_tcb_at' 2790 ignore: getObject setObject threadSet) 2791 2792lemma unbindNotification_bound_tcb_at': 2793 "\<lbrace>\<lambda>_. True\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. bound_tcb_at' ((=) None) t\<rbrace>" 2794 apply (simp add: unbindNotification_def) 2795 apply (wp setBoundNotification_bound_tcb gbn_wp' | wpc | simp)+ 2796 done 2797 2798lemma unbindMaybeNotification_bound_tcb_at': 2799 "\<lbrace>bound_tcb_at' (\<lambda>ntfn. ntfn = Some a \<or> ntfn = None) t 2800 and sym_refs o state_refs_of'\<rbrace> 2801 unbindMaybeNotification a 2802 \<lbrace>\<lambda>rv s. bound_tcb_at' ((=) None) t s\<rbrace>" 2803 apply (simp add: unbindMaybeNotification_def) 2804 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 2805 apply (case_tac "ntfnBoundTCB ntfn") 2806 apply (((wp threadSet_pred_tcb_at_state static_imp_wp hoare_drop_imps 2807 | clarsimp simp: setBoundNotification_def)+, 2808 drule (1) sym_refs_bound_tcb_atD', 2809 auto simp: tcb_ntfn_is_bound'_def obj_at'_def projectKOs ko_wp_at'_def 2810 pred_tcb_at'_def ntfn_q_refs_of'_def 2811 split: ntfn.splits)[1])+ 2812 done 2813 2814crunch valid_queues[wp]: unbindNotification, unbindMaybeNotification "Invariants_H.valid_queues" 2815 (wp: sbn_valid_queues) 2816 2817crunch weak_sch_act_wf[wp]: unbindNotification, unbindMaybeNotification "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s" 2818 2819lemma unbindNotification_tcb_at'[wp]: 2820 "\<lbrace>tcb_at' t'\<rbrace> unbindNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" 2821 apply (simp add: unbindNotification_def) 2822 apply (wp gbn_wp' | wpc | simp)+ 2823 done 2824 2825lemma unbindMaybeNotification_tcb_at'[wp]: 2826 "\<lbrace>tcb_at' t'\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>rv. tcb_at' t'\<rbrace>" 2827 apply (simp add: unbindMaybeNotification_def) 2828 apply (wp gbn_wp' | wpc | simp)+ 2829 done 2830 2831crunch cte_wp_at'[wp]: prepareThreadDelete "cte_wp_at' P p" 2832crunch valid_cap'[wp]: prepareThreadDelete "valid_cap' cap" 2833crunch invs[wp]: prepareThreadDelete "invs'" 2834 2835end 2836 2837lemma (in delete_one_conc_pre) finaliseCap_replaceable: 2838 "\<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s 2839 \<and> (final_matters' cap \<longrightarrow> (final = isFinal cap slot (cteCaps_of s))) 2840 \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> 2841 finaliseCap cap final flag 2842 \<lbrace>\<lambda>rv s. (isNullCap (fst rv) \<and> removeable' slot s cap 2843 \<and> (snd rv \<noteq> NullCap \<longrightarrow> snd rv = cap \<and> cap_has_cleanup' cap 2844 \<and> isFinal cap slot (cteCaps_of s))) 2845 \<or> 2846 (isZombie (fst rv) \<and> snd rv = NullCap 2847 \<and> isFinal cap slot (cteCaps_of s) 2848 \<and> capClass cap = capClass (fst rv) 2849 \<and> capUntypedPtr (fst rv) = capUntypedPtr cap 2850 \<and> capBits (fst rv) = capBits cap 2851 \<and> capRange (fst rv) = capRange cap 2852 \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap) 2853 \<and> (\<forall>p \<in> threadCapRefs cap. st_tcb_at' ((=) Inactive) p s 2854 \<and> obj_at' (Not \<circ> tcbQueued) p s 2855 \<and> bound_tcb_at' ((=) None) p s 2856 \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr))))\<rbrace>" 2857 apply (simp add: finaliseCap_def Let_def getThreadCSpaceRoot 2858 cong: if_cong split del: if_split) 2859 apply (rule hoare_pre) 2860 apply (wp prepares_delete_helper'' [OF cancelAllIPC_unlive] 2861 prepares_delete_helper'' [OF cancelAllSignals_unlive] 2862 suspend_isFinal prepareThreadDelete_unqueued prepareThreadDelete_nonq 2863 prepareThreadDelete_inactive prepareThreadDelete_isFinal 2864 suspend_makes_inactive suspend_nonq 2865 deletingIRQHandler_removeable' 2866 deletingIRQHandler_final[where slot=slot ] 2867 unbindNotification_obj_at'_boundedness 2868 unbindMaybeNotification_obj_at'_bound 2869 getNotification_wp 2870 suspend_bound_tcb_at' 2871 unbindNotification_bound_tcb_at' 2872 | simp add: isZombie_Null isThreadCap_threadCapRefs_tcbptr 2873 isArchObjectCap_Cap_capCap 2874 | (rule hoare_strengthen_post [OF arch_finaliseCap_removeable[where slot=slot]], 2875 clarsimp simp: isCap_simps) 2876 | wpc)+ 2877 2878 apply clarsimp 2879 apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp+) 2880 apply (case_tac "cteCap cte", 2881 simp_all add: isCap_simps capRange_def cap_has_cleanup'_def 2882 final_matters'_def objBits_simps 2883 not_Final_removeable finaliseCap_def, 2884 simp_all add: removeable'_def) 2885 (* thread *) 2886 apply (frule capAligned_capUntypedPtr [OF valid_capAligned], simp) 2887 apply (clarsimp simp: valid_cap'_def) 2888 apply (drule valid_globals_cte_wpD'[rotated], clarsimp) 2889 apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) 2890 apply (clarsimp simp: obj_at'_def | rule conjI)+ 2891 done 2892 2893lemma cteDeleteOne_cte_wp_at_preserved: 2894 assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail" 2895 shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> 2896 cteDeleteOne ptr 2897 \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>" 2898 apply (simp add: tree_cte_cteCap_eq[unfolded o_def]) 2899 apply (rule hoare_pre, wp cteDeleteOne_cteCaps_of) 2900 apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of x) 2901 done 2902 2903crunch ctes_of[wp]: cancelSignal "\<lambda>s. P (ctes_of s)" 2904 (simp: crunch_simps wp: crunch_wps) 2905 2906lemma cancelIPC_cteCaps_of: 2907 "\<lbrace>\<lambda>s. (\<forall>p. cte_wp_at' (\<lambda>cte. \<exists>final. finaliseCap (cteCap cte) final True \<noteq> fail) p s \<longrightarrow> 2908 P (cteCaps_of s(p \<mapsto> NullCap))) \<and> 2909 P (cteCaps_of s)\<rbrace> 2910 cancelIPC t 2911 \<lbrace>\<lambda>rv s. P (cteCaps_of s)\<rbrace>" 2912 apply (simp add: cancelIPC_def Let_def capHasProperty_def 2913 getThreadReplySlot_def locateSlot_conv) 2914 apply (rule hoare_pre) 2915 apply (wp cteDeleteOne_cteCaps_of getCTE_wp' | wpcw 2916 | simp add: cte_wp_at_ctes_of 2917 | wp_once hoare_drop_imps ctes_of_cteCaps_of_lift)+ 2918 apply (wp hoare_convert_imp hoare_vcg_all_lift 2919 threadSet_ctes_of threadSet_cteCaps_of 2920 | clarsimp)+ 2921 apply (wp cteDeleteOne_cteCaps_of getCTE_wp' | wpcw | simp 2922 | wp_once hoare_drop_imps ctes_of_cteCaps_of_lift)+ 2923 apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) 2924 apply (drule_tac x="mdbNext (cteMDBNode x)" in spec) 2925 apply clarsimp 2926 apply (auto simp: o_def map_option_case fun_upd_def[symmetric]) 2927 done 2928 2929lemma cancelIPC_cte_wp_at': 2930 assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail" 2931 shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace> 2932 cancelIPC t 2933 \<lbrace>\<lambda>rv s. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p s\<rbrace>" 2934 apply (simp add: tree_cte_cteCap_eq[unfolded o_def]) 2935 apply (rule hoare_pre, wp cancelIPC_cteCaps_of) 2936 apply (clarsimp simp: cteCaps_of_def cte_wp_at_ctes_of x) 2937 done 2938 2939crunch cte_wp_at'[wp]: tcbSchedDequeue "cte_wp_at' P p" 2940 2941lemma suspend_cte_wp_at': 2942 assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail" 2943 shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> 2944 suspend t 2945 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>" 2946 apply (simp add: suspend_def unless_def) 2947 apply (rule hoare_pre) 2948 apply (wp threadSet_cte_wp_at' cancelIPC_cte_wp_at' 2949 | simp add: x)+ 2950 done 2951 2952context begin interpretation Arch . (*FIXME: arch_split*) 2953 2954crunch cte_wp_at'[wp]: deleteASIDPool "cte_wp_at' P p" 2955 (simp: crunch_simps assertE_def 2956 wp: crunch_wps getObject_inv loadObject_default_inv 2957 ignore: getObject setObject) 2958 2959lemma deleteASID_cte_wp_at'[wp]: 2960 "\<lbrace>cte_wp_at' P p\<rbrace> deleteASID param_a param_b \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>" 2961 apply (simp add: deleteASID_def invalidateHWASIDEntry_def invalidateASID_def 2962 cong: option.case_cong) 2963 apply (wp setObject_cte_wp_at'[where Q="\<top>"] getObject_inv 2964 loadObject_default_inv setVMRoot_cte_wp_at' 2965 | clarsimp simp: updateObject_default_def in_monad 2966 projectKOs 2967 | rule equals0I 2968 | wpc)+ 2969 done 2970 2971crunch cte_wp_at'[wp]: unmapPageTable, unmapPage, unbindNotification, finaliseCapTrue_standin 2972 "cte_wp_at' P p" 2973 (simp: crunch_simps wp: crunch_wps getObject_inv loadObject_default_inv 2974 ignore: getObject setObject) 2975 2976lemma arch_finaliseCap_cte_wp_at[wp]: 2977 "\<lbrace>cte_wp_at' P p\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>" 2978 apply (simp add: ARM_H.finaliseCap_def) 2979 apply (safe ; wpsimp wp: unmapPage_cte_wp_at') 2980 done 2981 2982lemma deletingIRQHandler_cte_preserved: 2983 assumes x: "\<And>cap final. P cap \<Longrightarrow> finaliseCap cap final True = fail" 2984 shows "\<lbrace>cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace> 2985 deletingIRQHandler irq 2986 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) p\<rbrace>" 2987 apply (simp add: deletingIRQHandler_def getSlotCap_def 2988 getIRQSlot_def locateSlot_conv getInterruptState_def) 2989 apply (wp cteDeleteOne_cte_wp_at_preserved getCTE_wp' 2990 | simp add: x)+ 2991 done 2992 2993lemma finaliseCap_equal_cap[wp]: 2994 "\<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> 2995 finaliseCap cap fin flag 2996 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>" 2997 apply (simp add: finaliseCap_def Let_def 2998 cong: if_cong split del: if_split) 2999 apply (rule hoare_pre) 3000 apply (wp suspend_cte_wp_at' deletingIRQHandler_cte_preserved 3001 | clarsimp simp: finaliseCap_def | wpc)+ 3002 apply (case_tac cap) 3003 apply auto 3004 done 3005 3006lemma setThreadState_st_tcb_at_simplish': 3007 "simple' st \<Longrightarrow> 3008 \<lbrace>st_tcb_at' (P or simple') t\<rbrace> 3009 setThreadState st t' 3010 \<lbrace>\<lambda>rv. st_tcb_at' (P or simple') t\<rbrace>" 3011 apply (wp sts_st_tcb_at'_cases) 3012 apply clarsimp 3013 done 3014 3015lemmas setThreadState_st_tcb_at_simplish 3016 = setThreadState_st_tcb_at_simplish'[unfolded pred_disj_def] 3017 3018crunch st_tcb_at_simplish: cteDeleteOne 3019 "st_tcb_at' (\<lambda>st. P st \<or> simple' st) t" 3020 (wp: crunch_wps getObject_inv loadObject_default_inv threadSet_pred_tcb_no_state 3021 simp: crunch_simps unless_def ignore: getObject threadSet) 3022 3023lemma cteDeleteOne_st_tcb_at[wp]: 3024 assumes x[simp]: "\<And>st. simple' st \<longrightarrow> P st" shows 3025 "\<lbrace>st_tcb_at' P t\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv. st_tcb_at' P t\<rbrace>" 3026 apply (subgoal_tac "\<exists>Q. P = (Q or simple')") 3027 apply (clarsimp simp: pred_disj_def) 3028 apply (rule cteDeleteOne_st_tcb_at_simplish) 3029 apply (rule_tac x=P in exI) 3030 apply (auto intro!: ext) 3031 done 3032 3033lemma cteDeleteOne_reply_pred_tcb_at: 3034 "\<lbrace>\<lambda>s. pred_tcb_at' proj P t s \<and> (\<exists>t'. cte_wp_at' (\<lambda>cte. cteCap cte = ReplyCap t' False) slot s)\<rbrace> 3035 cteDeleteOne slot 3036 \<lbrace>\<lambda>rv. pred_tcb_at' proj P t\<rbrace>" 3037 apply (simp add: cteDeleteOne_def unless_def isFinalCapability_def) 3038 apply (rule hoare_seq_ext [OF _ getCTE_sp]) 3039 apply (rule hoare_assume_pre) 3040 apply (clarsimp simp: cte_wp_at_ctes_of when_def isCap_simps 3041 Let_def finaliseCapTrue_standin_def) 3042 apply (intro impI conjI, (wp | simp)+) 3043 done 3044 3045crunch sch_act_simple[wp]: cteDeleteOne, unbindNotification sch_act_simple 3046 (wp: crunch_wps ssa_sch_act_simple sts_sch_act_simple getObject_inv 3047 loadObject_default_inv 3048 simp: crunch_simps unless_def 3049 rule: sch_act_simple_lift 3050 ignore: getObject) 3051 3052crunch valid_queues[wp]: setSchedulerAction "Invariants_H.valid_queues" 3053 (simp: Invariants_H.valid_queues_def bitmapQ_defs valid_queues_no_bitmap_def) 3054 3055lemma rescheduleRequired_sch_act_not[wp]: 3056 "\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>rv. sch_act_not t\<rbrace>" 3057 apply (simp add: rescheduleRequired_def setSchedulerAction_def) 3058 apply (wp hoare_post_taut | simp)+ 3059 done 3060 3061crunch sch_act_not[wp]: cteDeleteOne "sch_act_not t" 3062 (simp: crunch_simps case_Null_If unless_def 3063 wp: crunch_wps getObject_inv loadObject_default_inv 3064 ignore: getObject) 3065 3066lemma cancelAllIPC_mapM_x_valid_queues: 3067 "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. \<forall>t\<in>set q. tcb_at' t s)\<rbrace> 3068 mapM_x (\<lambda>t. do 3069 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3070 tcbSchedEnqueue t 3071 od) q 3072 \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" 3073 apply (rule_tac R="\<lambda>_ s. (\<forall>t\<in>set q. tcb_at' t s) \<and> valid_objs' s" 3074 in hoare_post_add) 3075 apply (rule hoare_pre) 3076 apply (rule mapM_x_wp') 3077 apply (rule hoare_name_pre_state) 3078 apply (wp hoare_vcg_const_Ball_lift 3079 tcbSchedEnqueue_valid_queues tcbSchedEnqueue_not_st 3080 sts_valid_queues sts_st_tcb_at'_cases setThreadState_not_st 3081 | simp 3082 | ((elim conjE)?, drule (1) bspec, clarsimp elim!: obj_at'_weakenE simp: valid_tcb_state'_def))+ 3083 done 3084 3085lemma cancelAllIPC_mapM_x_ksSchedulerAction: 3086 "\<lbrace>sch_act_simple\<rbrace> 3087 mapM_x (\<lambda>t. do 3088 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3089 tcbSchedEnqueue t 3090 od) q 3091 \<lbrace>\<lambda>_. sch_act_simple\<rbrace>" 3092 apply (rule mapM_x_wp_inv) 3093 apply (wp tcbSchedEnqueue_nosch) 3094 done 3095 3096lemma cancelAllIPC_mapM_x_sch_act: 3097 "\<lbrace>\<lambda>s. sch_act_wf (ksSchedulerAction s) s\<rbrace> 3098 mapM_x (\<lambda>t. do 3099 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3100 tcbSchedEnqueue t 3101 od) q 3102 \<lbrace>\<lambda>rv s. sch_act_wf (ksSchedulerAction s) s\<rbrace>" 3103 apply (rule mapM_x_wp_inv) 3104 apply (wp) 3105 apply (clarsimp) 3106 done 3107 3108lemma cancelAllIPC_mapM_x_weak_sch_act: 3109 "\<lbrace>\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> 3110 mapM_x (\<lambda>t. do 3111 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3112 tcbSchedEnqueue t 3113 od) q 3114 \<lbrace>\<lambda>rv s. weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>" 3115 apply (rule mapM_x_wp_inv) 3116 apply (wp) 3117 apply (clarsimp) 3118 done 3119 3120lemma cancelAllIPC_mapM_x_valid_objs': 3121 "\<lbrace>valid_objs'\<rbrace> 3122 mapM_x (\<lambda>t. do 3123 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3124 tcbSchedEnqueue t 3125 od) q 3126 \<lbrace>\<lambda>_. valid_objs'\<rbrace>" 3127 apply (wp mapM_x_wp' sts_valid_objs') 3128 apply (clarsimp simp: valid_tcb_state'_def)+ 3129 done 3130 3131lemma cancelAllIPC_mapM_x_tcbDomain_obj_at': 3132 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> 3133 mapM_x (\<lambda>t. do 3134 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3135 tcbSchedEnqueue t 3136 od) q 3137 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3138apply (wp mapM_x_wp' tcbSchedEnqueue_not_st setThreadState_oa_queued | simp)+ 3139done 3140 3141lemma rescheduleRequired_oa_queued': 3142 "\<lbrace>obj_at' (\<lambda>tcb. Q (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace> 3143 rescheduleRequired 3144 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. Q (tcbDomain tcb) (tcbPriority tcb)) t'\<rbrace>" 3145apply (simp add: rescheduleRequired_def) 3146apply (wp tcbSchedEnqueue_not_st 3147 | wpc 3148 | simp)+ 3149done 3150 3151lemma cancelAllIPC_tcbDomain_obj_at': 3152 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> 3153 cancelAllIPC epptr 3154 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3155apply (simp add: cancelAllIPC_def) 3156apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift 3157 rescheduleRequired_oa_queued' cancelAllIPC_mapM_x_tcbDomain_obj_at' cancelAllIPC_mapM_x_ksSchedulerAction 3158 getEndpoint_wp 3159 | wpc 3160 | simp)+ 3161done 3162 3163lemma cancelAllIPC_valid_queues[wp]: 3164 "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> 3165 cancelAllIPC ep_ptr 3166 \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" 3167 apply (simp add: cancelAllIPC_def ep'_Idle_case_helper) 3168 apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift 3169 cancelAllIPC_mapM_x_valid_queues cancelAllIPC_mapM_x_valid_objs' cancelAllIPC_mapM_x_weak_sch_act 3170 set_ep_valid_objs' getEndpoint_wp) 3171 apply (clarsimp simp: valid_ep'_def) 3172 apply (drule (1) ko_at_valid_objs') 3173 apply (auto simp: valid_obj'_def valid_ep'_def valid_tcb'_def projectKOs 3174 split: endpoint.splits 3175 elim: valid_objs_valid_tcbE) 3176 done 3177 3178lemma cancelAllSignals_tcbDomain_obj_at': 3179 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> 3180 cancelAllSignals epptr 3181 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3182apply (simp add: cancelAllSignals_def) 3183apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift 3184 rescheduleRequired_oa_queued' cancelAllIPC_mapM_x_tcbDomain_obj_at' cancelAllIPC_mapM_x_ksSchedulerAction 3185 getNotification_wp 3186 | wpc 3187 | simp)+ 3188done 3189 3190lemma unbindNotification_tcbDomain_obj_at': 3191 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> 3192 unbindNotification t 3193 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3194 apply (simp add: unbindNotification_def) 3195 apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+ 3196 done 3197 3198lemma unbindMaybeNotification_tcbDomain_obj_at': 3199 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> 3200 unbindMaybeNotification r 3201 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3202 apply (simp add: unbindMaybeNotification_def) 3203 apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+ 3204 done 3205 3206lemma bindNotification_tcbDomain_obj_at': 3207 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> 3208 bindNotification t ntfn 3209 \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3210 apply (simp add: bindNotification_def) 3211 apply (wp setBoundNotification_oa_queued getNotification_wp gbn_wp' | wpc | simp)+ 3212 done 3213 3214lemma cancelAllSignals_valid_queues[wp]: 3215 "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> 3216 cancelAllSignals ntfn 3217 \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>" 3218 apply (simp add: cancelAllSignals_def) 3219 apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) 3220 apply (case_tac "ntfnObj ntfna", simp_all) 3221 apply (wp, simp)+ 3222 apply (wp hoare_vcg_conj_lift hoare_vcg_const_Ball_lift 3223 cancelAllIPC_mapM_x_valid_queues cancelAllIPC_mapM_x_valid_objs' cancelAllIPC_mapM_x_weak_sch_act 3224 set_ntfn_valid_objs' 3225 | simp)+ 3226 apply (clarsimp simp: valid_ep'_def) 3227 apply (drule (1) ko_at_valid_objs') 3228 apply (auto simp: valid_obj'_def valid_ntfn'_def valid_tcb'_def projectKOs 3229 split: endpoint.splits 3230 elim: valid_objs_valid_tcbE) 3231 done 3232 3233lemma finaliseCap_True_valid_queues[wp]: 3234 "\<lbrace> Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> 3235 finaliseCap cap final True 3236 \<lbrace>\<lambda>_. Invariants_H.valid_queues \<rbrace>" 3237 apply (simp add: finaliseCap_def Let_def) 3238 apply safe 3239 apply (wp irqs_masked_lift| simp | wpc)+ 3240 done 3241 3242lemma finaliseCapTrue_standin_valid_queues[wp]: 3243 "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> 3244 finaliseCapTrue_standin cap final 3245 \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" 3246 apply (simp add: finaliseCapTrue_standin_def Let_def) 3247 apply (safe) 3248 apply (wp | clarsimp | wpc)+ 3249 done 3250 3251 3252crunch valid_queues[wp]: isFinalCapability "Invariants_H.valid_queues" 3253 (simp: crunch_simps) 3254 3255crunch sch_act[wp]: isFinalCapability "\<lambda>s. sch_act_wf (ksSchedulerAction s) s" 3256 (simp: crunch_simps) 3257 3258crunch weak_sch_act[wp]: 3259 isFinalCapability "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s" 3260 (simp: crunch_simps) 3261 3262lemma cteDeleteOne_queues[wp]: 3263 "\<lbrace>Invariants_H.valid_queues and valid_objs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace> 3264 cteDeleteOne sl 3265 \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") 3266 apply (simp add: cteDeleteOne_def unless_def split_def) 3267 apply (wp isFinalCapability_inv getCTE_wp | rule hoare_drop_imps | simp)+ 3268 apply (clarsimp simp: cte_wp_at'_def) 3269 done 3270 3271lemma valid_inQ_queues_lift: 3272 assumes tat: "\<And>d p tcb. \<lbrace>obj_at' (inQ d p) tcb\<rbrace> f \<lbrace>\<lambda>_. obj_at' (inQ d p) tcb\<rbrace>" 3273 and prq: "\<And>P. \<lbrace>\<lambda>s. P (ksReadyQueues s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ksReadyQueues s)\<rbrace>" 3274 shows "\<lbrace>valid_inQ_queues\<rbrace> f \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" 3275 proof - 3276 show ?thesis 3277 apply (clarsimp simp: valid_def valid_inQ_queues_def) 3278 apply safe 3279 apply (rule use_valid [OF _ tat], assumption) 3280 apply (drule spec, drule spec, erule conjE, erule bspec) 3281 apply (rule ccontr) 3282 apply (erule notE[rotated], erule(1) use_valid [OF _ prq]) 3283 apply (erule use_valid [OF _ prq]) 3284 apply simp 3285 done 3286 qed 3287 3288lemma emptySlot_valid_inQ_queues [wp]: 3289 "\<lbrace>valid_inQ_queues\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" 3290 unfolding emptySlot_def 3291 by (wp opt_return_pres_lift | wpcw | wp valid_inQ_queues_lift | simp)+ 3292 3293crunch valid_inQ_queues[wp]: emptySlot valid_inQ_queues 3294 (simp: crunch_simps ignore: updateObject setObject) 3295 3296lemma cancelAllIPC_mapM_x_valid_inQ_queues: 3297 "\<lbrace>valid_inQ_queues\<rbrace> 3298 mapM_x (\<lambda>t. do 3299 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 3300 tcbSchedEnqueue t 3301 od) q 3302 \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" 3303 apply (rule mapM_x_wp_inv) 3304 apply (wp sts_valid_queues [where st="Structures_H.thread_state.Restart", simplified] 3305 setThreadState_st_tcb) 3306 done 3307 3308lemma cancelAllIPC_valid_inQ_queues[wp]: 3309 "\<lbrace>valid_inQ_queues\<rbrace> 3310 cancelAllIPC ep_ptr 3311 \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" 3312 apply (simp add: cancelAllIPC_def ep'_Idle_case_helper) 3313 apply (wp cancelAllIPC_mapM_x_valid_inQ_queues) 3314 apply (wp hoare_conjI hoare_drop_imp | simp)+ 3315 done 3316 3317lemma cancelAllSignals_valid_inQ_queues[wp]: 3318 "\<lbrace>valid_inQ_queues\<rbrace> 3319 cancelAllSignals ntfn 3320 \<lbrace>\<lambda>rv. valid_inQ_queues\<rbrace>" 3321 apply (simp add: cancelAllSignals_def) 3322 apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) 3323 apply (case_tac "ntfnObj ntfna", simp_all) 3324 apply (wp, simp)+ 3325 apply (wp cancelAllIPC_mapM_x_valid_inQ_queues)+ 3326 apply (simp) 3327 done 3328 3329crunch valid_inQ_queues[wp]: unbindNotification, unbindMaybeNotification "valid_inQ_queues" 3330 3331lemma finaliseCapTrue_standin_valid_inQ_queues[wp]: 3332 "\<lbrace>valid_inQ_queues\<rbrace> 3333 finaliseCapTrue_standin cap final 3334 \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" 3335 apply (simp add: finaliseCapTrue_standin_def Let_def) 3336 apply (safe) 3337 apply (wp | clarsimp | wpc)+ 3338 done 3339 3340crunch valid_inQ_queues[wp]: isFinalCapability valid_inQ_queues 3341 (simp: crunch_simps) 3342 3343lemma cteDeleteOne_valid_inQ_queues[wp]: 3344 "\<lbrace>valid_inQ_queues\<rbrace> 3345 cteDeleteOne sl 3346 \<lbrace>\<lambda>_. valid_inQ_queues\<rbrace>" 3347 apply (simp add: cteDeleteOne_def unless_def) 3348 apply (wpsimp wp: hoare_drop_imp hoare_vcg_all_lift) 3349 done 3350 3351crunch ksCurDomain[wp]: cteDeleteOne "\<lambda>s. P (ksCurDomain s)" 3352 (wp: crunch_wps simp: crunch_simps unless_def) 3353 3354lemma cteDeleteOne_tcbDomain_obj_at': 3355 "\<lbrace>obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>_. obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t'\<rbrace>" 3356 apply (simp add: cteDeleteOne_def unless_def split_def) 3357 apply (wp emptySlot_tcbDomain cancelAllIPC_tcbDomain_obj_at' cancelAllSignals_tcbDomain_obj_at' 3358 isFinalCapability_inv getCTE_wp unbindNotification_tcbDomain_obj_at' 3359 unbindMaybeNotification_tcbDomain_obj_at' 3360 | rule hoare_drop_imp 3361 | simp add: finaliseCapTrue_standin_def Let_def 3362 split del: if_split 3363 | wpc)+ 3364 apply (clarsimp simp: cte_wp_at'_def) 3365 done 3366 3367end 3368 3369global_interpretation delete_one_conc_pre 3370 by (unfold_locales, wp) (wp cteDeleteOne_tcbDomain_obj_at' cteDeleteOne_typ_at' cteDeleteOne_reply_pred_tcb_at | simp)+ 3371 3372lemma cteDeleteOne_invs[wp]: 3373 "\<lbrace>invs'\<rbrace> cteDeleteOne ptr \<lbrace>\<lambda>rv. invs'\<rbrace>" 3374 apply (simp add: cteDeleteOne_def unless_def 3375 split_def finaliseCapTrue_standin_simple_def) 3376 apply wp 3377 apply (rule hoare_strengthen_post) 3378 apply (rule hoare_vcg_conj_lift) 3379 apply (rule finaliseCap_True_invs) 3380 apply (rule hoare_vcg_conj_lift) 3381 apply (rule finaliseCap_replaceable[where slot=ptr]) 3382 apply (rule hoare_vcg_conj_lift) 3383 apply (rule finaliseCap_cte_refs) 3384 apply (rule finaliseCap_equal_cap[where sl=ptr]) 3385 apply (clarsimp simp: cte_wp_at_ctes_of) 3386 apply (erule disjE) 3387 apply simp 3388 apply (clarsimp dest!: isCapDs simp: capRemovable_def) 3389 apply (clarsimp simp: removeable'_def fun_eq_iff[where f="cte_refs' cap" for cap] 3390 del: disjCI) 3391 apply (rule disjI2) 3392 apply (rule conjI) 3393 subgoal by auto 3394 subgoal by (auto dest!: isCapDs simp: pred_tcb_at'_def obj_at'_def projectKOs 3395 ko_wp_at'_def) 3396 apply (wp isFinalCapability_inv getCTE_wp' static_imp_wp 3397 | wp_once isFinal[where x=ptr])+ 3398 apply (fastforce simp: cte_wp_at_ctes_of) 3399 done 3400 3401global_interpretation delete_one_conc_fr: delete_one_conc 3402 by unfold_locales wp 3403 3404declare cteDeleteOne_invs[wp] 3405 3406lemma deletingIRQHandler_invs' [wp]: 3407 "\<lbrace>invs'\<rbrace> deletingIRQHandler i \<lbrace>\<lambda>_. invs'\<rbrace>" 3408 apply (simp add: deletingIRQHandler_def getSlotCap_def 3409 getIRQSlot_def locateSlot_conv getInterruptState_def) 3410 apply (wp getCTE_wp') 3411 apply simp 3412 done 3413 3414crunch tcb_at'[wp]: unbindNotification, unbindMaybeNotification "tcb_at' t" 3415 3416lemma finaliseCap_invs: 3417 "\<lbrace>invs' and sch_act_simple and valid_cap' cap 3418 and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> 3419 finaliseCap cap fin flag 3420 \<lbrace>\<lambda>rv. invs'\<rbrace>" 3421 apply (simp add: finaliseCap_def Let_def 3422 cong: if_cong split del: if_split) 3423 apply (rule hoare_pre) 3424 apply (wp hoare_drop_imps hoare_vcg_all_lift | simp only: o_def | wpc)+ 3425 3426 apply clarsimp 3427 apply (intro conjI impI) 3428 apply (clarsimp dest!: isCapDs simp: valid_cap'_def) 3429 apply (drule invs_valid_global', drule(1) valid_globals_cte_wpD') 3430 apply (drule valid_capAligned, drule capAligned_capUntypedPtr) 3431 apply (clarsimp dest!: isCapDs) 3432 apply (clarsimp dest!: isCapDs) 3433 apply (clarsimp dest!: isCapDs) 3434 done 3435 3436lemma finaliseCap_zombie_cap[wp]: 3437 "\<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace> 3438 finaliseCap cap fin flag 3439 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace>" 3440 apply (simp add: finaliseCap_def Let_def 3441 cong: if_cong split del: if_split) 3442 apply (rule hoare_pre) 3443 apply (wp suspend_cte_wp_at' 3444 deletingIRQHandler_cte_preserved 3445 | clarsimp simp: finaliseCap_def isCap_simps | wpc)+ 3446 done 3447 3448lemma finaliseCap_zombie_cap': 3449 "\<lbrace>cte_wp_at' (\<lambda>cte. (P and isZombie) (cteCap cte)) sl\<rbrace> 3450 finaliseCap cap fin flag 3451 \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. P (cteCap cte)) sl\<rbrace>" 3452 apply (rule hoare_strengthen_post) 3453 apply (rule finaliseCap_zombie_cap) 3454 apply (clarsimp simp: cte_wp_at_ctes_of) 3455 done 3456 3457lemma finaliseCap_cte_cap_wp_to[wp]: 3458 "\<lbrace>ex_cte_cap_wp_to' P sl\<rbrace> finaliseCap cap fin flag \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P sl\<rbrace>" 3459 apply (simp add: ex_cte_cap_to'_def) 3460 apply (rule hoare_pre, rule hoare_use_eq_irq_node' [OF finaliseCap_irq_node']) 3461 apply (simp add: finaliseCap_def Let_def 3462 cong: if_cong split del: if_split) 3463 apply (wp suspend_cte_wp_at' 3464 deletingIRQHandler_cte_preserved 3465 hoare_vcg_ex_lift 3466 | clarsimp simp: finaliseCap_def isCap_simps 3467 | rule conjI 3468 | wpc)+ 3469 apply fastforce 3470 done 3471 3472crunch valid_cap'[wp]: unbindNotification "valid_cap' cap" 3473 3474lemma finaliseCap_valid_cap[wp]: 3475 "\<lbrace>valid_cap' cap\<rbrace> finaliseCap cap final flag \<lbrace>\<lambda>rv. valid_cap' (fst rv)\<rbrace>" 3476 apply (simp add: finaliseCap_def Let_def 3477 getThreadCSpaceRoot 3478 ARM_H.finaliseCap_def 3479 cong: if_cong split del: if_split) 3480 apply (rule hoare_pre) 3481 apply (wp | simp only: valid_NullCap o_def fst_conv | wpc)+ 3482 apply simp 3483 apply (intro conjI impI) 3484 apply (clarsimp simp: valid_cap'_def isCap_simps capAligned_def 3485 objBits_simps shiftL_nat)+ 3486 done 3487 3488 3489context begin interpretation Arch . (*FIXME: arch_split*) 3490 3491crunch nosch[wp]: "Arch.finaliseCap" "\<lambda>s. P (ksSchedulerAction s)" 3492 (wp: crunch_wps getObject_inv simp: loadObject_default_def updateObject_default_def 3493 ignore: getObject) 3494 3495crunch sch_act_simple[wp]: finaliseCap sch_act_simple 3496 (simp: crunch_simps 3497 rule: sch_act_simple_lift 3498 wp: getObject_inv loadObject_default_inv crunch_wps 3499 ignore: getObject) 3500 3501end 3502 3503 3504lemma interrupt_cap_null_or_ntfn: 3505 "invs s 3506 \<Longrightarrow> cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) (interrupt_irq_node s irq, []) s" 3507 apply (frule invs_valid_irq_node) 3508 apply (clarsimp simp: valid_irq_node_def) 3509 apply (drule_tac x=irq in spec) 3510 apply (drule cte_at_0) 3511 apply (clarsimp simp: cte_wp_at_caps_of_state) 3512 apply (drule caps_of_state_cteD) 3513 apply (frule if_unsafe_then_capD, clarsimp+) 3514 apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) 3515 apply (frule cte_refs_obj_refs_elem, erule disjE) 3516 apply (clarsimp | drule caps_of_state_cteD valid_global_refsD[rotated] 3517 | rule irq_node_global_refs[where irq=irq])+ 3518 apply (simp add: cap_range_def) 3519 apply (clarsimp simp: appropriate_cte_cap_def 3520 split: cap.split_asm) 3521 done 3522 3523lemma (in delete_one) deleting_irq_corres: 3524 "corres dc (einvs) (invs') 3525 (deleting_irq_handler irq) (deletingIRQHandler irq)" 3526 apply (simp add: deleting_irq_handler_def deletingIRQHandler_def) 3527 apply (rule corres_guard_imp) 3528 apply (rule corres_split [OF _ get_irq_slot_corres]) 3529 apply simp 3530 apply (rule_tac P'="cte_at' (cte_map slot)" in corres_symb_exec_r_conj) 3531 apply (rule_tac F="isNotificationCap rv \<or> rv = capability.NullCap" 3532 and P="cte_wp_at (\<lambda>cp. is_ntfn_cap cp \<or> cp = cap.NullCap) slot 3533 and einvs" 3534 and P'="invs' and cte_wp_at' (\<lambda>cte. cteCap cte = rv) 3535 (cte_map slot)" in corres_req) 3536 apply (clarsimp simp: cte_wp_at_caps_of_state state_relation_def) 3537 apply (drule caps_of_state_cteD) 3538 apply (drule(1) pspace_relation_cte_wp_at, clarsimp+) 3539 apply (auto simp: cte_wp_at_ctes_of is_cap_simps isCap_simps)[1] 3540 apply simp 3541 apply (rule corres_guard_imp, rule delete_one_corres[unfolded dc_def]) 3542 apply (auto simp: cte_wp_at_caps_of_state is_cap_simps can_fast_finalise_def)[1] 3543 apply (clarsimp simp: cte_wp_at_ctes_of) 3544 apply (wp getCTE_wp' | simp add: getSlotCap_def)+ 3545 apply (wp | simp add: get_irq_slot_def getIRQSlot_def 3546 locateSlot_conv getInterruptState_def)+ 3547 apply (clarsimp simp: ex_cte_cap_wp_to_def interrupt_cap_null_or_ntfn) 3548 apply (clarsimp simp: cte_wp_at_ctes_of) 3549 done 3550 3551context begin interpretation Arch . (*FIXME: arch_split*) 3552 3553lemma arch_finalise_cap_corres: 3554 "\<lbrakk> final_matters' (ArchObjectCap cap') \<Longrightarrow> final = final'; acap_relation cap cap' \<rbrakk> 3555 \<Longrightarrow> corres (\<lambda>r r'. cap_relation (fst r) (fst r') \<and> cap_relation (snd r) (snd r')) 3556 (\<lambda>s. invs s \<and> valid_etcbs s 3557 \<and> s \<turnstile> cap.ArchObjectCap cap 3558 \<and> (final_matters (cap.ArchObjectCap cap) 3559 \<longrightarrow> final = is_final_cap' (cap.ArchObjectCap cap) s) 3560 \<and> cte_wp_at ((=) (cap.ArchObjectCap cap)) sl s) 3561 (\<lambda>s. invs' s \<and> s \<turnstile>' ArchObjectCap cap' \<and> 3562 (final_matters' (ArchObjectCap cap') \<longrightarrow> 3563 final' = isFinal (ArchObjectCap cap') (cte_map sl) (cteCaps_of s))) 3564 (arch_finalise_cap cap final) (Arch.finaliseCap cap' final')" 3565 apply (cases cap; 3566 clarsimp simp: arch_finalise_cap_def ARM_H.finaliseCap_def 3567 final_matters'_def case_bool_If liftM_def[symmetric] 3568 isASIDPoolCap_def isPageCap_def isPageDirectoryCap_def 3569 isPageTableCap_def 3570 o_def dc_def[symmetric] 3571 split: option.split) 3572 apply (rule corres_guard_imp, rule delete_asid_pool_corres) 3573 apply (clarsimp simp: valid_cap_def mask_def) 3574 apply (clarsimp simp: valid_cap'_def) 3575 apply auto[1] 3576 apply (rule corres_guard_imp, rule unmap_page_corres) 3577 apply simp 3578 apply (clarsimp simp: valid_cap_def valid_unmap_def) 3579 apply (auto simp: vmsz_aligned_def pbfs_atleast_pageBits mask_def 3580 elim: is_aligned_weaken invs_valid_asid_map)[2] 3581 apply (rule corres_guard_imp, rule unmap_page_table_corres) 3582 apply (auto simp: valid_cap_def valid_cap'_def mask_def 3583 elim!: is_aligned_weaken invs_valid_asid_map)[2] 3584 apply (rule corres_guard_imp, rule delete_asid_corres) 3585 apply (auto elim!: invs_valid_asid_map simp: mask_def valid_cap_def)[2] 3586 done 3587 3588lemma ntfnBoundTCB_update_ntfnObj_inv[simp]: 3589 "ntfnObj (ntfnBoundTCB_update f ntfn) = ntfnObj ntfn" 3590 by auto 3591 3592lemma unbind_notification_corres: 3593 "corres dc 3594 (invs and tcb_at t) 3595 (invs' and tcb_at' t) 3596 (unbind_notification t) 3597 (unbindNotification t)" 3598 apply (simp add: unbind_notification_def unbindNotification_def) 3599 apply (rule corres_guard_imp) 3600 apply (rule corres_split[OF _ gbn_corres]) 3601 apply (rule corres_option_split) 3602 apply simp 3603 apply (rule corres_return_trivial) 3604 apply (rule corres_split[OF _ get_ntfn_corres]) 3605 apply clarsimp 3606 apply (rule corres_split[OF _ set_ntfn_corres]) 3607 apply (rule sbn_corres) 3608 apply (clarsimp simp: ntfn_relation_def split:Structures_A.ntfn.splits) 3609 apply (wp gbn_wp' gbn_wp)+ 3610 apply (clarsimp elim!: obj_at_valid_objsE 3611 dest!: bound_tcb_at_state_refs_ofD invs_valid_objs 3612 simp: valid_obj_def is_tcb tcb_ntfn_is_bound_def 3613 valid_tcb_def valid_bound_ntfn_def 3614 split: option.splits) 3615 apply (clarsimp dest!: obj_at_valid_objs' bound_tcb_at_state_refs_ofD' invs_valid_objs' 3616 simp: projectKOs valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def 3617 tcb_ntfn_is_bound'_def 3618 split: option.splits) 3619 done 3620 3621lemma unbind_maybe_notification_corres: 3622 "corres dc 3623 (invs and ntfn_at ntfnptr) (invs' and ntfn_at' ntfnptr) 3624 (unbind_maybe_notification ntfnptr) 3625 (unbindMaybeNotification ntfnptr)" 3626 apply (simp add: unbind_maybe_notification_def unbindMaybeNotification_def) 3627 apply (rule corres_guard_imp) 3628 apply (rule corres_split[OF _ get_ntfn_corres]) 3629 apply (rule corres_option_split) 3630 apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) 3631 apply (rule corres_return_trivial) 3632 apply simp 3633 apply (rule corres_split[OF _ set_ntfn_corres]) 3634 apply (rule sbn_corres) 3635 apply (clarsimp simp: ntfn_relation_def split: Structures_A.ntfn.splits) 3636 apply (wp get_simple_ko_wp getNotification_wp)+ 3637 apply (clarsimp elim!: obj_at_valid_objsE 3638 dest!: bound_tcb_at_state_refs_ofD invs_valid_objs 3639 simp: valid_obj_def is_tcb tcb_ntfn_is_bound_def 3640 valid_tcb_def valid_bound_ntfn_def valid_ntfn_def 3641 split: option.splits) 3642 apply (clarsimp dest!: obj_at_valid_objs' bound_tcb_at_state_refs_ofD' invs_valid_objs' 3643 simp: projectKOs valid_obj'_def valid_tcb'_def valid_bound_ntfn'_def 3644 tcb_ntfn_is_bound'_def valid_ntfn'_def 3645 split: option.splits) 3646 done 3647 3648lemma fast_finalise_corres: 3649 "\<lbrakk> final_matters' cap' \<longrightarrow> final = final'; cap_relation cap cap'; 3650 can_fast_finalise cap \<rbrakk> 3651 \<Longrightarrow> corres dc 3652 (\<lambda>s. invs s \<and> valid_sched s \<and> s \<turnstile> cap 3653 \<and> cte_wp_at ((=) cap) sl s) 3654 (\<lambda>s. invs' s \<and> s \<turnstile>' cap') 3655 (fast_finalise cap final) 3656 (do 3657 p \<leftarrow> finaliseCap cap' final' True; 3658 assert (capRemovable (fst p) (cte_map ptr) \<and> snd p = NullCap) 3659 od)" 3660 apply (cases cap, simp_all add: finaliseCap_def isCap_simps 3661 corres_liftM2_simp[unfolded liftM_def] 3662 o_def dc_def[symmetric] when_def 3663 can_fast_finalise_def capRemovable_def 3664 split del: if_split cong: if_cong) 3665 apply (clarsimp simp: final_matters'_def) 3666 apply (rule corres_guard_imp) 3667 apply (rule corres_rel_imp) 3668 apply (rule ep_cancel_corres) 3669 apply simp 3670 apply (simp add: valid_cap_def) 3671 apply (simp add: valid_cap'_def) 3672 apply (clarsimp simp: final_matters'_def) 3673 apply (rule corres_guard_imp) 3674 apply (rule corres_split[OF _ unbind_maybe_notification_corres]) 3675 apply (rule ntfn_cancel_corres) 3676 apply (wp abs_typ_at_lifts unbind_maybe_notification_invs typ_at_lifts hoare_drop_imps getNotification_wp 3677 | wpc)+ 3678 apply (clarsimp simp: valid_cap_def) 3679 apply (clarsimp simp: valid_cap'_def projectKOs valid_obj'_def 3680 dest!: invs_valid_objs' obj_at_valid_objs' ) 3681 done 3682 3683lemma cap_delete_one_corres: 3684 "corres dc (einvs and cte_wp_at can_fast_finalise ptr) 3685 (invs' and cte_at' (cte_map ptr)) 3686 (cap_delete_one ptr) (cteDeleteOne (cte_map ptr))" 3687 apply (simp add: cap_delete_one_def cteDeleteOne_def' 3688 unless_def when_def) 3689 apply (rule corres_guard_imp) 3690 apply (rule corres_split [OF _ get_cap_corres]) 3691 apply (rule_tac F="can_fast_finalise cap" in corres_gen_asm) 3692 apply (rule corres_if) 3693 apply fastforce 3694 apply (rule corres_split [OF _ final_cap_corres[where ptr=ptr]]) 3695 apply (simp add: split_def bind_assoc [THEN sym]) 3696 apply (rule corres_split [OF _ fast_finalise_corres[where sl=ptr]]) 3697 apply (rule empty_slot_corres) 3698 apply simp+ 3699 apply (wp hoare_drop_imps)+ 3700 apply (wp isFinalCapability_inv | wp_once isFinal[where x="cte_map ptr"])+ 3701 apply (rule corres_trivial, simp) 3702 apply (wp get_cap_wp getCTE_wp)+ 3703 apply (clarsimp simp: cte_wp_at_caps_of_state can_fast_finalise_Null 3704 elim!: caps_of_state_valid_cap) 3705 apply (clarsimp simp: cte_wp_at_ctes_of) 3706 apply fastforce 3707 done 3708end 3709(* FIXME: strengthen locale instead *) 3710 3711global_interpretation delete_one 3712 apply unfold_locales 3713 apply (rule corres_guard_imp) 3714 apply (rule cap_delete_one_corres) 3715 apply auto 3716 done 3717 3718lemma finalise_cap_corres: 3719 "\<lbrakk> final_matters' cap' \<Longrightarrow> final = final'; cap_relation cap cap'; 3720 flag \<longrightarrow> can_fast_finalise cap \<rbrakk> 3721 \<Longrightarrow> corres (\<lambda>x y. cap_relation (fst x) (fst y) \<and> cap_relation (snd x) (snd y)) 3722 (\<lambda>s. einvs s \<and> s \<turnstile> cap \<and> (final_matters cap \<longrightarrow> final = is_final_cap' cap s) 3723 \<and> cte_wp_at ((=) cap) sl s) 3724 (\<lambda>s. invs' s \<and> s \<turnstile>' cap' \<and> 3725 (final_matters' cap' \<longrightarrow> 3726 final' = isFinal cap' (cte_map sl) (cteCaps_of s))) 3727 (finalise_cap cap final) (finaliseCap cap' final' flag)" 3728 apply (cases cap, simp_all add: finaliseCap_def isCap_simps 3729 corres_liftM2_simp[unfolded liftM_def] 3730 o_def dc_def[symmetric] when_def 3731 can_fast_finalise_def 3732 split del: if_split cong: if_cong) 3733 apply (clarsimp simp: final_matters'_def) 3734 apply (rule corres_guard_imp) 3735 apply (rule ep_cancel_corres) 3736 apply (simp add: valid_cap_def) 3737 apply (simp add: valid_cap'_def) 3738 apply (clarsimp simp add: final_matters'_def) 3739 apply (rule corres_guard_imp) 3740 apply (rule corres_split[OF _ unbind_maybe_notification_corres]) 3741 apply (rule ntfn_cancel_corres) 3742 apply (wp abs_typ_at_lifts unbind_maybe_notification_invs typ_at_lifts hoare_drop_imps hoare_vcg_all_lift | wpc)+ 3743 apply (clarsimp simp: valid_cap_def) 3744 apply (clarsimp simp: valid_cap'_def) 3745 apply (fastforce simp: final_matters'_def shiftL_nat zbits_map_def) 3746 apply (clarsimp simp add: final_matters'_def getThreadCSpaceRoot 3747 liftM_def[symmetric] o_def zbits_map_def 3748 dc_def[symmetric]) 3749 apply (rule corres_guard_imp) 3750 apply (rule corres_split[OF _ unbind_notification_corres]) 3751 apply (rule corres_split[OF _ suspend_corres]) 3752 apply (clarsimp simp: liftM_def[symmetric] o_def dc_def[symmetric] zbits_map_def) 3753 apply (rule prepareThreadDelete_corres) 3754 apply (wp unbind_notification_invs unbind_notification_simple_sched_action)+ 3755 apply (simp add: valid_cap_def) 3756 apply (simp add: valid_cap'_def) 3757 apply (simp add: final_matters'_def liftM_def[symmetric] 3758 o_def dc_def[symmetric]) 3759 apply (intro impI, rule corres_guard_imp) 3760 apply (rule deleting_irq_corres) 3761 apply simp 3762 apply simp 3763 apply (clarsimp simp: final_matters'_def) 3764 apply (rule_tac F="False" in corres_req) 3765 apply clarsimp 3766 apply (frule zombies_finalD, (clarsimp simp: is_cap_simps)+) 3767 apply (clarsimp simp: cte_wp_at_caps_of_state) 3768 apply simp 3769 apply (clarsimp split del: if_split simp: o_def) 3770 apply (rule corres_guard_imp [OF arch_finalise_cap_corres], (fastforce simp: valid_sched_def)+) 3771 done 3772context begin interpretation Arch . (*FIXME: arch_split*) 3773lemma arch_recycleCap_improve_cases: 3774 "\<lbrakk> \<not> isPageCap cap; \<not> isPageTableCap cap; \<not> isPageDirectoryCap cap; 3775 \<not> isASIDControlCap cap \<rbrakk> \<Longrightarrow> (if isASIDPoolCap cap then v else undefined) = v" 3776 by (cases cap, simp_all add: isCap_simps) 3777 3778crunch queues[wp]: copyGlobalMappings "Invariants_H.valid_queues" 3779 (wp: crunch_wps ignore: storePDE getObject) 3780 3781crunch queues'[wp]: copyGlobalMappings "Invariants_H.valid_queues'" 3782 (wp: crunch_wps ignore: storePDE getObject) 3783 3784crunch ifunsafe'[wp]: copyGlobalMappings "if_unsafe_then_cap'" 3785 (wp: crunch_wps ignore: storePDE getObject) 3786 3787lemma copyGlobalMappings_pde_mappings2': 3788 "\<lbrace>valid_pde_mappings' and valid_arch_state' 3789 and K (is_aligned pd pdBits)\<rbrace> 3790 copyGlobalMappings pd \<lbrace>\<lambda>rv. valid_pde_mappings'\<rbrace>" 3791 apply (wp copyGlobalMappings_pde_mappings') 3792 apply (clarsimp simp: valid_arch_state'_def page_directory_at'_def) 3793 done 3794 3795crunch pred_tcb_at'[wp]: copyGlobalMappings "pred_tcb_at' proj P t" 3796 (wp: crunch_wps ignore: storePDE getObject) 3797 3798crunch vms'[wp]: copyGlobalMappings "valid_machine_state'" 3799 (wp: crunch_wps ignore: storePDE getObject) 3800 3801crunch ct_not_inQ[wp]: copyGlobalMappings "ct_not_inQ" 3802 (wp: crunch_wps ignore: storePDE getObject) 3803 3804crunch tcb_in_cur_domain'[wp]: copyGlobalMappings "tcb_in_cur_domain' t" 3805 (wp: crunch_wps ignore: getObject) 3806 3807crunch ct__in_cur_domain'[wp]: copyGlobalMappings ct_idle_or_in_cur_domain' 3808 (wp: crunch_wps ignore: getObject) 3809 3810crunch gsUntypedZeroRanges[wp]: copyGlobalMappings "\<lambda>s. P (gsUntypedZeroRanges s)" 3811 (wp: crunch_wps ignore: getObject) 3812 3813lemma copyGlobalMappings_invs'[wp]: 3814 "\<lbrace>invs' and K (is_aligned pd pdBits)\<rbrace> copyGlobalMappings pd \<lbrace>\<lambda>rv. invs'\<rbrace>" 3815 apply (simp add: invs'_def valid_state'_def valid_pspace'_def) 3816 apply (rule hoare_pre) 3817 apply (wp valid_irq_node_lift_asm valid_global_refs_lift' sch_act_wf_lift 3818 valid_irq_handlers_lift'' cur_tcb_lift typ_at_lifts irqs_masked_lift 3819 copyGlobalMappings_pde_mappings2' 3820 untyped_ranges_zero_lift 3821 | clarsimp simp: cteCaps_of_def o_def)+ 3822 done 3823 3824lemma dmo'_bind_return: 3825 "\<lbrace>P\<rbrace> doMachineOp f \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> 3826 \<lbrace>P\<rbrace> doMachineOp (do _ \<leftarrow> f; return x od) \<lbrace>\<lambda>_. Q\<rbrace>" 3827 by (clarsimp simp: doMachineOp_def bind_def return_def valid_def select_f_def 3828 split_def) 3829 3830lemma ct_in_current_domain_ArchState_update[simp]: 3831 "ct_idle_or_in_cur_domain' (s\<lparr>ksArchState := v\<rparr>) = ct_idle_or_in_cur_domain' s" 3832 by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 3833 3834lemma threadSet_ct_idle_or_in_cur_domain': 3835 "\<lbrace>ct_idle_or_in_cur_domain' and (\<lambda>s. \<forall>tcb. tcbDomain tcb = ksCurDomain s \<longrightarrow> tcbDomain (F tcb) = ksCurDomain s)\<rbrace> 3836 threadSet F t 3837 \<lbrace>\<lambda>_. ct_idle_or_in_cur_domain'\<rbrace>" 3838apply (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 3839apply (wp hoare_vcg_disj_lift hoare_vcg_imp_lift) 3840 apply wps 3841 apply wp 3842 apply wps 3843 apply wp 3844apply (auto simp: obj_at'_def) 3845done 3846 3847crunch typ_at'[wp]: invalidateTLBByASID "\<lambda>s. P (typ_at' T p s)" 3848crunch valid_arch_state'[wp]: invalidateTLBByASID "valid_arch_state'" 3849lemmas invalidateTLBByASID_typ_ats[wp] = typ_at_lifts [OF invalidateTLBByASID_typ_at'] 3850 3851lemma cte_wp_at_norm_eq': 3852 "cte_wp_at' P p s = (\<exists>cte. cte_wp_at' ((=) cte) p s \<and> P cte)" 3853 by (simp add: cte_wp_at_ctes_of) 3854 3855lemma isFinal_cte_wp_def: 3856 "isFinal cap p (cteCaps_of s) = 3857 (\<not>isUntypedCap cap \<and> 3858 (\<forall>p'. p \<noteq> p' \<longrightarrow> 3859 cte_at' p' s \<longrightarrow> 3860 cte_wp_at' (\<lambda>cte'. \<not> isUntypedCap (cteCap cte') \<longrightarrow> 3861 \<not> sameObjectAs cap (cteCap cte')) p' s))" 3862 apply (simp add: isFinal_def cte_wp_at_ctes_of cteCaps_of_def) 3863 apply (rule iffI) 3864 apply clarsimp 3865 apply (case_tac cte) 3866 apply fastforce 3867 apply fastforce 3868 done 3869 3870lemma valid_cte_at_neg_typ': 3871 assumes T: "\<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>" 3872 shows "\<lbrace>\<lambda>s. \<not> cte_at' p' s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> cte_at' p' s\<rbrace>" 3873 apply (simp add: cte_at_typ') 3874 apply (rule hoare_vcg_conj_lift [OF T]) 3875 apply (simp only: imp_conv_disj) 3876 apply (rule hoare_vcg_all_lift) 3877 apply (rule hoare_vcg_disj_lift [OF T]) 3878 apply (rule hoare_vcg_prop) 3879 done 3880 3881lemma isFinal_lift: 3882 assumes x: "\<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>_. cte_wp_at' P p\<rbrace>" 3883 assumes y: "\<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>" 3884 shows "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>cte. isFinal (cteCap cte) sl (cteCaps_of s)) sl s\<rbrace> 3885 f 3886 \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>cte. isFinal (cteCap cte) sl (cteCaps_of s)) sl s\<rbrace>" 3887 apply (subst cte_wp_at_norm_eq') 3888 apply (subst cte_wp_at_norm_eq' [where P="\<lambda>cte. isFinal (cteCap cte) sl m" for sl m]) 3889 apply (simp only: isFinal_cte_wp_def imp_conv_disj de_Morgan_conj) 3890 apply (wp hoare_vcg_ex_lift hoare_vcg_all_lift x hoare_vcg_disj_lift 3891 valid_cte_at_neg_typ' [OF y]) 3892 done 3893 3894crunch cteCaps_of: invalidateTLBByASID "\<lambda>s. P (cteCaps_of s)" 3895 3896crunch valid_etcbs[wp]: invalidate_tlb_by_asid valid_etcbs 3897 3898lemma cteCaps_of_ctes_of_lift: 3899 "(\<And>P. \<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> f \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. P (cteCaps_of s) \<rbrace> f \<lbrace>\<lambda>_ s. P (cteCaps_of s)\<rbrace>" 3900 unfolding cteCaps_of_def . 3901 3902lemmas final_matters'_simps = final_matters'_def [split_simps capability.split arch_capability.split] 3903 3904definition set_thread_all :: "obj_ref \<Rightarrow> Structures_A.tcb \<Rightarrow> etcb 3905 \<Rightarrow> unit det_ext_monad" where 3906 "set_thread_all ptr tcb etcb \<equiv> 3907 do s \<leftarrow> get; 3908 kh \<leftarrow> return $ kheap s(ptr \<mapsto> (TCB tcb)); 3909 ekh \<leftarrow> return $ (ekheap s)(ptr \<mapsto> etcb); 3910 put (s\<lparr>kheap := kh, ekheap := ekh\<rparr>) 3911 od" 3912 3913definition thread_gets_the_all :: "obj_ref \<Rightarrow> (Structures_A.tcb \<times> etcb) det_ext_monad" where 3914 "thread_gets_the_all tptr \<equiv> 3915 do tcb \<leftarrow> gets_the $ get_tcb tptr; 3916 etcb \<leftarrow> gets_the $ get_etcb tptr; 3917 return $ (tcb, etcb) od" 3918 3919definition thread_set_all :: "(Structures_A.tcb \<Rightarrow> Structures_A.tcb) \<Rightarrow> (etcb \<Rightarrow> etcb) 3920 \<Rightarrow> obj_ref \<Rightarrow> unit det_ext_monad" where 3921 "thread_set_all f g tptr \<equiv> 3922 do (tcb, etcb) \<leftarrow> thread_gets_the_all tptr; 3923 set_thread_all tptr (f tcb) (g etcb) 3924 od" 3925 3926lemma thread_set_ethread_set_all: 3927 "do thread_set f t; ethread_set g t od 3928 = thread_set_all f g t" 3929 by (rule ext) (clarsimp simp: thread_set_def ethread_set_def gets_the_def set_object_def set_object_def fail_def assert_opt_def split_def do_extended_op_def thread_set_all_def set_thread_all_def set_eobject_def thread_gets_the_all_def bind_def gets_def get_def return_def put_def get_etcb_def split: option.splits) 3930 3931lemma set_thread_all_corres: 3932 fixes ob' :: "'a :: pspace_storable" 3933 assumes x: "updateObject ob' = updateObject_default ob'" 3934 assumes z: "\<And>s. obj_at' P ptr s 3935 \<Longrightarrow> map_to_ctes ((ksPSpace s) (ptr \<mapsto> injectKO ob')) = map_to_ctes (ksPSpace s)" 3936 assumes b: "\<And>ko. P ko \<Longrightarrow> objBits ko = objBits ob'" 3937 assumes P: "\<And>(v::'a::pspace_storable). (1 :: word32) < 2 ^ (objBits v)" 3938 assumes e: "etcb_relation etcb tcb'" 3939 assumes is_t: "injectKO (ob' :: 'a :: pspace_storable) = KOTCB tcb'" 3940 shows "other_obj_relation (TCB tcb) (injectKO (ob' :: 'a :: pspace_storable)) \<Longrightarrow> 3941 corres dc (obj_at (same_caps (TCB tcb)) ptr and is_etcb_at ptr) 3942 (obj_at' (P :: 'a \<Rightarrow> bool) ptr) 3943 (set_thread_all ptr tcb etcb) (setObject ptr ob')" 3944 apply (rule corres_no_failI) 3945 apply (rule no_fail_pre) 3946 apply wp 3947 apply (rule x) 3948 apply (clarsimp simp: b elim!: obj_at'_weakenE) 3949 apply (unfold set_thread_all_def setObject_def) 3950 apply (clarsimp simp: in_monad split_def bind_def gets_def get_def Bex_def 3951 put_def return_def modify_def get_object_def x 3952 projectKOs 3953 updateObject_default_def in_magnitude_check [OF _ P]) 3954 apply (clarsimp simp add: state_relation_def z) 3955 apply (simp add: trans_state_update'[symmetric] trans_state_update[symmetric] 3956 del: trans_state_update) 3957 apply (clarsimp simp add: swp_def fun_upd_def obj_at_def is_etcb_at_def) 3958 apply (subst cte_wp_at_after_update,fastforce simp add: obj_at_def) 3959 apply (subst caps_of_state_after_update,fastforce simp add: obj_at_def) 3960 apply clarsimp 3961 apply (subst conj_assoc[symmetric]) 3962 apply (rule conjI[rotated]) 3963 apply (clarsimp simp add: ghost_relation_def) 3964 apply (erule_tac x=ptr in allE)+ 3965 apply (clarsimp simp: obj_at_def 3966 split: Structures_A.kernel_object.splits if_split_asm) 3967 3968 apply (fold fun_upd_def) 3969 apply (simp only: pspace_relation_def dom_fun_upd2 simp_thms) 3970 apply (subst pspace_dom_update) 3971 apply assumption 3972 apply simp 3973 apply (simp only: dom_fun_upd2 simp_thms) 3974 apply (elim conjE) 3975 apply (frule bspec, erule domI) 3976 apply (rule conjI) 3977 apply (rule ballI, drule(1) bspec) 3978 apply (drule domD) 3979 apply (clarsimp simp: is_other_obj_relation_type) 3980 apply (drule(1) bspec) 3981 apply clarsimp 3982 apply (frule_tac ko'="TCB tcb'" and x'=ptr in obj_relation_cut_same_type, 3983 (fastforce simp add: is_other_obj_relation_type)+)[1] 3984 apply (simp only: ekheap_relation_def dom_fun_upd2 simp_thms) 3985 apply (frule bspec, erule domI) 3986 apply (rule ballI, drule(1) bspec) 3987 apply (drule domD) 3988 apply (clarsimp simp: obj_at'_def) 3989 apply (clarsimp simp: projectKOs) 3990 apply (insert e is_t) 3991 by (clarsimp simp: other_obj_relation_def etcb_relation_def is_other_obj_relation_type split: Structures_A.kernel_object.splits Structures_H.kernel_object.splits ARM_A.arch_kernel_obj.splits) 3992 3993lemma tcb_update_all_corres': 3994 assumes tcbs: "tcb_relation tcb tcb' \<Longrightarrow> tcb_relation tcbu tcbu'" 3995 assumes tables: "\<forall>(getF, v) \<in> ran tcb_cap_cases. getF tcbu = getF tcb" 3996 assumes tables': "\<forall>(getF, v) \<in> ran tcb_cte_cases. getF tcbu' = getF tcb'" 3997 assumes r: "r () ()" 3998 assumes e: "etcb_relation etcb tcb' \<Longrightarrow> etcb_relation etcbu tcbu'" 3999 shows "corres r (ko_at (TCB tcb) add and (\<lambda>s. ekheap s add = Some etcb)) 4000 (ko_at' tcb' add) 4001 (set_thread_all add tcbu etcbu) (setObject add tcbu')" 4002 apply (rule_tac F="tcb_relation tcb tcb' \<and> etcb_relation etcbu tcbu'" in corres_req) 4003 apply (clarsimp simp: state_relation_def obj_at_def obj_at'_def) 4004 apply (frule(1) pspace_relation_absD) 4005 apply (force simp: projectKOs other_obj_relation_def ekheap_relation_def e) 4006 apply (erule conjE) 4007 apply (rule corres_guard_imp) 4008 apply (rule corres_rel_imp) 4009 apply (rule set_thread_all_corres[where P="(=) tcb'"]) 4010 apply (rule ext)+ 4011 apply simp 4012 defer 4013 apply (simp add: is_other_obj_relation_type_def 4014 projectKOs objBits_simps' 4015 other_obj_relation_def tcbs r)+ 4016 apply (fastforce simp: is_etcb_at_def elim!: obj_at_weakenE dest: bspec[OF tables]) 4017 apply (subst(asm) eq_commute, assumption) 4018 apply (clarsimp simp: projectKOs obj_at'_def objBits_simps) 4019 apply (subst map_to_ctes_upd_tcb, assumption+) 4020 apply (simp add: ps_clear_def3 field_simps objBits_defs mask_def) 4021 apply (subst if_not_P) 4022 apply (fastforce dest: bspec [OF tables', OF ranI]) 4023 apply simp 4024 done 4025 4026lemma thread_gets_the_all_corres: 4027 shows "corres (\<lambda>(tcb, etcb) tcb'. tcb_relation tcb tcb' \<and> etcb_relation etcb tcb') 4028 (tcb_at t and is_etcb_at t) (tcb_at' t) 4029 (thread_gets_the_all t) (getObject t)" 4030 apply (rule corres_no_failI) 4031 apply wp 4032 apply (clarsimp simp add: gets_def get_def return_def bind_def get_tcb_def thread_gets_the_all_def threadGet_def ethread_get_def gets_the_def assert_opt_def get_etcb_def is_etcb_at_def tcb_at_def liftM_def split: option.splits Structures_A.kernel_object.splits) 4033 apply (frule in_inv_by_hoareD [OF getObject_inv_tcb]) 4034 apply (clarsimp simp add: obj_at_def is_tcb obj_at'_def projectKO_def 4035 projectKO_opt_tcb split_def 4036 getObject_def loadObject_default_def in_monad) 4037 apply (case_tac ko) 4038 apply (simp_all add: fail_def return_def) 4039 apply (clarsimp simp add: state_relation_def pspace_relation_def ekheap_relation_def) 4040 apply (drule bspec) 4041 apply clarsimp 4042 apply blast 4043 apply (drule bspec, erule domI) 4044 apply (clarsimp simp add: other_obj_relation_def 4045 lookupAround2_known1) 4046 done 4047 4048lemma thread_set_all_corresT: 4049 assumes x: "\<And>tcb tcb'. tcb_relation tcb tcb' \<Longrightarrow> 4050 tcb_relation (f tcb) (f' tcb')" 4051 assumes y: "\<And>tcb. \<forall>(getF, setF) \<in> ran tcb_cap_cases. getF (f tcb) = getF tcb" 4052 assumes z: "\<forall>tcb. \<forall>(getF, setF) \<in> ran tcb_cte_cases. 4053 getF (f' tcb) = getF tcb" 4054 assumes e: "\<And>etcb tcb'. etcb_relation etcb tcb' \<Longrightarrow> 4055 etcb_relation (g etcb) (f' tcb')" 4056 shows "corres dc (tcb_at t and valid_etcbs) 4057 (tcb_at' t) 4058 (thread_set_all f g t) (threadSet f' t)" 4059 apply (simp add: thread_set_all_def threadSet_def bind_assoc) 4060 apply (rule corres_guard_imp) 4061 apply (rule corres_split [OF _ thread_gets_the_all_corres]) 4062 apply (simp add: split_def) 4063 apply (rule tcb_update_all_corres') 4064 apply (erule x) 4065 apply (rule y) 4066 apply (clarsimp simp: bspec_split [OF spec [OF z]]) 4067 apply fastforce 4068 apply (erule e) 4069 apply (simp add: thread_gets_the_all_def, wp+) 4070 apply clarsimp 4071 apply (frule(1) tcb_at_is_etcb_at) 4072 apply (clarsimp simp add: tcb_at_def get_etcb_def obj_at_def) 4073 apply (drule get_tcb_SomeD) 4074 apply fastforce 4075 apply simp 4076 done 4077 4078lemmas thread_set_all_corres = 4079 thread_set_all_corresT [OF _ _ all_tcbI, OF _ ball_tcb_cap_casesI ball_tcb_cte_casesI] 4080 4081lemma thread_get_thread_get: 4082 "do x \<leftarrow> thread_get f tptr; y \<leftarrow> thread_get g tptr; h x y od 4083 = do tcb \<leftarrow> thread_get id tptr; h (f tcb) (g tcb) od" 4084 apply (rule ext) 4085 apply (clarsimp simp: thread_get_def gets_the_def bind_assoc 4086 exec_gets assert_opt_def 4087 split: option.split) 4088 done 4089 4090lemma thread_set_gets_futz: 4091 "thread_set F t >>= (\<lambda>_. gets cur_domain >>= g) 4092 = gets cur_domain >>= (\<lambda>cdom. thread_set F t >>= K (g cdom))" 4093apply (rule ext) 4094apply (simp add: assert_opt_def bind_def fail_def get_def gets_def gets_the_def put_def return_def set_object_def thread_set_def split_def 4095 split: option.splits) 4096done 4097 4098lemma tcb_relation_convert_for_recycle_assert: 4099 "\<lbrakk>tcb_relation tcb rv'; inactive (tcb_state tcb); tcb_bound_notification tcb = None\<rbrakk> \<Longrightarrow> 4100 tcbState rv' = Structures_H.thread_state.Inactive \<and> tcbBoundNotification rv' = None" 4101 by (simp add: tcb_relation_def) 4102 4103crunch idle_thread[wp]: deleteCallerCap "\<lambda>s. P (ksIdleThread s)" 4104 (wp: crunch_wps) 4105crunch sch_act_simple: deleteCallerCap sch_act_simple 4106 (wp: crunch_wps) 4107crunch sch_act_not[wp]: deleteCallerCap "sch_act_not t" 4108 (wp: crunch_wps) 4109crunch typ_at'[wp]: deleteCallerCap "\<lambda>s. P (typ_at' T p s)" 4110 (wp: crunch_wps) 4111lemmas deleteCallerCap_typ_ats[wp] = typ_at_lifts [OF deleteCallerCap_typ_at'] 4112 4113crunch ksQ[wp]: emptySlot "\<lambda>s. P (ksReadyQueues s p)" 4114 4115lemma setEndpoint_sch_act_not_ct[wp]: 4116 "\<lbrace>\<lambda>s. sch_act_not (ksCurThread s) s\<rbrace> 4117 setEndpoint ptr val \<lbrace>\<lambda>_ s. sch_act_not (ksCurThread s) s\<rbrace>" 4118 by (rule hoare_weaken_pre, wps setEndpoint_ct', wp, simp) 4119 4120lemma cancelAll_ct_not_ksQ_helper: 4121 "\<lbrace>(\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p)) and (\<lambda>s. ksCurThread s \<notin> set q) \<rbrace> 4122 mapM_x (\<lambda>t. do 4123 y \<leftarrow> setThreadState Structures_H.thread_state.Restart t; 4124 tcbSchedEnqueue t 4125 od) q 4126 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4127 apply (rule mapM_x_inv_wp2, simp) 4128 apply (wp) 4129 apply (wps tcbSchedEnqueue_ct') 4130 apply (wp tcbSchedEnqueue_ksQ) 4131 apply (wps setThreadState_ct') 4132 apply (wp sts_ksQ') 4133 apply (clarsimp) 4134 done 4135 4136lemma cancelAllIPC_ct_not_ksQ: 4137 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane 4138 and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> 4139 cancelAllIPC epptr 4140 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4141 (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") 4142 apply (simp add: cancelAllIPC_def) 4143 apply (wp, wpc, wp) 4144 apply (wps rescheduleRequired_ct') 4145 apply (wp rescheduleRequired_ksQ') 4146 apply (clarsimp simp: forM_x_def) 4147 apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv) 4148 apply (wp hoare_lift_Pf2 [OF setEndpoint_ksQ setEndpoint_ct'])+ 4149 apply (wps rescheduleRequired_ct') 4150 apply (wp rescheduleRequired_ksQ') 4151 apply (clarsimp simp: forM_x_def) 4152 apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv) 4153 apply (wp hoare_lift_Pf2 [OF setEndpoint_ksQ setEndpoint_ct'])+ 4154 prefer 2 4155 apply assumption 4156 apply (rule_tac Q="\<lambda>ep. ?PRE and ko_at' ep epptr" in hoare_post_imp) 4157 apply (clarsimp) 4158 apply (rule conjI) 4159 apply ((clarsimp simp: invs'_def valid_state'_def 4160 sch_act_sane_def 4161 | drule(1) ct_not_in_epQueue)+)[2] 4162 apply (wp get_ep_sp') 4163 done 4164 4165lemma cancelAllSignals_ct_not_ksQ: 4166 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane 4167 and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> 4168 cancelAllSignals ntfnptr 4169 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4170 (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") 4171 apply (simp add: cancelAllSignals_def) 4172 apply (wp, wpc, wp+) 4173 apply (wps rescheduleRequired_ct') 4174 apply (wp rescheduleRequired_ksQ') 4175 apply clarsimp 4176 apply (wp cancelAll_ct_not_ksQ_helper mapM_x_wp_inv) 4177 apply (wp hoare_lift_Pf2 [OF setNotification_ksQ setNotification_ksCurThread]) 4178 apply (wps setNotification_ksCurThread, wp) 4179 prefer 2 4180 apply assumption 4181 apply (rule_tac Q="\<lambda>ep. ?PRE and ko_at' ep ntfnptr" in hoare_post_imp) 4182 apply ((clarsimp simp: invs'_def valid_state'_def sch_act_sane_def 4183 | drule(1) ct_not_in_ntfnQueue)+)[1] 4184 apply (wp get_ntfn_sp') 4185 done 4186 4187lemma unbindNotification_ct_not_ksQ: 4188 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane 4189 and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> 4190 unbindNotification t 4191 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4192 apply (simp add: unbindNotification_def) 4193 apply (rule hoare_seq_ext[OF _ gbn_sp']) 4194 apply (case_tac ntfnPtr, simp, wp, simp) 4195 apply (clarsimp) 4196 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 4197 apply (rule hoare_pre) 4198 apply (wp) 4199 apply (wps setBoundNotification_ct') 4200 apply (wp sbn_ksQ) 4201 apply (wps setNotification_ksCurThread, wp) 4202 apply clarsimp 4203 done 4204 4205lemma unbindMaybeNotification_ct_not_ksQ: 4206 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane 4207 and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> 4208 unbindMaybeNotification t 4209 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4210 apply (simp add: unbindMaybeNotification_def) 4211 apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) 4212 apply (case_tac "ntfnBoundTCB ntfn", simp, wp, simp+) 4213 apply (rule hoare_pre) 4214 apply wp 4215 apply (wps setBoundNotification_ct') 4216 apply (wp sbn_ksQ) 4217 apply (wps setNotification_ksCurThread, wp) 4218 apply clarsimp 4219 done 4220 4221lemma sbn_ct_in_state'[wp]: 4222 "\<lbrace>ct_in_state' P\<rbrace> setBoundNotification ntfn t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" 4223 apply (simp add: ct_in_state'_def) 4224 apply (rule hoare_pre) 4225 apply (wps setBoundNotification_ct') 4226 apply (wp sbn_st_tcb', clarsimp) 4227 done 4228 4229lemma set_ntfn_ct_in_state'[wp]: 4230 "\<lbrace>ct_in_state' P\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" 4231 apply (simp add: ct_in_state'_def) 4232 apply (rule hoare_pre) 4233 apply (wps setNotification_ksCurThread, wp, clarsimp) 4234 done 4235 4236lemma unbindNotification_ct_in_state'[wp]: 4237 "\<lbrace>ct_in_state' P\<rbrace> unbindNotification t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" 4238 apply (simp add: unbindNotification_def) 4239 apply (wp | wpc | simp)+ 4240 done 4241 4242lemma unbindMaybeNotification_ct_in_state'[wp]: 4243 "\<lbrace>ct_in_state' P\<rbrace> unbindMaybeNotification t \<lbrace>\<lambda>_. ct_in_state' P\<rbrace>" 4244 apply (simp add: unbindMaybeNotification_def) 4245 apply (wp | wpc | simp)+ 4246 done 4247 4248lemma setNotification_sch_act_sane: 4249 "\<lbrace>sch_act_sane\<rbrace> setNotification a ntfn \<lbrace>\<lambda>_. sch_act_sane\<rbrace>" 4250 by (wp sch_act_sane_lift) 4251 4252crunch sch_act_sane[wp]: unbindNotification, unbindMaybeNotification "sch_act_sane" 4253 4254lemma finaliseCapTrue_standin_ct_not_ksQ: 4255 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane 4256 and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> 4257 finaliseCapTrue_standin cap final 4258 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4259 apply (simp add: finaliseCapTrue_standin_def Let_def) 4260 apply (safe) 4261 apply (wp cancelAllIPC_ct_not_ksQ cancelAllSignals_ct_not_ksQ unbindNotification_ct_not_ksQ 4262 hoare_drop_imps unbindMaybeNotification_ct_not_ksQ 4263 | wpc 4264 | clarsimp simp: isNotificationCap_def isReplyCap_def split:capability.splits)+ 4265 done 4266 4267lemma cteDeleteOne_ct_not_ksQ: 4268 "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane 4269 and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> 4270 cteDeleteOne slot 4271 \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrace>" 4272 apply (simp add: cteDeleteOne_def unless_def split_def) 4273 apply (rule hoare_seq_ext [OF _ getCTE_sp]) 4274 apply (case_tac "\<forall>final. finaliseCap (cteCap cte) final True = fail") 4275 apply (simp add: finaliseCapTrue_standin_simple_def) 4276 apply wp 4277 apply (clarsimp) 4278 apply (wp emptySlot_cteCaps_of hoare_lift_Pf2 [OF emptySlot_ksRQ emptySlot_ct]) 4279 apply (simp add: cteCaps_of_def) 4280 apply (wp_once hoare_drop_imps) 4281 apply (wp finaliseCapTrue_standin_ct_not_ksQ isFinalCapability_inv)+ 4282 apply (clarsimp) 4283 done 4284 4285end 4286 4287end 4288