1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory ArchCNodeInv_AI 12imports "../CNodeInv_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems CNodeInv_AI_assms 18 19lemma set_cap_in_device_frame[wp]: 20 "\<lbrace>in_device_frame buffer\<rbrace> set_cap cap ref \<lbrace>\<lambda>_. in_device_frame buffer\<rbrace>" 21 by (simp add: in_device_frame_def) (wp hoare_vcg_ex_lift set_cap_typ_at) 22 23lemma valid_cnode_capI: 24 "\<lbrakk>cap_table_at n w s; valid_objs s; pspace_aligned s; n > 0; length g \<le> 32\<rbrakk> 25 \<Longrightarrow> s \<turnstile> cap.CNodeCap w n g" 26 apply (simp add: valid_cap_def cap_aligned_def) 27 apply (rule conjI) 28 apply (clarsimp simp add: pspace_aligned_def obj_at_def) 29 apply (drule bspec, fastforce) 30 apply (clarsimp simp: is_obj_defs wf_obj_bits) 31 apply (clarsimp simp add: obj_at_def is_obj_defs valid_objs_def dom_def) 32 apply (erule allE, erule impE, blast) 33 apply (simp add: valid_obj_def valid_cs_def valid_cs_size_def) 34 apply (simp add: word_bits_def cte_level_bits_def) 35 done 36 37(* unused *) 38lemma derive_cap_objrefs [CNodeInv_AI_assms]: 39 "\<lbrace>\<lambda>s. P (obj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv)\<rbrace>,-" 40 apply (cases cap, simp_all add: derive_cap_def is_zombie_def) 41 apply ((wpsimp wp: ensure_no_children_inv simp: o_def)+)[11] 42 apply (rename_tac arch_cap) 43 apply (case_tac arch_cap, simp_all add: arch_derive_cap_def) 44 apply (wpsimp simp: o_def)+ 45 done 46 47 48lemma derive_cap_zobjrefs [CNodeInv_AI_assms]: 49 "\<lbrace>\<lambda>s. P (zobj_refs cap)\<rbrace> derive_cap slot cap \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (zobj_refs rv)\<rbrace>,-" 50 apply (cases cap, simp_all add: derive_cap_def is_zombie_def) 51 apply ((wpsimp wp: ensure_no_children_inv simp: o_def)+)[11] 52 apply (rename_tac arch_cap) 53 apply (case_tac arch_cap, simp_all add: arch_derive_cap_def) 54 apply (wpsimp simp: o_def)+ 55 done 56 57lemma update_cap_objrefs [CNodeInv_AI_assms]: 58 "\<lbrakk> update_cap_data P dt cap \<noteq> NullCap \<rbrakk> \<Longrightarrow> 59 obj_refs (update_cap_data P dt cap) = obj_refs cap" 60 by (case_tac cap, 61 simp_all add: update_cap_data_closedform 62 split: if_split_asm) 63 64 65lemma update_cap_zobjrefs [CNodeInv_AI_assms]: 66 "\<lbrakk> update_cap_data P dt cap \<noteq> cap.NullCap \<rbrakk> \<Longrightarrow> 67 zobj_refs (update_cap_data P dt cap) = zobj_refs cap" 68 apply (case_tac cap, 69 simp_all add: update_cap_data_closedform arch_update_cap_data_def 70 split: if_split_asm) 71 done 72 73 74lemma copy_mask [simp, CNodeInv_AI_assms]: 75 "copy_of (mask_cap R c) = copy_of c" 76 apply (rule ext) 77 apply (auto simp: copy_of_def is_cap_simps mask_cap_def 78 cap_rights_update_def same_object_as_def 79 bits_of_def acap_rights_update_def 80 split: cap.splits arch_cap.splits) 81 done 82 83lemma update_cap_data_mask_Null [simp, CNodeInv_AI_assms]: 84 "(update_cap_data P x (mask_cap m c) = NullCap) = (update_cap_data P x c = NullCap)" 85 unfolding update_cap_data_def mask_cap_def 86 apply (cases c) 87 by (auto simp add: the_cnode_cap_def Let_def is_cap_simps cap_rights_update_def badge_update_def 88 arch_update_cap_data_def) 89 90lemma cap_master_update_cap_data [CNodeInv_AI_assms]: 91 "\<lbrakk> update_cap_data P x c \<noteq> NullCap \<rbrakk> 92 \<Longrightarrow> cap_master_cap (update_cap_data P x c) = cap_master_cap c" 93 apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) 94 apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def 95 badge_update_def arch_update_cap_data_def 96 split: arch_cap.split) 97 done 98 99 100lemma same_object_as_def2: 101 "same_object_as cp cp' = (cap_master_cap cp = cap_master_cap cp' 102 \<and> \<not> cp = NullCap \<and> \<not> is_untyped_cap cp 103 \<and> \<not> is_zombie cp 104 \<and> (is_arch_cap cp \<longrightarrow> 105 (case the_arch_cap cp of PageCap dev x rs sz v 106 \<Rightarrow> x \<le> x + 2 ^ pageBitsForSize sz - 1 107 | _ \<Rightarrow> True)))" 108 apply (simp add: same_object_as_def is_cap_simps split: cap.split) 109 apply (auto simp: cap_master_cap_def bits_of_def 110 split: arch_cap.split_asm) 111 apply (auto split: arch_cap.split) 112 done 113 114 115lemma same_object_as_cap_master [CNodeInv_AI_assms]: 116 "same_object_as cap cap' \<Longrightarrow> cap_master_cap cap = cap_master_cap cap'" 117 by (simp add: same_object_as_def2) 118 119 120lemma weak_derived_cap_is_device[CNodeInv_AI_assms]: 121 "\<lbrakk>weak_derived c' c\<rbrakk> \<Longrightarrow> cap_is_device c = cap_is_device c'" 122 apply (auto simp: weak_derived_def copy_of_def is_cap_simps 123 same_object_as_def2 124 split: if_split_asm 125 dest!: master_cap_eq_is_device_cap_eq) 126 done 127 128lemma cap_asid_update_cap_data [CNodeInv_AI_assms]: 129 "update_cap_data P x c \<noteq> NullCap 130 \<Longrightarrow> cap_asid (update_cap_data P x c) = cap_asid c" 131 apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) 132 apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def 133 badge_update_def arch_update_cap_data_def 134 split: arch_cap.split) 135 done 136 137lemma cap_vptr_update_cap_data [CNodeInv_AI_assms]: 138 "update_cap_data P x c \<noteq> NullCap 139 \<Longrightarrow> cap_vptr (update_cap_data P x c) = cap_vptr c" 140 apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) 141 apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def 142 badge_update_def arch_update_cap_data_def 143 split: arch_cap.split) 144 done 145 146lemma cap_asid_base_update_cap_data [CNodeInv_AI_assms]: 147 "update_cap_data P x c \<noteq> NullCap 148 \<Longrightarrow> cap_asid_base (update_cap_data P x c) = cap_asid_base c" 149 apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) 150 apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def 151 badge_update_def arch_update_cap_data_def 152 split: arch_cap.split) 153 done 154 155lemma same_object_as_update_cap_data [CNodeInv_AI_assms]: 156 "\<lbrakk> update_cap_data P x c \<noteq> NullCap; same_object_as c' c \<rbrakk> \<Longrightarrow> 157 same_object_as c' (update_cap_data P x c)" 158 apply (clarsimp simp: same_object_as_def is_cap_simps 159 split: cap.split_asm arch_cap.splits if_split_asm) 160 apply (simp add: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps arch_update_cap_data_def 161 Let_def split_def the_cnode_cap_def bits_of_def split: if_split_asm cap.splits)+ 162 done 163 164lemma weak_derived_update_cap_data [CNodeInv_AI_assms]: 165 "\<lbrakk>update_cap_data P x c \<noteq> NullCap; weak_derived c c'\<rbrakk> 166 \<Longrightarrow> weak_derived (update_cap_data P x c) c'" 167 apply (simp add: weak_derived_def copy_of_def 168 cap_master_update_cap_data cap_asid_update_cap_data 169 cap_asid_base_update_cap_data 170 cap_vptr_update_cap_data 171 del: cap_asid_base_simps cap_vptr_simps cap_asid_simps 172 split del: if_split cong: if_cong) 173 apply (erule disjE) 174 apply (clarsimp split: if_split_asm) 175 apply (erule disjE) 176 apply (clarsimp simp: is_cap_simps) 177 apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps) 178 apply (erule disjE) 179 apply (clarsimp simp: is_cap_simps) 180 apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps) 181 apply (clarsimp simp: is_cap_simps) 182 apply (simp add: update_cap_data_def arch_update_cap_data_def is_cap_simps) 183 apply (erule (1) same_object_as_update_cap_data) 184 apply clarsimp 185 apply (rule conjI, clarsimp simp: is_cap_simps update_cap_data_def split del: if_split)+ 186 apply clarsimp 187 apply (clarsimp simp: same_object_as_def is_cap_simps 188 split: cap.split_asm arch_cap.splits if_split_asm) 189 apply (simp add: update_cap_data_def badge_update_def cap_rights_update_def is_cap_simps arch_update_cap_data_def 190 Let_def split_def the_cnode_cap_def bits_of_def split: if_split_asm cap.splits)+ 191 done 192 193lemma cap_badge_update_cap_data [CNodeInv_AI_assms]: 194 "update_cap_data False x c \<noteq> NullCap \<and> (bdg, cap_badge c) \<in> capBadge_ordering False 195 \<longrightarrow> (bdg, cap_badge (update_cap_data False x c)) \<in> capBadge_ordering False" 196 apply clarsimp 197 apply (erule capBadge_ordering_trans) 198 apply (simp add: update_cap_data_def split del: if_split split: if_split_asm) 199 apply (auto simp: is_cap_simps Let_def the_cnode_cap_def cap_master_cap_def 200 badge_update_def arch_update_cap_data_def 201 split: arch_cap.split) 202 done 203 204 205lemma cap_vptr_rights_update[simp, CNodeInv_AI_assms]: 206 "cap_vptr (cap_rights_update f c) = cap_vptr c" 207 by (simp add: cap_vptr_def cap_rights_update_def acap_rights_update_def 208 split: cap.splits arch_cap.splits) 209 210lemma cap_vptr_mask[simp, CNodeInv_AI_assms]: 211 "cap_vptr (mask_cap m c) = cap_vptr c" 212 by (simp add: mask_cap_def del: cap_vptr_simps) 213 214lemma cap_asid_base_rights [simp, CNodeInv_AI_assms]: 215 "cap_asid_base (cap_rights_update R c) = cap_asid_base c" 216 by (simp add: cap_rights_update_def acap_rights_update_def 217 split: cap.splits arch_cap.splits) 218 219lemma cap_asid_base_mask[simp, CNodeInv_AI_assms]: 220 "cap_asid_base (mask_cap m c) = cap_asid_base c" 221 by (simp add: mask_cap_def del: cap_asid_base_simps) 222 223lemma weak_derived_mask [CNodeInv_AI_assms]: 224 "\<lbrakk> weak_derived c c'; cap_aligned c \<rbrakk> \<Longrightarrow> weak_derived (mask_cap m c) c'" 225 unfolding weak_derived_def 226 apply (simp del: cap_asid_base_simps cap_vptr_simps cap_asid_simps) 227 apply (erule disjE) 228 apply simp 229 apply (simp add: mask_cap_def cap_rights_update_def 230 copy_of_def same_object_as_def bits_of_def 231 is_cap_simps acap_rights_update_def 232 split: cap.split arch_cap.split)+ 233 apply (clarsimp simp: cap_aligned_def 234 is_aligned_no_overflow) 235 done 236 237 238lemma vs_cap_ref_update_cap_data[simp, CNodeInv_AI_assms]: 239 "vs_cap_ref (update_cap_data P d cap) = vs_cap_ref cap" 240 by (simp add: vs_cap_ref_def update_cap_data_closedform 241 arch_update_cap_data_def 242 split: cap.split) 243 244 245lemma in_preempt[simp, intro, CNodeInv_AI_assms]: 246 "(Inr rv, s') \<in> fst (preemption_point s) \<Longrightarrow> 247 (\<exists>f es. s' = s \<lparr> machine_state := machine_state s \<lparr> irq_state := f (irq_state (machine_state s)) \<rparr>, exst := es\<rparr>)" 248 apply (clarsimp simp: preemption_point_def in_monad do_machine_op_def 249 return_def returnOk_def throwError_def o_def 250 select_f_def select_def getActiveIRQ_def) 251 done 252 253 254lemma invs_irq_state_independent[intro!, simp, CNodeInv_AI_assms]: 255 "invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) 256 = invs s" 257 apply (clarsimp simp: irq_state_independent_A_def invs_def 258 valid_state_def valid_pspace_def valid_mdb_def valid_ioc_def valid_idle_def 259 only_idle_def if_unsafe_then_cap_def valid_reply_caps_def 260 valid_reply_masters_def valid_global_refs_def valid_arch_state_def 261 valid_irq_node_def valid_irq_handlers_def valid_machine_state_def 262 valid_arch_caps_def 263 valid_kernel_mappings_def equal_kernel_mappings_def 264 valid_asid_map_def 265 pspace_in_kernel_window_def cap_refs_in_kernel_window_def 266 cur_tcb_def sym_refs_def state_refs_of_def state_hyp_refs_of_def vspace_at_asid_def 267 swp_def valid_irq_states_def split: option.splits) 268 done 269 270 271lemma cte_at_nat_to_cref_zbits [CNodeInv_AI_assms]: 272 "\<lbrakk> s \<turnstile> Zombie oref zb n; m < n \<rbrakk> 273 \<Longrightarrow> cte_at (oref, nat_to_cref (zombie_cte_bits zb) m) s" 274 apply (subst(asm) valid_cap_def) 275 apply (cases zb, simp_all add: valid_cap_def) 276 apply (clarsimp simp: obj_at_def is_tcb) 277 apply (drule(1) tcb_cap_cases_lt [OF order_less_le_trans]) 278 apply clarsimp 279 apply (rule cte_wp_at_tcbI, fastforce+) 280 apply (clarsimp elim!: cap_table_at_cte_at simp: cap_aligned_def) 281 apply (simp add: nat_to_cref_def word_bits_conv) 282 done 283 284 285lemma copy_of_cap_range [CNodeInv_AI_assms]: 286 "copy_of cap cap' \<Longrightarrow> cap_range cap = cap_range cap'" 287 apply (clarsimp simp: copy_of_def split: if_split_asm) 288 apply (cases cap', simp_all add: same_object_as_def) 289 apply (clarsimp simp: is_cap_simps bits_of_def cap_range_def 290 split: cap.split_asm)+ 291 apply (rename_tac acap' acap) 292 apply (case_tac acap, simp_all) 293 apply (clarsimp split: arch_cap.split_asm cap.split_asm)+ 294 done 295 296 297lemma copy_of_zobj_refs [CNodeInv_AI_assms]: 298 "copy_of cap cap' \<Longrightarrow> zobj_refs cap = zobj_refs cap'" 299 apply (clarsimp simp: copy_of_def split: if_split_asm) 300 apply (cases cap', simp_all add: same_object_as_def) 301 apply (clarsimp simp: is_cap_simps bits_of_def 302 split: cap.split_asm)+ 303 apply (rename_tac acap' acap) 304 apply (case_tac acap, simp_all) 305 apply (clarsimp split: arch_cap.split_asm cap.split_asm)+ 306 done 307 308 309lemma vs_cap_ref_master [CNodeInv_AI_assms]: 310 "\<lbrakk> cap_master_cap cap = cap_master_cap cap'; 311 cap_asid cap = cap_asid cap'; 312 cap_asid_base cap = cap_asid_base cap'; 313 cap_vptr cap = cap_vptr cap' \<rbrakk> 314 \<Longrightarrow> vs_cap_ref cap = vs_cap_ref cap'" 315 apply (rule ccontr) 316 apply (clarsimp simp: vs_cap_ref_def cap_master_cap_def 317 split: cap.split_asm) 318 apply (clarsimp simp: cap_asid_def split: arch_cap.split_asm option.split_asm) 319 done 320 321lemma weak_derived_vs_cap_ref [CNodeInv_AI_assms]: 322 "weak_derived c c' \<Longrightarrow> vs_cap_ref c = vs_cap_ref c'" 323 by (auto simp: weak_derived_def copy_of_def 324 same_object_as_def2 325 split: if_split_asm elim: vs_cap_ref_master[OF sym]) 326 327lemma weak_derived_table_cap_ref [CNodeInv_AI_assms]: 328 "weak_derived c c' \<Longrightarrow> table_cap_ref c = table_cap_ref c'" 329 apply (clarsimp simp: weak_derived_def copy_of_def 330 same_object_as_def2 331 split: if_split_asm) 332 apply (elim disjE,simp_all add:is_cap_simps) 333 apply (elim disjE,simp_all) 334 apply clarsimp 335 apply (frule vs_cap_ref_master[OF sym],simp+) 336 apply (drule vs_cap_ref_eq_imp_table_cap_ref_eq') 337 apply simp 338 apply simp 339 done 340 341 342lemma weak_derived_pd_pt_asid: 343 "weak_derived c c' \<Longrightarrow> cap_asid c = cap_asid c' 344 \<and> is_pt_cap c = is_pt_cap c' 345 \<and> is_pd_cap c = is_pd_cap c'" 346 by (auto simp: weak_derived_def copy_of_def is_cap_simps 347 same_object_as_def2 is_pt_cap_def 348 cap_master_cap_simps 349 split: if_split_asm 350 dest!: cap_master_cap_eqDs) 351 352lemma weak_derived_ASIDPool1: 353 "weak_derived (cap.ArchObjectCap (ASIDPoolCap ap asid)) cap = 354 (cap = cap.ArchObjectCap (ASIDPoolCap ap asid))" 355 apply (rule iffI) 356 prefer 2 357 apply simp 358 apply (clarsimp simp: weak_derived_def copy_of_def split: if_split_asm) 359 apply (clarsimp simp: same_object_as_def2 cap_master_cap_simps dest!: cap_master_cap_eqDs) 360 done 361 362lemma weak_derived_ASIDPool2: 363 "weak_derived cap (ArchObjectCap (ASIDPoolCap ap asid)) = 364 (cap = ArchObjectCap (ASIDPoolCap ap asid))" 365 apply (rule iffI) 366 prefer 2 367 apply simp 368 apply (clarsimp simp: weak_derived_def copy_of_def split: if_split_asm) 369 apply (auto simp: same_object_as_def2 cap_master_cap_simps dest!: cap_master_cap_eqDs) 370 done 371 372lemmas weak_derived_ASIDPool [simp] = 373 weak_derived_ASIDPool1 weak_derived_ASIDPool2 374 375 376lemma swap_of_caps_valid_arch_caps [CNodeInv_AI_assms]: 377 "\<lbrace>valid_arch_caps and 378 cte_wp_at (weak_derived c) a and 379 cte_wp_at (weak_derived c') b\<rbrace> 380 do 381 y \<leftarrow> set_cap c b; 382 set_cap c' a 383 od 384 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 385 apply (rule hoare_pre) 386 apply (simp add: valid_arch_caps_def 387 valid_vs_lookup_def valid_table_caps_def pred_conj_def 388 del: split_paired_Ex split_paired_All imp_disjL) 389 apply (wp hoare_vcg_all_lift hoare_convert_imp[OF set_cap.vs_lookup_pages] 390 hoare_vcg_disj_lift hoare_convert_imp[OF set_cap_caps_of_state] 391 hoare_use_eq[OF set_cap_arch set_cap_obj_at_impossible[where P="\<lambda>x. x"]]) 392 apply (clarsimp simp: valid_arch_caps_def cte_wp_at_caps_of_state 393 simp del: split_paired_Ex split_paired_All imp_disjL) 394 apply (frule weak_derived_obj_refs[where dcap=c]) 395 apply (frule weak_derived_obj_refs[where dcap=c']) 396 apply (frule weak_derived_pd_pt_asid[where c=c]) 397 apply (frule weak_derived_pd_pt_asid[where c=c']) 398 apply (intro conjI) 399 apply (simp add: valid_vs_lookup_def del: split_paired_Ex split_paired_All) 400 apply (elim allEI) 401 apply (intro impI disjCI2) 402 apply (simp del: split_paired_Ex split_paired_All) 403 apply (elim conjE) 404 apply (erule exfEI[where f="id (a := b, b := a)"]) 405 apply (auto dest!: weak_derived_vs_cap_ref)[1] 406 apply (simp add: valid_table_caps_def empty_table_caps_of 407 del: split_paired_Ex split_paired_All imp_disjL) 408 apply (simp add: unique_table_caps_def 409 del: split_paired_Ex split_paired_All imp_disjL 410 split del: if_split) 411 apply (erule allfEI[where f="id (a := b, b := a)"]) 412 apply (erule allfEI[where f="id (a := b, b := a)"]) 413 apply (clarsimp split del: if_split split: if_split_asm) 414 apply (simp add: unique_table_refs_def 415 del: split_paired_All split del: if_split) 416 apply (erule allfEI[where f="id (a := b, b := a)"]) 417 apply (erule allfEI[where f="id (a := b, b := a)"]) 418 apply (clarsimp split del: if_split split: if_split_asm dest!:vs_cap_ref_to_table_cap_ref 419 dest!: weak_derived_table_cap_ref) 420 done 421 422 423lemma cap_swap_asid_map[wp, CNodeInv_AI_assms]: 424 "\<lbrace>valid_asid_map and 425 cte_wp_at (weak_derived c) a and 426 cte_wp_at (weak_derived c') b\<rbrace> 427 cap_swap c a c' b \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" 428 apply (simp add: cap_swap_def set_cdt_def valid_asid_map_def vspace_at_asid_def) 429 apply (rule hoare_pre) 430 apply (wp set_cap.vs_lookup|simp 431 |rule hoare_lift_Pf [where f=arch_state])+ 432 done 433 434 435lemma cap_swap_cap_refs_in_kernel_window[wp, CNodeInv_AI_assms]: 436 "\<lbrace>cap_refs_in_kernel_window and 437 cte_wp_at (weak_derived c) a and 438 cte_wp_at (weak_derived c') b\<rbrace> 439 cap_swap c a c' b \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 440 apply (simp add: cap_swap_def) 441 apply (rule hoare_pre) 442 apply (wp | simp split del: if_split)+ 443 apply (auto dest!: cap_refs_in_kernel_windowD 444 simp: cte_wp_at_caps_of_state weak_derived_cap_range) 445 done 446 447 448lemma cap_swap_vms[wp, CNodeInv_AI_assms]: 449 "\<lbrace>valid_machine_state\<rbrace> cap_swap c a c' b \<lbrace>\<lambda>rv. valid_machine_state\<rbrace>" 450 apply (simp add: valid_machine_state_def in_user_frame_def) 451 apply (wp cap_swap_typ_at 452 hoare_vcg_all_lift hoare_vcg_ex_lift hoare_vcg_disj_lift) 453 done 454 455 456lemma unat_of_bl_nat_to_cref[CNodeInv_AI_assms]: 457 "\<lbrakk> n < 2 ^ len; len < word_bits \<rbrakk> 458 \<Longrightarrow> unat (of_bl (nat_to_cref len n) :: word32) = n" 459 apply (simp add: nat_to_cref_def word_bits_conv of_drop_to_bl 460 word_size) 461 apply (subst less_mask_eq) 462 apply (rule order_less_le_trans) 463 apply (erule of_nat_mono_maybe[rotated]) 464 apply (rule power_strict_increasing) 465 apply simp 466 apply simp 467 apply simp 468 apply (rule unat_of_nat32) 469 apply (erule order_less_trans) 470 apply (rule power_strict_increasing) 471 apply (simp add: word_bits_conv) 472 apply simp 473 done 474 475lemma zombie_is_cap_toE_pre[CNodeInv_AI_assms]: 476 "\<lbrakk> s \<turnstile> Zombie ptr zbits n; invs s; m < n \<rbrakk> 477 \<Longrightarrow> (ptr, nat_to_cref (zombie_cte_bits zbits) m) \<in> cte_refs (Zombie ptr zbits n) irqn" 478 apply (clarsimp simp add: valid_cap_def cap_aligned_def) 479 apply (clarsimp split: option.split_asm) 480 apply (simp add: unat_of_bl_nat_to_cref) 481 apply (simp add: nat_to_cref_def word_bits_conv) 482 apply (simp add: unat_of_bl_nat_to_cref) 483 apply (simp add: nat_to_cref_def word_bits_conv) 484 done 485 486crunch st_tcb_at_halted[wp]: prepare_thread_delete "st_tcb_at halted t" 487 (wp: dissociate_vcpu_tcb_pred_tcb_at) 488 489lemma finalise_cap_makes_halted_proof: 490 "\<lbrace>invs and valid_cap cap and (\<lambda>s. ex = is_final_cap' cap s) 491 and cte_wp_at ((=) cap) slot\<rbrace> 492 finalise_cap cap ex 493 \<lbrace>\<lambda>rv s. \<forall>t \<in> obj_refs (fst rv). halted_if_tcb t s\<rbrace>" 494 apply (case_tac cap, simp_all) 495 apply (wp unbind_notification_valid_objs hoare_vcg_conj_lift 496 | clarsimp simp: o_def valid_cap_def cap_table_at_typ 497 is_tcb obj_at_def 498 | clarsimp simp: halted_if_tcb_def 499 split: option.split 500 | intro impI conjI 501 | rule hoare_drop_imp)+ 502 apply (drule_tac final_zombie_not_live; (assumption | simp add: invs_iflive)?) 503 apply (clarsimp simp: pred_tcb_at_def is_tcb obj_at_def live_def, elim disjE) 504 apply (clarsimp; case_tac "tcb_state tcb"; simp)+ 505 apply (rename_tac arch_cap) 506 apply (case_tac arch_cap, simp_all add: arch_finalise_cap_def) 507 apply (wp 508 | clarsimp simp: valid_cap_def obj_at_def is_tcb_def is_cap_table_def 509 split: option.splits bool.split 510 | intro impI conjI)+ 511 done 512 513lemmas finalise_cap_makes_halted = finalise_cap_makes_halted_proof 514 515crunch emptyable[wp, CNodeInv_AI_assms]: finalise_cap "emptyable sl" 516 (simp: crunch_simps rule: emptyable_lift 517 wp: crunch_wps suspend_emptyable unbind_notification_invs 518 unbind_maybe_notification_invs arch_finalise_cap_pred_tcb_at) 519 520lemma finalise_cap_not_reply_master_unlifted [CNodeInv_AI_assms]: 521 "(rv, s') \<in> fst (finalise_cap cap sl s) \<Longrightarrow> 522 \<not> is_master_reply_cap (fst rv)" 523 by (case_tac cap, auto simp: is_cap_simps in_monad liftM_def 524 arch_finalise_cap_def 525 split: if_split_asm arch_cap.split_asm bool.split_asm option.split_asm) 526 527 528lemma nat_to_cref_0_replicate [CNodeInv_AI_assms]: 529 "\<And>n. n < word_bits \<Longrightarrow> nat_to_cref n 0 = replicate n False" 530 apply (subgoal_tac "nat_to_cref n (unat (of_bl (replicate n False))) = replicate n False") 531 apply simp 532 apply (rule nat_to_cref_unat_of_bl') 533 apply (simp add: word_bits_def) 534 apply simp 535 done 536 537 538lemma prepare_thread_delete_thread_cap [CNodeInv_AI_assms]: 539 "\<lbrace>\<lambda>s. caps_of_state s x = Some (cap.ThreadCap p)\<rbrace> 540 prepare_thread_delete t 541 \<lbrace>\<lambda>rv s. caps_of_state s x = Some (cap.ThreadCap p)\<rbrace>" 542 by (wpsimp simp: prepare_thread_delete_def) 543 544lemma cap_swap_ioports[wp, CNodeInv_AI_assms]: 545 "\<lbrace>valid_ioports and cte_wp_at (weak_derived c) a and cte_wp_at (weak_derived c') b\<rbrace> 546 cap_swap c a c' b 547 \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" 548 by wpsimp 549 550end 551 552 553global_interpretation CNodeInv_AI?: CNodeInv_AI 554 proof goal_cases 555 interpret Arch . 556 case 1 show ?case by (unfold_locales; (fact CNodeInv_AI_assms)?) 557 qed 558 559 560termination rec_del by (rule rec_del_termination) 561 562 563context Arch begin global_naming ARM 564 565lemma post_cap_delete_pre_is_final_cap': 566 "\<And>rv s'' rva s''a s. 567 \<lbrakk>valid_ioports s; caps_of_state s slot = Some cap; is_final_cap' cap s; cap_cleanup_opt cap \<noteq> NullCap\<rbrakk> 568 \<Longrightarrow> post_cap_delete_pre (cap_cleanup_opt cap) (caps_of_state s(slot \<mapsto> NullCap))" 569 apply (clarsimp simp: cap_cleanup_opt_def cte_wp_at_def post_cap_delete_pre_def arch_cap_cleanup_opt_def 570 split: cap.split_asm if_split_asm 571 elim!: ranE dest!: caps_of_state_cteD) 572 (* IRQHandlerCap case *) 573 apply (drule(2) final_cap_duplicate_irq) 574 apply simp+ 575 done 576 577lemma rec_del_invs'': 578 notes Inr_in_liftE_simp[simp del] 579 assumes set_cap_Q[wp]: "\<And>cap p. \<lbrace>Q and invs\<rbrace> set_cap cap p \<lbrace>\<lambda>_.Q\<rbrace>" 580 assumes empty_slot_Q[wp]: "\<And>slot free_irq. \<lbrace>Q and invs\<rbrace> empty_slot slot free_irq\<lbrace>\<lambda>_.Q\<rbrace>" 581 assumes finalise_cap_Q[wp]: "\<And>cap final. \<lbrace>Q and invs\<rbrace> finalise_cap cap final \<lbrace>\<lambda>_.Q\<rbrace>" 582 assumes cap_swap_for_delete_Q[wp]: "\<And>a b. \<lbrace>Q and invs and cte_at a and cte_at b and K (a \<noteq> b)\<rbrace> 583 cap_swap_for_delete a b 584 \<lbrace>\<lambda>_.Q\<rbrace>" 585 assumes preemption_point_Q: "\<And>cap final. \<lbrace>Q and invs\<rbrace> preemption_point \<lbrace>\<lambda>_.Q\<rbrace>" 586 shows 587 "s \<turnstile> \<lbrace>Q and invs and valid_rec_del_call call 588 and (\<lambda>s. \<not> exposed_rdcall call 589 \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) 590 (slot_rdcall call) s) 591 and emptyable (slot_rdcall call) 592 and (\<lambda>s. case call of ReduceZombieCall cap sl ex \<Rightarrow> 593 \<not> cap_removeable cap sl 594 \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) 595 | _ \<Rightarrow> True)\<rbrace> 596 rec_del call 597 \<lbrace>\<lambda>rv s. Q s \<and> invs s \<and> 598 (case call of FinaliseSlotCall sl x \<Rightarrow> 599 ((fst rv \<or> x) \<longrightarrow> cte_wp_at (replaceable s sl cap.NullCap) sl s) 600 \<and> (snd rv \<noteq> NullCap \<longrightarrow> 601 post_cap_delete_pre (snd rv) ((caps_of_state s) (sl \<mapsto> cap.NullCap))) 602 | ReduceZombieCall cap sl x \<Rightarrow> 603 (\<not> x \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) sl s) 604 | _ \<Rightarrow> True) \<and> 605 emptyable (slot_rdcall call) s\<rbrace>, 606 \<lbrace>\<lambda>rv. Q and invs\<rbrace>" 607proof (induct rule: rec_del.induct, 608 simp_all only: rec_del_fails) 609 case (1 slot exposed s) 610 show ?case 611 apply (subst rec_del.simps) 612 apply (simp only: split_def) 613 apply wp+ 614 apply (simp(no_asm)) 615 apply (wp empty_slot_invs empty_slot_emptyable)[1] 616 apply (rule hoare_pre_spec_validE) 617 apply (rule spec_strengthen_postE, unfold slot_rdcall.simps) 618 apply (rule "1.hyps"[simplified rec_del_call.simps slot_rdcall.simps]) 619 apply clarsimp 620 apply (auto simp: cte_wp_at_caps_of_state) 621 done 622next 623 case (2 slot exposed s) 624 show ?case 625 apply (subst rec_del.simps) 626 apply (simp only: split_def) 627 apply (rule split_spec_bindE[rotated]) 628 apply (rule drop_spec_validE, simp) 629 apply (rule get_cap_sp) 630 apply (rule hoare_pre_spec_validE) 631 apply (wp replace_cap_invs | simp)+ 632 apply (erule finalise_cap_not_reply_master) 633 apply (wp "2.hyps" | assumption)+ 634 apply (wp preemption_point_Q | simp)+ 635 apply (wp preemption_point_inv, simp+) 636 apply (wp preemption_point_Q) 637 apply ((wp preemption_point_inv irq_state_independent_A_conjI irq_state_independent_AI 638 emptyable_irq_state_independent invs_irq_state_independent 639 | simp add: valid_rec_del_call_def irq_state_independent_A_def)+)[1] 640 apply (simp(no_asm)) 641 apply (rule spec_strengthen_postE) 642 apply (rule "2.hyps"[simplified rec_del_call.simps slot_rdcall.simps conj_assoc], assumption+) 643 apply (simp add: cte_wp_at_eq_simp 644 | wp replace_cap_invs set_cap_sets final_cap_same_objrefs 645 set_cap_cte_cap_wp_to static_imp_wp 646 | erule finalise_cap_not_reply_master)+ 647 apply (wp hoare_vcg_const_Ball_lift)+ 648 apply (rule hoare_strengthen_post) 649 apply (rule_tac Q="\<lambda>fin s. Q s \<and> invs s \<and> replaceable s slot (fst fin) rv 650 \<and> cte_wp_at ((=) rv) slot s \<and> s \<turnstile> (fst fin) 651 \<and> ex_cte_cap_wp_to (appropriate_cte_cap rv) slot s 652 \<and> emptyable slot s 653 \<and> (\<forall>t\<in>obj_refs (fst fin). halted_if_tcb t s)" 654 in hoare_vcg_conj_lift) 655 apply (wp finalise_cap_invs[where slot=slot] 656 finalise_cap_replaceable[where sl=slot] 657 finalise_cap_makes_halted[where slot=slot])[1] 658 apply (rule finalise_cap_cases[where slot=slot]) 659 apply (clarsimp simp: cte_wp_at_caps_of_state) 660 apply (erule disjE) 661 apply clarsimp 662 apply (rule post_cap_delete_pre_is_final_cap', clarsimp+) 663 apply (rule conjI, clarsimp) 664 apply (subst replaceable_def) 665 apply (clarsimp simp: is_cap_simps tcb_cap_valid_NullCapD 666 no_cap_to_obj_with_diff_ref_Null gen_obj_refs_eq 667 del: disjCI) 668 apply (thin_tac "appropriate_cte_cap a = appropriate_cte_cap b" for a b) 669 apply (rule conjI) 670 apply (clarsimp simp: replaceable_def) 671 apply (erule disjE) 672 apply (simp only: zobj_refs.simps mem_simps) 673 apply clarsimp+ 674 apply (drule sym, simp) 675 apply (drule sym, simp) 676 apply clarsimp 677 apply (simp add: unat_eq_0) 678 apply (drule of_bl_eq_0) 679 apply (drule zombie_cte_bits_less, simp add: word_bits_def) 680 apply (clarsimp simp: cte_wp_at_caps_of_state) 681 apply (drule_tac s="appropriate_cte_cap c" for c in sym) 682 apply (clarsimp simp: is_cap_simps appropriate_Zombie gen_obj_refs_eq) 683 apply (simp add: is_final_cap_def) 684 apply wp 685 apply (clarsimp simp: cte_wp_at_eq_simp) 686 apply (rule conjI) 687 apply (clarsimp simp: cte_wp_at_caps_of_state replaceable_def) 688 apply (frule cte_wp_at_valid_objs_valid_cap, clarsimp+) 689 apply (frule invs_valid_asid_table) 690 apply (frule invs_sym_refs) 691 apply (clarsimp simp add: invs_def valid_state_def 692 invs_valid_objs invs_psp_aligned) 693 apply (drule(1) if_unsafe_then_capD, clarsimp+) 694 done 695next 696 have replicate_helper: 697 "\<And>x n. True \<in> set x \<Longrightarrow> replicate n False \<noteq> x" 698 by (clarsimp simp: replicate_not_True) 699 case (3 ptr bits n slot s) 700 show ?case 701 apply simp 702 apply wp+ 703 apply clarsimp 704 apply (rule context_conjI') 705 apply (rule context_conjI') 706 apply (rule conjI) 707 apply (erule zombie_is_cap_toE2) 708 apply simp+ 709 apply (clarsimp simp: halted_emptyable) 710 apply (rule conjI, clarsimp simp: cte_wp_at_caps_of_state) 711 apply (erule tcb_valid_nonspecial_cap) 712 apply fastforce 713 apply (clarsimp simp: ran_tcb_cap_cases is_cap_simps is_nondevice_page_cap_simps 714 split: Structures_A.thread_state.splits) 715 apply (clarsimp simp: is_cap_simps is_nondevice_page_cap_simps) 716 apply (rule conjI) 717 apply (drule cte_wp_valid_cap, clarsimp) 718 apply (frule cte_at_nat_to_cref_zbits [where m=0], simp) 719 apply (rule cte_wp_at_not_reply_master) 720 apply (simp add: replicate_helper tcb_cnode_index_def) 721 apply (subst(asm) nat_to_cref_0_replicate) 722 apply (simp add: zombie_cte_bits_less) 723 apply assumption 724 apply clarsimp 725 apply (simp add: invs_def valid_state_def) 726 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) 727 apply (erule cte_wp_at_weakenE | clarsimp)+ 728 done 729next 730 have nat_helper: 731 "\<And>x n. \<lbrakk> x < Suc n; x \<noteq> n \<rbrakk> \<Longrightarrow> x < n" 732 by (simp add: le_simps) 733 case (4 ptr bits n slot s) 734 show ?case 735 apply simp 736 apply (rule hoare_pre_spec_validE) 737 apply (wp replace_cap_invs | simp add: is_cap_simps)+ 738 apply (rule_tac Q="\<lambda>rv s. Q s \<and> invs s \<and> cte_wp_at (\<lambda>cap. cap = rv) slot s 739 \<and> cte_wp_at (\<lambda>cap. cap = cap.NullCap 740 \<or> \<not> False \<and> is_zombie cap 741 \<and> (ptr, nat_to_cref (zombie_cte_bits bits) n) 742 \<in> fst_cte_ptrs cap) 743 (ptr, nat_to_cref (zombie_cte_bits bits) n) s 744 \<and> \<not> cap_removeable (cap.Zombie ptr bits (Suc n)) slot" 745 in hoare_post_imp) 746 apply (thin_tac "(a, b) \<in> fst c" for a b c) 747 apply clarsimp 748 apply (frule cte_wp_at_emptyableD, clarsimp, assumption) 749 apply (rule conjI[rotated], (clarsimp simp: is_cap_simps)+) 750 apply (frule cte_wp_at_valid_objs_valid_cap, clarsimp+) 751 apply (frule if_unsafe_then_capD, clarsimp+) 752 apply (rule conjI) 753 apply (frule zombies_finalD, (clarsimp simp: is_cap_simps)+) 754 apply (clarsimp simp: cte_wp_at_caps_of_state) 755 apply (erule disjE[where P="val = cap.NullCap" for val]) 756 apply (clarsimp simp: replaceable_def cap_range_def is_cap_simps 757 gen_obj_refs_subset vs_cap_ref_def) 758 apply (rule conjI[rotated]) 759 apply (rule conjI) 760 apply (rule mp [OF tcb_cap_valid_imp']) 761 apply (fastforce simp: ran_tcb_cap_cases is_cap_simps 762 is_pt_cap_def vs_cap_ref_def 763 is_nondevice_page_cap_simps 764 valid_ipc_buffer_cap_def 765 split: Structures_A.thread_state.splits) 766 apply (drule unique_table_refs_no_cap_asidD) 767 apply (simp add: invs_def valid_state_def valid_arch_caps_def) 768 apply (simp add: no_cap_to_obj_with_diff_ref_def Ball_def 769 table_cap_ref_def) 770 apply clarsimp 771 apply (rule ccontr, erule notE, erule nat_helper) 772 apply clarsimp 773 apply (erule disjE[where Q="val = slot" for val]) 774 apply (clarsimp simp: cte_wp_at_caps_of_state) 775 apply (erule notE[rotated, where P="val = Some cap.NullCap" for val]) 776 apply (drule sym, simp, subst nat_to_cref_unat_of_bl) 777 apply (drule zombie_cte_bits_less, simp add: word_bits_def) 778 apply assumption 779 apply clarsimp 780 apply (drule sym, simp) 781 apply (subst(asm) nat_to_cref_unat_of_bl) 782 apply (drule zombie_cte_bits_less, simp add: word_bits_conv) 783 apply simp 784 apply (clarsimp simp: is_final_cap'_def3 simp del: split_paired_All) 785 apply (frule_tac x=slot in spec) 786 apply (drule_tac x="(ptr, nat_to_cref (zombie_cte_bits bits) n)" in spec) 787 apply (clarsimp simp: cte_wp_at_caps_of_state fst_cte_ptrs_def 788 gen_obj_refs_Int) 789 apply (drule(1) nat_to_cref_replicate_Zombie[OF sym]) 790 apply simp 791 apply simp 792 apply (clarsimp simp: valid_cap_def cap_aligned_def is_cap_simps 793 cte_wp_at_cte_at appropriate_Zombie 794 split: option.split_asm) 795 apply (wp get_cap_cte_wp_at)[1] 796 apply simp 797 apply (subst conj_assoc[symmetric]) 798 apply (rule spec_valid_conj_liftE2) 799 apply (wp rec_del_delete_cases[where ex=False, simplified])[1] 800 apply (rule spec_strengthen_postE) 801 apply (rule "4.hyps"[simplified rec_del_call.simps slot_rdcall.simps simp_thms pred_conj_def]) 802 apply (simp add: in_monad) 803 apply simp 804 apply (clarsimp simp: halted_emptyable) 805 apply (erule(1) zombie_is_cap_toE) 806 apply simp 807 apply simp 808 done 809qed 810 811 812lemmas rec_del_invs'[CNodeInv_AI_assms] = rec_del_invs'' [where Q=\<top>, 813 simplified hoare_post_taut pred_conj_def simp_thms, OF TrueI TrueI TrueI TrueI, simplified] 814 815end 816 817 818global_interpretation CNodeInv_AI_2?: CNodeInv_AI_2 819 proof goal_cases 820 interpret Arch . 821 case 1 show ?case by (unfold_locales; (fact CNodeInv_AI_assms)?) 822 qed 823 824 825context Arch begin global_naming ARM 826 827crunch rvk_prog: prepare_thread_delete "\<lambda>s. revoke_progress_ord m (\<lambda>x. option_map cap_to_rpo (caps_of_state s x))" 828 (simp: crunch_simps o_def unless_def is_final_cap_def 829 wp: crunch_wps empty_slot_rvk_prog' select_wp ignore: dissociate_vcpu_tcb) 830 831lemma finalise_cap_rvk_prog [CNodeInv_AI_assms]: 832 "\<lbrace>\<lambda>s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace> 833 finalise_cap a b 834 \<lbrace>\<lambda>_ s. revoke_progress_ord m (\<lambda>x. map_option cap_to_rpo (caps_of_state s x))\<rbrace>" 835 apply (case_tac a,simp_all add:liftM_def) 836 apply (wp suspend_rvk_prog deleting_irq_handler_rvk_prog 837 | clarsimp simp:is_final_cap_def comp_def)+ 838 done 839 840 841lemma rec_del_rvk_prog [CNodeInv_AI_assms]: 842 "st \<turnstile> \<lbrace>\<lambda>s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s) 843 \<and> (case args of ReduceZombieCall cap sl ex \<Rightarrow> 844 cte_wp_at (\<lambda>c. c = cap) sl s \<and> is_final_cap' cap s 845 | _ \<Rightarrow> True)\<rbrace> 846 rec_del args 847 \<lbrace>\<lambda>rv s. revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)\<rbrace>,\<lbrace>\<top>\<top>\<rbrace>" 848proof (induct rule: rec_del.induct, 849 simp_all only: rec_del_fails) 850 case (1 slot exposed s) 851 note wp = "1.hyps"[simplified rdcall_simps simp_thms] 852 show ?case 853 apply (subst rec_del.simps) 854 apply (simp only: rdcall_simps simp_thms split_def) 855 apply wp 856 apply (simp(no_asm) del: o_apply) 857 apply (wp empty_slot_rvk_prog)[1] 858 apply (simp del: o_apply) 859 apply (rule wp) 860 done 861next 862 case (2 sl exp s) 863 note wp = "2.hyps" [simplified rdcall_simps simp_thms] 864 show ?case 865 apply (subst rec_del.simps) 866 apply (simp only: rdcall_simps simp_thms split_def) 867 apply (rule hoare_pre_spec_validE) 868 apply wp 869 apply ((wp | simp)+)[1] 870 apply (wp wp | assumption)+ 871 apply ((wp preemption_point_inv | simp)+)[1] 872 apply (simp(no_asm)) 873 apply (rule wp, assumption+) 874 apply (wp final_cap_same_objrefs 875 set_cap_cte_wp_at_cases 876 | simp)+ 877 apply (rule hoare_strengthen_post) 878 apply (rule_tac Q="\<lambda>fc s. cte_wp_at ((=) rv) sl s 879 \<and> revoke_progress_ord m (option_map cap_to_rpo \<circ> caps_of_state s)" 880 in hoare_vcg_conj_lift) 881 apply (wp finalise_cap_rvk_prog[folded o_def])[1] 882 apply (rule finalise_cap_cases[where slot=sl]) 883 apply (clarsimp simp: o_def) 884 apply (strengthen rvk_prog_update_strg[unfolded fun_upd_def o_def]) 885 apply (clarsimp simp: cte_wp_at_caps_of_state) 886 apply (erule disjE) 887 apply clarsimp 888 apply (clarsimp simp: is_cap_simps) 889 apply (case_tac "is_zombie rv") 890 apply (clarsimp simp: cap_to_rpo_def is_cap_simps fst_cte_ptrs_def) 891 apply (simp add: is_final_cap'_def) 892 apply (case_tac rv, simp_all add: cap_to_rpo_def is_cap_simps gen_obj_refs_eq)[1] 893 apply (rename_tac arch_cap) 894 apply (case_tac arch_cap, simp_all)[1] 895 apply (simp add: is_final_cap_def, wp) 896 apply (simp, wp get_cap_wp) 897 apply (clarsimp simp: o_def) 898 done 899next 900 case (3 ptr bits n slot s) 901 show ?case 902 apply simp 903 apply (fold o_def) 904 apply (rule hoare_pre_spec_validE) 905 apply (simp del: o_apply | wp_once cap_swap_fd_rvk_prog)+ 906 apply (clarsimp simp: cte_wp_at_caps_of_state cap_to_rpo_def) 907 done 908next 909 case (4 ptr zb znum sl s) 910 note wp = "4.hyps"[simplified rdcall_simps] 911 show ?case 912 apply (subst rec_del.simps) 913 apply wp 914 apply (wp | simp)+ 915 apply (wp get_cap_wp)[1] 916 apply (rule spec_strengthen_postE) 917 apply (rule wp, assumption+) 918 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_defs) 919 apply (strengthen rvk_prog_update_strg[unfolded fun_upd_def o_def]) 920 apply (clarsimp simp: cte_wp_at_caps_of_state cap_to_rpo_def) 921 apply (wp | simp add: o_def)+ 922 done 923qed 924 925end 926 927 928global_interpretation CNodeInv_AI_3?: CNodeInv_AI_3 929 proof goal_cases 930 interpret Arch . 931 case 1 show ?case by (unfold_locales; (fact CNodeInv_AI_assms)?) 932 qed 933 934 935termination cap_revoke by (rule cap_revoke_termination) 936 937declare cap_revoke.simps[simp del] 938 939 940context Arch begin global_naming ARM 941 942crunch typ_at[wp, CNodeInv_AI_assms]: finalise_slot "\<lambda>s. P (typ_at T p s)" 943 (wp: crunch_wps simp: crunch_simps filterM_mapM unless_def 944 ignore: without_preemption filterM set_object clearMemory) 945 946 947lemma weak_derived_appropriate [CNodeInv_AI_assms]: 948 "weak_derived cap cap' \<Longrightarrow> appropriate_cte_cap cap = appropriate_cte_cap cap'" 949 by (auto simp: weak_derived_def copy_of_def same_object_as_def2 950 appropriate_cte_master 951 split: if_split_asm 952 dest!: arg_cong[where f=appropriate_cte_cap]) 953 954end 955 956 957global_interpretation CNodeInv_AI_4?: CNodeInv_AI_4 958 proof goal_cases 959 interpret Arch . 960 case 1 show ?case by (unfold_locales; (fact CNodeInv_AI_assms)?) 961 qed 962 963 964context Arch begin global_naming ARM 965 966lemma cap_move_invs[wp, CNodeInv_AI_assms]: 967 "\<lbrace>invs and valid_cap cap and cte_wp_at ((=) cap.NullCap) ptr' 968 and tcb_cap_valid cap ptr' 969 and cte_wp_at (weak_derived cap) ptr 970 and cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) ptr 971 and ex_cte_cap_wp_to (appropriate_cte_cap cap) ptr' and K (ptr \<noteq> ptr') 972 and K (\<not> is_master_reply_cap cap)\<rbrace> 973 cap_move cap ptr ptr' 974 \<lbrace>\<lambda>rv. invs\<rbrace>" 975 unfolding invs_def valid_state_def valid_pspace_def 976 apply (simp add: pred_conj_def conj_comms [where Q = "valid_mdb S" for S]) 977 apply wp 978 apply (wpe cap_move_zombies_final) 979 apply (wpe cap_move_if_live) 980 apply (wpe cap_move_if_unsafe) 981 apply (wpe cap_move_irq_handlers) 982 apply (wpe cap_move_replies) 983 apply (wpe cap_move_valid_arch_caps) 984 apply (wpe cap_move_valid_ioc) 985 apply (simp add: cap_move_def set_cdt_def) 986 apply (wp set_cap_valid_objs set_cap_idle set_cap_typ_at 987 cap_table_at_lift_irq tcb_at_typ_at 988 hoare_vcg_disj_lift hoare_vcg_all_lift 989 set_cap_cap_refs_respects_device_region_NullCap 990 | wp set_cap_cap_refs_respects_device_region_spec[where ptr = ptr] 991 | simp del: split_paired_Ex split_paired_All 992 | simp add: valid_irq_node_def valid_machine_state_def 993 del: split_paired_All split_paired_Ex)+ 994 apply (clarsimp simp: tcb_cap_valid_def cte_wp_at_caps_of_state) 995 apply (frule(1) valid_global_refsD2[where ptr=ptr]) 996 apply (frule(1) cap_refs_in_kernel_windowD[where ptr=ptr]) 997 apply (frule weak_derived_cap_range) 998 apply (frule weak_derived_is_reply_master) 999 apply (simp add: cap_range_NullCap valid_ipc_buffer_cap_def[where c=cap.NullCap]) 1000 apply (simp add: is_cap_simps) 1001 apply (subgoal_tac "tcb_cap_valid cap.NullCap ptr s") 1002 apply (simp add: tcb_cap_valid_def weak_derived_cap_is_device) 1003 apply (rule tcb_cap_valid_NullCapD) 1004 apply (erule(1) tcb_cap_valid_caps_of_stateD) 1005 apply (simp add: is_cap_simps) 1006 done 1007 1008lemma arch_derive_is_arch: 1009 "\<lbrace>\<top>\<rbrace> arch_derive_cap c \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> is_arch_cap rv\<rbrace>,-" 1010 by (wpsimp simp: is_arch_cap_def arch_derive_cap_def) 1011 1012end 1013 1014 1015global_interpretation CNodeInv_AI_5?: CNodeInv_AI_5 1016 proof goal_cases 1017 interpret Arch . 1018 case 1 show ?case by (unfold_locales; (fact CNodeInv_AI_assms)?) 1019 qed 1020 1021 1022end 1023