1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory Finalise_DR 12imports 13 KHeap_DR 14 "AInvs.VSpaceEntries_AI" 15begin 16 17context begin interpretation Arch . (*FIXME: arch_split*) 18 19definition 20 "transform_pd_slot_ref x 21 = (x && ~~ mask pd_bits, 22 unat ((x && mask pd_bits) >> 2))" 23definition 24 "transform_pt_slot_ref x 25 = (x && ~~ mask pt_bits, 26 unat ((x && mask pt_bits) >> 2))" 27 28lemma trancl_image: 29 assumes inj: "inj_on f (Domain S \<union> Range S)" 30 shows "trancl ((\<lambda>(x, y). (f x, f y)) ` S) = (\<lambda>(x, y). (f x, f y)) ` trancl S" 31 (is "?lhs = ?rhs") 32 apply safe 33 apply (erule trancl.induct) 34 apply clarsimp 35 apply (erule image_eqI[rotated, OF r_into_trancl]) 36 apply simp 37 apply (clarsimp simp: inj_on_eq_iff[OF inj] 38 RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]] 39 DomainI) 40 apply (erule(1) image_eqI[rotated, OF trancl_into_trancl]) 41 apply simp 42 apply (erule trancl.induct) 43 apply (rule r_into_trancl, erule image_eqI[rotated]) 44 apply simp 45 apply (erule trancl_into_trancl) 46 apply (erule image_eqI[rotated]) 47 apply simp 48 done 49 50lemma descendants_of_eqv: 51 assumes cte_at: "mdb_cte_at (swp (cte_wp_at P) s) (cdt s)" 52 and cte_at_p: "cte_at p s" 53 shows "KHeap_D.descendants_of (transform_cslot_ptr p) (transform s) 54 = transform_cslot_ptr ` CSpaceAcc_A.descendants_of p (cdt s)" 55proof - 56 note inj = transform_cdt_slot_inj_on_mdb_cte_at[OF cte_at] 57 have P: "{(x, y). KHeap_D.is_cdt_parent (transform s) x y} 58 = (\<lambda>(x, y). (transform_cslot_ptr x, transform_cslot_ptr y)) 59 ` {(x, y). CSpaceAcc_A.is_cdt_parent (cdt s) x y}" 60 apply (simp add: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def) 61 apply (simp add: transform_def transform_cdt_def map_lift_over_eq_Some 62 inj) 63 apply auto 64 done 65 have inj': "inj_on transform_cslot_ptr ({p} \<union> dom (cdt s) \<union> ran (cdt s))" 66 using cte_at_p mdb_cte_atD[OF _ cte_at] 67 apply - 68 apply (rule transform_cdt_slot_inj_on_cte_at[where P=\<top> and s=s]) 69 apply (fastforce simp: cte_wp_at_caps_of_state elim!: ranE) 70 done 71 show ?thesis 72 apply (simp add: KHeap_D.descendants_of_def CSpaceAcc_A.descendants_of_def 73 KHeap_D.cdt_parent_rel_def CSpaceAcc_A.cdt_parent_rel_def) 74 apply (simp add: P) 75 apply (subst trancl_image) 76 apply (rule subset_inj_on[OF inj]) 77 apply (auto simp: KHeap_D.is_cdt_parent_def CSpaceAcc_A.is_cdt_parent_def)[1] 78 apply safe 79 apply (subst(asm) inj_on_eq_iff[OF inj'], simp_all) 80 apply (drule DomainI[THEN eqset_imp_iff[OF trancl_domain, THEN iffD1]]) 81 apply (auto simp: CSpaceAcc_A.is_cdt_parent_def) 82 done 83qed 84 85(* 86(* Fast finalise is done in TCB_DR, this file only deals with finalise *) 87lemma dcorres_unmap_page_empty: 88 "dcorres dc \<top> \<top> (PageTableUnmap_D.unmap_page x) (return a)" 89 apply (simp add:PageTableUnmap_D.unmap_page_def) 90 apply (rule corres_symb_exec_l) 91 apply (rule corres_guard_imp) 92 apply (rule_tac x = "[]" in select_pick_corres) 93 apply (clarsimp simp:mapM_x_def sequence_x_def del:hoare_post_taut) 94prefer 4 95 apply (rule hoare_post_taut) 96 apply simp_all 97 apply (simp add:exs_valid_def slots_with_def gets_def has_slots_def get_def bind_def return_def ) 98done 99*) 100 101lemma dcorres_revoke_cap_no_descendants: 102 "slot' = transform_cslot_ptr slot \<Longrightarrow> 103 dcorres dc \<top> (\<lambda>s. valid_mdb s \<and> cte_at slot s \<and> CSpaceAcc_A.descendants_of slot (cdt s) = {}) 104 (revoke_cap_simple slot') 105 (return x)" 106 apply (rule dcorres_revoke_cap_simple_helper) 107 apply (simp add:gets_def) 108 apply (rule dcorres_absorb_get_l) 109 apply (subgoal_tac "(KHeap_D.descendants_of slot' (transform s')) = {}") 110 apply clarsimp 111 apply (rule dcorres_absorb_get_l) 112 apply clarsimp 113 apply (clarsimp simp:descendants_of_eqv valid_mdb_def) 114 done 115 116lemma dcorres_revoke_cap_unnecessary: 117 "dcorres dc \<top> (valid_reply_caps and valid_objs and only_idle and valid_mdb and st_tcb_at (Not \<circ> awaiting_reply) ptr 118 and cte_at (ptr,tcb_cnode_index 2) and not_idle_thread ptr and valid_idle) 119 (revoke_cap_simple (ptr, tcb_replycap_slot)) 120 (return x)" 121 apply (subst transform_tcb_slot_simp[symmetric]) 122 apply (rule corres_guard_imp) 123 apply (rule dcorres_revoke_cap_no_descendants) 124 apply (simp add:transform_tcb_slot_simp[symmetric])+ 125 apply (rule not_waiting_reply_slot_no_descendants) 126 apply simp_all 127done 128 129lemma descendants_exist_in_cdt: 130 "\<lbrakk> a \<in> descendants_of p (cdt s) \<rbrakk> 131 \<Longrightarrow> cdt s a \<noteq> None" 132 apply (simp add: descendants_of_def cdt_parent_rel_def) 133 apply (frule RangeI[THEN eqset_imp_iff[OF trancl_range, THEN iffD1]]) 134 apply (clarsimp simp: is_cdt_parent_def) 135 done 136 137lemma descendants_exist_in_cdl_cdt: 138 "\<lbrakk> a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk> 139 \<Longrightarrow> cdl_cdt (transform s) a \<noteq> None" 140 apply (simp add: KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def) 141 apply (frule RangeI) 142 apply (frule DomainI) 143 apply (clarsimp simp: KHeap_D.is_cdt_parent_def) 144done 145 146lemma cdl_cdt_parent_cte_at_lift: 147 "\<lbrakk> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) ; a \<in> KHeap_D.descendants_of p (transform s) \<rbrakk> 148 \<Longrightarrow> (\<exists>slot. cte_at slot s \<and> p = transform_cslot_ptr slot)" 149 apply (simp add:KHeap_D.descendants_of_def KHeap_D.cdt_parent_rel_def) 150 apply (frule DomainI) 151 apply (clarsimp simp:KHeap_D.is_cdt_parent_def) 152 apply (simp add:transform_def transform_cdt_def) 153 apply (clarsimp simp:transform_cdt_slot_inj_on_mdb_cte_at map_lift_over_eq_Some split:if_splits) 154 apply (rule_tac x = ab in exI,rule_tac x = bb in exI) 155 apply (drule(1) mdb_cte_atD) 156 apply (clarsimp simp :cte_wp_at_cte_at) 157done 158 159lemma descendants_not_null_cap: 160 "\<lbrakk> a \<in> descendants_of p (cdt s); mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<rbrakk> 161 \<Longrightarrow> cte_wp_at P a s" 162 apply (drule descendants_exist_in_cdt) 163 apply clarsimp 164 apply (drule(1) mdb_cte_atD) 165 apply simp 166 done 167 168lemma descendants_in_cte_wp_set: 169 "mdb_cte_at (swp (cte_wp_at P ) s) (cdt s) 170 \<Longrightarrow> CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> Collect (\<lambda>x. cte_wp_at (P) x s)" 171 by (auto simp:descendants_not_null_cap) 172 173lemma ex_in_none_empty_set: 174 "a\<noteq>{} \<Longrightarrow> \<exists>x. x\<in>a" 175 by auto 176 177lemma finite_descendants_if_from_transform: 178 " mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<Longrightarrow> finite (KHeap_D.descendants_of x (transform s))" 179 apply (case_tac "KHeap_D.descendants_of x (transform s) = {}") 180 apply simp 181 apply (drule ex_in_none_empty_set) 182 apply clarsimp 183 apply (frule(1) cdl_cdt_parent_cte_at_lift) 184 apply clarsimp 185 apply (frule(1) descendants_of_eqv) 186 apply clarsimp 187 apply (rule finite_imageI) 188 apply (rule finite_subset) 189 apply (rule descendants_in_cte_wp_set) 190 apply simp 191 apply (simp add:cte_wp_at_set_finite) 192done 193 194lemma delete_cdt_slot_shrink_descendants: 195 "\<lbrace>\<lambda>s. valid_mdb s \<and> x = cdt s \<and> slot \<in> CSpaceAcc_A.descendants_of p x \<and> x = y \<rbrace> 196 set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None)) 197 \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> 198 CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p y \<rbrace>" 199 apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def) 200 apply (rule conjI) 201 apply (subgoal_tac "mdb_empty_abs s") 202 apply (clarsimp simp:mdb_empty_abs.descendants mdb_empty_abs_def vmdb_abs_def)+ 203done 204 205lemma delete_cap_one_shrink_descendants: 206 "\<lbrace>\<lambda>s. s = pres \<and> invs s \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace> cap_delete_one slot 207 \<lbrace>\<lambda>r s. slot \<notin> CSpaceAcc_A.descendants_of p (cdt s) \<and> 208 CSpaceAcc_A.descendants_of p (cdt s) \<subseteq> CSpaceAcc_A.descendants_of p (cdt pres) \<rbrace>" 209 including no_pre 210 apply (simp add:cap_delete_one_def unless_def) 211 apply wp 212 apply (clarsimp simp add:empty_slot_def) 213 apply (wp dxo_wp_weak) 214 apply simp 215 apply (rule_tac P="\<lambda>s. valid_mdb s \<and> cdt s = xa \<and> cdt pres = xa \<and> slot \<in> CSpaceAcc_A.descendants_of p (cdt s) 216 \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)" 217 in hoare_vcg_precond_imp) 218 apply (rule_tac Q ="\<lambda>r s. Q r s \<and> (mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))" for Q in hoare_strengthen_post) 219 apply (rule hoare_vcg_conj_lift) 220 apply (rule delete_cdt_slot_shrink_descendants[where y= "cdt pres" and p = p]) 221 apply (rule_tac Q="\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s ) xa" in hoare_vcg_precond_imp) 222 apply (case_tac slot) 223 apply (clarsimp simp:set_cdt_def get_def put_def bind_def valid_def mdb_cte_at_def) 224 apply (assumption) 225 apply clarsimp+ 226 apply wp+ 227 apply (rule hoare_vcg_conj_lift[where P="\<lambda>s. cdt s = cdt pres \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s)"]) 228 prefer 2 229 apply (rule hoare_drop_imp) 230 apply wp 231 apply (clarsimp simp:valid_def in_get_cap_cte_wp_at) 232 apply (drule sym) 233 apply clarsimp 234 apply (drule descendants_not_null_cap) 235 apply simp 236 apply (simp add:cte_wp_at_def) 237 apply (wp|simp)+ 238 apply (rule hoare_vcg_conj_lift) 239 apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise]) 240 apply (clarsimp simp:valid_mdb_def swp_def) 241 apply wp 242 apply (rule hoare_strengthen_post[OF invs_mdb_fast_finalise]) 243 apply (clarsimp simp:valid_mdb_def swp_def) 244 apply wp 245 apply (clarsimp simp:valid_def in_get_cap_cte_wp_at) 246 apply (clarsimp simp:invs_def valid_mdb_def valid_state_def) 247 apply (drule descendants_not_null_cap) 248 apply simp 249 apply (clarsimp simp:cte_wp_at_def) 250done 251 252lemma invs_emptyable_descendants: 253 "\<lbrakk>invs s;CSpaceAcc_A.descendants_of slot (cdt s) = {(a, b)}\<rbrakk> 254 \<Longrightarrow> emptyable (a, b) s" 255 apply (clarsimp simp:emptyable_def) 256 apply (frule reply_slot_not_descendant) 257 apply simp 258 apply fastforce 259done 260 261lemma cap_delete_one_cte_at: 262 "\<lbrace>invs and emptyable sl and cte_at x\<rbrace> cap_delete_one sl \<lbrace>\<lambda>_. cte_at x\<rbrace>" 263 apply (simp add:cap_delete_one_def) 264 apply wp 265 apply (clarsimp simp:unless_def when_def | rule conjI)+ 266 apply (wp|clarsimp)+ 267done 268 269lemma nat_to_bl_zero_zero: 270 "(nat_to_bl 0 0) = (Some [])" 271 by (clarsimp simp: nat_to_bl_def) 272 273lemma caps_of_state_transform_opt_cap_no_idle: 274 "\<lbrakk>caps_of_state s p = Some cap; valid_etcbs s\<rbrakk> 275 \<Longrightarrow> opt_cap (transform_cslot_ptr p) (transform s) 276 = Some (transform_cap cap) \<or> 277 opt_cap (transform_cslot_ptr p) (transform s) 278 = None" 279 apply (frule caps_of_state_cteD) 280 apply (cases p) 281 apply (erule cte_wp_atE) 282 apply (clarsimp simp: opt_cap_def transform_cslot_ptr_def object_slots_def 283 slots_of_def opt_object_def transform_def transform_objects_def 284 transform_cnode_contents_def well_formed_cnode_n_def 285 restrict_map_def 286 split: option.splits if_split_asm nat.splits) 287 apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI]) 288 apply (simp add: nat_to_bl_zero_zero option_map_join_def) 289 apply clarsimp 290 apply (frule(1) eqset_imp_iff[THEN iffD1, OF _ domI]) 291 apply (simp add: option_map_join_def nat_to_bl_dest) 292 apply (clarsimp simp: cap_installed_at_irq_def valid_irq_node_def 293 obj_at_def is_cap_table_def well_formed_cnode_n_def 294 length_set_helper word_bl.Abs_inverse 295 object_slots_def nat_bl_to_bin_lt2p) 296 apply (frule(1) valid_etcbs_tcb_etcb) 297 by (clarsimp simp: opt_cap_def transform_cslot_ptr_def 298 slots_of_def opt_object_def restrict_map_def 299 transform_def object_slots_def transform_objects_def 300 valid_irq_node_def obj_at_def is_cap_table_def tcb_cap_cases_def 301 transform_tcb_def tcb_slot_defs infer_tcb_bound_notification_def 302 bl_to_bin_tcb_cnode_index bl_to_bin_tcb_cnode_index_le0 303 split: if_split_asm option.splits) 304 305lemma transform_cap_Null [simp]: 306 "(transform_cap cap = cdl_cap.NullCap) = (cap = cap.NullCap)" 307 apply (cases cap, simp_all) 308 apply (rename_tac arch_cap) 309 apply (case_tac arch_cap, simp_all) 310 done 311 312lemma dcorres_revoke_the_cap_corres: 313 "dcorres dc \<top> 314 (invs and cte_at slot and valid_etcbs) 315 (revoke_cap_simple (transform_cslot_ptr slot)) 316 (do descs \<leftarrow> gets (CSpaceAcc_A.descendants_of slot \<circ> cdt); 317 when (descs \<noteq> {}) (do y \<leftarrow> assert (\<exists>a b. descs = {(a, b)}); 318 select descs >>= cap_delete_one 319 od) 320 od)" 321 apply (rule dcorres_revoke_cap_simple_helper) 322 apply (simp add:gets_def) 323 apply (rule dcorres_absorb_get_l) 324 apply (rule dcorres_absorb_get_r) 325 apply (subgoal_tac "finite (KHeap_D.descendants_of (transform_cslot_ptr slot) (transform s'))") 326 apply (clarsimp simp: finite_descendants_if_from_transform valid_mdb_def 327 invs_def valid_state_def descendants_of_eqv) 328 apply (rule dcorres_absorb_get_l) 329 apply (clarsimp simp: when_def assert_def corres_free_fail) 330 apply (subgoal_tac "cte_wp_at ((\<noteq>) cap.NullCap) (a,b) s'") 331 prefer 2 332 apply (erule descendants_not_null_cap [rotated]) 333 apply fastforce 334 apply (rule conjI) 335 prefer 2 336 apply (clarsimp simp: cte_wp_at_caps_of_state) 337 apply (subgoal_tac "a \<noteq> idle_thread s'") 338 apply (drule_tac p="(a,b)" in caps_of_state_transform_opt_cap) 339 apply clarsimp 340 apply clarsimp 341 apply clarsimp 342 apply clarsimp 343 apply (erule notE, rule sym) 344 apply (erule (4) valid_idle_has_null_cap) 345 apply clarsimp 346 apply (rule corres_dummy_return_r) 347 apply (rule corres_guard_imp) 348 apply (rule corres_split[OF dcorres_revoke_cap_no_descendants]) 349 apply simp 350 apply (rule delete_cap_simple_corres) 351 apply (wp cap_delete_one_cte_at)+ 352 apply (rule_tac pres1 = s' and p1 = slot in hoare_strengthen_post[OF delete_cap_one_shrink_descendants]) 353 apply (simp_all add:invs_def valid_state_def valid_mdb_def) 354 apply fastforce 355 apply (rule conjI) 356 apply (rule ccontr) 357 apply (subgoal_tac "cte_wp_at ((\<noteq>)cap.NullCap) (a,b) s") 358 apply (clarsimp simp: cte_wp_at_caps_of_state) 359 apply (drule valid_idle_has_null_cap) 360 apply (simp add:not_idle_thread_def)+ 361 apply (rule invs_emptyable_descendants) 362 apply (simp add:invs_def valid_state_def valid_mdb_def)+ 363 apply (clarsimp simp:finite_descendants_if_from_transform) 364 done 365 366lemma valid_ntfn_after_remove_slot: 367 "\<lbrakk>valid_ntfn ntfn s'; ntfn_obj ntfn = (Structures_A.ntfn.WaitingNtfn list)\<rbrakk> 368 \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfn 369 (case remove1 ptr list of [] \<Rightarrow> Structures_A.ntfn.IdleNtfn 370 | a # lista \<Rightarrow> Structures_A.ntfn.WaitingNtfn (remove1 ptr list))) s'" 371 apply (clarsimp simp: valid_ntfn_def 372 split: ntfn.splits list.split_asm list.splits option.splits) 373 by (metis (mono_tags) distinct.simps(2) distinct_length_2_or_more distinct_remove1 set_remove1) 374 375lemma finalise_cancel_ipc: 376 "dcorres dc \<top> (not_idle_thread ptr and invs and valid_etcbs) 377 (CSpace_D.cancel_ipc ptr) 378 (cancel_ipc ptr)" 379 apply (simp add:CSpace_D.cancel_ipc_def cancel_ipc_def get_thread_state_def thread_get_def) 380 apply (rule dcorres_gets_the) 381 apply (simp add:opt_object_tcb not_idle_thread_def transform_tcb_def, clarsimp) 382 apply (frule(1) valid_etcbs_get_tcb_get_etcb) 383 apply (clarsimp simp: opt_cap_tcb tcb_pending_op_slot_def 384 tcb_caller_slot_def tcb_cspace_slot_def tcb_ipcbuffer_slot_def 385 tcb_replycap_slot_def tcb_vspace_slot_def assert_opt_def) 386 apply (case_tac "tcb_state obj'") 387 apply (simp_all add:not_idle_thread_def infer_tcb_pending_op_def 388 tcb_pending_op_slot_def[symmetric] tcb_replycap_slot_def[symmetric]) 389 apply (simp add:blocked_cancel_ipc_def) 390 apply (rule corres_guard_imp) 391 apply (rule corres_symb_exec_r) 392 apply (rule corres_symb_exec_r) 393 apply (rule corres_symb_exec_r) 394 apply (rule corres_dummy_return_pl) 395 apply (rule corres_split[ OF _ corres_dummy_set_sync_ep]) 396 apply clarsimp 397 apply (rule corres_dummy_return_pr) 398 apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary]) 399 apply (simp add: when_def dc_def[symmetric]) 400 apply (rule set_thread_state_corres) 401 apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset 402 | clarsimp simp:not_idle_thread_def a_type_def)+ 403 apply (simp add:get_blocking_object_def | wp)+ 404 apply (clarsimp dest!:get_tcb_rev simp:invs_def ep_at_def2[symmetric, simplified]) 405 apply (frule(1) valid_tcb_if_valid_state) 406 apply (clarsimp simp:valid_tcb_def valid_tcb_state_def 407 valid_state_def valid_pspace_def infer_tcb_pending_op_def 408 st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD) 409 apply (rule tcb_at_cte_at_2,clarsimp simp:tcb_at_def dest!:get_tcb_rev,simp) 410 apply (simp add:blocked_cancel_ipc_def) 411 apply (rule corres_guard_imp) 412 apply (rule corres_symb_exec_r) 413 apply (rule corres_symb_exec_r) 414 apply (rule corres_symb_exec_r) 415 apply (rule corres_dummy_return_pl) 416 apply (rule corres_split[ OF _ corres_dummy_set_sync_ep]) 417 apply clarsimp 418 apply (rule corres_dummy_return_pr) 419 apply (rule corres_split [OF _ dcorres_revoke_cap_unnecessary]) 420 unfolding K_bind_def 421 apply (rule set_thread_state_corres) 422 apply (wp sts_only_idle sts_st_tcb_at' valid_ep_queue_subset 423 | clarsimp simp:not_idle_thread_def a_type_def)+ 424 apply (simp add:get_blocking_object_def | wp)+ 425 apply (clarsimp dest!:get_tcb_rev simp:invs_def ep_at_def2[symmetric, simplified]) 426 apply (frule(1) valid_tcb_if_valid_state) 427 apply (clarsimp simp:valid_tcb_def valid_tcb_state_def 428 valid_state_def valid_pspace_def infer_tcb_pending_op_def 429 st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD) 430 apply (rule tcb_at_cte_at_2,clarsimp simp:tcb_at_def dest!:get_tcb_rev,simp) 431 apply (simp add:reply_cancel_ipc_def) 432 apply (rule corres_guard_imp) 433 apply (rule corres_split[OF _ thread_set_fault_corres]) 434 apply (rule corres_symb_exec_r) 435 apply (simp add: revoke_cap_simple.simps) 436 apply (subst transform_tcb_slot_simp[symmetric]) 437 apply (rule dcorres_revoke_the_cap_corres) 438 apply (wp thread_set_invs_trivial[OF ball_tcb_cap_casesI] 439 thread_set_cte_at|clarsimp)+ 440 apply (clarsimp simp: not_idle_thread_def 441 tcb_at_cte_at_2[unfolded tcb_at_def]) 442 apply (simp add:cancel_signal_def) 443 apply (rule corres_guard_imp) 444 apply (rule_tac Q'="\<lambda>r. valid_ntfn r and (=) s'" in corres_symb_exec_r) 445 apply (rule corres_symb_exec_r) 446 apply (rule corres_dummy_return_pl) 447 apply (rule corres_split[ OF _ corres_dummy_set_notification]) 448 unfolding K_bind_def 449 apply (rule corres_dummy_return_pr) 450 apply (rule corres_split[OF _ dcorres_revoke_cap_unnecessary]) 451 unfolding K_bind_def 452 apply (rule set_thread_state_corres) 453 including no_pre 454 apply (wpsimp wp: set_simple_ko_valid_objs simp: not_idle_thread_def a_type_def)+ 455 apply (clarsimp simp:valid_def fail_def return_def split:Structures_A.ntfn.splits)+ 456 apply (clarsimp simp:invs_def ntfn_at_def2[symmetric, simplified]) 457 apply (frule(1) valid_tcb_if_valid_state) 458 apply (clarsimp simp:valid_tcb_def tcb_at_cte_at_2 459 valid_tcb_state_def invs_def valid_state_def valid_pspace_def 460 st_tcb_at_def generates_pending_def obj_at_def infer_tcb_pending_op_def 461 dest!:get_tcb_SomeD) 462 apply (simp add:valid_ntfn_after_remove_slot) 463 apply (wp | clarsimp split:Structures_A.ntfn.splits)+ 464 apply (clarsimp simp:invs_def, frule(1) valid_tcb_if_valid_state) 465 apply (clarsimp simp:valid_tcb_def tcb_at_cte_at_2 valid_tcb_state_def invs_def valid_state_def valid_pspace_def 466 st_tcb_at_def generates_pending_def obj_at_def dest!:get_tcb_SomeD) 467 apply (clarsimp, frule(1) valid_etcbs_get_tcb_get_etcb) 468 apply (clarsimp simp:opt_object_tcb opt_cap_tcb) 469 done 470 471lemma dcorres_get_irq_slot: 472 "dcorres (\<lambda>r r'. r = transform_cslot_ptr r') \<top> \<top> (gets (CSpace_D.get_irq_slot x)) (KHeap_A.get_irq_slot x)" 473 apply (simp add:gets_def CSpace_D.get_irq_slot_def KHeap_A.get_irq_slot_def) 474 apply (rule dcorres_absorb_get_l) 475 apply (rule dcorres_absorb_get_r) 476 apply (clarsimp simp: return_def transform_def corres_underlying_def transform_cslot_ptr_def) 477done 478 479lemma dcorres_deleting_irq_handler: 480 "dcorres dc \<top> (invs and valid_etcbs) 481 (CSpace_D.deleting_irq_handler word) 482 (CSpace_A.deleting_irq_handler word)" 483 apply (simp add:CSpace_D.deleting_irq_handler_def CSpace_A.deleting_irq_handler_def) 484 apply (rule corres_guard_imp) 485 apply (rule corres_split[OF _ dcorres_get_irq_slot]) 486 apply (simp, rule delete_cap_simple_corres,simp) 487 apply (rule hoare_vcg_precond_imp [where Q="invs and valid_etcbs"]) 488 including no_pre 489 apply (wpsimp simp:get_irq_slot_def)+ 490 apply (rule irq_node_image_not_idle) 491 apply (simp add:invs_def valid_state_def)+ 492done 493 494lemma do_machine_op_wp: 495 "\<forall>m. \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> mop \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace> 496 \<Longrightarrow> \<lbrace>\<lambda>ps. transform ps = cs\<rbrace> do_machine_op mop \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>" 497 apply (clarsimp simp:do_machine_op_def gets_def get_def return_def bind_def select_f_def simpler_modify_def) 498 apply (clarsimp simp:valid_def) 499 apply (drule_tac x = "(machine_state s)" in spec) 500 apply (drule_tac x = "(a,b)" in bspec) 501 apply simp 502 apply clarsimp 503 apply (clarsimp simp:transform_def transform_current_thread_def) 504 apply (simp add: transform_objects_def2) 505 done 506 507lemmas dmo_dwp = do_machine_op_wp [OF allI] 508 509lemma machine_op_lift[wp]: 510 "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> machine_op_lift x \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 511 apply (clarsimp simp:machine_rest_lift_def ignore_failure_def machine_op_lift_def) 512 apply (wpsimp simp:simpler_modify_def valid_def) 513 done 514 515lemma invalidateLocalTLB_ASID_underlying_memory[wp]: 516 "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_ASID a \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 517 apply (clarsimp simp: invalidateLocalTLB_ASID_def, wp) 518 done 519 520lemma dsb_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> dsb \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 521 apply (clarsimp simp: dsb_def, wp) 522done 523 524lemma invalidate_I_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidate_I_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 525 apply (clarsimp simp: invalidate_I_PoU_def , wp) 526done 527 528lemma clean_D_PoU_underlying_memory[wp]: "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace>clean_D_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 529 apply (clarsimp simp: clean_D_PoU_def , wp) 530done 531 532lemma cleanCachesPoU_underlying_memory[wp]: 533 "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> cleanCaches_PoU \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 534 apply (clarsimp simp: cleanCaches_PoU_def, wp) 535done 536 537lemma flush_space_dwp[wp]: 538 "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> flush_space x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>" 539 apply (clarsimp simp:flush_space_def) 540 apply (wp|wpc)+ 541 apply (clarsimp split:option.splits) 542 apply (rule do_machine_op_wp) 543 apply clarsimp 544 apply (wp static_imp_wp)+ 545 apply (rule do_machine_op_wp) 546 apply clarsimp 547 apply wp 548 apply (rule hoare_allI) 549 apply (rule hoare_drop_imp) 550 apply (rule do_machine_op_wp) 551 apply clarsimp 552 apply wp 553 apply (rule hoare_conjI) 554 apply (rule hoare_drop_imp) 555 apply (clarsimp simp:load_hw_asid_def) 556 apply wp 557 apply (clarsimp simp:load_hw_asid_def) 558 apply wp 559 apply assumption 560 done 561 562lemma invalidate_asid_dwp[wp]: 563 "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid (the (hw_asid_table next_asid)) \<lbrace>\<lambda>x ps. transform ps = cs\<rbrace>" 564 apply (clarsimp simp:invalidate_asid_def) 565 apply wp 566 apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) 567 done 568 569lemma invalidate_asid_entry_dwp[wp]: 570 "\<lbrace>\<lambda>ps. transform ps = cs\<rbrace> invalidate_asid_entry x \<lbrace>\<lambda>r ps. transform ps = cs\<rbrace>" 571 apply (clarsimp simp:invalidate_asid_entry_def) 572 apply wp 573 apply (clarsimp simp:invalidate_asid_def) 574 apply wp+ 575 apply (clarsimp simp:invalidate_hw_asid_entry_def) 576 apply wp+ 577 apply (clarsimp simp:load_hw_asid_def) 578 apply wp 579 apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) 580 done 581 582lemma invalidate_hw_asid_entry_dwp[wp]: 583 "\<lbrace>\<lambda>s. transform s = cs\<rbrace> invalidate_hw_asid_entry next_asid \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>" 584 apply (clarsimp simp:invalidate_hw_asid_entry_def) 585 apply wp 586 apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) 587done 588 589lemma set_current_pd_dwp[wp]: 590 " \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> set_current_pd (addrFromPPtr x) \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 591 by (clarsimp simp:set_current_pd_def writeTTBR0_def isb_def dsb_def,wp) 592 593lemma set_hardware_asid_dwp[wp]: 594 " \<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> setHardwareASID hw_asid \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 595 by (clarsimp simp:setHardwareASID_def,wp) 596 597 598lemma store_hardware_asid_dwp[wp]: 599 "\<lbrace>\<lambda>s. transform s = cs\<rbrace> store_hw_asid a xa \<lbrace>\<lambda>xb a. transform a = cs\<rbrace>" 600 apply (clarsimp simp:store_hw_asid_def) 601 apply wp 602 apply (simp add:find_pd_for_asid_assert_def) 603 apply wp 604 apply (simp add:find_pd_for_asid_def) 605 apply (wp|wpc)+ 606 apply (clarsimp simp:transform_def transform_objects_def2 transform_current_thread_def transform_cdt_def transform_asid_table_def) 607done 608 609lemma transform_arch_state: 610 "\<lbrakk> arm_globals_frame (arch_state a) = arm_globals_frame x; 611 arm_asid_table (arch_state a) = arm_asid_table x \<rbrakk> 612 \<Longrightarrow> transform (a\<lparr>arch_state := x \<rparr>) = transform a" 613 by (clarsimp simp:transform_def transform_objects_def2 transform_cdt_def 614 transform_current_thread_def transform_asid_table_def) 615 616lemma find_free_hw_asid_dwp[wp]: 617 "\<lbrace>\<lambda>s. transform s = cs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>xa s. transform s = cs\<rbrace>" 618 apply (clarsimp simp:find_free_hw_asid_def) 619 apply (wp|wpc)+ 620 apply (clarsimp simp:transform_arch_state) 621 apply (wp do_machine_op_wp |clarsimp simp:)+ 622done 623 624lemma arch_obj_not_idle: 625 "\<lbrakk>valid_idle s;kheap s ptr = Some (ArchObj x )\<rbrakk> \<Longrightarrow> not_idle_thread ptr s" 626 by (clarsimp simp:not_idle_thread_def valid_idle_def obj_at_def pred_tcb_at_def) 627 628lemma asid_pool_at_rev: 629 "\<lbrakk> kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow> asid_pool_at a s" 630 apply (clarsimp simp: obj_at_def valid_idle_def st_tcb_at_def) 631 apply (clarsimp simp: a_type_def 632 split: arch_kernel_obj.splits Structures_A.kernel_object.split_asm if_splits) 633 done 634 635lemma asid_pool_not_idle: 636 "\<lbrakk> valid_idle s; asid_pool_at a s \<rbrakk> \<Longrightarrow> not_idle_thread a s" 637 apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) 638 apply (clarsimp simp: not_idle_thread_def 639 split: if_splits) 640 done 641 642lemma opt_object_asid_pool: 643 "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.ASIDPool fun)) \<rbrakk> \<Longrightarrow> 644 opt_object a (transform s) = Some (cdl_object.AsidPool \<lparr>cdl_asid_pool_caps = transform_asid_pool_contents fun\<rparr>)" 645 apply (frule asid_pool_at_rev) 646 apply (frule(1) asid_pool_not_idle) 647 apply (clarsimp simp:transform_objects_def opt_object_def transform_def 648 not_idle_thread_def restrict_map_def) 649done 650 651lemma transform_asid_pool_contents_upd: 652 "transform_asid_pool_contents (pool(ucast asid := pd)) = 653 transform_asid_pool_contents pool(snd (transform_asid asid) \<mapsto> transform_asid_pool_entry pd)" 654 apply (clarsimp simp:transform_asid_pool_contents_def transform_asid_def) 655 apply (rule ext) 656 apply (case_tac x) 657 apply (clarsimp simp:unat_eq_0 unat_map_def) 658 apply (safe | clarsimp)+ 659 apply (safe | clarsimp simp:unat_map_def)+ 660 apply (subst (asm) of_nat_Suc[symmetric]) 661 apply (rule_tac P="Suc nat = unat (ucast asid)" in notE, simp) 662 apply (cut_tac x="Suc nat" and y="unat (ucast asid :: 10 word)" in word_unat.Abs_inject[symmetric, where 'a=10]) 663 apply (simp add:unats_def)+ 664 apply (rule unat_lt2p[where x="ucast asid :: 10 word", simplified]) 665 apply simp 666 done 667 668lemma dcorres_set_asid_pool: 669 "\<lbrakk> pool' = pool (ucast asid := pd); slot = snd (transform_asid asid); 670 cap = transform_asid_pool_entry pd \<rbrakk> \<Longrightarrow> 671 dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) a) 672 (KHeap_D.set_cap (a, slot) cap) 673 (set_asid_pool a pool')" 674 apply (simp add:KHeap_D.set_cap_def set_asid_pool_def get_object_def gets_the_def 675 gets_def bind_assoc) 676 apply (rule dcorres_absorb_get_l) 677 apply (clarsimp simp:obj_at_def opt_object_asid_pool assert_opt_def has_slots_def) 678 apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def 679 corres_underlying_def update_slots_def return_def object_slots_def) 680 apply (clarsimp simp:KHeap_A.set_object_def get_def put_def bind_def return_def) 681 apply (clarsimp simp:transform_def transform_current_thread_def) 682 apply (drule(1) arch_obj_not_idle) 683 apply (rule ext) 684 apply (clarsimp simp:not_idle_thread_def transform_objects_def restrict_map_def map_add_def) 685 apply (rule transform_asid_pool_contents_upd) 686 done 687 688lemma dcorres_set_vm_root: 689 "dcorres dc \<top> \<top> (return x) (set_vm_root rvd)" 690 apply (clarsimp simp: set_vm_root_def) 691 apply (rule dcorres_symb_exec_r)+ 692 apply (clarsimp simp:catch_def throwError_def) 693 apply (rule corres_dummy_return_r) 694 apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]])+ 695 apply wp+ 696 apply wpc 697 apply (wp do_machine_op_wp | clarsimp)+ 698 apply (rule_tac Q = "\<lambda>_ s. transform s = cs" in hoare_post_imp) 699 apply simp 700 apply (wpsimp wp: hoare_whenE_wp do_machine_op_wp [OF allI] hoare_drop_imps find_pd_for_asid_inv 701 simp: arm_context_switch_def get_hw_asid_def load_hw_asid_def if_apply_def2)+ 702 done 703 704lemma dcorres_delete_asid_pool: 705 "dcorres dc \<top> \<top> 706 (CSpace_D.delete_asid_pool (unat (asid_high_bits_of asid)) oid) 707 (ARM_A.delete_asid_pool asid oid)" 708 apply (simp add:CSpace_D.delete_asid_pool_def ARM_A.delete_asid_pool_def) 709 apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified]) 710 apply (clarsimp simp:gets_def) 711 apply (rule dcorres_absorb_get_r) 712 apply (clarsimp simp:when_def) 713 apply (rule conjI) 714 prefer 2 715 apply (clarsimp, rule corres_alternate2) 716 apply (clarsimp) 717 apply clarsimp 718 apply (rule corres_alternate1) 719 apply (rule dcorres_absorb_get_l) 720 apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified]) 721 apply (rule dcorres_symb_exec_r[where Q'="\<lambda>rv. \<top>", simplified]) 722 apply (rule corres_dummy_return_l) 723 apply (rule corres_underlying_split[where r'=dc and P="\<lambda>rv. \<top>" and P'="\<lambda>rv. \<top>", simplified]) 724 prefer 2 725 apply clarsimp 726 apply (rule dcorres_absorb_get_r) 727 apply (rule corres_guard_imp) 728 apply (rule dcorres_set_vm_root) 729 apply clarsimp+ 730 apply (rule corres_guard_imp[where Q=\<top> and Q'=\<top>, simplified]) 731 apply (clarsimp simp:simpler_modify_def put_def bind_def corres_underlying_def) 732 apply (clarsimp simp:transform_def transform_objects_def transform_cdt_def 733 transform_current_thread_def) 734 apply (clarsimp simp:transform_asid_table_def) 735 apply (rule ext) 736 apply (clarsimp simp:unat_map_def asid_high_bits_of_def 737 transform_asid_table_entry_def transform_asid_def) 738 apply safe 739 apply (drule unat_cong) 740 apply (subst (asm) word_unat.Abs_inverse) 741 apply (clarsimp simp:unats_def unat_ucast)+ 742 apply (rule mapM_wp) 743 apply clarsimp 744 apply wp 745 apply fastforce 746 apply wpsimp+ 747done 748 749lemma descendants_of_page: 750 "\<lbrakk>valid_mdb s;page_table_at oid s\<rbrakk>\<Longrightarrow> KHeap_D.descendants_of (oid, 0) (transform s) = {}" 751 apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def) 752 apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits) 753 apply (rule ccontr) 754 apply (clarsimp simp:valid_mdb_def dest!:not_emptyI) 755 apply (frule(1) cdl_cdt_parent_cte_at_lift) 756 apply clarsimp 757 apply (simp add:descendants_of_eqv cte_at_cases) 758 apply (clarsimp simp:transform_cslot_ptr_def) 759done 760 761lemma page_table_aligned: 762 "\<lbrakk>pspace_aligned s;page_table_at oid s\<rbrakk> \<Longrightarrow> 763 (oid && ~~ mask pt_bits) = oid" 764 apply (clarsimp simp:pspace_aligned_def obj_at_def a_type_def) 765 apply (clarsimp split:arch_kernel_obj.split_asm Structures_A.kernel_object.split_asm if_splits) 766 apply (drule_tac x = oid in bspec) 767 apply clarsimp 768 apply (clarsimp simp:obj_bits_def arch_kobj_size_def pt_bits_def pageBits_def) 769done 770 771lemma invalidateLocalTLB_VAASID_underlying_memory[wp]: 772 "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> invalidateLocalTLB_VAASID word \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 773 by (clarsimp simp: invalidateLocalTLB_VAASID_def, wp) 774 775lemma dcorres_flush_page: 776 "dcorres dc \<top> \<top> (return x) (flush_page aa a b word)" 777 apply (rule corres_dummy_return_r) 778 apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]]) 779 apply wp 780 apply (simp add:flush_page_def) 781 apply wp 782 apply (rule dcorres_to_wp[OF dcorres_set_vm_root]) 783 apply wp 784 apply clarsimp 785 apply (wp do_machine_op_wp, clarsimp) 786 apply (wp) 787 apply (simp add:load_hw_asid_def) 788 apply wp 789 apply (clarsimp simp:set_vm_root_for_flush_def) 790 apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+ 791 apply (wpc) 792 apply wp+ 793 apply (rule hoare_conjI,rule hoare_drop_imp) 794 apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+ 795 apply (wpc|wp)+ 796 apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post) 797 apply (wp|clarsimp)+ 798done 799 800lemma dcorres_flush_table: 801 "dcorres dc \<top> \<top> (return x) (flush_table aa a b word)" 802 apply (rule corres_dummy_return_r) 803 apply (rule dcorres_symb_exec_r[OF corres_free_return[where P=\<top> and P'=\<top>]]) 804 apply wp 805 apply (simp add:flush_table_def) 806 apply wp 807 apply (rule dcorres_to_wp[OF dcorres_set_vm_root]) 808 apply wp 809 apply clarsimp 810 apply (wp do_machine_op_wp|clarsimp)+ 811 apply (clarsimp simp:load_hw_asid_def) 812 apply wp 813 apply (clarsimp simp:set_vm_root_for_flush_def) 814 apply (wp do_machine_op_wp|clarsimp simp:arm_context_switch_def get_hw_asid_def)+ 815 apply wpc 816 apply wp+ 817 apply (rule hoare_conjI,rule hoare_drop_imp) 818 apply (wp do_machine_op_wp|clarsimp simp:load_hw_asid_def)+ 819 apply (wpc|wp)+ 820 apply (rule_tac Q="\<lambda>rv s. transform s = cs" in hoare_strengthen_post) 821 apply (wp|clarsimp)+ 822done 823 824lemma flush_table_exec: 825 "\<lbrakk>dcorres dc R (Q rv) h (g rv); \<lbrace>P\<rbrace> flush_table aa a b word \<lbrace>Q\<rbrace>\<rbrakk>\<Longrightarrow>dcorres dc R P h ((flush_table aa a b word) >>= g)" 826 apply (rule corres_dummy_return_pl) 827 apply (rule corres_guard_imp) 828 apply (rule corres_split[OF _ dcorres_flush_table]) 829 apply (simp|wp)+ 830 done 831 832 833lemma transform_cap_not_new_invented: 834 "transform_cap z \<noteq> cdl_cap.PageTableCap word Fake asid" 835 by (auto simp:transform_cap_def split:arch_cap.splits cap.splits) 836 837lemma page_table_not_idle: 838 "\<lbrakk>valid_idle s;page_table_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s" 839 apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) 840 apply (clarsimp simp: not_idle_thread_def split: if_splits) 841 done 842 843lemma page_directory_not_idle: 844 "\<lbrakk>valid_idle s;page_directory_at a s\<rbrakk> \<Longrightarrow> not_idle_thread a s" 845 apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) 846 apply (clarsimp simp: not_idle_thread_def split: if_splits) 847 done 848 849lemma page_table_at_rev: 850 "\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> \<Longrightarrow> page_table_at a s" 851 apply (clarsimp simp:obj_at_def valid_idle_def pred_tcb_at_def) 852 apply (clarsimp simp:a_type_def split: if_splits) 853 done 854 855lemma page_directory_at_rev: 856 "\<lbrakk>kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> \<Longrightarrow> page_directory_at a s" 857 apply (clarsimp simp:obj_at_def valid_idle_def st_tcb_at_def) 858 apply (clarsimp simp:a_type_def split: if_splits) 859 done 860 861lemma mask_pd_bits_less': 862 "uint ((ptr::word32) && mask pd_bits >> (2::nat)) < (4096::int)" 863 apply (clarsimp simp:pd_bits_def pageBits_def) 864 using shiftr_less_t2n'[where m = 12 and x ="(ptr && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] 865 apply (clarsimp simp:mask_twice) 866 done 867 868lemma mask_pd_bits_less: 869 "nat (uint ((y::word32) && mask pd_bits >> 2)) < 4096" 870 apply (clarsimp simp:pd_bits_def pageBits_def) 871 apply (rule iffD2[OF nat_less_eq_zless[where z = 4096,simplified]]) 872 apply (simp) 873 using shiftr_less_t2n'[where m = 12 and x ="(y && mask 14)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] 874 apply (clarsimp simp:mask_twice) 875done 876 877lemma mask_pt_bits_less': 878 "uint (((ptr::word32) && mask pt_bits) >> 2)< 256" 879 apply (clarsimp simp:pt_bits_def pageBits_def) 880 using shiftr_less_t2n'[where m = 8 and x ="(ptr && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] 881 apply (clarsimp simp:mask_twice ) 882done 883 884lemma mask_pt_bits_less: 885 "nat (uint ((y::word32) && mask pt_bits >> 2)) < 256" 886 apply (clarsimp simp:pt_bits_def pageBits_def) 887 apply (rule iffD2[OF nat_less_eq_zless[where z = 256,simplified]]) 888 apply (simp) 889 using shiftr_less_t2n'[where m = 8 and x ="(y && mask 10)" and n =2 ,simplified,THEN iffD1[OF word_less_alt]] 890 apply (clarsimp simp:mask_twice) 891done 892 893definition pd_pt_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool" 894where "pd_pt_relation pd pt offset s \<equiv> 895 \<exists>fun u v ref. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun)) 896 \<and> page_table_at pt s \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.PageTablePDE ref u v 897 \<and> pt = ptrFromPAddr ref )" 898 899definition pd_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool" 900where "pd_section_relation pd pt offset s \<equiv> 901 \<exists>fun u v ref1 ref2. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun)) 902 \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.SectionPDE ref1 u ref2 v 903 \<and> pt = ptrFromPAddr ref1 )" 904 905definition pd_super_section_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>'z::state_ext state\<Rightarrow>bool" 906where "pd_super_section_relation pd pt offset s \<equiv> 907 \<exists>fun u v ref1. ( kheap s pd = Some (ArchObj (arch_kernel_obj.PageDirectory fun)) 908 \<and> fun (ucast (offset && mask pd_bits >> 2)) = ARM_A.pde.SuperSectionPDE ref1 u v 909 \<and> pt = ptrFromPAddr ref1 )" 910 911definition pt_page_relation :: "word32\<Rightarrow>word32\<Rightarrow>word32\<Rightarrow>vmpage_size set\<Rightarrow>'z::state_ext state\<Rightarrow>bool" 912where "pt_page_relation pt page offset S s \<equiv> 913 \<exists>fun. (kheap s pt = Some (ArchObj (arch_kernel_obj.PageTable fun))) 914 \<and> (case fun (ucast (offset && mask pt_bits >> 2)) of 915 ARM_A.pte.LargePagePTE ref fun1 fun2 \<Rightarrow> 916 page = ptrFromPAddr ref \<and> ARMLargePage \<in> S 917 | ARM_A.pte.SmallPagePTE ref fun1 fun2 \<Rightarrow> 918 page = ptrFromPAddr ref \<and> ARMSmallPage \<in> S 919 | _ \<Rightarrow> False)" 920 921lemma slot_with_pt_frame_relation: 922 "\<lbrakk>valid_idle s;pt_page_relation a oid y S s\<rbrakk>\<Longrightarrow> 923 (a, nat (uint (y && mask pt_bits >> 2))) \<in> 924 ((slots_with (\<lambda>x. \<exists>rights sz asid. x = FrameCap False oid rights sz Fake asid)) (transform s))" 925 apply (clarsimp simp:pt_page_relation_def) 926 apply (frule page_table_at_rev) 927 apply (frule(1) page_table_not_idle) 928 apply (clarsimp simp:slots_with_def transform_def transform_objects_def restrict_map_def) 929 apply (clarsimp simp:not_idle_thread_def has_slots_def object_slots_def) 930 apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def) 931 apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ) 932 apply (clarsimp simp:mask_pt_bits_less split:ARM_A.pte.split_asm) 933done 934 935lemma below_kernel_base: 936 "ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots 937 \<Longrightarrow> kernel_pde_mask f (of_nat (unat (y && mask pd_bits >> 2))) 938 = f (of_nat (unat (y && mask pd_bits >> 2)))" 939 apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def ) 940 apply (simp add:ucast_nat_def[symmetric] unat_def) 941done 942 943(* we need an int version for 2016 *) 944lemma below_kernel_base_int: 945 "ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots 946 \<Longrightarrow> kernel_pde_mask f (of_int (uint (y && mask pd_bits >> 2))) 947 = f (of_int (uint (y && mask pd_bits >> 2)))" 948 apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def ) 949 apply (simp add:ucast_nat_def[symmetric] unat_def) 950done 951 952lemma slot_with_pd_pt_relation: 953 "\<lbrakk>valid_idle s; pd_pt_relation a b y s; ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> 954 (a, unat (y && mask pd_bits >> 2)) \<in> 955 (slots_with (\<lambda>x. \<exists>asid. x = cdl_cap.PageTableCap b Fake asid)) (transform s)" 956 apply (clarsimp simp :pd_pt_relation_def) 957 apply (frule page_directory_at_rev) 958 apply (frule(1) page_directory_not_idle) 959 apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def) 960 apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) 961 apply (clarsimp simp:has_slots_def object_slots_def) 962 apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) 963 apply (clarsimp simp:ucast_def) 964 apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def below_kernel_base) 965 apply (simp add:mask_pd_bits_less) 966done 967 968lemma slot_with_pd_section_relation: 969 "\<lbrakk>valid_idle s; pd_super_section_relation a b y s \<or> pd_section_relation a b y s; 970 ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> 971 (a, unat (y && mask pd_bits >> 2)) \<in> 972 (slots_with (\<lambda>x. \<exists>rights sz asid. x = cdl_cap.FrameCap False b rights sz Fake asid)) (transform s)" 973 apply (erule disjE) 974 apply (clarsimp simp :pd_super_section_relation_def) 975 apply (frule page_directory_at_rev) 976 apply (frule(1) page_directory_not_idle) 977 apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def) 978 apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) 979 apply (clarsimp simp:has_slots_def object_slots_def) 980 apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) 981 apply (clarsimp simp:ucast_def) 982 apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def mask_pd_bits_less) 983 apply (clarsimp simp :pd_section_relation_def) 984 apply (frule page_directory_at_rev) 985 apply (frule(1) page_directory_not_idle) 986 apply (clarsimp simp:transform_def slots_with_def transform_objects_def obj_at_def) 987 apply (clarsimp simp:restrict_map_def page_table_not_idle not_idle_thread_def pt_bits_def) 988 apply (clarsimp simp:has_slots_def object_slots_def) 989 apply (clarsimp simp:transform_page_directory_contents_def transform_pde_def unat_map_def below_kernel_base) 990 apply (clarsimp simp:ucast_def) 991 apply (simp add: word_of_int_nat[OF uint_ge_0,simplified] unat_def) 992 apply (simp add:mask_pd_bits_less) 993done 994 995lemma opt_cap_page_table:"\<lbrakk>valid_idle s;pd_pt_relation a pt_id x s;ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow> 996(opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s)) 997 = Some (cdl_cap.PageTableCap pt_id Fake None)" 998 apply (clarsimp simp:pd_pt_relation_def opt_cap_def transform_def unat_def slots_of_def opt_object_def) 999 apply (frule page_directory_at_rev) 1000 apply (frule(1) page_directory_not_idle) 1001 apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle 1002 restrict_map_def object_slots_def) 1003 apply (clarsimp simp:transform_page_directory_contents_def unat_def[symmetric] unat_map_def | rule conjI )+ 1004 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def) 1005 apply (clarsimp simp:below_kernel_base) 1006 apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] unat_def ucast_def) 1007 apply (simp add:mask_pd_bits_less unat_def) 1008done 1009 1010lemma opt_cap_page:"\<lbrakk>valid_idle s;pt_page_relation a pg x S s \<rbrakk>\<Longrightarrow> 1011\<exists>f sz. (opt_cap (a, unat (x && mask pt_bits >> 2) ) (transform s)) 1012 = Some (cdl_cap.FrameCap False pg f sz Fake None)" 1013 apply (clarsimp simp:pt_page_relation_def unat_def opt_cap_def transform_def slots_of_def opt_object_def) 1014 apply (frule page_table_at_rev) 1015 apply (frule(1) page_table_not_idle) 1016 apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle 1017 restrict_map_def object_slots_def) 1018 apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI )+ 1019 apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def) 1020 apply (simp add:word_of_int_nat[OF uint_ge_0,simplified] ucast_def mask_pt_bits_less)+ 1021 apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def) 1022done 1023 1024lemma opt_cap_section: 1025 "\<lbrakk>valid_idle s;pd_section_relation a pg x s \<or> pd_super_section_relation a pg x s; 1026 ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow> 1027 \<exists>f sz. (opt_cap (a, unat (x && mask pd_bits >> 2) ) (transform s)) 1028 = Some (cdl_cap.FrameCap False pg f sz Fake None)" 1029 unfolding unat_def 1030 apply (erule disjE) 1031 1032 apply (clarsimp simp: pd_section_relation_def opt_cap_def transform_def slots_of_def opt_object_def) 1033 apply (frule page_directory_at_rev) 1034 apply (frule(1) page_directory_not_idle) 1035 apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle 1036 restrict_map_def object_slots_def) 1037 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+ 1038 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base_int) 1039 apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+ 1040 apply (simp add:mask_pd_bits_less) 1041 apply (clarsimp simp:pd_super_section_relation_def opt_cap_def transform_def slots_of_def opt_object_def) 1042 apply (frule page_directory_at_rev) 1043 apply (frule(1) page_directory_not_idle) 1044 apply (clarsimp simp:transform_objects_def not_idle_thread_def page_directory_not_idle 1045 restrict_map_def object_slots_def) 1046 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:ARM_A.pte.split_asm | rule conjI)+ 1047 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def unat_def[symmetric] below_kernel_base_int) 1048 apply (simp add:word_of_int ucast_def unat_def mask_pt_bits_less)+ 1049 apply (simp add:mask_pd_bits_less) 1050done 1051 1052lemma opt_object_page_table:"\<lbrakk>valid_idle s;kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun))\<rbrakk> 1053\<Longrightarrow>opt_object a (transform s) = 1054 Some (cdl_object.PageTable \<lparr>cdl_page_table_caps = transform_page_table_contents fun\<rparr>)" 1055 apply (frule page_table_at_rev) 1056 apply (frule(1) page_table_not_idle) 1057 apply (clarsimp simp:transform_objects_def opt_object_def transform_def 1058 not_idle_thread_def restrict_map_def) 1059done 1060 1061lemma opt_object_page_directory:"\<lbrakk>valid_idle s;kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> 1062\<Longrightarrow>opt_object a (transform s) = 1063 Some (cdl_object.PageDirectory \<lparr>cdl_page_directory_caps = transform_page_directory_contents fun\<rparr>)" 1064 apply (frule page_directory_at_rev) 1065 apply (frule(1) page_directory_not_idle) 1066 apply (clarsimp simp:transform_objects_def opt_object_def transform_def 1067 not_idle_thread_def restrict_map_def) 1068done 1069 1070lemma remove_cdt_pt_slot_exec: 1071 "\<lbrakk>dcorres dc \<top> Q (g ()) f; 1072 \<And>s. Q s\<longrightarrow> ( (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and pt_page_relation a pg_id ptr UNIV) s\<rbrakk> 1073 \<Longrightarrow> dcorres dc P Q 1074 (remove_parent (a ,aptr) >>= g) f" 1075 apply (rule corres_dummy_return_pr) 1076 apply (rule corres_guard_imp) 1077 apply (rule corres_split[OF _ dummy_remove_cdt_pt_slot]) 1078 apply (rule_tac F="rv = ()" in corres_gen_asm) 1079 unfolding K_bind_def 1080 apply clarsimp 1081 apply (assumption) 1082 apply (simp|wp)+ 1083 apply (drule_tac x = s in meta_spec) 1084 apply (clarsimp simp:pt_page_relation_def dest!:page_table_at_rev) 1085done 1086 1087lemma remove_cdt_pd_slot_exec: 1088 "\<lbrakk>dcorres dc \<top> Q (g ()) f; 1089 \<And>s. Q s\<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and page_directory_at a) s\<rbrakk> 1090 \<Longrightarrow> dcorres dc P Q 1091 (remove_parent (a ,aptr) >>= g) f" 1092 apply (rule corres_dummy_return_pr) 1093 apply (rule corres_guard_imp) 1094 apply (rule corres_split[OF _ dummy_remove_cdt_pd_slot]) 1095 unfolding K_bind_def 1096 apply (simp|wp)+ 1097done 1098 1099lemma remove_cdt_asid_pool_slot_exec: 1100 "\<lbrakk>dcorres dc \<top> Q (g ()) f; 1101 \<And>s. Q s\<longrightarrow> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) and valid_idle and asid_pool_at a) s\<rbrakk> 1102 \<Longrightarrow> dcorres dc P Q 1103 (remove_parent (a ,aptr) >>= g) f" 1104 apply (rule corres_dummy_return_pr) 1105 apply (rule corres_guard_imp) 1106 apply (rule corres_split[OF _ dummy_remove_cdt_asid_pool_slot]) 1107 unfolding K_bind_def 1108 apply (simp|wp)+ 1109done 1110 1111lemma dcorres_set_pte_cap: 1112 "\<lbrakk> (x::word32) = (ptr && mask pt_bits >> 2);pte_cap = transform_pte a_pte\<rbrakk>\<Longrightarrow> 1113 dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.PageTable fun)) a ) 1114 (KHeap_D.set_cap (a, unat (ptr && mask pt_bits >> 2)) pte_cap) 1115 (KHeap_A.set_object a 1116 (ArchObj (arch_kernel_obj.PageTable (fun(ucast (ptr && mask pt_bits >> 2) := a_pte)))))" 1117 apply (simp add:KHeap_D.set_cap_def KHeap_A.set_object_def gets_the_def gets_def bind_assoc unat_def) 1118 apply (rule dcorres_absorb_get_r) 1119 apply (rule dcorres_absorb_get_l) 1120 apply (clarsimp simp:obj_at_def opt_object_page_table assert_opt_def has_slots_def object_slots_def) 1121 apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def 1122 corres_underlying_def update_slots_def return_def object_slots_def) 1123 apply (rule sym) 1124 apply (clarsimp simp:transform_def transform_current_thread_def) 1125 apply (rule ext) 1126 apply (clarsimp | rule conjI)+ 1127 apply (frule page_table_at_rev) 1128 apply (frule(1) page_table_not_idle) 1129 apply (clarsimp simp:transform_objects_def not_idle_thread_def) 1130 apply (rule ext) 1131 apply (clarsimp simp:transform_page_table_contents_def transform_pte_def unat_map_def ucast_def) 1132 apply (clarsimp simp:word_of_int word_of_nat mask_pt_bits_less mask_pt_bits_less' ucast_def) 1133 apply (subst (asm) word_of_int_inj) 1134 apply (clarsimp simp:mask_pt_bits_less')+ 1135 apply (clarsimp simp:uint_nat) 1136 apply clarify 1137 apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def) 1138done 1139 1140lemma dcorres_delete_cap_simple_set_pt: 1141 "dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) 1142 and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV 1143 and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageTable fun)) (ptr && ~~ mask pt_bits)) 1144 (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) 1145 (set_pt (ptr && ~~ mask pt_bits) (fun(ucast (ptr && mask pt_bits >> 2) := ARM_A.pte.InvalidPTE)))" 1146 apply (simp add:delete_cap_simple_def set_pt_def gets_the_def gets_def bind_assoc get_object_def) 1147 apply (rule dcorres_absorb_get_l) 1148 apply (rule dcorres_absorb_get_r) 1149 apply (clarsimp simp:assert_def corres_free_fail 1150 split:Structures_A.kernel_object.split_asm arch_kernel_obj.splits) 1151 apply (frule opt_cap_page) 1152 apply (simp add:)+ 1153 apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def) 1154 apply (rule dcorres_absorb_get_l) 1155 apply (clarsimp simp: always_empty_slot_def gets_the_def gets_def bind_assoc) 1156 apply (rule remove_cdt_pt_slot_exec[where pg_id = pg_id]) 1157 apply (rule corres_guard_imp) 1158 apply (rule dcorres_set_pte_cap) 1159 apply (simp add:transform_pte_def)+ 1160 apply clarsimp 1161 apply simp 1162 done 1163 1164 1165lemma transform_page_table_contents_upd: 1166 "transform_page_table_contents fun(unat (y && mask pt_bits >> 2) \<mapsto> transform_pte pte) = 1167 transform_page_table_contents 1168 (fun(ucast ((y::word32) && mask pt_bits >> 2) := pte))" 1169 apply (rule ext) 1170 apply (clarsimp simp:transform_page_table_contents_def unat_map_def ) 1171 apply (clarsimp simp:ucast_nat_def[symmetric]) 1172 apply (subgoal_tac "unat (y && mask pt_bits >> 2) < 256") 1173 apply (rule conjI|clarsimp)+ 1174 apply (drule word_unat.Abs_eqD) 1175 apply (simp add: unats_def)+ 1176 apply (rule unat_less_helper) 1177 apply (subst shiftr_div_2n_w) 1178 apply (clarsimp simp:word_size)+ 1179 apply (rule word_div_mult,simp) 1180 apply (clarsimp simp:pt_bits_def pageBits_def) 1181 apply (rule and_mask_less_size[where n = 10,simplified],simp add:word_size) 1182done 1183 1184lemma transform_page_directory_contents_upd: 1185 "ucast ((ptr::word32) && mask pd_bits >> 2) \<notin> kernel_mapping_slots 1186 \<Longrightarrow> transform_page_directory_contents f(unat (ptr && mask pd_bits >> 2) \<mapsto> transform_pde a_pde) 1187 = transform_page_directory_contents (f(ucast (ptr && mask pd_bits >> 2) := a_pde))" 1188 apply (rule ext) 1189 apply (simp (no_asm) add:transform_page_directory_contents_def unat_map_def) 1190 apply (simp add:below_kernel_base) 1191 apply (clarsimp simp: unat_def mask_pd_bits_less|rule conjI)+ 1192 apply (clarsimp simp:kernel_pde_mask_def kernel_mapping_slots_def) 1193 apply (clarsimp simp:ucast_nat_def[symmetric]) 1194 apply (drule sym) 1195 apply (drule word_unat.Abs_eqD) 1196 apply (simp add:unats_def unat_def[symmetric])+ 1197 apply (rule unat_less_helper) 1198 apply (subst shiftr_div_2n_w,(simp add:word_size)+) 1199 apply (rule word_div_mult,simp) 1200 apply (clarsimp simp:pt_bits_def pd_bits_def pageBits_def) 1201 apply (rule and_mask_less_size[where n = 14,simplified],simp add:word_size) 1202 apply (simp add:word_of_int unat_def) 1203 apply (clarsimp simp:ucast_def word_of_int_nat[OF uint_ge_0,simplified]) 1204done 1205 1206lemma dcorres_set_pde_cap: 1207 "\<lbrakk> (x::word32) = (ptr && mask pd_bits >> 2);pde_cap = transform_pde a_pde; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk>\<Longrightarrow> 1208 dcorres dc \<top> (valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) a ) 1209 (KHeap_D.set_cap (a, unat x) pde_cap) 1210 (KHeap_A.set_object a (ArchObj 1211 (arch_kernel_obj.PageDirectory (fun(ucast x := a_pde)))))" 1212 apply (simp add:KHeap_D.set_cap_def KHeap_A.set_object_def gets_the_def gets_def bind_assoc) 1213 apply (rule dcorres_absorb_get_r) 1214 apply (rule dcorres_absorb_get_l) 1215 apply (clarsimp simp:obj_at_def opt_object_page_directory assert_opt_def has_slots_def object_slots_def) 1216 apply (clarsimp simp:KHeap_D.set_object_def simpler_modify_def put_def bind_def corres_underlying_def update_slots_def object_slots_def return_def) 1217 apply (clarsimp simp:transform_def transform_current_thread_def) 1218 apply (rule ext) 1219 apply (clarsimp | rule conjI)+ 1220 apply (frule page_directory_at_rev) 1221 apply (frule(1) page_directory_not_idle) 1222 apply (clarsimp simp:transform_objects_def not_idle_thread_def) 1223 apply (rule sym) 1224 apply (erule transform_page_directory_contents_upd) 1225 apply (clarsimp simp: transform_objects_def restrict_map_def map_add_def) 1226done 1227 1228lemma dcorres_delete_cap_simple_set_pde: 1229 " ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots 1230 \<Longrightarrow>dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) 1231 and (pd_pt_relation (ptr && ~~ mask pd_bits) oid ptr 1232 or pd_section_relation (ptr && ~~ mask pd_bits) oid ptr 1233 or pd_super_section_relation (ptr && ~~ mask pd_bits) oid ptr) 1234 and valid_idle and ko_at (ArchObj (arch_kernel_obj.PageDirectory fun)) (ptr && ~~ mask pd_bits)) 1235 (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) 1236 (set_pd (ptr && ~~ mask pd_bits) (fun(ucast (ptr && mask pd_bits >> 2) := ARM_A.pde.InvalidPDE)))" 1237 apply (simp add:delete_cap_simple_def set_pd_def gets_the_def gets_def bind_assoc get_object_def) 1238 apply (rule dcorres_absorb_get_l) 1239 apply (rule dcorres_absorb_get_r) 1240 apply (clarsimp simp:assert_def corres_free_fail 1241 split:Structures_A.kernel_object.split_asm arch_kernel_obj.splits) 1242 apply (erule disjE) 1243 apply (frule opt_cap_page_table,simp+) 1244 apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def) 1245 apply (rule dcorres_absorb_get_l) 1246 apply (clarsimp simp:always_empty_slot_def gets_the_def gets_def bind_assoc) 1247 apply (rule remove_cdt_pd_slot_exec) 1248 apply (rule corres_guard_imp) 1249 apply (rule dcorres_set_pde_cap) 1250 apply (simp add:transform_pte_def)+ 1251 apply (clarsimp simp:pd_pt_relation_def transform_pde_def)+ 1252 apply (rule page_directory_at_rev) 1253 apply simp 1254 apply (frule opt_cap_section,simp+) 1255 apply (clarsimp simp:gets_def assert_opt_def PageTableUnmap_D.is_final_cap_def PageTableUnmap_D.is_final_cap'_def) 1256 apply (rule dcorres_absorb_get_l) 1257 apply (clarsimp simp:always_empty_slot_def gets_the_def gets_def bind_assoc) 1258 apply (rule remove_cdt_pd_slot_exec) 1259 apply (rule corres_guard_imp) 1260 apply (rule dcorres_set_pde_cap) 1261 apply simp+ 1262 apply (clarsimp simp:pd_pt_relation_def transform_pde_def)+ 1263 apply (rule page_directory_at_rev) 1264 apply simp 1265done 1266 1267lemma dcorres_lookup_pd_slot: 1268 "is_aligned pd 14 1269 \<Longrightarrow> (cdl_lookup_pd_slot pd vptr = transform_pd_slot_ref (lookup_pd_slot pd vptr))" 1270 apply (clarsimp simp:cdl_lookup_pd_slot_def 1271 transform_pd_slot_ref_def lookup_pd_slot_def) 1272 by (simp add:vaddr_segment_nonsense vaddr_segment_nonsense2) 1273 1274 1275lemma dcorres_delete_cap_simple_section: 1276 "dcorres dc \<top> (invs and pd_section_relation (lookup_pd_slot pd v && ~~ mask pd_bits) oid 1277 (lookup_pd_slot pd v) and K (is_aligned pd pd_bits \<and> v < kernel_base)) 1278 (delete_cap_simple (cdl_lookup_pd_slot pd v)) 1279 (store_pde (lookup_pd_slot pd v) ARM_A.pde.InvalidPDE)" 1280 apply (clarsimp simp: store_pde_def transform_pd_slot_ref_def lookup_pd_slot_def) 1281 apply (rule corres_gen_asm2) 1282 apply (subst dcorres_lookup_pd_slot, simp add: pd_bits_def pageBits_def) 1283 apply (clarsimp simp: transform_pd_slot_ref_def lookup_pd_slot_def) 1284 apply (rule corres_guard_imp) 1285 apply (rule corres_symb_exec_r) 1286 apply (rule dcorres_delete_cap_simple_set_pde[where oid = oid]) 1287 apply (drule(1) less_kernel_base_mapping_slots) 1288 apply (simp add: lookup_pd_slot_def) 1289 apply wpsimp+ 1290 apply fastforce 1291 done 1292 1293lemma large_frame_range_helper: 1294 fixes t :: word32 1295 shows 1296 "t \<in> set [0 , 4 .e. 0x3C] \<Longrightarrow> t < 0x40" 1297 apply (clarsimp simp: upto_enum_step_def) 1298 apply (subgoal_tac "x < 0x10") 1299 apply (subst mult.commute) 1300 apply (subst shiftl_t2n[where n =2,simplified,symmetric]) 1301 apply (rule shiftl_less_t2n[where m = 6 and n =2,simplified]) 1302 apply simp+ 1303 apply (rule le_less_trans) 1304 apply simp+ 1305done 1306 1307lemma zip_map_eqv: 1308 "(y, x) \<in> set (zip (map g xs) (map f xs)) = (\<exists>t. (y = g t \<and> x = f t \<and> t \<in> set xs))" 1309 apply (clarsimp simp:zip_map1 zip_map2) 1310 apply (rule iffI) 1311 apply (fastforce simp: in_set_zip) 1312 apply (clarsimp simp:set_zip_same) 1313 using imageI[where f ="(\<lambda>(a, b). (a, f b)) \<circ> (\<lambda>(x, y). (g x, y))",simplified] 1314 apply clarify 1315 apply (drule_tac x = t in meta_spec) 1316 apply (drule_tac x = t in meta_spec) 1317 apply (drule_tac x = "Id \<inter> (set xs) \<times> (set xs) " in meta_spec) 1318 apply clarsimp 1319done 1320 1321lemma page_directory_address_eq: 1322 fixes ptr :: word32 1323 shows 1324 "\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pd_bits = ptr + t && ~~ mask pd_bits" 1325 apply (drule large_frame_range_helper) 1326 using mask_lower_twice[where m = 14 and n = 6 and x= ptr,symmetric] 1327 apply (clarsimp simp:pd_bits_def pageBits_def) 1328 using mask_lower_twice[where m = 14 and n = 6 and x= "ptr+t",symmetric] 1329 apply (clarsimp simp:pd_bits_def pageBits_def) 1330 apply (subgoal_tac "(ptr && ~~ mask 6) = (ptr + t && ~~ mask 6)") 1331 apply simp 1332 apply (frule is_aligned_neg_mask_eq) 1333 apply simp 1334 apply (drule_tac q = t in mask_out_add_aligned) 1335 apply (subst(asm) less_mask_eq [THEN mask_eq_x_eq_0[THEN iffD1]], erule order_less_le_trans) 1336 apply clarsimp+ 1337done 1338 1339lemma page_table_address_eq: 1340 fixes ptr :: word32 1341 shows 1342 "\<lbrakk>is_aligned ptr 6; t \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptr && ~~ mask pt_bits = ptr + t && ~~ mask pt_bits" 1343 apply (drule large_frame_range_helper) 1344 using mask_lower_twice[where m = 10 and n = 6 and x= ptr,symmetric] 1345 apply (clarsimp simp:pt_bits_def pageBits_def) 1346 using mask_lower_twice[where m = 10 and n = 6 and x= "ptr+t",symmetric] 1347 apply (clarsimp simp:pt_bits_def pageBits_def) 1348 apply (subgoal_tac "(ptr && ~~ mask 6) = (ptr + t && ~~ mask 6)") 1349 apply simp 1350 apply (frule is_aligned_neg_mask_eq) 1351 apply simp 1352 apply (drule_tac q = t in mask_out_add_aligned) 1353 apply (subst(asm) less_mask_eq [THEN mask_eq_x_eq_0[THEN iffD1]], erule order_less_le_trans) 1354 apply clarsimp+ 1355done 1356 1357lemma shiftl_inj_if: 1358 "\<lbrakk>(shiftl a n) = (shiftl b n); shiftr (shiftl a n) n = a; shiftr (shiftl b n) n = b\<rbrakk> \<Longrightarrow> a = b" 1359 apply (drule arg_cong[where f = "\<lambda>x. shiftr x n"]) 1360 apply (rule box_equals) 1361 defer 1362 apply (assumption)+ 1363done 1364 1365lemma ucast_inj_mask: 1366 "((ucast (x::'a::len word)) :: ('b::len word)) = ((ucast (y::'a::len word)) :: ('b::len word)) 1367 \<Longrightarrow> (x && mask (len_of TYPE('b))) = (y && mask (len_of TYPE('b)))" 1368 apply (simp add:ucast_def) 1369 apply (simp add:word_ubin.inverse_norm) 1370 apply (simp add:word_ubin.eq_norm) 1371 apply (simp add:and_mask_bintr) 1372done 1373 1374lemma split_word_noteq_on_mask: 1375 "(x \<noteq> y) = (x && mask k \<noteq> y && mask k \<or> x && ~~ mask k \<noteq> y && ~~ mask k)" 1376 apply (rule iffI) 1377 using split_word_eq_on_mask[symmetric] 1378 apply auto 1379done 1380 1381lemma test_bits_mask: 1382 "\<lbrakk>x && mask l = y && mask l;na < size x; size x = size y\<rbrakk> 1383 \<Longrightarrow> na<l \<longrightarrow> x !! na = y !! na" 1384 apply (drule word_eqD) 1385 apply (auto simp:word_size) 1386done 1387 1388lemma test_bits_neg_mask: 1389 "\<lbrakk>x && ~~ mask l = y && ~~ mask l;na < size x; size x = size y\<rbrakk> 1390 \<Longrightarrow> l\<le> na \<longrightarrow> x !! na = y !! na" 1391 apply (drule word_eqD) 1392 apply (auto simp:word_size neg_mask_bang) 1393done 1394 1395lemma mask_compare_imply: 1396 "\<lbrakk> (x && mask k >> l) && mask n = (y && mask k >> l) && mask n;size x= size y; k\<le> size x; l+n \<le> k; x\<noteq>y\<rbrakk> 1397 \<Longrightarrow> (x && mask l \<noteq>y && mask l) \<or> (x && ~~ mask (l+n)) \<noteq> (y && ~~ mask (l+n))" 1398 apply (rule ccontr) 1399 apply (subgoal_tac "x = y") 1400 apply simp 1401 apply (rule word_eqI) 1402 apply clarsimp 1403 apply (case_tac "na<l") 1404 apply (drule_tac na = na in test_bits_mask[where l = l and y = y]) 1405 apply clarsimp+ 1406 apply (case_tac "l+n\<le> na") 1407 apply (drule_tac na = na in test_bits_neg_mask) 1408 apply clarsimp+ 1409 apply (drule_tac na = "na-l" in test_bits_mask) 1410 apply (clarsimp simp: linorder_not_le) 1411 apply (subst (asm) add.commute[where a = l])+ 1412 apply (drule nat_diff_less) 1413 apply (clarsimp simp:word_size)+ 1414 apply (clarsimp simp:nth_shiftr) 1415 apply (auto simp:word_size) 1416done 1417 1418lemma aligned_in_step_up_to: 1419 "\<lbrakk>x\<in> set (map (\<lambda>x. x + ptr) [0 , (2^t) .e. up]); t < word_bits; is_aligned ptr t\<rbrakk> 1420 \<Longrightarrow> is_aligned x t" 1421 apply (clarsimp simp:upto_enum_step_def image_def) 1422 apply (rule aligned_add_aligned[where n = t]) 1423 apply (rule is_aligned_mult_triv2) 1424 apply (simp add:word_bits_def)+ 1425done 1426 1427lemma remain_pt_pd_relation: 1428 "\<lbrakk>is_aligned ptr 2; \<forall>a\<in>ys. is_aligned a 2; ptr\<notin> ys\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace> 1429 store_pte ptr sp 1430 \<lbrace>\<lambda>r s. \<forall>y\<in>ys. pt_page_relation (y && ~~ mask pt_bits) pg_id y S s\<rbrace>" 1431 apply (rule hoare_vcg_const_Ball_lift) 1432 apply (subgoal_tac "ptr\<noteq> y") 1433 apply (simp add:store_pte_def) 1434 apply wp 1435 apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits) 1436 and pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_vcg_precond_imp) 1437 apply (clarsimp simp:set_pt_def) 1438 apply wp 1439 apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageTable x)) (ptr && ~~ mask pt_bits) 1440 and pt_page_relation (y && ~~ mask pt_bits) pg_id y S" in hoare_vcg_precond_imp) 1441 apply (clarsimp simp:valid_def set_object_def in_monad) 1442 apply (drule_tac x= y in bspec,simp) 1443 apply (clarsimp simp:pt_page_relation_def dest!: ucast_inj_mask| rule conjI)+ 1444 apply (drule mask_compare_imply) 1445 apply ((simp add:word_size pt_bits_def pageBits_def is_aligned_mask)+) 1446 1447 apply (clarsimp simp:pt_page_relation_def obj_at_def) 1448 apply (assumption) 1449 apply wp 1450 apply (simp add:get_object_def) 1451 apply wp 1452 apply (clarsimp simp:obj_at_def)+ 1453 apply (assumption) 1454 apply wp 1455 apply (clarsimp simp:obj_at_def pt_page_relation_def)+ 1456 done 1457 1458lemma remain_pd_section_relation: 1459 "\<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> 1460 \<Longrightarrow> \<lbrace>\<lambda>s. pd_section_relation ( y && ~~ mask pd_bits) sid y s\<rbrace> store_pde ptr sp 1461 \<lbrace>\<lambda>r s. pd_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>" 1462 apply (simp add:store_pde_def) 1463 apply wp 1464 apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits) 1465 and pd_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp) 1466 apply (clarsimp simp:set_pd_def) 1467 apply wp 1468 apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits) 1469 and pd_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp) 1470 apply (clarsimp simp:valid_def set_object_def in_monad) 1471 apply (clarsimp simp:pd_section_relation_def dest!:ucast_inj_mask | rule conjI)+ 1472 apply (drule mask_compare_imply) 1473 apply (simp add:word_size pd_bits_def pt_bits_def pageBits_def is_aligned_mask)+ 1474 apply (clarsimp simp:pt_page_relation_def obj_at_def) 1475 apply (assumption) 1476 apply wp 1477 apply (simp add:get_object_def) 1478 apply wp 1479 apply (clarsimp simp:obj_at_def)+ 1480 apply (assumption) 1481 apply wp 1482 apply (clarsimp simp:obj_at_def pt_page_relation_def)+ 1483done 1484 1485lemma remain_pd_super_section_relation: 1486 "\<lbrakk>is_aligned ptr 2; is_aligned y 2; ptr \<noteq> y\<rbrakk> 1487 \<Longrightarrow> \<lbrace>\<lambda>s. pd_super_section_relation ( y && ~~ mask pd_bits) sid y s\<rbrace> store_pde ptr sp 1488 \<lbrace>\<lambda>r s. pd_super_section_relation (y && ~~ mask pd_bits) sid y s\<rbrace>" 1489 apply (simp add:store_pde_def) 1490 apply wp 1491 apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits) 1492 and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp) 1493 apply (clarsimp simp:set_pd_def) 1494 apply wp 1495 apply (rule_tac Q = "ko_at (ArchObj (arch_kernel_obj.PageDirectory x)) (ptr && ~~ mask pd_bits) 1496 and pd_super_section_relation (y && ~~ mask pd_bits) sid y " in hoare_vcg_precond_imp) 1497 apply (clarsimp simp:valid_def set_object_def in_monad) 1498 apply (clarsimp simp:pd_super_section_relation_def dest!:ucast_inj_mask | rule conjI)+ 1499 apply (drule mask_compare_imply) 1500 apply (simp add:word_size pd_bits_def pt_bits_def pageBits_def is_aligned_mask)+ 1501 apply (clarsimp simp:pt_page_relation_def obj_at_def) 1502 apply (assumption) 1503 apply wp 1504 apply (simp add:get_object_def) 1505 apply wp 1506 apply (clarsimp simp:obj_at_def)+ 1507 apply (assumption) 1508 apply wp 1509 apply (clarsimp simp:obj_at_def pt_page_relation_def) 1510 done 1511 1512lemma remain_pd_either_section_relation: 1513 "\<lbrakk>\<forall>y \<in> set ys. is_aligned y 2;ptr\<notin> set ys;is_aligned ptr 2\<rbrakk> 1514 \<Longrightarrow> \<lbrace>\<lambda>s. \<forall>y\<in> set ys. (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> 1515 pd_section_relation (y && ~~ mask pd_bits) pg_id y s) \<rbrace> 1516 store_pde ptr ARM_A.pde.InvalidPDE 1517 \<lbrace>\<lambda>r s. \<forall>y\<in>set ys. 1518 (pd_super_section_relation (y && ~~ mask pd_bits) pg_id y s \<or> 1519 pd_section_relation (y && ~~ mask pd_bits) pg_id y s)\<rbrace>" 1520 including no_pre 1521 apply (rule hoare_vcg_const_Ball_lift) 1522 apply (wp hoare_vcg_disj_lift) 1523 apply (rule hoare_strengthen_post[OF remain_pd_super_section_relation]; fastforce) 1524 apply (rule hoare_strengthen_post[OF remain_pd_section_relation]; fastforce) 1525 done 1526 1527lemma is_aligned_less_kernel_base_helper: 1528 "\<lbrakk>is_aligned (ptr :: word32) 6; 1529 ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; x < 0x40 \<rbrakk> 1530 \<Longrightarrow> ucast (x + ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots" 1531 apply (simp add: kernel_mapping_slots_def) 1532 apply (simp add: word_le_nat_alt shiftr_20_unat_ucast 1533 unat_ucast_pd_bits_shift) 1534 apply (fold word_le_nat_alt, unfold linorder_not_le) 1535 apply (drule minus_one_helper3[where x=x]) 1536 apply (subst add.commute, subst is_aligned_add_or, assumption) 1537 apply (erule order_le_less_trans, simp) 1538 apply (simp add: word_ao_dist shiftr_over_or_dist) 1539 apply (subst less_mask_eq, erule order_le_less_trans) 1540 apply (simp add: pd_bits_def pageBits_def) 1541 apply (subst is_aligned_add_or[symmetric]) 1542 apply (rule_tac n=4 in is_aligned_shiftr) 1543 apply (simp add: is_aligned_andI1) 1544 apply (rule shiftr_less_t2n) 1545 apply (erule order_le_less_trans, simp) 1546 apply (rule aligned_add_offset_less) 1547 apply (rule_tac n=4 in is_aligned_shiftr) 1548 apply (simp add: is_aligned_andI1) 1549 apply (simp add: kernel_base_def is_aligned_def) 1550 apply assumption 1551 apply (rule shiftr_less_t2n) 1552 apply (erule order_le_less_trans) 1553 apply simp 1554 done 1555 1556lemma neg_aligned_less_kernel_base_helper: 1557 "\<lbrakk> is_aligned (ptr :: word32) 6; 1558 ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; 1559 y - ptr < 0x40 \<rbrakk> 1560 \<Longrightarrow> ucast (y && mask pd_bits >> 2) \<notin> kernel_mapping_slots" 1561 by (drule(2) is_aligned_less_kernel_base_helper, simp) 1562 1563lemma mapM_Cons_split: 1564 "xs \<noteq> [] \<Longrightarrow> (mapM f xs) = (do y \<leftarrow> f (hd xs); ys \<leftarrow> mapM f (tl xs); return (y # ys) od)" 1565 by (clarsimp simp:neq_Nil_conv mapM_Cons) 1566 1567lemma dcorres_store_invalid_pde_super_section: 1568 "dcorres dc \<top> (pd_super_section_relation (ptr && ~~ mask pd_bits) pg_id ptr 1569 and invs 1570 and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) 1571 (delete_cap_simple (ptr && ~~ mask pd_bits, unat (ptr && mask pd_bits >> 2))) 1572 (store_pde ptr ARM_A.pde.InvalidPDE)" 1573 apply simp 1574 apply (rule corres_gen_asm2) 1575 apply (rule corres_guard_imp) 1576 apply (simp add:store_pde_def) 1577 apply (rule corres_symb_exec_r) 1578 apply (rule dcorres_delete_cap_simple_set_pde[where oid = pg_id]) 1579 apply simp 1580 apply (wp|simp)+ 1581 apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def) 1582 done 1583 1584lemma dcorres_store_invalid_pte: 1585 "dcorres dc \<top> (pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr UNIV 1586 and invs ) 1587 (delete_cap_simple (ptr && ~~ mask pt_bits, unat (ptr && mask pt_bits >> 2))) 1588 (store_pte ptr ARM_A.pte.InvalidPTE)" 1589 apply (rule corres_guard_imp) 1590 apply (simp add:store_pte_def) 1591 apply (rule corres_symb_exec_r) 1592 apply (rule dcorres_delete_cap_simple_set_pt[where pg_id = pg_id]) 1593 apply (wp|simp)+ 1594 apply (clarsimp simp: invs_def valid_mdb_def valid_state_def valid_pspace_def) 1595 done 1596 1597lemma dcorres_store_pde_non_sense: 1598 "dcorres dc \<top> (valid_idle and 1599 (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s 1600 \<and> (f (ucast (slot && mask pd_bits >> 2)) = pde))) 1601 (return a) (store_pde slot pde)" 1602 apply (simp add:store_pde_def) 1603 apply (simp add:get_pd_def bind_assoc get_object_def set_pd_def gets_def) 1604 apply (rule dcorres_absorb_get_r) 1605 apply (clarsimp simp add:assert_def corres_free_fail 1606 split:Structures_A.kernel_object.splits arch_kernel_obj.splits) 1607 apply (rule dcorres_absorb_get_r) 1608 apply (clarsimp simp:corres_free_fail 1609 split:Structures_A.kernel_object.splits arch_kernel_obj.splits) 1610 apply (simp add:set_object_def put_def) 1611 apply (rule dcorres_absorb_get_r) 1612 apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def) 1613 apply (frule page_directory_at_rev) 1614 apply (drule(1) page_directory_not_idle[rotated]) 1615 apply (rule ext)+ 1616 apply (simp add:transform_objects_def not_idle_thread_def obj_at_def) 1617 done 1618 1619lemma dcorres_store_pte_non_sense: 1620 "dcorres dc \<top> (valid_idle and 1621 (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s 1622 \<and> (f (ucast (slot && mask pt_bits >> 2)) = pte))) 1623 (return a) (store_pte slot pte)" 1624 apply (simp add:store_pte_def) 1625 apply (simp add:get_pt_def bind_assoc get_object_def set_pt_def gets_def) 1626 apply (rule dcorres_absorb_get_r) 1627 apply (clarsimp simp add:assert_def corres_free_fail 1628 split:Structures_A.kernel_object.splits arch_kernel_obj.splits) 1629 apply (rule dcorres_absorb_get_r) 1630 apply (clarsimp simp:corres_free_fail 1631 split:Structures_A.kernel_object.splits arch_kernel_obj.splits) 1632 apply (simp add:set_object_def put_def) 1633 apply (rule dcorres_absorb_get_r) 1634 apply (simp add:corres_underlying_def return_def transform_def transform_current_thread_def) 1635 apply (frule page_table_at_rev) 1636 apply (drule(1) page_table_not_idle[rotated]) 1637 apply (rule ext)+ 1638 apply (simp add:transform_objects_def not_idle_thread_def obj_at_def) 1639 done 1640 1641lemma store_pde_non_sense_wp: 1642 "\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s 1643 \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE)) \<rbrace> 1644 store_pde x ARM_A.pde.InvalidPDE 1645 \<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s 1646 \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE))\<rbrace>" 1647 apply (simp add:store_pde_def get_object_def get_pde_def set_pd_def set_object_def) 1648 apply wp 1649 apply (clarsimp simp:obj_at_def split:Structures_A.kernel_object.splits) 1650 done 1651 1652lemma dcorres_store_invalid_pde_tail_super_section: 1653 "dcorres dc \<top> (valid_idle and 1654 (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (slot && ~~ mask pd_bits) s 1655 \<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pd_bits >> 2)) = ARM_A.pde.InvalidPDE)) 1656 and K (\<forall>sl\<in> set slots. sl && ~~ mask pd_bits = slot && ~~ mask pd_bits)) 1657 (return a) 1658 (mapM (swp store_pde ARM_A.pde.InvalidPDE) slots)" 1659 proof (induct slots arbitrary:a) 1660 case Nil 1661 show ?case 1662 by (simp add:mapM_Nil) 1663 next 1664 case (Cons x xs) 1665 show ?case 1666 apply (rule corres_guard_imp) 1667 apply (simp add:mapM_Cons dc_def[symmetric]) 1668 apply (rule corres_dummy_return_l) 1669 apply (rule corres_split[OF _ dcorres_store_pde_non_sense]) 1670 apply (rule corres_dummy_return_l) 1671 apply (rule corres_split[OF _ Cons.hyps[unfolded swp_def]]) 1672 apply (rule corres_free_return[where P=\<top> and P'=\<top>]) 1673 apply wp+ 1674 apply simp 1675 apply (wp store_pde_non_sense_wp) 1676 apply simp 1677 apply (clarsimp simp:obj_at_def) 1678 done 1679qed 1680 1681lemma store_pte_non_sense_wp: 1682 "\<lbrace>\<lambda>s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s 1683 \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE)) \<rbrace> 1684 store_pte x ARM_A.pte.InvalidPTE 1685 \<lbrace>\<lambda>r s. (\<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s 1686 \<and> (\<forall>slot\<in>set xs. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE))\<rbrace>" 1687 apply (simp add:store_pte_def get_object_def get_pte_def set_pt_def set_object_def) 1688 apply wp 1689 apply (clarsimp simp:obj_at_def split: Structures_A.kernel_object.splits) 1690 done 1691 1692lemma dcorres_store_invalid_pte_tail_large_page: 1693 "dcorres dc \<top> (valid_idle and 1694 (\<lambda>s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageTable f)) (slot && ~~ mask pt_bits) s 1695 \<and> (\<forall>slot\<in> set slots. f (ucast (slot && mask pt_bits >> 2)) = ARM_A.pte.InvalidPTE)) 1696 and K (\<forall>sl\<in> set slots. sl && ~~ mask pt_bits = slot && ~~ mask pt_bits)) 1697 (return a) 1698 (mapM (swp store_pte ARM_A.pte.InvalidPTE) slots)" 1699 proof (induct slots arbitrary:a) 1700 case Nil 1701 show ?case 1702 by (simp add:mapM_Nil) 1703 next 1704 case (Cons x xs) 1705 show ?case 1706 apply (rule corres_guard_imp) 1707 apply (simp add:mapM_Cons dc_def[symmetric]) 1708 apply (rule corres_dummy_return_l) 1709 apply (rule corres_split[OF _ dcorres_store_pte_non_sense]) 1710 apply (rule corres_dummy_return_l) 1711 apply (rule corres_split[OF _ Cons.hyps[unfolded swp_def]]) 1712 apply (rule corres_free_return[where P=\<top> and P'=\<top>]) 1713 apply wp+ 1714 apply simp 1715 apply (wp store_pte_non_sense_wp) 1716 apply simp 1717 apply (clarsimp simp:obj_at_def) 1718 done 1719qed 1720 1721lemma and_mask_plus: 1722 "\<lbrakk>is_aligned ptr m; m \<le> n; n < 32; a < 2 ^m\<rbrakk> 1723 \<Longrightarrow> (ptr::word32) + a && mask n = (ptr && mask n) + a" 1724 apply (rule mask_eqI[where n = m]) 1725 apply (simp add:mask_twice min_def) 1726 apply (simp add:is_aligned_add_helper) 1727 apply (subst is_aligned_add_helper[THEN conjunct1]) 1728 apply (erule is_aligned_after_mask) 1729 apply simp 1730 apply simp 1731 apply simp 1732 apply (subgoal_tac "(ptr + a && mask n) && ~~ mask m 1733 = (ptr + a && ~~ mask m ) && mask n") 1734 apply (simp add:is_aligned_add_helper) 1735 apply (subst is_aligned_add_helper[THEN conjunct2]) 1736 apply (simp add:is_aligned_after_mask) 1737 apply simp 1738 apply simp 1739 apply (simp add:word_bw_comms word_bw_lcs) 1740 done 1741 1742lemma dcorres_unmap_large_section: 1743 "\<lbrakk>vmsz_aligned v ARMSuperSection; is_aligned ptr 14; 1744 v < kernel_base \<rbrakk> 1745 \<Longrightarrow> dcorres dc \<top> 1746 (invs and valid_pdpt_objs 1747 and (pd_super_section_relation ((lookup_pd_slot ptr v) && ~~ mask pd_bits) 1748 pg_id (lookup_pd_slot ptr v))) 1749 (delete_cap_simple (cdl_lookup_pd_slot ptr v)) 1750 (mapM (swp store_pde ARM_A.pde.InvalidPDE) 1751 (map (\<lambda>x. x + lookup_pd_slot ptr v) [0 , 4 .e. 0x3C]))" 1752 supply is_aligned_neg_mask_eq[simp del] is_aligned_neg_mask_weaken[simp del] 1753 apply (subst mapM_Cons_split) 1754 apply (simp add:upto_enum_step_def upto_enum_def) 1755 apply (simp add:store_pte_def PageTableUnmap_D.unmap_page_def) 1756 apply (rule corres_dummy_return_l) 1757 apply (simp add: upto_enum_step_def transform_pt_slot_ref_def upto_enum_def hd_map_simp 1758 dcorres_lookup_pd_slot)+ 1759 apply (rule corres_guard_imp) 1760 apply (simp add:transform_pd_slot_ref_def) 1761 apply (rule corres_dummy_return_l) 1762 apply (rule corres_split[OF _ dcorres_store_invalid_pde_super_section[where pg_id = pg_id]]) 1763 apply(rule corres_dummy_return_l) 1764 apply (rule_tac r'=dc in corres_split[OF corres_free_return[where P=\<top> and P'=\<top>]]) 1765 apply (rule dcorres_store_invalid_pde_tail_super_section[where slot = ptr]) 1766 apply wp+ 1767 apply (wp store_pde_non_sense_wp) 1768 apply simp 1769 apply (simp add: hd_map_simp upto_enum_step_def upto_enum_def drop_map) 1770 apply (rule conjI) 1771 apply (rule less_kernel_base_mapping_slots) 1772 apply (simp add:pd_bits_def pageBits_def)+ 1773 apply (rule conjI, fastforce) \<comment> \<open>valid_idle\<close> 1774 apply (rule conj_comms[THEN iffD1]) 1775 apply (rule context_conjI) 1776 apply (clarsimp simp: tl_map tl_upt) 1777 apply (clarsimp simp: field_simps) 1778 apply (subst mask_lower_twice[symmetric,where n = 6]) 1779 apply (simp add:pd_bits_def pageBits_def) 1780 apply (subst is_aligned_add_helper) 1781 apply (erule(1) lookup_pd_slot_aligned_6) 1782 apply (simp add:upto_0_to_n) 1783 apply (rule word_less_power_trans_ofnat[where k = 2 and m = 6,simplified]) 1784 apply simp 1785 apply simp 1786 apply (simp add: lookup_pd_slot_def is_aligned_neg_mask_eq 1787 pd_shifting[unfolded pd_bits_def pageBits_def,simplified]) 1788 apply (clarsimp simp:pd_super_section_relation_def obj_at_def) 1789 apply (simp add: lookup_pd_slot_pd[unfolded pd_bits_def pageBits_def,simplified] 1790 is_aligned_neg_mask_eq pd_shifting[unfolded pd_bits_def pageBits_def,simplified]) 1791 apply (rule ballI, drule (1) bspec) 1792 supply is_aligned_neg_mask2[simp del] 1793 apply (clarsimp simp: upto_0_to_n tl_map) 1794 apply (frule (1) lookup_pd_slot_aligned_6[unfolded pd_bits_def pageBits_def,simplified]) 1795 apply (drule(1) valid_pdpt_objs_pdD) 1796 apply clarsimp 1797 apply (frule (1) lookup_pd_slot_aligned_6[unfolded pd_bits_def pageBits_def,simplified]) 1798 apply (rename_tac pd rights attr ref s slot) 1799 apply (drule_tac x = "(ucast (lookup_pd_slot ptr v + of_nat slot * 4 && mask pd_bits >> 2))" 1800 and y = "ucast (lookup_pd_slot ptr v && mask pd_bits >> 2)" 1801 in valid_entriesD[rotated]) 1802 apply (rule ccontr) 1803 apply simp 1804 apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(12 word\<Rightarrow>word32)"]) 1805 apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"]) 1806 apply (subst (asm) ucast_ucast_len) 1807 apply (rule shiftr_less_t2n) 1808 apply (rule less_le_trans[OF and_mask_less']) 1809 apply (simp add:pd_bits_def pageBits_def) 1810 apply (simp add:pd_bits_def pageBits_def) 1811 apply (subst (asm) ucast_ucast_len) 1812 apply (rule shiftr_less_t2n) 1813 apply (rule less_le_trans[OF and_mask_less']) 1814 apply (simp add:pd_bits_def pageBits_def) 1815 apply (simp add:pd_bits_def pageBits_def) 1816 apply (simp add:shiftr_shiftl1) 1817 apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) 1818 apply (erule is_aligned_andI1[OF aligned_add_aligned]) 1819 apply (simp add: shiftl_t2n[symmetric,where n =2, simplified field_simps,simplified] 1820 is_aligned_shiftl_self) 1821 apply simp 1822 apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) 1823 apply (erule is_aligned_andI1[OF is_aligned_weaken]) 1824 apply simp 1825 apply (subst (asm) and_mask_plus) 1826 apply (erule lookup_pd_slot_aligned_6, simp) 1827 apply (simp add:pd_bits_def pageBits_def)+ 1828 apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified]) 1829 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1830 apply (simp add:word_of_nat_less) 1831 apply simp 1832 apply simp 1833 apply (subgoal_tac "0 < (of_nat (slot * 4)::word32)") 1834 apply simp 1835 apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]]) 1836 apply fastforce 1837 apply simp 1838 apply fastforce 1839 apply (rule ccontr) 1840 apply (erule_tac x = "ucast (lookup_pd_slot ptr v + of_nat slot * 4 && mask pd_bits >> 2)" 1841 in in_empty_interE) 1842 apply (rule non_invalid_in_pde_range) 1843 apply (simp add: pd_bits_def pageBits_def field_simps) 1844 apply (simp add: ucast_neg_mask) 1845 apply (simp add:is_aligned_shiftr) 1846 apply (rule arg_cong[where f = ucast]) 1847 apply (rule shiftr_eq_neg_mask_eq) 1848 apply (simp add:shiftr_shiftr shiftr_over_and_dist) 1849 apply (subst aligned_shift') 1850 apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified]) 1851 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1852 apply (simp add:word_of_nat_less) 1853 apply simp+ 1854 done 1855 1856lemma pt_page_relation_weaken: 1857 "\<lbrakk> pt_page_relation a b c S s; S \<subseteq> T \<rbrakk> \<Longrightarrow> pt_page_relation a b c T s" 1858 apply (clarsimp simp: pt_page_relation_def) 1859 apply (auto split: ARM_A.pte.split) 1860 done 1861 1862lemma pt_page_relation_univ: 1863 "pt_page_relation a b c {ARMLargePage} s 1864 \<Longrightarrow> pt_page_relation a b c UNIV s" 1865 apply (clarsimp simp:pt_page_relation_def) 1866 apply (clarsimp split: ARM_A.pte.splits) 1867 done 1868 1869lemma dcorres_unmap_large_page: 1870 "is_aligned ptr 6 1871 \<Longrightarrow> dcorres dc \<top> (invs and valid_pdpt_objs 1872 and pt_page_relation (ptr && ~~ mask pt_bits) pg_id ptr {ARMLargePage}) 1873 (delete_cap_simple (transform_pt_slot_ref ptr)) 1874 (mapM (swp store_pte ARM_A.pte.InvalidPTE) (map (\<lambda>x. x + ptr) [0 , 4 .e. 0x3C]))" 1875 supply is_aligned_neg_mask_eq[simp del] 1876 is_aligned_neg_mask_weaken[simp del] 1877 apply (subst mapM_Cons_split) 1878 apply (simp add:upto_enum_step_def upto_enum_def) 1879 apply (simp add: PageTableUnmap_D.unmap_page_def) 1880 apply (rule corres_dummy_return_l) 1881 apply (simp add:upto_enum_step_def transform_pt_slot_ref_def upto_enum_def hd_map_simp)+ 1882 apply (rule corres_guard_imp) 1883 apply(rule corres_dummy_return_l) 1884 apply (rule corres_split[OF _ dcorres_store_invalid_pte[where pg_id = pg_id]]) 1885 apply(rule corres_dummy_return_l) 1886 apply (rule_tac r'=dc in corres_split[OF corres_free_return[where P=\<top> and P'=\<top>]]) 1887 apply (rule dcorres_store_invalid_pte_tail_large_page[where slot = ptr]) 1888 apply wp+ 1889 apply (wp store_pte_non_sense_wp) 1890 apply simp 1891 apply (clarsimp simp:unat_def pt_page_relation_univ) 1892 apply (rule conjI,fastforce) 1893 apply (rule conj_comms[THEN iffD1]) 1894 apply (rule context_conjI) 1895 apply (clarsimp simp:tl_map drop_map tl_upt) 1896 apply (simp add:field_simps) 1897 apply (subst mask_lower_twice[symmetric,where n = 6]) 1898 apply (simp add:pt_bits_def pageBits_def) 1899 apply (subst is_aligned_add_helper) 1900 apply simp 1901 apply (simp add:upto_0_to_n) 1902 apply (rule word_less_power_trans_ofnat[where k = 2 and m = 6,simplified]) 1903 apply simp 1904 apply simp 1905 apply simp 1906 apply (clarsimp simp:pt_page_relation_def obj_at_def) 1907 apply (drule(1) bspec) 1908 apply (clarsimp simp:tl_map drop_map upto_0_to_n) 1909 apply (simp add: field_simps) 1910 apply (drule(1) valid_pdpt_objs_ptD,clarify) 1911 apply (drule_tac x = "(ucast (ptr + of_nat x * 4 && mask pt_bits >> 2))" 1912 and y = "ucast (ptr && mask pt_bits >> 2)" 1913 in valid_entriesD[rotated]) 1914 apply (rule ccontr) 1915 apply simp 1916 apply (drule_tac x="ucast v" for v in arg_cong[where f = "ucast::(word8\<Rightarrow>word32)"]) 1917 apply (drule_tac x="ucast v" for v in arg_cong[where f = "\<lambda>x. shiftl x 2"]) 1918 apply (subst (asm) ucast_ucast_len) 1919 apply (rule shiftr_less_t2n) 1920 apply (rule less_le_trans[OF and_mask_less']) 1921 apply (simp add:pt_bits_def pageBits_def) 1922 apply (simp add:pt_bits_def pageBits_def) 1923 apply (subst (asm) ucast_ucast_len) 1924 apply (rule shiftr_less_t2n) 1925 apply (rule less_le_trans[OF and_mask_less']) 1926 apply (simp add:pt_bits_def pageBits_def) 1927 apply (simp add:pt_bits_def pageBits_def) 1928 apply (simp add:shiftr_shiftl1) 1929 apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) 1930 apply (erule is_aligned_andI1[OF aligned_add_aligned]) 1931 apply (simp add: shiftl_t2n[symmetric, where n=2, simplified field_simps, simplified] 1932 is_aligned_shiftl_self) 1933 apply simp 1934 apply (subst (asm) is_aligned_neg_mask_eq[where n = 2]) 1935 apply (erule is_aligned_andI1[OF is_aligned_weaken]) 1936 apply simp 1937 apply (subst (asm) and_mask_plus) 1938 apply simp 1939 apply (simp add:pt_bits_def pageBits_def)+ 1940 apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified]) 1941 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1942 apply (simp add:word_of_nat_less) 1943 apply simp 1944 apply simp 1945 apply (subgoal_tac "0 < (of_nat (x * 4)::word32)") 1946 apply simp 1947 apply (rule le_less_trans[OF _ of_nat_mono_maybe[where y = 0]]) 1948 apply fastforce 1949 apply simp 1950 apply fastforce 1951 apply (clarsimp split:if_splits pte.split_asm) 1952 apply (rule ccontr) 1953 apply (erule_tac x = "ucast (ptr + of_nat x * 4 && mask pt_bits >> 2)" in in_empty_interE) 1954 apply (rule non_invalid_in_pte_range) 1955 apply simp 1956 apply (simp add: ucast_neg_mask) 1957 apply (rule arg_cong[where f = ucast]) 1958 apply (rule shiftr_eq_neg_mask_eq) 1959 apply (simp add:shiftr_shiftr shiftr_over_and_dist) 1960 apply (subst aligned_shift') 1961 apply (simp add:shiftl_t2n[symmetric,where n =2,simplified field_simps,simplified]) 1962 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1963 apply (simp add:word_of_nat_less) 1964 apply (simp+)[4] 1965 apply (simp add: is_aligned_shiftr) 1966 done 1967 1968end 1969 1970lemma (in pspace_update_eq) pd_pt_relation_update[iff]: 1971 "pd_pt_relation a b c (f s) = pd_pt_relation a b c s" 1972 by (simp add: pd_pt_relation_def pspace) 1973 1974context begin interpretation Arch . (*FIXME: arch_split*) 1975 1976crunch cdt[wp] :flush_page "\<lambda>s. P (cdt s)" 1977 (wp: crunch_wps simp:crunch_simps) 1978 1979crunch valid_idle[wp]: flush_page "valid_idle" 1980 (wp: crunch_wps simp:crunch_simps) 1981 1982lemma mdb_cte_at_flush_page[wp]: 1983 "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> flush_page a b c d 1984 \<lbrace>\<lambda>_ s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" 1985 apply (simp add:mdb_cte_at_def) 1986 apply (simp only: imp_conv_disj) 1987 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) 1988 done 1989 1990crunch pd_pt_relation[wp]: flush_table "pd_pt_relation a b c" 1991 (wp: crunch_wps simp: crunch_simps) 1992 1993crunch valid_idle[wp]: flush_table "valid_idle" 1994 (wp: crunch_wps simp:crunch_simps) 1995 1996crunch valid_idle[wp]: page_table_mapped "valid_idle" 1997 (wp: crunch_wps simp:crunch_simps) 1998 1999crunch valid_idle[wp]: invalidate_asid_entry "valid_idle" 2000 (wp: crunch_wps simp:crunch_simps) 2001 2002crunch valid_idle[wp]: flush_space "valid_idle" 2003 (wp: crunch_wps simp:crunch_simps) 2004 2005lemma page_table_mapped_stable[wp]: 2006 "\<lbrace>(=) s\<rbrace> page_table_mapped a b w \<lbrace>\<lambda>r. (=) s\<rbrace>" 2007 apply (simp add:page_table_mapped_def) 2008 apply (wp|wpc)+ 2009 apply (simp add:get_pde_def) 2010 apply wp 2011 apply (simp add:find_pd_for_asid_def) 2012 apply (wp|wpc)+ 2013 apply clarsimp 2014done 2015 2016lemma eqv_imply_stable: 2017assumes "\<And>cs. \<lbrace>(=) cs\<rbrace> f \<lbrace>\<lambda>r. (=) cs\<rbrace>" 2018shows "\<lbrace>P\<rbrace> f \<lbrace>\<lambda>r. P\<rbrace>" 2019 using assms 2020 apply (fastforce simp:valid_def) 2021done 2022 2023lemma check_mapping_pptr_pt_relation: 2024 "\<lbrace>\<lambda>s. vmpage_size \<in> S\<rbrace> check_mapping_pptr w vmpage_size (Inl b) 2025 \<lbrace>\<lambda>r s. r \<longrightarrow> pt_page_relation (b && ~~ mask pt_bits) w b S s\<rbrace>" 2026 apply (simp add:check_mapping_pptr_def get_pte_def) 2027 apply (rule hoare_pre, wp get_pte_wp) 2028 apply (clarsimp simp: obj_at_def) 2029 apply (clarsimp simp: pt_page_relation_def) 2030 apply (simp split: ARM_A.pte.split_asm) 2031 done 2032 2033lemma check_mapping_pptr_section_relation: 2034 "\<lbrace>\<top>\<rbrace> check_mapping_pptr w ARMSection (Inr (lookup_pd_slot rv' b)) 2035 \<lbrace>\<lambda>rv s. rv \<longrightarrow> 2036 pd_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>" 2037 apply (rule hoare_vcg_precond_imp) 2038 apply (simp add:check_mapping_pptr_def) 2039 apply (wp get_pde_wp) 2040 apply (clarsimp simp: obj_at_def) 2041 apply (clarsimp simp: pd_section_relation_def pd_super_section_relation_def 2042 split: ARM_A.pde.split_asm) 2043done 2044 2045lemma check_mapping_pptr_super_section_relation: 2046 "\<lbrace>\<top>\<rbrace> check_mapping_pptr w ARMSuperSection (Inr (lookup_pd_slot rv' b)) 2047 \<lbrace>\<lambda>rv s. rv \<longrightarrow> pd_super_section_relation (lookup_pd_slot rv' b && ~~ mask pd_bits) w (lookup_pd_slot rv' b) s\<rbrace>" 2048 apply (rule hoare_vcg_precond_imp) 2049 apply (simp add:check_mapping_pptr_def) 2050 apply (wp get_pde_wp) 2051 apply (clarsimp simp: obj_at_def) 2052 apply (clarsimp simp: pd_section_relation_def pd_super_section_relation_def 2053 split: ARM_A.pde.split_asm) 2054done 2055 2056lemma lookup_pt_slot_aligned: 2057 "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits \<and> is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace> 2058 lookup_pt_slot pd vptr \<lbrace>\<lambda>rb s. is_aligned rb 6\<rbrace>, -" 2059 apply (rule hoare_gen_asmE)+ 2060 apply (rule hoare_pre, rule hoare_post_imp_R, rule lookup_pt_slot_cap_to) 2061 apply auto 2062 done 2063 2064lemma get_pde_pd_relation: 2065 "\<lbrace>P\<rbrace> get_pde x 2066 \<lbrace>\<lambda>r s. \<exists>f. ko_at (ArchObj (arch_kernel_obj.PageDirectory f)) (x && ~~ mask pd_bits) s 2067 \<and> r = f (ucast (x && mask pd_bits >> 2))\<rbrace>" 2068 apply (simp add:get_pde_def) 2069 apply wp 2070 apply (clarsimp simp:obj_at_def) 2071done 2072 2073lemma pd_pt_relation_page_table_mapped_wp: 2074 "\<lbrace>page_table_at w\<rbrace> page_table_mapped a b w 2075 \<lbrace>\<lambda>r s. (case r of Some pd \<Rightarrow> pd_pt_relation 2076 (lookup_pd_slot pd b && ~~ mask pd_bits) w (lookup_pd_slot pd b) s | _ \<Rightarrow> True)\<rbrace>" 2077 apply (simp add:page_table_mapped_def) 2078 apply wp 2079 apply wpc 2080 apply (clarsimp simp:validE_def valid_def return_def returnOk_def) 2081 apply wp+ 2082 apply simp 2083 apply (simp add:get_pde_def) 2084 apply wp 2085 apply (simp add:validE_def) 2086 apply (rule hoare_strengthen_post[where Q="\<lambda>rv. page_table_at w"]) 2087 apply wp 2088 apply (clarsimp simp:pd_pt_relation_def obj_at_def)+ 2089 done 2090 2091lemma hoare_post_Some_conj: 2092 "\<lbrakk> \<lbrace>P\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> Q a s | _ \<Rightarrow> S \<rbrace>; 2093 \<lbrace>P'\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> R a s | _ \<Rightarrow> S \<rbrace> 2094 \<rbrakk> \<Longrightarrow>\<lbrace>P and P'\<rbrace>f\<lbrace>\<lambda>r s. case r of Some a \<Rightarrow> Q a s \<and> R a s | _ \<Rightarrow> S\<rbrace>" 2095 apply (clarsimp simp:valid_def) 2096 apply (drule_tac x = s in spec)+ 2097 apply clarsimp 2098 apply (drule_tac x= "(a,b)" in bspec,simp)+ 2099 apply (clarsimp split:option.splits) 2100done 2101 2102lemma cleanByVA_PoU_underlying_memory[wp]: " \<lbrace>\<lambda>m'. underlying_memory m' = m\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' = m\<rbrace>" 2103 apply(clarsimp simp: cleanByVA_PoU_def, wp) 2104done 2105 2106lemma cdl_asid_table_transform: 2107 "cdl_asid_table (transform sa) x 2108 = unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table (arch_state sa)) x" 2109 by (simp add:transform_def transform_asid_table_def) 2110 2111lemma dcorres_find_pd_for_asid: 2112 "dcorres ( dc \<oplus> (=)) \<top> valid_idle 2113 (cdl_find_pd_for_asid (transform_asid a, b)) 2114 (find_pd_for_asid a)" 2115 apply (simp add:cdl_find_pd_for_asid_def find_pd_for_asid_def transform_asid_def) 2116 apply (simp add:liftE_bindE assertE_assert) 2117 apply (rule dcorres_symb_exec_r[where Q' = "\<lambda>r. valid_idle"]) 2118 apply (simp add:gets_def) 2119 apply (rule dcorres_get) 2120 apply (clarsimp simp:cdl_asid_table_transform liftE_bindE 2121 transform_asid_table_entry_def split:option.splits) 2122 apply (simp add:get_asid_pool_def get_object_def gets_the_def gets_def bind_assoc) 2123 apply (rule dcorres_get) 2124 apply (clarsimp simp: obj_at_def opt_object_asid_pool 2125 assert_opt_def has_slots_def opt_cap_def slots_of_def assert_def 2126 corres_free_fail 2127 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 2128 apply (clarsimp simp:transform_asid_pool_contents_def 2129 object_slots_def transform_asid_pool_entry_def split:option.splits) 2130 apply (rule corres_guard_imp[OF dcorres_returnOk]) 2131 apply (simp|wp)+ 2132 done 2133 2134lemma unat_pd_bits_less_4096_helper[simp]: 2135 "\<And>x. unat (x && mask pd_bits >> 2 :: word32) < 4096" 2136 apply (rule order_less_le_trans[where y="2^12"]) 2137 apply (rule unat_less_power[rotated]) 2138 apply (rule shiftr_less_t2n) 2139 apply (rule order_less_le_trans, rule and_mask_less') 2140 apply (simp_all add: pd_bits_def pageBits_def word_bits_conv) 2141 done 2142 2143lemma pd_at_cdl_pd_at: 2144 "\<lbrakk>valid_idle s ; ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; 2145 kheap s (ptr && ~~ mask pd_bits) = Some (ArchObj (arch_kernel_obj.PageDirectory fun))\<rbrakk> 2146 \<Longrightarrow> opt_cap (transform_pd_slot_ref ptr) (transform s) = 2147 Some (transform_pde (fun (of_nat (unat (ptr && mask pd_bits >> 2)))))" 2148 apply (clarsimp simp:opt_cap_def transform_pd_slot_ref_def transform_def 2149 slots_of_def opt_object_def transform_objects_def pred_tcb_def2 2150 valid_idle_def restrict_map_def object_slots_def 2151 transform_page_directory_contents_def unat_map_def 2152 dest!:get_tcb_SomeD split:option.splits) 2153 apply (simp add: below_kernel_base) 2154 apply (auto simp:transform_page_directory_contents_def unat_map_def) 2155 done 2156 2157lemma dcorres_get_pde_helper: 2158 "ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots 2159 \<Longrightarrow> dcorres (\<lambda>r r'. r = transform_pde r') \<top> valid_idle 2160 (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)" 2161 apply (simp add:cdl_get_pde_def 2162 get_pde_def gets_def gets_the_def 2163 get_pd_def get_object_def bind_assoc) 2164 apply (rule dcorres_absorb_get_l) 2165 apply (rule dcorres_absorb_get_r) 2166 apply (clarsimp simp:assert_def assert_opt_def 2167 corres_free_fail 2168 split:Structures_A.kernel_object.splits 2169 arch_kernel_obj.splits) 2170 apply (drule(2) pd_at_cdl_pd_at) 2171 apply (simp add:ucast_nat_def) 2172 done 2173 2174lemma dcorres_get_pde: 2175 "dcorres (\<lambda>r r'. r = transform_pde r') \<top> 2176 (valid_idle and K (ucast (ptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) 2177 (cdl_get_pde (transform_pd_slot_ref ptr)) (get_pde ptr)" 2178 apply (rule corres_guard_imp[OF corres_gen_asm2]) 2179 apply (rule dcorres_get_pde_helper) 2180 apply simp+ 2181 done 2182 2183lemma PPtrPAddr: 2184 "(addrFromPPtr w = v) = (ptrFromPAddr v = w)" 2185 by (auto simp:addrFromPPtr_def ptrFromPAddr_def) 2186 2187lemma dcorres_page_table_mapped: 2188 "b < kernel_base 2189 \<Longrightarrow> dcorres (\<lambda>r r'. r = option_map (\<lambda>x. cdl_lookup_pd_slot x b) r') 2190 \<top> (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) 2191 (cdl_page_table_mapped (transform_asid a, b) w) 2192 (page_table_mapped a b w)" 2193 apply (simp add:cdl_page_table_mapped_def page_table_mapped_def 2194 dcorres_lookup_pd_slot) 2195 apply (rule corres_guard_imp[OF corres_split_catch 2196 [where f = dc and E = dc and E' =dc]]) 2197 apply simp 2198 apply (rule corres_splitEE[OF _ dcorres_find_pd_for_asid]) 2199 apply (rule_tac F =" is_aligned pda 14" in corres_gen_asm2) 2200 apply (clarsimp simp:liftE_bindE dcorres_lookup_pd_slot) 2201 apply (rule corres_split[OF _ dcorres_get_pde]) 2202 apply (case_tac rv') 2203 apply (simp add:transform_pde_def) 2204 apply (rule dcorres_returnOk,simp) 2205 apply (simp add:transform_pde_def PPtrPAddr) 2206 apply (intro conjI impI) 2207 apply (rule dcorres_returnOk,simp) 2208 apply (rule dcorres_returnOk,simp) 2209 apply (simp add:transform_pde_def) 2210 apply (rule dcorres_returnOk,simp) 2211 apply (simp add:transform_pde_def) 2212 apply (rule dcorres_returnOk,simp) 2213 apply wp+ 2214 apply (rule hoare_post_imp_R[OF find_pd_for_asid_aligned_pd]) 2215 apply simp 2216 apply (erule less_kernel_base_mapping_slots) 2217 apply (simp add:pd_bits_def pageBits_def) 2218 apply wp 2219 apply ((simp add:dc_def,rule hoareE_TrueI[where P = \<top>])|wp)+ 2220 apply simp+ 2221 apply fastforce 2222 done 2223 2224lemma lookup_pd_slot_aligned_simp: 2225 "is_aligned pd pd_bits 2226 \<Longrightarrow> lookup_pd_slot pd vptr && mask pd_bits >> 2 = vptr >> 20" 2227 by (simp add:lookup_pd_slot_def mask_add_aligned 2228 shiftr_shiftl_mask_pd_bits vptr_shifting_3_ways) 2229 2230 2231lemma dcorres_unmap_page_table_store_pde: 2232 "dcorres dc \<top> ((\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)) 2233 and valid_idle and K (is_aligned pd 14 \<and> vptr < kernel_base) 2234 and pd_pt_relation (lookup_pd_slot pd vptr && ~~ mask pd_bits) pt_id (lookup_pd_slot pd vptr) ) 2235 (delete_cap_simple (cdl_lookup_pd_slot pd vptr)) 2236 (store_pde (lookup_pd_slot pd vptr) ARM_A.pde.InvalidPDE)" 2237 apply (rule corres_guard_imp) 2238 apply (rule corres_gen_asm2) 2239 apply (subst dcorres_lookup_pd_slot,assumption) 2240 apply (simp add:store_pde_def) 2241 apply (rule corres_symb_exec_r) 2242 apply (simp add:transform_pd_slot_ref_def) 2243 apply (rule corres_gen_asm2) 2244 apply (rule dcorres_delete_cap_simple_set_pde[where oid = pt_id]) 2245 apply assumption 2246 apply (wp|simp)+ 2247 apply (rule impI) 2248 apply (rule less_kernel_base_mapping_slots) 2249 apply (simp add: pd_bits_def pageBits_def)+ 2250 done 2251 2252lemma dcorres_option: 2253 "\<lbrakk> x = None \<Longrightarrow> dcorres sr T P g (C None); 2254 \<And>z. x = Some z \<Longrightarrow> dcorres sr T (Q z) g (C (Some z))\<rbrakk> \<Longrightarrow> 2255 dcorres sr T (\<lambda>s. case x of None \<Rightarrow> P s | Some z \<Rightarrow> Q z s) g (C x)" 2256 by (case_tac x ,auto) 2257 2258lemma dcorres_unmap_page_table: 2259 "\<lbrakk>a \<le> mask asid_bits ; b < kernel_base ; vmsz_aligned b ARMSection\<rbrakk> 2260 \<Longrightarrow> dcorres dc \<top> (invs and valid_cap (cap.ArchObjectCap (arch_cap.PageTableCap w (Some (a, b))))) 2261 (PageTableUnmap_D.unmap_page_table (transform_asid a,b) w) 2262 (ARM_A.unmap_page_table a b w)" 2263 apply (simp add: unmap_page_table_def PageTableUnmap_D.unmap_page_table_def) 2264 apply (rule corres_guard_imp) 2265 apply (rule corres_split[OF _ dcorres_page_table_mapped]) 2266 apply (rule dcorres_option[where P = \<top>]) 2267 apply simp 2268 apply (simp add: dc_def[symmetric]) 2269 apply (rule corres_dummy_return_l) 2270 apply (rule corres_split[where r'=dc]) 2271 apply clarify 2272 apply (rule corres_dummy_return_l) 2273 apply (rule corres_split[where r'=dc]) 2274 apply (rule dcorres_flush_table) 2275 apply (clarsimp) 2276 apply (rule dcorres_machine_op_noop) 2277 apply wp+ 2278 apply (rule dcorres_unmap_page_table_store_pde) 2279 apply (wp|simp)+ 2280 apply (wp hoare_post_Some_conj) 2281 apply (wp page_table_mapped_wp)[1] 2282 apply (wp hoare_post_Some_conj) 2283 apply (wp page_table_mapped_wp)[1] 2284 apply (wp hoare_post_Some_conj) 2285 apply (wp page_table_mapped_wp)[1] 2286 apply (wp pd_pt_relation_page_table_mapped_wp) 2287 apply simp 2288 apply (clarsimp simp:invs_psp_aligned invs_vspace_objs 2289 invs_mdb_cte[unfolded swp_def] invs_valid_idle 2290 valid_cap_def pd_bits_def pageBits_def) 2291 done 2292 2293lemma imp_strength: 2294 "(A \<and> (B\<longrightarrow>C)) \<longrightarrow> (B \<longrightarrow> (A\<and>C))" 2295 by clarsimp 2296 2297lemma cleanCacheRange_PoU_underlying_memory[wp]: 2298 "\<lbrace>\<lambda>ms. underlying_memory ms = m\<rbrace> 2299 cleanCacheRange_PoU a b c 2300 \<lbrace>\<lambda>rv ms. underlying_memory ms = m\<rbrace>" 2301 apply (clarsimp simp: cleanCacheRange_PoU_def, wp) 2302done 2303 2304lemma valid_pde_pt_at: 2305 "\<lbrakk>valid_pde (ARM_A.pde.PageTablePDE word1 se word2) s \<and> pspace_aligned s\<rbrakk> 2306 \<Longrightarrow> (ptrFromPAddr word1, unat ((vaddr >> 12) && 0xFF)) = 2307 transform_pt_slot_ref (ptrFromPAddr word1 + ((vaddr >> 12) && 0xFF << 2))" 2308 apply (clarsimp simp :transform_pt_slot_ref_def ) 2309 apply (drule(1) pt_aligned) 2310 apply (simp add:vaddr_segment_nonsense3 2311 vaddr_segment_nonsense4) 2312 apply (subst shiftl_shiftr_id) 2313 apply simp 2314 apply (rule le_less_trans[OF word_and_le1]) 2315 apply simp 2316 apply simp 2317 done 2318 2319lemma dcorres_lookup_pt_slot: 2320 "dcorres (dc \<oplus> (\<lambda>r r'. r = transform_pt_slot_ref r')) \<top> 2321 (valid_vspace_objs and \<exists>\<rhd> (lookup_pd_slot v a && ~~ mask pd_bits) and pspace_aligned 2322 and valid_idle and K(is_aligned v pd_bits) 2323 and K (ucast (lookup_pd_slot v a && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) 2324 (cdl_lookup_pt_slot v a) 2325 (lookup_pt_slot v a)" 2326 apply (simp add:cdl_lookup_pt_slot_def lookup_pt_slot_def) 2327 apply (rule corres_guard_imp) 2328 apply (rule_tac F =" is_aligned v 14" in corres_gen_asm2) 2329 apply (clarsimp simp:dcorres_lookup_pd_slot) 2330 apply (rule corres_splitEE[OF _ 2331 corres_liftE_rel_sum[THEN iffD2,OF dcorres_get_pde] ]) 2332 apply (case_tac rv') 2333 prefer 2 2334 apply (simp add:transform_pde_def) 2335 apply (rule corres_returnOk) 2336 apply (erule valid_pde_pt_at) 2337 apply (simp add:transform_pde_def)+ 2338 apply (rule hoare_TrueI) 2339 apply (wp|simp)+ 2340 apply (simp add:pd_bits_def pageBits_def) 2341 done 2342 2343lemma find_pd_for_asid_kernel_mapping_help: 2344 "\<lbrace>pspace_aligned and valid_vspace_objs and K (v<kernel_base) \<rbrace> find_pd_for_asid a 2345 \<lbrace>\<lambda>rv s. ucast (lookup_pd_slot rv v && mask pd_bits >> 2) \<notin> kernel_mapping_slots \<rbrace>,-" 2346 apply (rule hoare_gen_asmE) 2347 apply (rule hoare_post_imp_R) 2348 apply (rule find_pd_for_asid_aligned_pd_bits) 2349 apply simp 2350 apply (rule less_kernel_base_mapping_slots) 2351 apply simp+ 2352 done 2353 2354lemma dcorres_might_throw: 2355 "\<lbrakk>\<And>s. \<lbrace>(=) s\<rbrace> b \<lbrace>\<lambda>r. (=) s\<rbrace>\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) \<top> \<top> might_throw (throw_on_false a b)" 2356 apply (simp add: liftE_bindE unlessE_def 2357 might_throw_def throw_on_false_def split:if_splits) 2358 apply (rule corres_symb_exec_r) 2359 apply (clarsimp split:if_splits) 2360 apply (intro conjI impI) 2361 apply (rule corres_alternate1) 2362 apply (simp add:returnOk_def) 2363 apply (rule corres_alternate2) 2364 apply simp 2365 apply (wp hoare_TrueI) 2366 apply simp 2367 apply simp 2368 done 2369 2370lemma corres_dummy_returnOk_l: 2371 "dcorres cr P P' (f >>=E returnOk) g \<Longrightarrow> dcorres cr P P' f g" 2372 by (simp add:liftE_def) 2373 2374lemma dcorres_unmap_page: 2375 notes swp_apply[simp del] 2376 shows "dcorres dc \<top> (invs and valid_pdpt_objs and 2377 valid_cap (cap.ArchObjectCap (arch_cap.PageCap dev pg fun vmpage_size (Some (a, v))))) 2378 (PageTableUnmap_D.unmap_page (transform_asid a,v) pg (pageBitsForSize vmpage_size)) 2379 (ARM_A.unmap_page vmpage_size a v pg)" 2380 apply (rule dcorres_expand_pfx) 2381 apply (clarsimp simp:valid_cap_def) 2382 apply (case_tac vmpage_size) 2383\<comment> \<open>ARMSmallPage\<close> 2384 apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton 2385 PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) 2386 apply (rule corres_guard_imp) 2387 apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'" 2388 in corres_split_catch [where f = dc and E = dc and E' =dc]) 2389 apply simp 2390 apply (rule corres_guard_imp) 2391 apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) 2392 apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib 2393 pageBitsForSize_def bindE_assoc mapM_x_singleton) 2394 apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot]) 2395 apply (rule corres_splitEE[OF _ dcorres_might_throw]) 2396 apply (rule corres_dummy_returnOk_l) 2397 apply (rule corres_splitEE) 2398prefer 2 2399 apply (simp add:transform_pt_slot_ref_def) 2400 apply (rule dcorres_store_invalid_pte[where pg_id = pg]) 2401 apply (simp add:liftE_distrib[symmetric] returnOk_liftE) 2402 apply (rule dcorres_symb_exec_r) 2403 apply (rule dcorres_flush_page) 2404 apply (wp do_machine_op_wp | clarsimp)+ 2405 apply (simp add: imp_conjR) 2406 apply ((wp check_mapping_pptr_pt_relation | wp_once hoare_drop_imps)+)[1] 2407 apply (simp | wp lookup_pt_slot_inv)+ 2408 apply (simp add: dc_def 2409 | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help 2410 | rule conjI | clarify)+ 2411 2412\<comment> \<open>ARMLargePage\<close> 2413 2414 apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton 2415 PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) 2416 apply (rule corres_guard_imp) 2417 apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'" 2418 in corres_split_catch [where f = dc and E = dc and E' =dc]) 2419 apply simp 2420 apply (rule corres_guard_imp) 2421 apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) 2422 apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib 2423 pageBitsForSize_def bindE_assoc mapM_x_singleton) 2424 apply (rule corres_splitEE[OF _ dcorres_lookup_pt_slot]) 2425 apply (rule corres_splitEE[OF _ dcorres_might_throw]) 2426 apply (rule dcorres_symb_exec_rE) 2427 apply (rule corres_dummy_returnOk_l) 2428 apply (rule corres_splitEE) 2429prefer 2 2430 apply simp 2431 apply (rule_tac F = "is_aligned xa 6" in corres_gen_asm2) 2432 apply (erule dcorres_unmap_large_page[where pg_id = pg]) 2433 apply (simp add:liftE_distrib[symmetric] returnOk_liftE) 2434 apply (rule dcorres_symb_exec_r) 2435 apply (rule dcorres_flush_page[unfolded dc_def]) 2436 apply (wp do_machine_op_wp | clarsimp)+ 2437 apply (simp add: imp_conjR is_aligned_mask) 2438 apply (rule hoare_vcg_conj_lift) 2439 apply (wp hoare_drop_imps)[1] 2440 apply (rule hoare_vcg_conj_lift) 2441 apply (wp hoare_drop_imps)[1] 2442 apply (rule hoare_strengthen_post[OF check_mapping_pptr_pt_relation]) 2443 apply fastforce 2444 apply (simp | wp lookup_pt_slot_inv)+ 2445 apply (simp add: dc_def 2446 | wp lookup_pt_slot_inv hoare_drop_imps 2447 find_pd_for_asid_kernel_mapping_help 2448 | safe)+ 2449 2450\<comment> \<open>Section\<close> 2451 apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton 2452 PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) 2453 apply (rule corres_guard_imp) 2454 apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'" 2455 in corres_split_catch [where f = dc and E = dc and E' =dc]) 2456 apply simp 2457 apply (rule corres_guard_imp) 2458 apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) 2459 apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib 2460 pageBitsForSize_def bindE_assoc mapM_x_singleton) 2461 apply (rule corres_splitEE[OF _ dcorres_might_throw]) 2462 apply (rule corres_dummy_returnOk_l) 2463 apply (rule corres_splitEE) 2464prefer 2 2465 apply simp 2466 apply (rule dcorres_delete_cap_simple_section[where oid = pg]) 2467 apply (simp add:liftE_distrib[symmetric] returnOk_liftE) 2468 apply (rule dcorres_symb_exec_r) 2469 apply (rule dcorres_flush_page[unfolded dc_def]) 2470 apply (wp do_machine_op_wp | clarsimp)+ 2471 apply (simp add: imp_conjR) 2472 apply ((wp check_mapping_pptr_section_relation | wp_once hoare_drop_imps)+)[1] 2473 apply (simp | wp lookup_pt_slot_inv)+ 2474 apply (simp add: dc_def 2475 | wp lookup_pt_slot_inv find_pd_for_asid_kernel_mapping_help 2476 | safe)+ 2477 2478\<comment> \<open>SuperSection\<close> 2479 2480 apply (simp add:ARM_A.unmap_page_def bindE_assoc mapM_x_singleton 2481 PageTableUnmap_D.unmap_page_def cdl_page_mapping_entries_def) 2482 apply (rule corres_guard_imp) 2483 apply (rule_tac P = "\<lambda>x. x = transform s'" and P' = "(=) s'" 2484 in corres_split_catch [where f = dc and E = dc and E' =dc]) 2485 apply simp 2486 apply (rule corres_guard_imp) 2487 apply (rule_tac corres_splitEE[OF _ dcorres_find_pd_for_asid,simplified]) 2488 apply (simp_all add:cdl_page_mapping_entries_def liftE_distrib 2489 pageBitsForSize_def bindE_assoc mapM_x_singleton) 2490 apply (rule corres_splitEE[OF _ dcorres_might_throw]) 2491 apply (rule dcorres_symb_exec_rE) 2492 apply (rule corres_dummy_returnOk_l) 2493 apply (rule corres_splitEE) 2494prefer 2 2495 apply simp 2496 apply (rule_tac F = "is_aligned pda 14" in corres_gen_asm2) 2497 apply (erule(2) dcorres_unmap_large_section[where pg_id = pg]) 2498 apply (simp add:liftE_distrib[symmetric] returnOk_liftE) 2499 apply (rule dcorres_symb_exec_r) 2500 apply (rule dcorres_flush_page[unfolded dc_def]) 2501 apply (wp do_machine_op_wp | clarsimp)+ 2502 apply (simp add: imp_conjR is_aligned_mask) 2503 apply (rule hoare_vcg_conj_lift) 2504 apply (wp hoare_drop_imps)[1] 2505 apply (rule hoare_vcg_conj_lift) 2506 apply (wp hoare_drop_imps)[1] 2507 apply (rule hoare_vcg_conj_lift) 2508 apply (rule hoare_strengthen_post[OF check_mapping_pptr_super_section_relation]) 2509 apply clarsimp 2510 apply (simp add:is_aligned_mask[symmetric] dc_def 2511 | wp lookup_pt_slot_inv hoare_drop_imps 2512 find_pd_for_asid_kernel_mapping_help 2513 | safe)+ 2514done 2515 2516 2517lemma dcorres_delete_asid_none: 2518 "dcorres dc \<top> \<top> (CSpace_D.delete_asid x word) (return ())" 2519 apply (clarsimp simp:CSpace_D.delete_asid_def) 2520 apply (rule corres_alternate2) 2521 apply clarsimp 2522 done 2523 2524lemma asid_table_transform: 2525 "cdl_asid_table (transform s) slot = 2526 unat_map (Some \<circ> transform_asid_table_entry \<circ> arm_asid_table (arch_state s)) slot" 2527 apply (simp add:transform_def transform_asid_table_def transform_asid_table_entry_def) 2528 done 2529 2530lemma dcorres_delete_asid: 2531 "dcorres dc \<top> (valid_idle) 2532 (CSpace_D.delete_asid (transform_asid asid) word) 2533 (ARM_A.delete_asid asid word)" 2534 apply (clarsimp simp:CSpace_D.delete_asid_def ARM_A.delete_asid_def) 2535 apply (clarsimp simp:gets_def) 2536 apply (rule dcorres_absorb_get_r) 2537 apply (clarsimp simp:when_def split:option.splits) 2538 apply (rule conjI) 2539 apply clarsimp 2540 apply (rule corres_alternate2) 2541 apply clarsimp 2542 apply clarsimp 2543 apply (rule dcorres_symb_exec_r_strong) 2544 apply clarsimp 2545 apply (rule conjI) 2546 apply clarsimp 2547 apply (rule corres_alternate1) 2548 apply (rule dcorres_absorb_get_l) 2549 apply (drule_tac s="transform s'" in sym) 2550 apply (clarsimp simp:when_def asid_table_transform transform_asid_def 2551 transform_asid_table_entry_def 2552 split:option.splits if_splits) 2553 apply (rule dcorres_symb_exec_r_strong) 2554 apply (rule dcorres_symb_exec_r_strong) 2555 apply (rule corres_guard_imp) 2556 apply (rule corres_dummy_return_l) 2557 apply (rule corres_split[OF corres_trivial,where r'=dc]) 2558 apply (rule dcorres_symb_exec_r[OF dcorres_set_vm_root]) 2559 apply wp+ 2560 apply (rule dcorres_set_asid_pool) 2561 apply simp 2562 apply (clarsimp simp:transform_asid_def) 2563 apply (clarsimp simp:transform_asid_pool_entry_def) 2564 apply (wp | clarsimp)+ 2565 apply simp 2566 apply (wp | clarsimp)+ 2567 apply (rule hoare_pre, wp) 2568 apply simp 2569 apply (wp | clarsimp)+ 2570 apply (rule corres_alternate2) 2571 apply simp 2572 apply (wp | clarsimp)+ 2573done 2574 2575lemma thread_in_thread_cap_not_idle: 2576 "\<lbrakk>valid_global_refs s;cte_wp_at ((=) (cap.ThreadCap ptr)) slot s\<rbrakk> 2577 \<Longrightarrow> not_idle_thread ptr s" 2578 apply (rule ccontr) 2579 apply (clarsimp simp:valid_cap_def valid_global_refs_def valid_refs_def) 2580 apply (case_tac slot) 2581 apply (drule_tac x = a in spec) 2582 apply (drule_tac x = b in spec) 2583 apply (clarsimp simp:cte_wp_at_def not_idle_thread_def) 2584 apply (simp add:cap_range_def global_refs_def) 2585done 2586 2587lemma set_cap_set_thread_state_inactive: 2588 "dcorres dc \<top> (not_idle_thread thread and valid_etcbs) 2589 (KHeap_D.set_cap (thread, tcb_pending_op_slot) cdl_cap.NullCap) 2590 (set_thread_state thread Structures_A.thread_state.Inactive)" 2591 apply (clarsimp simp:set_thread_state_def) 2592 apply (rule dcorres_absorb_gets_the) 2593 apply (rule corres_guard_imp) 2594 apply (rule dcorres_rhs_noop_below_True[OF set_thread_state_ext_dcorres]) 2595 apply (rule set_pending_cap_corres) 2596 apply simp 2597 apply (clarsimp dest!:get_tcb_SomeD 2598 simp:obj_at_def infer_tcb_pending_op_def) 2599 done 2600 2601lemma prepare_thread_delete_dcorres: "dcorres dc P P' (CSpace_D.prepare_thread_delete t) (prepare_thread_delete t)" 2602 apply (clarsimp simp: CSpace_D.prepare_thread_delete_def prepare_thread_delete_def) 2603 done 2604 2605lemma dcorres_finalise_cap: 2606 "cdlcap = transform_cap cap \<Longrightarrow> 2607 dcorres (\<lambda>r r'. fst r = transform_cap (fst r')) 2608 \<top> (invs and valid_cap cap and valid_pdpt_objs and cte_wp_at ((=) cap) slot and valid_etcbs) 2609 (CSpace_D.finalise_cap cdlcap final) 2610 (CSpace_A.finalise_cap cap final)" 2611 apply (case_tac cap) 2612 apply (simp_all add: when_def) 2613 apply clarsimp 2614 apply (rule corres_rel_imp) 2615 apply (rule corres_guard_imp[OF dcorres_cancel_all_ipc]) 2616 apply (clarsimp simp:invs_def valid_state_def)+ 2617 apply (rule corres_rel_imp) 2618 apply (rule corres_guard_imp) 2619 apply (rule corres_split[OF dcorres_cancel_all_signals dcorres_unbind_maybe_notification]) 2620 apply (wp unbind_maybe_notification_valid_etcbs | simp | wpc)+ 2621 apply ((clarsimp simp:invs_def valid_state_def)+)[2] 2622 apply (simp add:IpcCancel_A.suspend_def bind_assoc) 2623 apply clarsimp 2624 apply (rule corres_guard_imp) 2625 apply (rule corres_split[OF _ dcorres_unbind_notification]) 2626 apply (rule corres_split[OF _ finalise_cancel_ipc]) 2627 apply (rule corres_split) 2628 unfolding K_bind_def 2629 apply (rule dcorres_rhs_noop_above_True[OF tcb_sched_action_dcorres[where P=\<top> and P'=\<top>]]) 2630 apply (rule corres_split'[OF prepare_thread_delete_dcorres]) 2631 apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]]) 2632 apply (clarsimp simp:transform_cap_def) 2633 apply wp+ 2634 apply (rule set_cap_set_thread_state_inactive) 2635 apply wp+ 2636 apply (simp add:not_idle_thread_def) 2637 apply (wp unbind_notification_invs | simp add: not_idle_thread_def)+ 2638 apply clarsimp 2639 apply (drule(1) thread_in_thread_cap_not_idle[OF invs_valid_global_refs]) 2640 apply (simp add:not_idle_thread_def) 2641 apply clarsimp 2642 apply (rule corres_guard_imp) 2643 apply (rule corres_split[OF _ dcorres_deleting_irq_handler]) 2644 apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]]) 2645 apply (clarsimp simp:transform_cap_def) 2646 apply (wp|clarsimp)+ 2647 apply (clarsimp simp:assert_def corres_free_fail) 2648 apply (rename_tac arch_cap) 2649 apply (case_tac arch_cap) 2650 apply (simp_all add: arch_finalise_cap_def split:arch_cap.split_asm) 2651 apply clarsimp 2652 \<comment> \<open>arch_cap.ASIDPoolCap\<close> 2653 apply (rule corres_guard_imp) 2654 apply (simp add:transform_asid_def) 2655 apply (rule corres_split[OF _ dcorres_delete_asid_pool]) 2656 apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]]) 2657 apply (clarsimp simp:transform_cap_def) 2658 apply (wp|clarsimp)+ 2659 apply (clarsimp split:option.splits | rule conjI)+ 2660 \<comment> \<open>arch_cap.PageCap\<close> 2661 apply (simp add:transform_mapping_def) 2662 apply (clarsimp simp:transform_mapping_def) 2663 apply (rule corres_guard_imp) 2664 apply (rule_tac corres_split[OF _ dcorres_unmap_page]) 2665 apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]]) 2666 apply (clarsimp simp:transform_cap_def) 2667 apply (wp | clarsimp )+ 2668 apply simp 2669 \<comment> \<open>arch_cap.PageTableCap\<close> 2670 apply (clarsimp simp:transform_mapping_def split:option.splits) 2671 apply (rule dcorres_expand_pfx) 2672 apply (rule corres_guard_imp) 2673 apply (rule corres_split[OF _ dcorres_unmap_page_table]) 2674 apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]]) 2675 apply (clarsimp simp:transform_cap_def) 2676 apply ((wp|clarsimp )+)[4] 2677 apply (rule iffD1[OF le_mask_iff_lt_2n,THEN iffD2],simp add:word_size asid_bits_def) 2678 apply (clarsimp simp:valid_cap_def cap_aligned_def )+ 2679 apply (simp add:vmsz_aligned_def) 2680 apply (wp|clarsimp)+ 2681 apply (rule conjI | clarsimp split:option.splits)+ 2682 apply (rule corres_guard_imp) 2683 apply (rule corres_split[OF _ dcorres_delete_asid]) 2684 apply (rule iffD2[OF corres_return[where P=\<top> and P'=\<top>]]) 2685 apply (clarsimp simp:transform_cap_def) 2686 apply (wp|clarsimp split:option.splits)+ 2687 done 2688 2689lemma dcorres_splits: 2690 "\<lbrakk> T a \<Longrightarrow> dcorres r P (Q a) f (g a); 2691 \<not> T a \<Longrightarrow> dcorres r P (Q' a) f (g a)\<rbrakk>\<Longrightarrow> 2692 dcorres r P ( (\<lambda>s. (T a) \<longrightarrow> (Q a s)) and (\<lambda>s. (\<not> (T a)) \<longrightarrow> (Q' a s)) ) f (g a)" 2693 apply (case_tac "T a") 2694 apply clarsimp+ 2695done 2696 2697lemma get_cap_weak_wp: 2698 "\<lbrace>cte_wp_at Q slot\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>rv s. Q rv\<rbrace>" 2699 by (clarsimp simp:valid_def cte_wp_at_def) 2700 2701definition remainder_cap :: "bool \<Rightarrow> cap \<Rightarrow> cap" 2702where "remainder_cap final c\<equiv> case c of 2703 cap.CNodeCap r bits g \<Rightarrow> if final then cap.Zombie r (Some bits) (2 ^ bits) else cap.NullCap 2704| cap.ThreadCap r \<Rightarrow> if final then cap.Zombie r None 5 else cap.NullCap 2705| cap.Zombie r b n \<Rightarrow> cap.Zombie r b n 2706| cap.ArchObjectCap a \<Rightarrow> cap.NullCap 2707| _ \<Rightarrow> cap.NullCap" 2708 2709lemma finalise_cap_remainder: 2710 "\<lbrace>\<top>\<rbrace>CSpace_A.finalise_cap cap final \<lbrace>\<lambda>r s. fst (r) = (remainder_cap final cap) \<rbrace>" 2711 apply (case_tac cap; simp add: remainder_cap_def) 2712 apply (wp|clarsimp)+ 2713 apply (fastforce simp:valid_def) 2714 apply (simp add: liftM_def |clarify)+ 2715 apply (wp|clarsimp|rule conjI)+ 2716 apply (simp add:arch_finalise_cap_def) 2717 apply (cases final) 2718 2719 apply (rename_tac arch_cap) 2720 2721 2722 apply (case_tac arch_cap) 2723 apply (simp_all) 2724 apply (wp|clarsimp)+ 2725 apply (simp_all split:option.splits) 2726 apply (wp | clarsimp | rule conjI)+ 2727 apply (rename_tac arch_cap) 2728 apply (case_tac arch_cap; simp) 2729 apply (wp|clarsimp split:option.splits | rule conjI)+ 2730 done 2731 2732lemma obj_ref_not_idle: 2733 "\<lbrakk>valid_objs s;valid_global_refs s;cte_at slot s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>cap. \<forall>x\<in>obj_refs cap. not_idle_thread x s) slot s" 2734 apply (simp add:valid_global_refs_def valid_refs_def) 2735 apply (case_tac slot) 2736 apply clarsimp 2737 apply (drule_tac x = a in spec) 2738 apply (drule_tac x = b in spec) 2739 apply (clarsimp simp:cte_wp_at_def not_idle_thread_def cap_range_def global_refs_def) 2740 done 2741 2742lemma singleton_set_eq: 2743 "\<lbrakk>x = {a}; b\<in> x\<rbrakk>\<Longrightarrow> b = a" 2744 by clarsimp 2745 2746lemma zombies_final_ccontr: 2747 "\<lbrakk>caps_of_state s p = Some cap; r \<in> obj_refs cap; is_zombie cap; zombies_final s; 2748 caps_of_state s p' = Some cap'\<rbrakk> 2749 \<Longrightarrow> r\<in> obj_refs cap' \<longrightarrow> is_zombie cap' \<and> p = p'" 2750 apply (rule ccontr) 2751 apply (case_tac p) 2752 apply (clarsimp simp:zombies_final_def) 2753 apply (drule_tac x = a in spec,drule_tac x = b in spec) 2754 apply (frule caps_of_state_cteD) 2755 apply (simp add:cte_wp_at_def) 2756 apply (clarsimp simp:IpcCancel_A.is_final_cap'_def) 2757 apply (frule_tac a = "(aa,ba)" and b = p' in singleton_set_eq) 2758 apply (clarsimp) 2759 apply (drule_tac a = "(aa,ba)" and b = p' in singleton_set_eq) 2760 apply (clarsimp dest!:caps_of_state_cteD simp:cte_wp_at_def) 2761 apply (drule IntI) 2762 apply (simp add: gen_obj_refs_Int)+ 2763 apply (drule_tac a = "(aa,ba)" and b = "(a,b)" in singleton_set_eq) 2764 apply clarsimp 2765 apply clarsimp 2766done 2767 2768lemma zombie_cap_has_all: 2769 "\<lbrakk>valid_objs s;if_unsafe_then_cap s; zombies_final s;valid_global_refs s; 2770 caps_of_state s slot = Some (cap.Zombie w option n); 2771 (w,x) \<notin> cte_refs (cap.Zombie w option n) f \<rbrakk> 2772 \<Longrightarrow> caps_of_state s (w,x) = None \<or> caps_of_state s (w,x) = Some cap.NullCap" 2773 apply (clarsimp simp:if_unsafe_then_cap_def valid_cap_def split:option.splits) 2774 apply (drule_tac x = w in spec,drule_tac x = x in spec) 2775 apply (rule ccontr) 2776 apply clarsimp 2777 apply (clarsimp simp:ex_cte_cap_wp_to_def appropriate_cte_cap_def) 2778 apply (drule iffD1[OF cte_wp_at_caps_of_state]) 2779 apply clarsimp 2780 apply (frule_tac p = slot and p'="(a,b)" in zombies_final_ccontr) 2781 apply simp+ 2782 apply (simp add:is_zombie_def) 2783 apply simp+ 2784 apply (case_tac cap; simp) 2785 apply (case_tac y; simp) 2786 apply (frule_tac p = "(a,b)" in caps_of_state_valid_cap) 2787 apply simp 2788 apply (frule_tac p = slot in caps_of_state_valid_cap) 2789 apply simp 2790 apply (rename_tac word w2 w3 rights) 2791 apply (clarsimp simp:valid_cap_def tcb_at_def dest!:get_tcb_SomeD) 2792 apply (drule_tac p = "(interrupt_irq_node s word,[])" in caps_of_state_cteD) 2793 apply (clarsimp simp:cte_wp_at_cases) 2794 apply (clarsimp simp:obj_at_def tcb_cap_cases_def tcb_cnode_index_def to_bl_1 split:if_splits) 2795 apply (drule valid_globals_irq_node[OF _ caps_of_state_cteD]) 2796 apply simp 2797 apply (fastforce simp:cap_range_def) 2798 done 2799 2800lemma monadic_trancl_steps: 2801 "monadic_rewrite False False \<top> 2802 (monadic_trancl f x) 2803 (do y \<leftarrow> monadic_trancl f x; 2804 monadic_trancl f y od)" 2805 apply (simp add: monadic_rewrite_def monadic_trancl_def 2806 bind_def split_def monadic_option_dest_def) 2807 apply (safe, simp_all) 2808 done 2809 2810lemma monadic_trancl_f: 2811 "monadic_rewrite False False \<top> 2812 (monadic_trancl f x) (f x)" 2813 apply (simp add: monadic_rewrite_def monadic_trancl_def 2814 bind_def split_def monadic_option_dest_def) 2815 apply (safe, simp_all) 2816 apply (simp add: r_into_rtrancl monadic_rel_optionation_form_def)+ 2817 done 2818 2819lemma monadic_trancl_step: 2820 "monadic_rewrite False False \<top> 2821 (monadic_trancl f x) (do y \<leftarrow> f x; monadic_trancl f y od)" 2822 apply (rule monadic_rewrite_imp) 2823 apply (rule monadic_rewrite_trans) 2824 apply (rule monadic_trancl_steps) 2825 apply (rule monadic_rewrite_bind_head) 2826 apply (rule monadic_trancl_f) 2827 apply simp 2828 done 2829 2830lemma monadic_trancl_return: 2831 "monadic_rewrite False False \<top> 2832 (monadic_trancl f x) (return x)" 2833 by (simp add: monadic_rewrite_def monadic_trancl_def 2834 monadic_option_dest_def return_def) 2835 2836lemma monadic_rewrite_if_lhs: 2837 "\<lbrakk> P \<Longrightarrow> monadic_rewrite F E Q b a; 2838 \<not> P \<Longrightarrow> monadic_rewrite F E R c a\<rbrakk> 2839 \<Longrightarrow> monadic_rewrite F E (\<lambda>s. (P \<longrightarrow> Q s) \<and> (\<not> P \<longrightarrow> R s)) 2840 (if P then b else c) a" 2841 by (cases P, simp_all) 2842 2843lemma monadic_rewrite_case_option: 2844 "\<lbrakk> \<And>y. x = Some y \<Longrightarrow> monadic_rewrite E F (P x) f (g y); 2845 x = None \<Longrightarrow> monadic_rewrite E F Q f h \<rbrakk> 2846 \<Longrightarrow> monadic_rewrite E F (\<lambda>s. (\<forall>y. x = Some y \<longrightarrow> P x s) \<and> (x = None \<longrightarrow> Q s)) 2847 f (case x of Some y \<Rightarrow> g y | None \<Rightarrow> h)" 2848 by (cases x, simp_all) 2849 2850lemma rtrancl_idem: 2851 assumes S: "S `` T = T" 2852 shows "S\<^sup>* `` T = T" 2853proof - 2854 note P = eqset_imp_iff[OF S, THEN iffD1, OF ImageI] 2855 have Q: "\<And>x y. (x, y) \<in> S\<^sup>* \<Longrightarrow> x \<in> T \<longrightarrow> y \<in> T" 2856 by (erule rtrancl.induct, auto dest: P) 2857 2858 thus ?thesis 2859 by auto 2860qed 2861 2862lemma monadic_trancl_lift_Inl: 2863 "monadic_trancl (lift f) (Inl err) = throwError err" 2864 apply (rule ext) 2865 apply (simp add: throwError_def return_def monadic_trancl_def) 2866 apply (subst rtrancl_idem) 2867 apply (auto simp: monadic_rel_optionation_form_def lift_def 2868 throwError_def return_def monadic_option_dest_def) 2869 done 2870 2871lemma monadic_trancl_preemptible_steps: 2872 "monadic_rewrite False False \<top> 2873 (monadic_trancl_preemptible f x) 2874 (doE y \<leftarrow> monadic_trancl_preemptible f x; 2875 monadic_trancl_preemptible f y odE)" 2876 apply (simp add: monadic_trancl_preemptible_def) 2877 apply (rule monadic_rewrite_imp) 2878 apply (rule monadic_rewrite_trans) 2879 apply (rule monadic_trancl_steps) 2880 apply (simp add: bindE_def) 2881 apply (rule_tac Q="\<top>\<top>" in monadic_rewrite_bind_tail) 2882 apply (case_tac x) 2883 apply (simp add: lift_def monadic_trancl_lift_Inl) 2884 apply (rule monadic_rewrite_refl) 2885 apply (simp add: lift_def) 2886 apply (rule monadic_rewrite_refl) 2887 apply (wp | simp)+ 2888 done 2889 2890lemma monadic_trancl_preemptible_f: 2891 "monadic_rewrite False False (\<lambda>_. True) 2892 (monadic_trancl_preemptible f x) (f x)" 2893 apply (simp add: monadic_trancl_preemptible_def) 2894 apply (rule monadic_rewrite_imp) 2895 apply (rule monadic_rewrite_trans) 2896 apply (rule monadic_trancl_f) 2897 apply (simp add: lift_def) 2898 apply (rule monadic_rewrite_refl) 2899 apply simp 2900 done 2901 2902lemmas monadic_rewrite_bindE_head 2903 = monadic_rewrite_bindE[OF _ monadic_rewrite_refl hoare_vcg_propE_R] 2904 2905lemma monadic_trancl_preemptible_step: 2906 "monadic_rewrite False False \<top> 2907 (monadic_trancl_preemptible f x) 2908 (doE y \<leftarrow> f x; 2909 monadic_trancl_preemptible f y odE)" 2910 apply (rule monadic_rewrite_imp) 2911 apply (rule monadic_rewrite_trans) 2912 apply (rule monadic_trancl_preemptible_steps) 2913 apply (rule monadic_rewrite_bindE_head) 2914 apply (rule monadic_trancl_preemptible_f) 2915 apply simp 2916 done 2917 2918lemma monadic_trancl_preemptible_return: 2919 "monadic_rewrite False False (\<lambda>_. True) 2920 (monadic_trancl_preemptible f x) (returnOk x)" 2921 apply (simp add: monadic_trancl_preemptible_def) 2922 apply (rule monadic_rewrite_imp) 2923 apply (rule monadic_rewrite_trans) 2924 apply (rule monadic_trancl_return) 2925 apply (simp add: returnOk_def) 2926 apply (rule monadic_rewrite_refl) 2927 apply simp 2928 done 2929 2930lemma monadic_rewrite_corres2: 2931 "\<lbrakk> monadic_rewrite False E Q a a'; 2932 corres_underlying R False F r P P' a' c \<rbrakk> 2933 \<Longrightarrow> corres_underlying R False F r (P and Q) P' a c" 2934 apply (simp add: corres_underlying_def monadic_rewrite_def) 2935 apply (erule ballEI, clarsimp) 2936 apply (drule(1) bspec, clarsimp) 2937 apply (drule spec, drule(1) mp) 2938 apply fastforce 2939 done 2940 2941lemma dcorres_get_cap_symb_exec: 2942 "\<lbrakk> \<And>cap. dcorres r (P cap) (P' cap) f (g cap) \<rbrakk> 2943 \<Longrightarrow> dcorres r 2944 (\<lambda>s. \<forall>cap. opt_cap (transform_cslot_ptr slot) s = Some (transform_cap cap) \<longrightarrow> P cap s) 2945 (\<lambda>s. fst slot \<noteq> idle_thread s \<and> (\<forall>cap. caps_of_state s slot = Some cap \<longrightarrow> P' cap s) \<and> valid_etcbs s) 2946 f (do cap \<leftarrow> get_cap slot; g cap od)" 2947 apply (rule corres_symb_exec_r[OF _ get_cap_sp]) 2948 apply (rule stronger_corres_guard_imp, assumption) 2949 apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap) 2950 apply (clarsimp simp: cte_wp_at_caps_of_state) 2951 apply (wp | simp)+ 2952 done 2953 2954lemma set_cdt_modify: 2955 "set_cdt c = modify (\<lambda>s. s \<lparr> cdt := c \<rparr>)" 2956 by (simp add: set_cdt_def modify_def) 2957 2958lemma no_cdt_loop_mloop: 2959 "no_mloop m \<Longrightarrow> m x \<noteq> Some x" 2960 apply (rule notI) 2961 apply (simp add: no_mloop_def cdt_parent_rel_def del: split_paired_All) 2962 apply (drule_tac x=x in spec) 2963 apply (erule notE, rule r_into_trancl) 2964 apply (simp add: is_cdt_parent_def) 2965 done 2966 2967lemma set_cdt_list_modify: 2968 "set_cdt_list c = modify (\<lambda>s. s \<lparr> cdt_list := c \<rparr>)" 2969 by (simp add: set_cdt_list_def modify_def) 2970 2971lemma swap_cap_corres: 2972 "dcorres dc \<top> (valid_idle and valid_mdb and cte_at slot_a and cte_at slot_b 2973 and valid_etcbs and K (slot_a \<noteq> slot_b) 2974 and not_idle_thread (fst slot_a) 2975 and not_idle_thread (fst slot_b)) 2976 (swap_cap (transform_cap cap_a) (transform_cslot_ptr slot_a) 2977 (transform_cap cap_b) (transform_cslot_ptr slot_b)) 2978 (cap_swap cap_a slot_a cap_b slot_b)" 2979proof - 2980 note inj_on_insert[iff del] 2981 show ?thesis 2982 apply (simp add: swap_cap_def cap_swap_def) 2983 apply (rule corres_guard_imp) 2984 apply (rule corres_split_nor [OF _ set_cap_corres[OF refl refl]]) 2985 apply (rule corres_split_nor [OF _ set_cap_corres[OF refl refl]]) 2986 apply (simp add: swap_parents_def set_original_def 2987 set_cdt_modify gets_fold_into_modify bind_assoc 2988 cap_swap_ext_def update_cdt_list_def set_cdt_list_modify) 2989 apply (simp add: gets_fold_into_modify modify_modify Fun.swap_def o_def) 2990 apply (rule_tac P'="K (slot_a \<noteq> slot_b) and cte_at slot_a and cte_at slot_b 2991 and (\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s)) 2992 and no_mloop o cdt" 2993 and P=\<top> in corres_modify) 2994 2995 apply (clarsimp simp:transform_def transform_current_thread_def 2996 transform_asid_table_def transform_objects_def 2997 transform_cdt_def split del: if_split) 2998 apply (rule sym) 2999 apply (subgoal_tac "inj_on transform_cslot_ptr 3000 ({slot_a, slot_b} \<union> dom (cdt s') \<union> ran (cdt s')) 3001 \<and> cdt s' slot_a \<noteq> Some slot_a \<and> cdt s' slot_b \<noteq> Some slot_b") 3002 apply (elim conjE) 3003 apply (subst map_lift_over_upd, erule subset_inj_on) 3004 apply (safe elim!: ranE, simp_all split: if_split_asm, 3005 simp_all add: ranI)[1] 3006 apply (subst map_lift_over_upd, erule subset_inj_on) 3007 apply (safe elim!: ranE, simp_all split: if_split_asm, 3008 simp_all add: ranI)[1] 3009 apply (subst map_lift_over_if_eq_twice) 3010 apply (erule subset_inj_on, fastforce) 3011 apply (rule ext) 3012 apply (cases slot_a, cases slot_b) 3013 apply (simp split del: if_split) 3014 apply (intro if_cong[OF refl], 3015 simp_all add: map_lift_over_eq_Some inj_on_eq_iff[where f=transform_cslot_ptr] 3016 ranI domI)[1] 3017 apply (subst subset_inj_on, assumption, fastforce)+ 3018 prefer 2 3019 apply (subst subset_inj_on, assumption, fastforce)+ 3020 apply (auto simp: map_lift_over_eq_Some inj_on_eq_iff[where f=transform_cslot_ptr] 3021 ranI domI 3022 intro: map_lift_over_f_eq[THEN iffD2, OF _ refl] 3023 elim: subset_inj_on)[2] 3024 apply (clarsimp simp: no_cdt_loop_mloop) 3025 apply (rule_tac s=s' in transform_cdt_slot_inj_on_cte_at[where P=\<top>]) 3026 apply (auto simp: swp_def dest: mdb_cte_atD 3027 elim!: ranE)[1] 3028 apply (wp set_cap_caps_of_state2 set_cap_idle 3029 | simp add: swp_def cte_wp_at_caps_of_state)+ 3030 apply clarsimp 3031 apply (clarsimp simp: cte_wp_at_caps_of_state valid_mdb_def) 3032 apply (safe intro!: mdb_cte_atI) 3033 apply (auto simp: swp_def cte_wp_at_caps_of_state not_idle_thread_def 3034 dest: mdb_cte_atD elim!: ranE) 3035 done 3036qed 3037 3038lemma swap_for_delete_corres: 3039 "dcorres dc \<top> (valid_mdb and valid_idle and not_idle_thread (fst p) 3040 and not_idle_thread (fst p') and valid_etcbs and (\<lambda>_. p \<noteq> p')) 3041 (swap_for_delete (transform_cslot_ptr p) (transform_cslot_ptr p')) 3042 (cap_swap_for_delete p p')" 3043 apply (rule corres_gen_asm2) 3044 apply (simp add: swap_for_delete_def cap_swap_for_delete_def when_def) 3045 apply (rule corres_guard_imp) 3046 apply (rule corres_split[OF _ get_cap_corres[OF refl]])+ 3047 apply simp 3048 apply (rule swap_cap_corres) 3049 apply (wp get_cap_wp)+ 3050 apply simp 3051 apply (clarsimp simp: cte_wp_at_caps_of_state) 3052 done 3053 3054definition 3055 "arch_page_vmpage_size cap \<equiv> 3056 case cap of cap.ArchObjectCap (arch_cap.PageCap dev _ _ sz _) \<Rightarrow> sz 3057 | _ \<Rightarrow> undefined" 3058 3059lemma set_cap_noop_dcorres3: 3060 "dcorres dc \<top> (cte_wp_at (\<lambda>cap'. transform_cap cap = transform_cap cap' 3061 \<and> arch_page_vmpage_size cap = arch_page_vmpage_size cap') ptr) 3062 (return ()) (set_cap cap ptr)" 3063 apply (rule corres_noop, simp_all) 3064 apply (simp add: set_cap_def split_def set_object_def) 3065 apply (wp get_object_wp | wpc)+ 3066 apply (clarsimp simp: obj_at_def) 3067 apply (erule cte_wp_atE) 3068 apply (clarsimp simp: transform_def transform_current_thread_def 3069 transform_objects_def) 3070 apply (rule ext) 3071 apply (simp add: fun_upd_def[symmetric] 3072 del: dom_fun_upd) 3073 apply (simp add: restrict_map_def transform_cnode_contents_def 3074 fun_eq_iff option_map_join_def map_add_def 3075 split: option.split nat.split) 3076 apply (clarsimp simp: transform_def transform_current_thread_def 3077 transform_objects_def fun_eq_iff 3078 arch_page_vmpage_size_def) 3079 apply (simp add: restrict_map_def transform_cnode_contents_def map_add_def 3080 transform_tcb_def fun_eq_iff infer_tcb_pending_op_def 3081 split: option.split cong: Structures_A.thread_state.case_cong) 3082 apply (subgoal_tac "snd ptr = tcb_cnode_index 4 \<longrightarrow> 3083 (\<forall>ms ns. get_ipc_buffer_words ms (tcb\<lparr>tcb_ipcframe := cap\<rparr>) ns 3084 = get_ipc_buffer_words ms tcb ns)") 3085 apply (simp cong: transform_full_intent_cong) 3086 apply (simp add: transform_full_intent_def Let_def get_tcb_message_info_def 3087 get_tcb_mrs_def) 3088 apply fastforce 3089 apply clarsimp 3090 apply (simp add: transform_cap_def split: cap.split_asm arch_cap.split_asm if_split_asm, 3091 simp_all add: get_ipc_buffer_words_def) 3092 done 3093 3094lemma finalise_zombie: 3095 "is_zombie cap \<Longrightarrow> finalise_cap cap final 3096 = do assert final; return (cap, cap.NullCap) od" 3097 by (clarsimp simp add: is_cap_simps) 3098 3099lemma corres_assert_rhs: 3100 "(F \<Longrightarrow> corres_underlying sr False False r P P' f (g ())) 3101 \<Longrightarrow> corres_underlying sr False False r P (\<lambda>s. F \<longrightarrow> P' s) f (assert F >>= g)" 3102 by (cases F, simp_all add: corres_fail) 3103 3104lemma monadic_rewrite_select_x: 3105 "monadic_rewrite F False 3106 (\<lambda>s. x \<in> S) (select S) (return x)" 3107 by (simp add: monadic_rewrite_def return_def select_def) 3108 3109lemmas monadic_rewrite_select_pick_x 3110 = monadic_rewrite_bind_head 3111 [OF monadic_rewrite_select_x[where x=x], simplified, 3112 THEN monadic_rewrite_trans] for x 3113 3114lemma finalise_cap_zombie': 3115 "(case cap of ZombieCap _ \<Rightarrow> True | _ \<Rightarrow> False) 3116 \<Longrightarrow> CSpace_D.finalise_cap cap fin = 3117 do assert fin; return (cap, cdl_cap.NullCap) od" 3118 by (simp split: cdl_cap.split_asm) 3119 3120lemma corres_use_cutMon: 3121 "\<lbrakk> \<And>s. corres_underlying sr False fl r P P' f (cutMon ((=) s) g) \<rbrakk> 3122 \<Longrightarrow> corres_underlying sr False fl r P P' f g" 3123 apply atomize 3124 apply (simp add: corres_underlying_def cutMon_def fail_def 3125 split: if_split_asm) 3126 apply (clarsimp simp: split_def) 3127 done 3128 3129lemma corres_drop_cutMon: 3130 "corres_underlying sr False False r P P' f g 3131 \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g)" 3132 apply (simp add: corres_underlying_def cutMon_def fail_def 3133 split: if_split) 3134 apply (clarsimp simp: split_def) 3135 done 3136 3137lemma corres_drop_cutMon_bind: 3138 "corres_underlying sr False False r P P' f (g >>= h) 3139 \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g >>= h)" 3140 apply (simp add: corres_underlying_def cutMon_def fail_def bind_def 3141 split: if_split) 3142 apply (clarsimp simp: split_def) 3143 done 3144 3145lemma corres_drop_cutMon_bindE: 3146 "corres_underlying sr False False r P P' f (g >>=E h) 3147 \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g >>=E h)" 3148 apply (simp add: bindE_def) 3149 apply (erule corres_drop_cutMon_bind) 3150 done 3151 3152lemma corres_cutMon: 3153 "\<lbrakk> \<And>s. Q s \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon ((=) s) g) \<rbrakk> 3154 \<Longrightarrow> corres_underlying sr False False r P P' f (cutMon Q g)" 3155 apply atomize 3156 apply (simp add: corres_underlying_def cutMon_def fail_def 3157 split: if_split_asm) 3158 apply (clarsimp simp: split_def) 3159 done 3160 3161lemma underlying_memory_irq_state_independent[intro!, simp]: 3162 "underlying_memory (s\<lparr>irq_state := f (irq_state s)\<rparr>) 3163 = underlying_memory s" 3164 by simp 3165 3166lemma get_ipc_buffer_words_irq_state_independent[intro!, simp]: 3167 "get_ipc_buffer_words (s\<lparr>irq_state := f (irq_state s)\<rparr>) 3168 = get_ipc_buffer_words s" 3169 apply (rule ext, rule ext) 3170 apply (simp add: get_ipc_buffer_words_def) 3171 apply (case_tac "tcb_ipcframe x", simp_all) 3172 apply (clarsimp split: ARM_A.arch_cap.splits) 3173 apply (rule arg_cong[where f=the]) 3174 apply (rule evalMonad_mapM_cong) 3175 apply (simp add: evalMonad_def) 3176 apply safe 3177 apply ((clarsimp simp: loadWord_def bind_def gets_def get_def return_def in_monad)+)[3] 3178 apply (rule loadWord_inv) 3179 apply (rule df_loadWord) 3180 done 3181 3182lemma get_tcb_mrs_irq_state_independent[intro!, simp]: 3183 "get_tcb_mrs (s\<lparr>irq_state := f (irq_state s)\<rparr>) 3184 = get_tcb_mrs s" 3185 by (auto simp: get_tcb_mrs_def) 3186 3187lemma transform_full_intent_irq_state_independent[intro!, simp]: 3188 "transform_full_intent (s\<lparr>irq_state := f (irq_state s)\<rparr>) 3189 = transform_full_intent s" 3190 by (rule ext, rule ext, simp add: transform_full_intent_def) 3191 3192lemma transform_tcb_irq_state_independent[intro!, simp]: 3193 "transform_tcb (s\<lparr>irq_state := f (irq_state s)\<rparr>) 3194 = transform_tcb s" 3195 by (rule ext, rule ext, rule ext, simp add: transform_tcb_def) 3196 3197lemma transform_object_irq_state_independent[intro!, simp]: 3198 "transform_object (s \<lparr> irq_state := f (irq_state s) \<rparr>) 3199 = transform_object s" 3200 by (rule ext, rule ext, rule ext, 3201 simp add: transform_object_def 3202 split: Structures_A.kernel_object.splits) 3203 3204lemma transform_objects_irq_state_independent[intro!, simp]: 3205 "transform_objects (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>) 3206 = transform_objects s" 3207 by (simp add: transform_objects_def) 3208 3209lemma transform_irq_state_independent[intro!, simp]: 3210 "transform (s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr> \<rparr>) 3211 = transform s" 3212 by (simp add: transform_def transform_current_thread_def) 3213 3214lemma transform_work_units_independent[intro!, simp]: 3215 "transform (s \<lparr> work_units_completed := f (work_units_completed s) \<rparr>) 3216 = transform s" 3217 apply (simp add: transform_def transform_current_thread_def transform_objects_def transform_cdt_def transform_asid_table_def) 3218 done 3219 3220lemma transform_work_units_then_irq_state_independent[intro!, simp]: 3221 "transform (s \<lparr> work_units_completed := g (work_units_completed s) \<rparr> 3222 \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>\<rparr>) = 3223 transform s" 3224 apply (simp add: transform_def transform_current_thread_def transform_objects_def transform_cdt_def transform_asid_table_def) 3225 done 3226 3227lemma throw_or_return_preemption_corres: 3228 "dcorres (dc \<oplus> dc) P P' 3229 (Monads_D.throw \<sqinter> returnOk ()) 3230 preemption_point" 3231 apply (simp add: preemption_point_def) 3232 apply (auto simp: preemption_point_def o_def gets_def liftE_def whenE_def getActiveIRQ_def 3233 corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def 3234 alternative_def throwError_def returnOk_def return_def lift_def 3235 put_def do_machine_op_def 3236 update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def 3237 work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def 3238 split: option.splits kernel_object.splits) 3239 done 3240 3241lemma cutMon_fail: 3242 "cutMon P fail = fail" 3243 by (simp add: cutMon_def) 3244 3245declare rec_del.simps[simp del] 3246 3247lemma select_pick_corres_asm: 3248 "\<lbrakk> x \<in> S; corres_underlying sr nf nf' r P Q (f x) g \<rbrakk> 3249 \<Longrightarrow> corres_underlying sr nf nf' r P Q (select S >>= f) g" 3250 by (drule select_pick_corres[where x=x and S=S], simp) 3251 3252lemma invs_weak_valid_mdb: 3253 "invs s \<longrightarrow> weak_valid_mdb s" 3254 by (simp add: weak_valid_mdb_def invs_def valid_mdb_def valid_state_def) 3255 3256lemma invs_valid_idle_strg: 3257 "invs s \<longrightarrow> valid_idle s" 3258 by auto 3259 3260lemma cutMon_validE_R_drop: 3261 "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>,- \<Longrightarrow> \<lbrace>P\<rbrace> cutMon R f \<lbrace>Q\<rbrace>,-" 3262 by (simp add: validE_R_def validE_def cutMon_valid_drop) 3263 3264crunch idle_thread [wp]: cap_swap_for_delete "\<lambda>s::'a::state_ext state. P (idle_thread s)" 3265 (wp: dxo_wp_weak) 3266 3267crunch idle_thread [wp]: finalise_cap "\<lambda>s. P (idle_thread s)" 3268 (wp: crunch_wps simp: crunch_simps) 3269 3270lemma preemption_point_idle_thread[wp]: "\<lbrace> \<lambda>s. P (idle_thread s) \<rbrace> preemption_point \<lbrace> \<lambda>_ s. P (idle_thread s) \<rbrace>" 3271 apply (simp add: preemption_point_def OR_choiceE_def) 3272 apply (wpsimp wp: hoare_drop_imps dxo_wp_weak[where P="\<lambda>s. P (idle_thread s)"]) 3273 done 3274 3275lemma rec_del_idle_thread[wp]: 3276 "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> rec_del args \<lbrace>\<lambda>rv s::'a::state_ext state. P (idle_thread s)\<rbrace>" 3277 by (wp rec_del_preservation | simp)+ 3278 3279lemmas gets_constant = gets_to_return 3280 3281lemma monadic_rewrite_gets_the_gets: 3282 "monadic_rewrite F E (\<lambda>s. f s \<noteq> None) (gets_the f) (gets (the o f))" 3283 apply (simp add: monadic_rewrite_def gets_the_def assert_opt_def exec_gets 3284 split: option.split) 3285 apply (auto simp: simpler_gets_def return_def) 3286 done 3287 3288lemmas corres_gets_the_bind 3289 = monadic_rewrite_corres2[OF monadic_rewrite_bind_head [OF monadic_rewrite_gets_the_gets]] 3290 3291lemma finalise_slot_inner1_add_if_Null: 3292 "monadic_rewrite F False \<top> 3293 (finalise_slot_inner1 victim) 3294 (do cap \<leftarrow> KHeap_D.get_cap victim; 3295 if cap = cdl_cap.NullCap then return (cdl_cap.NullCap, True) 3296 else do 3297 final \<leftarrow> PageTableUnmap_D.is_final_cap cap; 3298 (cap', irqopt) \<leftarrow> CSpace_D.finalise_cap cap final; 3299 removeable \<leftarrow> gets $ CSpace_D.cap_removeable cap' victim; 3300 when (\<not> removeable) (KHeap_D.set_cap victim cap') 3301 \<sqinter> KHeap_D.set_cap victim cap'; 3302 return (cap', removeable) 3303 od 3304 od)" 3305 apply (simp add: finalise_slot_inner1_def) 3306 apply (rule monadic_rewrite_imp) 3307 apply (rule monadic_rewrite_bind_tail) 3308 apply (rule monadic_rewrite_if_rhs) 3309 apply (simp add: PageTableUnmap_D.is_final_cap_def) 3310 apply (rule monadic_rewrite_trans) 3311 apply (rule monadic_rewrite_bind_tail[where j="\<lambda>_. j" for j, OF _ gets_wp])+ 3312 apply (rename_tac remove, rule_tac P=remove in monadic_rewrite_gen_asm) 3313 apply simp 3314 apply (rule monadic_rewrite_refl) 3315 apply (simp add: gets_bind_ign when_def) 3316 apply (rule monadic_rewrite_trans) 3317 apply (rule monadic_rewrite_bind_head) 3318 apply (rule monadic_rewrite_pick_alternative_1) 3319 apply simp 3320 apply (rule monadic_rewrite_refl) 3321 apply (rule monadic_rewrite_refl) 3322 apply wp 3323 apply (clarsimp simp: CSpace_D.cap_removeable_def) 3324 done 3325 3326lemma corres_if_rhs_only: 3327 "\<lbrakk> G \<Longrightarrow> corres_underlying sr nf nf' rvr P Q a b; 3328 \<not> G \<Longrightarrow> corres_underlying sr nf nf' rvr P' Q' a c\<rbrakk> 3329 \<Longrightarrow> corres_underlying sr nf nf' rvr 3330 (P and P') (\<lambda>s. (G \<longrightarrow> Q s) \<and> (\<not> G \<longrightarrow> Q' s)) 3331 a (if G then b else c)" 3332 by (rule corres_guard_imp, rule corres_if_rhs, simp+) 3333 3334lemma OR_choiceE_det: 3335 "\<lbrakk>det c; \<And>P. \<lbrace>P\<rbrace> c \<lbrace>\<lambda>rv. P\<rbrace>\<rbrakk> \<Longrightarrow> (OR_choiceE c (f :: ('a + 'b) det_ext_monad) g) 3336 = (doE rv \<leftarrow> liftE c; if rv then f else g odE)" 3337 apply (rule ext) 3338 apply (clarsimp simp: OR_choiceE_def select_f_def bind_def det_def valid_def 3339 wrap_ext_bool_det_ext_ext_def get_def bindE_def ethread_get_def split_def 3340 gets_the_def assert_opt_def return_def gets_def fail_def mk_ef_def liftE_def no_fail_def 3341 split: option.splits prod.splits) 3342 apply atomize 3343 apply (erule_tac x="(=) x" in allE) 3344 apply (erule_tac x=x in allE)+ 3345 apply clarsimp 3346 done 3347 3348lemma transform_work_units_completed_update[simp]: "transform (s\<lparr> work_units_completed := a \<rparr>) = transform s" 3349 by (auto simp: transform_def transform_cdt_def transform_current_thread_def transform_asid_table_def transform_objects_def) 3350 3351lemma finalise_preemption_corres: 3352 "dcorres (dc \<oplus> (\<lambda>rv rv'. fst S \<subseteq> fst rv)) \<top> \<top> 3353 (monadic_trancl_preemptible finalise_slot_inner2 S) (preemption_point)" 3354 apply (simp add: finalise_slot_inner2_def preemption_point_def split_def) 3355 apply (subst OR_choiceE_det) 3356 apply (simp add: work_units_limit_reached_def) 3357 apply ((simp add: work_units_limit_reached_def | wp)+)[1] 3358 apply (rule corres_guard_imp) 3359 3360 3361 apply (rule dcorres_symb_exec_rE) 3362 apply (rule dcorres_symb_exec_rE) 3363 apply simp 3364 apply (rule conjI, clarsimp) 3365 apply (rule dcorres_symb_exec_rE) 3366 apply (rule dcorres_symb_exec_rE) 3367 apply (simp split: option.splits) 3368 apply (rule conjI, clarsimp) 3369 apply (rule monadic_rewrite_corres2) 3370 apply (rule monadic_trancl_preemptible_return) 3371 apply (rule dcorres_returnOk, simp) 3372 apply clarsimp 3373 apply (rule corres_guard_imp) 3374 apply (rule monadic_rewrite_corres2) 3375 apply (rule monadic_trancl_preemptible_f) 3376 apply (rule corres_alternate2[OF dcorres_throw], simp_all)[4] 3377 apply ((wp | simp)+)[1] 3378 apply (rule hoare_TrueI) 3379 apply ((simp add: reset_work_units_def | wp)+)[1] 3380 apply clarsimp 3381 apply (rule corres_guard_imp) 3382 apply (rule monadic_rewrite_corres2) 3383 apply (rule monadic_trancl_preemptible_return) 3384 apply (rule dcorres_returnOk, simp_all)[3] 3385 apply (rule hoare_TrueI) 3386 apply ((simp add: work_units_limit_reached_def | wp)+)[1] 3387 apply (rule hoare_TrueI) 3388 apply (simp add: update_work_units_def | wp)+ 3389 done 3390 3391lemma zombie_is_cap_toE_pre2: 3392 "\<lbrakk> s \<turnstile> cap.Zombie ptr zbits n; m < n \<rbrakk> 3393 \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (cap.Zombie ptr zbits n) irqn" 3394 apply (clarsimp simp add: valid_cap_def cap_aligned_def) 3395 apply (clarsimp split: option.split_asm) 3396 apply (simp add: unat_of_bl_nat_to_cref) 3397 apply (simp add: nat_to_cref_def word_bits_conv) 3398 apply (simp add: unat_of_bl_nat_to_cref) 3399 apply (simp add: nat_to_cref_def word_bits_conv) 3400 done 3401 3402lemma corres_note_assumption: 3403 "\<lbrakk> F; corres_underlying sr fl fl' r P P' f g \<rbrakk> 3404 \<Longrightarrow> corres_underlying sr fl fl' r (\<lambda>s. F \<longrightarrow> P s) P' f g" 3405 by simp 3406 3407lemma corres_req2: 3408 "\<lbrakk>\<And>s s'. \<lbrakk>(s, s') \<in> sr; P s; P' s'\<rbrakk> \<Longrightarrow> F; F \<Longrightarrow> corres_underlying sr nf nf' r Q Q' f g\<rbrakk> 3409 \<Longrightarrow> corres_underlying sr nf nf' r (P and Q) (P' and Q') f g" 3410 apply (rule_tac F=F in corres_req, simp_all) 3411 apply (erule corres_guard_imp, simp_all) 3412 done 3413 3414lemma nat_split_conv_to_if: 3415 "(case n of 0 \<Rightarrow> a | Suc nat' \<Rightarrow> f nat') = (if n = 0 then a else f (n - 1))" 3416 by (auto split: nat.splits) 3417 3418lemma opt_cap_cnode: 3419 "\<lbrakk> kheap s y = Some (CNode sz cn); y \<noteq> idle_thread s; well_formed_cnode_n sz cn \<rbrakk> 3420 \<Longrightarrow> (opt_cap (y, node) (transform s) = Some cap) 3421 = (\<exists>v cap'. transform_cslot_ptr (y, v) = (y, node) 3422 \<and> cn v = Some cap' \<and> cap = transform_cap cap')" 3423 apply clarsimp 3424 apply (simp add: opt_cap_def slots_of_def opt_object_def 3425 transform_def transform_objects_def restrict_map_def 3426 transform_cnode_contents_def option_map_join_def 3427 transform_cslot_ptr_def object_slots_def 3428 nat_split_conv_to_if 3429 split: option.split) 3430 apply (case_tac "sz = 0") 3431 apply (clarsimp, rule conjI) 3432 apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD) 3433 apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2 3434 option.inject wf_cs_nD) (* slow 20s *) 3435 (* "sz \<noteq> 0" *) 3436 apply (clarsimp, rule conjI) 3437 apply (metis nat_to_bl_id2 option.distinct(1) wf_cs_nD) 3438 apply (metis (full_types) nat_to_bl_to_bin nat_to_bl_id2 3439 option.inject wf_cs_nD) (* slow 30s *) 3440 done 3441 3442lemma preemption_point_valid_etcbs[wp]: "\<lbrace> valid_etcbs \<rbrace> preemption_point \<lbrace> \<lambda>_. valid_etcbs \<rbrace>" 3443 apply (clarsimp simp: preemption_point_def) 3444 apply (auto simp: valid_def o_def gets_def liftE_def whenE_def getActiveIRQ_def 3445 corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def 3446 alternative_def throwError_def returnOk_def return_def lift_def 3447 put_def do_machine_op_def 3448 update_work_units_def wrap_ext_bool_det_ext_ext_def work_units_limit_def 3449 work_units_limit_reached_def OR_choiceE_def reset_work_units_def mk_ef_def 3450 split: option.splits kernel_object.splits) 3451 done 3452 3453crunch valid_etcbs[wp]: cap_swap_ext, cap_swap_for_delete "valid_etcbs" 3454 3455lemma rec_del_valid_etcbs[wp]: 3456 "\<lbrace> valid_etcbs \<rbrace> rec_del args \<lbrace>\<lambda>_. valid_etcbs \<rbrace>" 3457 by (wp rec_del_preservation | simp)+ 3458 3459lemma dcorres_rec_del: 3460 "\<lbrakk> (case args of CTEDeleteCall slot e \<Rightarrow> \<not> e | _ \<Rightarrow> True); 3461 (transform_cslot_ptr (slot_rdcall args), \<not> exposed_rdcall args) \<in> fst S; 3462 (case args of ReduceZombieCall (cap.Zombie p zbits (Suc n)) _ _ \<Rightarrow> 3463 (transform_cslot_ptr (p, replicate (zombie_cte_bits zbits) False), True) \<in> fst S 3464 \<and> (transform_cslot_ptr (p, nat_to_cref (zombie_cte_bits zbits) n), True) \<in> fst S 3465 | _ \<Rightarrow> True) \<rbrakk> 3466 \<Longrightarrow> dcorres (dc \<oplus> (\<lambda>rv rv'. (case args of FinaliseSlotCall _ _ \<Rightarrow> 3467 fst rv' \<longrightarrow> (\<exists>v. (transform_cslot_ptr (slot_rdcall args), v) \<in> snd rv 3468 \<and> (\<not> exposed_rdcall args \<longrightarrow> v)) | _ \<Rightarrow> True) 3469 \<and> fst S \<subseteq> fst rv)) 3470 \<top> 3471 (invs and valid_rec_del_call args and cte_at (slot_rdcall args) 3472 and valid_etcbs 3473 and valid_pdpt_objs 3474 and emptyable (slot_rdcall args) and not_idle_thread (fst (slot_rdcall args)) 3475 and (\<lambda>s. \<not> exposed_rdcall args \<longrightarrow> 3476 ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall args) s) 3477 and (\<lambda>s. case args of 3478 ReduceZombieCall cap sl ex \<Rightarrow> \<forall>t\<in>obj_refs cap. halted_if_tcb t s 3479 | _ \<Rightarrow> True)) 3480 (doE S' \<leftarrow> monadic_trancl_preemptible 3481 finalise_slot_inner2 S; 3482 whenE ((case args of ReduceZombieCall _ _ _ \<Rightarrow> False | _ \<Rightarrow> True) 3483 \<and> exposed_rdcall args 3484 \<and> \<not> (transform_cslot_ptr (slot_rdcall args)) \<in> fst ` snd S') Monads_D.throw; 3485 returnOk S' 3486 odE) 3487 (cutMon ((=) s) (rec_del args))" 3488proof (induct arbitrary: S rule: rec_del.induct, 3489 simp_all(no_asm) only: rec_del_fails fail_bindE corres_free_fail cutMon_fail) 3490 case (1 slot exposed s S) 3491 note ps = "1.prems"[simplified] 3492 hence nexp[simp]: "\<not> exposed" by simp 3493 show ?case 3494 using ps 3495 apply (simp add: dc_def[symmetric]) 3496 apply (subst rec_del_simps_ext[unfolded split_def]) 3497 apply simp 3498 apply (rule corres_guard_imp) 3499 apply (rule monadic_rewrite_corres2) 3500 apply (rule monadic_trancl_preemptible_steps) 3501 apply (simp add: cutMon_walk_bindE) 3502 apply (rule corres_splitEE) 3503 prefer 2 3504 apply (rule "1.hyps"[simplified, folded dc_def], assumption+) 3505 apply (rule corres_drop_cutMon) 3506 apply (simp add: liftME_def[symmetric]) 3507 apply (rule_tac R="fst rv" in corres_cases) 3508 apply (simp add: when_def) 3509 apply (rule monadic_rewrite_corres2) 3510 apply (rule monadic_trancl_preemptible_f) 3511 apply (simp add: finalise_slot_inner2_def[unfolded split_def]) 3512 apply (rule corres_alternate1, rule corres_alternate2) 3513 apply simp 3514 apply (rule select_pick_corres_asm) 3515 apply clarsimp 3516 apply assumption 3517 apply (simp add: liftM_def[symmetric] o_def dc_def[symmetric]) 3518 apply (rule empty_slot_corres) 3519 apply (simp add: when_def) 3520 apply (rule monadic_rewrite_corres2) 3521 apply (rule monadic_trancl_preemptible_return) 3522 apply (rule corres_trivial, simp add: returnOk_liftE) 3523 apply wp 3524 apply (wp_trace cutMon_validE_R_drop rec_del_invs 3525 | simp add: not_idle_thread_def 3526 | strengthen invs_weak_valid_mdb invs_valid_idle_strg 3527 | rule hoare_vcg_E_elim[rotated])+ 3528 3529 done 3530next 3531 case (2 slot exposed s S) 3532 note if_split[split del] 3533 have removeables: 3534 "\<And>s cap fin. \<lbrakk> cte_wp_at ((=) cap) slot s; s \<turnstile> remainder_cap fin cap; invs s; valid_etcbs s; 3535 CSpace_A.cap_removeable (remainder_cap fin cap) slot \<rbrakk> 3536 \<Longrightarrow> CSpace_D.cap_removeable (transform_cap (remainder_cap fin cap)) 3537 (transform_cslot_ptr slot) (transform s)" 3538 apply (case_tac "remainder_cap fin cap = cap.NullCap") 3539 apply (simp add: CSpace_D.cap_removeable_def) 3540 apply (clarsimp simp: remainder_cap_def valid_cap_simps 3541 cte_wp_at_caps_of_state 3542 split: cap.split_asm if_split_asm) 3543 apply (rename_tac word nat option) 3544 apply (frule valid_global_refsD2, clarsimp) 3545 apply (clarsimp simp: CSpace_D.cap_removeable_def) 3546 apply (subgoal_tac "\<exists>x cap. (word, b) = transform_cslot_ptr (word, x) 3547 \<and> caps_of_state s (word, x) = Some cap \<and> cap \<noteq> cap.NullCap") 3548 apply clarsimp 3549 apply (case_tac "(word, x) \<in> cte_refs (the (caps_of_state s slot)) (interrupt_irq_node s)") 3550 apply (clarsimp simp: unat_eq_0) 3551 apply (drule of_bl_eq_0) 3552 apply (simp add: cap_aligned_def word_bits_conv split: option.split_asm) 3553 apply clarsimp 3554 apply (frule zombie_cap_has_all[rotated -2], simp, clarsimp+) 3555 apply (clarsimp simp: tcb_at_def cap_range_def global_refs_def 3556 opt_cap_tcb 3557 split: option.split_asm if_split_asm | drule(1) valid_etcbs_get_tcb_get_etcb)+ 3558 apply (rule_tac x="tcb_cnode_index b" in exI) 3559 apply (clarsimp simp: transform_cslot_ptr_def dest!: get_tcb_SomeD) 3560 apply (rule conjI, rule sym, rule bl_to_bin_tcb_cnode_index) 3561 apply (auto simp: tcb_slot_defs)[1] 3562 apply (rule iffD1[OF cte_wp_at_caps_of_state cte_wp_at_tcbI], (simp | rule conjI)+) 3563 apply (frule final_zombie_not_live[rotated 1, OF caps_of_state_cteD], clarsimp) 3564 apply (rule ccontr, erule zombies_finalE) 3565 apply (simp add: is_cap_simps) 3566 apply clarsimp 3567 apply (erule caps_of_state_cteD) 3568 3569 apply (clarsimp simp: obj_at_def live_def hyp_live_def dest!: get_tcb_SomeD) 3570 apply (auto simp: infer_tcb_pending_op_def)[1] 3571 apply (frule final_zombie_not_live[rotated 1, OF caps_of_state_cteD], clarsimp) 3572 apply (rule ccontr, erule zombies_finalE) 3573 apply (simp add: is_cap_simps) 3574 apply clarsimp 3575 apply (erule caps_of_state_cteD) 3576 apply (clarsimp simp: obj_at_def live_def hyp_live_def dest!: get_tcb_SomeD) 3577 apply (auto simp: infer_tcb_bound_notification_def)[1] 3578 apply (clarsimp simp: obj_at_def live_def hyp_live_def is_cap_table_def) 3579 apply (clarsimp simp: opt_cap_cnode 3580 split: Structures_A.kernel_object.split_asm) 3581 apply (rule exI, rule conjI, erule sym) 3582 apply (rule iffD1[OF cte_wp_at_caps_of_state cte_wp_at_cteI], 3583 (simp | rule conjI)+) 3584 done 3585 show ?case 3586 using "2.prems" 3587 apply (simp add: dc_def[symmetric]) 3588 apply (subst rec_del_simps_ext[unfolded split_def]) 3589 apply (simp add: bindE_assoc, simp add: liftE_bindE) 3590 apply (rule stronger_corres_guard_imp) 3591 apply (simp add: cutMon_walk_bind) 3592 apply (rule corres_drop_cutMon_bind) 3593 apply (rule monadic_rewrite_corres2) 3594 apply (rule monadic_rewrite_bindE_head) 3595 apply (rule monadic_trancl_preemptible_step) 3596 apply (simp add: finalise_slot_inner2_def 3597 [THEN fun_cong, unfolded split_def]) 3598 apply (simp add: alternative_bindE_distrib) 3599 apply (rule corres_alternate1)+ 3600 apply (simp add: liftE_bindE bind_bindE_assoc bind_assoc) 3601 apply (rule select_pick_corres_asm, assumption) 3602 apply (rule monadic_rewrite_corres2) 3603 apply (rule monadic_rewrite_bind_head) 3604 apply (rule finalise_slot_inner1_add_if_Null[unfolded split_def]) 3605 apply (simp add: bind_assoc if_to_top_of_bind) 3606 apply (rule corres_split[OF _ get_cap_corres[OF refl]]) 3607 apply (rename_tac cap) 3608 apply (rule corres_cutMon) 3609 apply (simp add: if_to_top_of_bindE cutMon_walk_if 3610 del: transform_cap_Null) 3611 apply (rule Corres_UL.corres_if2[unfolded if_apply_def2]) 3612 apply simp 3613 apply (rule corres_drop_cutMon) 3614 apply (rule corres_underlying_gets_pre_lhs)+ 3615 apply (rule monadic_rewrite_corres2) 3616 apply (rule monadic_rewrite_bindE_head) 3617 apply (rule monadic_trancl_preemptible_return) 3618 apply simp 3619 apply (rule corres_trivial, simp add: returnOk_liftE) 3620 apply (rule_tac F="cap \<noteq> cap.NullCap" in corres_gen_asm2) 3621 apply (rule corres_cutMon) 3622 apply (simp add: cutMon_walk_bind del: fst_conv) 3623 apply (rule corres_drop_cutMon_bind) 3624 apply (rule corres_split [OF _ is_final_cap_corres[OF refl]]) 3625 apply (rule corres_cutMon) 3626 apply (simp add: cutMon_walk_bind del: fst_conv) 3627 apply (rule corres_drop_cutMon_bind) 3628 apply (rule corres_split[OF _ dcorres_finalise_cap[where slot=slot]]) 3629 apply (rename_tac fin fin') 3630 apply (rule corres_cutMon) 3631 apply (simp(no_asm) add: cutMon_walk_if) 3632 apply (rule corres_underlying_gets_pre_lhs) 3633 apply (rename_tac remove) 3634 apply (rule_tac P="\<lambda>s. remove = CSpace_D.cap_removeable (fst fin) (transform_cslot_ptr slot) s" 3635 and P'="cte_wp_at ((=) cap) slot and invs and valid_etcbs and valid_cap (fst fin')" 3636 and F="CSpace_A.cap_removeable (fst fin') slot \<longrightarrow> remove" 3637 in corres_req2) 3638 apply (drule use_valid[OF _ finalise_cap_remainder, OF _ TrueI]) 3639 apply (clarsimp simp: removeables) 3640 apply (rule corres_if_rhs_only) 3641 apply (rule_tac F=remove in corres_note_assumption, simp) 3642 apply (simp add: when_def) 3643 apply (rule monadic_rewrite_corres2) 3644 apply (rule monadic_rewrite_bind) 3645 apply (rule monadic_rewrite_pick_alternative_1) 3646 apply (rule monadic_rewrite_bind_tail) 3647 apply (rule monadic_rewrite_bindE_head) 3648 apply (rule monadic_trancl_preemptible_return) 3649 apply wp+ 3650 apply simp 3651 apply (rule corres_underlying_gets_pre_lhs) 3652 apply (rule corres_drop_cutMon) 3653 apply (rule corres_trivial, simp add: returnOk_liftE) 3654 apply (rule corres_if_rhs_only) 3655 apply simp 3656 apply (rule corres_drop_cutMon) 3657 apply (rule monadic_rewrite_corres2) 3658 apply (rule monadic_rewrite_bind) 3659 apply (rule monadic_rewrite_pick_alternative_2) 3660 apply (rule monadic_rewrite_bind_tail) 3661 apply (rule monadic_trancl_preemptible_return) 3662 apply wp+ 3663 apply (rule corres_split[OF _ set_cap_corres]) 3664 apply (rule corres_underlying_gets_pre_lhs) 3665 apply (rule corres_trivial, simp add: returnOk_liftE) 3666 apply (wp | simp)+ 3667 apply (rule monadic_rewrite_corres2) 3668 apply (rule monadic_rewrite_bind_head) 3669 apply (rule monadic_rewrite_pick_alternative_2) 3670 apply (simp add: cutMon_walk_bind) 3671 apply (rule corres_drop_cutMon_bind) 3672 apply (rule corres_split[OF _ set_cap_corres]) 3673 apply (rule_tac P="dcorres r P P' f" for r P P' f in subst) 3674 apply (rule_tac f="\<lambda>_. ()" in gets_bind_ign) 3675 apply (rule_tac r'="\<lambda>rv rv'. transform_cslot_ptr ` 3676 (case fst fin' of cap.Zombie p zb (Suc n) \<Rightarrow> 3677 {(p, replicate (zombie_cte_bits zb) False), 3678 (p, nat_to_cref (zombie_cte_bits zb) n)} | _ \<Rightarrow> {}) \<subseteq> rv" 3679 and P=\<top> and P'="valid_cap (fst fin') and invs and valid_etcbs 3680 and (\<lambda>s. idle_thread s \<notin> obj_refs (fst fin'))" in corres_split) 3681 apply (rule monadic_rewrite_corres2) 3682 apply (rule monadic_rewrite_bindE_head) 3683 apply (rule monadic_rewrite_trans) 3684 apply (rule monadic_trancl_preemptible_steps) 3685 apply (rule monadic_rewrite_bindE[OF monadic_rewrite_refl]) 3686 apply (rule monadic_trancl_preemptible_steps) 3687 apply wp 3688 apply (rule corres_cutMon) 3689 apply (simp add: cutMon_walk_bindE bindE_assoc) 3690 apply (rule corres_splitEE) 3691 prefer 2 3692 apply (rule "2.hyps"[simplified, folded dc_def], 3693 (assumption | simp | rule conjI refl)+) 3694 apply (clarsimp split: cap.split nat.split) 3695 apply (rule corres_cutMon) 3696 apply (simp add: cutMon_walk_bindE dc_def[symmetric]) 3697 apply (rule corres_drop_cutMon_bindE) 3698 apply (rule corres_splitEE[OF _ finalise_preemption_corres]) 3699 apply (rule corres_cutMon) 3700 apply (rule corres_rel_imp, rule "2.hyps"[simplified, folded dc_def], 3701 (assumption | simp | rule conjI refl)+) 3702 apply clarsimp 3703 apply blast 3704 apply (rename_tac excr excr', case_tac excr, simp_all)[1] 3705 apply clarsimp 3706 apply blast 3707 apply (wp cutMon_validE_R_drop rec_del_invs rec_del_cte_at 3708 rec_del_ReduceZombie_emptyable reduce_zombie_cap_to preemption_point_valid_etcbs preemption_point_inv 3709 | simp add: not_idle_thread_def del: gets_to_return)+ 3710 apply (clarsimp simp: get_zombie_range_def dom_def 3711 split: cap.split nat.split) 3712 3713 apply (frule cte_at_nat_to_cref_zbits[OF _ lessI]) 3714 apply (frule cte_at_replicate_zbits) 3715 apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap) 3716 apply (clarsimp simp: transform_cslot_ptr_def) 3717 apply (wp | simp)+ 3718 apply (simp add: conj_comms) 3719 apply (wp replace_cap_invs final_cap_same_objrefs set_cap_cte_wp_at 3720 hoare_vcg_const_Ball_lift set_cap_cte_cap_wp_to static_imp_wp 3721 | erule finalise_cap_not_reply_master[simplified in_monad, simplified] 3722 | simp only: not_idle_thread_def pred_conj_def simp_thms)+ 3723 apply (rule hoare_strengthen_post) 3724 apply (rule_tac Q="\<lambda>fin s. invs s \<and> replaceable s slot (fst fin) cap 3725 \<and> valid_pdpt_objs s 3726 \<and> valid_etcbs s 3727 \<and> cte_wp_at ((=) cap) slot s \<and> s \<turnstile> fst fin 3728 \<and> emptyable slot s \<and> fst slot \<noteq> idle_thread s 3729 \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s)" 3730 in hoare_vcg_conj_lift) 3731 apply (wp finalise_cap_invs[where slot=slot] 3732 finalise_cap_replaceable 3733 finalise_cap_makes_halted[where slot=slot] 3734 hoare_vcg_disj_lift hoare_vcg_ex_lift)[1] 3735 apply (rule finalise_cap_cases[where slot=slot]) 3736 apply clarsimp 3737 apply (frule if_unsafe_then_capD, clarsimp+) 3738 apply (clarsimp simp: cte_wp_at_caps_of_state) 3739 apply (frule valid_global_refsD2, clarsimp+) 3740 apply (erule disjE[where P="c = cap.NullCap \<and> P" for c P]) 3741 apply clarsimp 3742 apply (clarsimp simp: conj_comms invs_valid_idle global_refs_def cap_range_def 3743 dest!: is_cap_simps [THEN iffD1]) 3744 apply (frule trans [OF _ appropriate_Zombie, OF sym]) 3745 apply (case_tac cap, 3746 simp_all add: fst_cte_ptrs_def is_cap_simps is_final_cap'_def)[1] 3747 apply assumption 3748 apply (wp get_cap_wp | simp add: is_final_cap_def)+ 3749 apply (auto simp: not_idle_thread_def cte_wp_at_caps_of_state 3750 elim: caps_of_state_valid_cap) 3751 done 3752next 3753 case (3 ptr bits n slot s S) 3754 show ?case 3755 using "3.prems" 3756 apply (subst rec_del.simps) 3757 apply (clarsimp simp: assertE_assert liftE_bindE assert_def 3758 corres_free_fail cutMon_fail) 3759 apply (case_tac "ptr = idle_thread s \<or> fst slot = idle_thread s") 3760 apply (clarsimp simp: cutMon_def corres_underlying_def fail_def) 3761 apply (clarsimp simp: cte_wp_at_caps_of_state 3762 dest!: zombie_cap_two_nonidles) 3763 apply (rule corres_drop_cutMon) 3764 apply (simp add: liftME_def[symmetric] liftE_bindE[symmetric]) 3765 apply (rule stronger_corres_guard_imp) 3766 apply (rule monadic_rewrite_corres2) 3767 apply (rule monadic_trancl_preemptible_f) 3768 apply (simp add: finalise_slot_inner2_def[unfolded split_def]) 3769 apply (rule corres_alternate1, rule corres_alternate1, rule corres_alternate2) 3770 apply simp 3771 apply (rule_tac x="(p, p')" for p p' in select_pick_corres) 3772 apply (simp add: liftM_def[symmetric] o_def dc_def[symmetric]) 3773 apply (rule swap_for_delete_corres) 3774 apply (clarsimp simp: cte_wp_at_caps_of_state) 3775 apply (frule(1) caps_of_state_valid, drule cte_at_replicate_zbits) 3776 apply (clarsimp simp: cte_wp_at_caps_of_state transform_cslot_ptr_inj) 3777 apply (clarsimp simp: cte_wp_at_caps_of_state) 3778 apply (auto simp: not_idle_thread_def dest: zombie_cap_two_nonidles) 3779 done 3780next 3781 case (4 ptr bits n slot s S) 3782 show ?case 3783 using "4.prems" 3784 apply (subst rec_del.simps) 3785 apply simp 3786 apply (rule stronger_corres_guard_imp) 3787 apply (simp add: cutMon_walk_bindE) 3788 apply (rule monadic_rewrite_corres2) 3789 apply (rule monadic_trancl_preemptible_steps) 3790 apply (rule corres_splitEE[OF _ "4.hyps"[simplified, folded dc_def]]) 3791 apply (rule corres_drop_cutMon) 3792 apply (simp add: liftE_bindE) 3793 apply (rule corres_symb_exec_r) 3794 apply (simp add: liftME_def[symmetric] split del: if_split) 3795 apply (rule monadic_rewrite_corres2) 3796 apply (rule monadic_trancl_preemptible_return) 3797 apply (rule corres_if_rhs_only) 3798 apply (simp add: returnOk_liftE) 3799 apply (rule corres_add_noop_lhs, 3800 simp only: liftM_def[symmetric] corres_liftM_simp) 3801 apply (simp add: o_def dc_def[symmetric]) 3802 apply (rule set_cap_noop_dcorres3) 3803 apply (simp add: assertE_assert liftE_def) 3804 apply (rule corres_assert_rhs) 3805 apply (rule corres_trivial, simp add: returnOk_def) 3806 apply (rule hoare_strengthen_post, rule get_cap_cte_wp_at) 3807 apply (clarsimp simp: cte_wp_at_caps_of_state arch_page_vmpage_size_def) 3808 apply (wp | simp)+ 3809 apply (simp add: in_monad) 3810 apply simp 3811 apply (wp cutMon_validE_R_drop)+ 3812 apply clarsimp 3813 apply (clarsimp simp: cte_wp_at_caps_of_state halted_emptyable) 3814 apply (frule valid_global_refsD2, clarsimp+) 3815 apply (frule(1) caps_of_state_valid, 3816 drule_tac m=n in cte_at_nat_to_cref_zbits) 3817 apply simp 3818 apply (auto simp: cte_wp_at_caps_of_state not_idle_thread_def 3819 global_refs_def cap_range_def 3820 elim: zombie_is_cap_toE[OF caps_of_state_cteD]) 3821 done 3822qed 3823 3824lemma dcorres_finalise_slot: 3825 "dcorres (dc \<oplus> dc) \<top> (invs and cte_at slot and valid_etcbs and valid_pdpt_objs and emptyable slot 3826 and not_idle_thread (fst slot)) 3827 (CSpace_D.finalise_slot (transform_cslot_ptr slot)) 3828 (rec_del (FinaliseSlotCall slot True))" 3829 apply (rule corres_use_cutMon) 3830 apply (cut_tac b="\<lambda>_. returnOk ()" and d="\<lambda>_. returnOk ()" and r=dc 3831 and args3="FinaliseSlotCall slot True" 3832 and S3="({(transform_cslot_ptr slot, False)}, {})" and s3=s 3833 in corres_splitEE[rotated, OF dcorres_rec_del wp_post_tautE wp_post_tautE]) 3834 apply (simp_all add: bindE_assoc CSpace_D.finalise_slot_def split_def) 3835 apply (simp_all add: liftME_def[symmetric]) 3836 apply (simp add: returnOk_def) 3837 done 3838 3839end 3840 3841end 3842