1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11(* 12ARM-specific CSpace invariants 13*) 14 15theory ArchCSpace_AI 16imports "../CSpace_AI" 17begin 18 19context Arch begin global_naming ARM 20 21named_theorems CSpace_AI_assms 22 23lemma cte_at_length_limit: 24 "\<lbrakk> cte_at p s; valid_objs s \<rbrakk> \<Longrightarrow> length (snd p) < word_bits - cte_level_bits" 25 apply (simp add: cte_at_cases) 26 apply (erule disjE) 27 apply clarsimp 28 apply (erule(1) valid_objsE) 29 apply (clarsimp simp: valid_obj_def well_formed_cnode_n_def valid_cs_def valid_cs_size_def 30 length_set_helper) 31 apply (drule arg_cong[where f="\<lambda>S. snd p \<in> S"]) 32 apply (simp add: domI) 33 apply (clarsimp simp add: tcb_cap_cases_length word_bits_conv cte_level_bits_def) 34 done 35 36(* FIXME: move? *) 37lemma getActiveIRQ_wp [CSpace_AI_assms]: 38 "irq_state_independent_A P \<Longrightarrow> 39 valid P (do_machine_op (getActiveIRQ in_kernel)) (\<lambda>_. P)" 40 apply (simp add: getActiveIRQ_def do_machine_op_def split_def exec_gets 41 select_f_select[simplified liftM_def] 42 select_modify_comm gets_machine_state_modify) 43 apply wp 44 apply (clarsimp simp: irq_state_independent_A_def in_monad return_def split: if_splits) 45 done 46 47lemma weak_derived_valid_cap [CSpace_AI_assms]: 48 "\<lbrakk> s \<turnstile> c; wellformed_cap c'; weak_derived c' c\<rbrakk> \<Longrightarrow> s \<turnstile> c'" 49 apply (case_tac "c = c'", simp) 50 apply (clarsimp simp: weak_derived_def) 51 apply (clarsimp simp: copy_of_def split: if_split_asm) 52 apply (auto simp: is_cap_simps same_object_as_def wellformed_cap_simps 53 valid_cap_def cap_aligned_def bits_of_def 54 aobj_ref_cases Let_def cap_asid_def 55 split: cap.splits arch_cap.splits option.splits) 56 done 57 58(* FIXME: unused *) 59lemma weak_derived_tcb_cap_valid: 60 "\<lbrakk> tcb_cap_valid cap p s; weak_derived cap cap' \<rbrakk> \<Longrightarrow> tcb_cap_valid cap' p s" 61 apply (clarsimp simp add: tcb_cap_valid_def weak_derived_def 62 obj_at_def is_tcb 63 split: option.split) 64 apply (clarsimp simp: st_tcb_def2) 65 apply (erule disjE; simp add: copy_of_def split: if_split_asm; (solves \<open>clarsimp\<close>)?) 66 apply (clarsimp simp: tcb_cap_cases_def split: if_split_asm) 67 apply (auto simp: is_cap_simps same_object_as_def 68 valid_ipc_buffer_cap_def is_nondevice_page_cap_simps 69 is_nondevice_page_cap_arch_def 70 split: cap.split_asm arch_cap.split_asm 71 thread_state.split_asm) 72 done 73 74lemma copy_obj_refs [CSpace_AI_assms]: 75 "copy_of cap cap' \<Longrightarrow> obj_refs cap' = obj_refs cap" 76 apply (cases cap) 77 apply (auto simp: copy_of_def same_object_as_def is_cap_simps 78 aobj_ref_cases 79 split: if_split_asm cap.splits arch_cap.splits) 80 done 81 82lemma weak_derived_cap_class[simp, CSpace_AI_assms]: 83 "weak_derived cap src_cap \<Longrightarrow> cap_class cap = cap_class src_cap" 84 apply (simp add:weak_derived_def) 85 apply (auto simp:copy_of_def same_object_as_def is_cap_simps cap_asid_base_def 86 split:if_splits cap.splits arch_cap.splits) 87 done 88 89lemma weak_derived_obj_refs [CSpace_AI_assms]: 90 "weak_derived dcap cap \<Longrightarrow> obj_refs dcap = obj_refs cap" 91 by (cases dcap, auto simp: is_cap_simps weak_derived_def copy_of_def 92 same_object_as_def aobj_ref_cases 93 split: if_split_asm cap.splits arch_cap.splits) 94 95lemma weak_derived_obj_ref_of [CSpace_AI_assms]: 96 "weak_derived dcap cap \<Longrightarrow> obj_ref_of dcap = obj_ref_of cap" 97 by (cases dcap, auto simp: is_cap_simps weak_derived_def copy_of_def 98 same_object_as_def aobj_ref_cases 99 split: if_split_asm cap.splits arch_cap.splits) 100 101lemma set_free_index_invs [CSpace_AI_assms]: 102 "\<lbrace>\<lambda>s. (free_index_of cap \<le> idx \<and> is_untyped_cap cap \<and> idx \<le> 2^cap_bits cap) \<and> 103 invs s \<and> cte_wp_at ((=) cap ) cref s\<rbrace> 104 set_cap (free_index_update (\<lambda>_. idx) cap) cref 105 \<lbrace>\<lambda>rv s'. invs s'\<rbrace>" 106 apply (rule hoare_grab_asm)+ 107 apply (simp add:invs_def valid_state_def) 108 apply (rule hoare_pre) 109 apply (wp set_free_index_valid_pspace[where cap = cap] set_free_index_valid_mdb 110 set_cap_idle update_cap_ifunsafe) 111 apply (simp add:valid_irq_node_def) 112 apply wps 113 114 apply (wp hoare_vcg_all_lift set_cap_irq_handlers set_cap_valid_arch_caps 115 set_cap_irq_handlers cap_table_at_lift_valid set_cap_typ_at 116 set_cap_cap_refs_respects_device_region_spec[where ptr = cref]) 117 apply (clarsimp simp:cte_wp_at_caps_of_state) 118 apply (rule conjI,simp add:valid_pspace_def) 119 apply (rule conjI,clarsimp simp:is_cap_simps) 120 apply (rule conjI,rule ext,clarsimp simp: is_cap_simps) 121 apply (clarsimp simp:is_cap_simps appropriate_cte_cap_def) 122 apply (intro conjI) 123 apply (clarsimp split:cap.splits) 124 apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD]) 125 apply clarsimp 126 apply (simp add:ex_cte_cap_wp_to_def appropriate_cte_cap_def) 127 apply (clarsimp dest!:valid_global_refsD2 simp:cap_range_def) 128 apply (simp add:valid_irq_node_def) 129 apply clarsimp 130 apply (clarsimp simp:valid_irq_node_def) 131 apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state vs_cap_ref_def) 132 apply (case_tac capa) 133 apply (simp_all add:table_cap_ref_def) 134 apply (rename_tac arch_cap) 135 apply (case_tac arch_cap) 136 apply simp_all 137 apply (clarsimp simp:cap_refs_in_kernel_window_def 138 valid_refs_def simp del:split_paired_All) 139 apply (drule_tac x = cref in spec) 140 apply (clarsimp simp:cte_wp_at_caps_of_state) 141 apply (drule_tac x = ref in orthD2[rotated]) 142 apply (simp add:cap_range_def) 143 apply simp 144 done 145 146lemma set_untyped_cap_as_full_valid_arch_caps [CSpace_AI_assms]: 147 "\<lbrace>valid_arch_caps and cte_wp_at ((=) src_cap) src\<rbrace> 148 set_untyped_cap_as_full src_cap cap src 149 \<lbrace>\<lambda>ya. valid_arch_caps\<rbrace>" 150 apply (clarsimp simp:valid_arch_caps_def set_untyped_cap_as_full_def) 151 apply (intro conjI impI) 152 apply (wp set_cap_valid_vs_lookup set_cap_valid_table_caps) 153 apply (clarsimp simp del:fun_upd_apply simp:cte_wp_at_caps_of_state) 154 apply (subst unique_table_refs_upd_eqD) 155 apply ((simp add: is_cap_simps table_cap_ref_def)+) 156 apply clarsimp 157 apply (subst unique_table_caps_upd_eqD) 158 apply simp+ 159 apply (clarsimp simp:is_cap_simps cte_wp_at_caps_of_state)+ 160 apply wp 161 apply clarsimp 162 done 163 164lemma set_untyped_cap_as_full[wp, CSpace_AI_assms]: 165 "\<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref a b s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> 166 set_untyped_cap_as_full src_cap cap src 167 \<lbrace>\<lambda>rv s. no_cap_to_obj_with_diff_ref a b s\<rbrace>" 168 apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def) 169 apply (wp hoare_vcg_ball_lift set_untyped_cap_as_full_cte_wp_at_neg) 170 apply (clarsimp simp:cte_wp_at_caps_of_state) 171 apply (drule_tac x=src in bspec, simp) 172 apply (erule_tac x=src_cap in allE) 173 apply (auto simp: table_cap_ref_def masked_as_full_def 174 split: Structures_A.cap.splits arch_cap.splits option.splits 175 vmpage_size.splits) 176 done 177 178lemma is_derived_is_cap: 179 "is_derived m p cap cap' \<Longrightarrow> 180 (is_pg_cap cap = is_pg_cap cap') 181 \<and> (is_pt_cap cap = is_pt_cap cap') 182 \<and> (is_pd_cap cap = is_pd_cap cap') 183 \<and> (is_ep_cap cap = is_ep_cap cap') 184 \<and> (is_ntfn_cap cap = is_ntfn_cap cap') 185 \<and> (is_cnode_cap cap = is_cnode_cap cap') 186 \<and> (is_thread_cap cap = is_thread_cap cap') 187 \<and> (is_zombie cap = is_zombie cap') 188 \<and> (is_arch_cap cap = is_arch_cap cap') 189 \<and> (cap_is_device cap = cap_is_device cap')" 190 apply (clarsimp simp: is_derived_def is_derived_arch_def split: if_split_asm) 191 apply (clarsimp simp: cap_master_cap_def is_cap_simps 192 split: cap.splits arch_cap.splits)+ 193 done 194 195(* FIXME: move to CSpace_I near lemma vs_lookup1_tcb_update *) 196lemma vs_lookup_pages1_tcb_update: 197 "kheap s p = Some (TCB t) \<Longrightarrow> 198 vs_lookup_pages1 (s\<lparr>kheap := kheap s(p \<mapsto> TCB t')\<rparr>) = vs_lookup_pages1 s" 199 by (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 200 intro!: set_eqI) 201 202(* FIXME: move to CSpace_I near lemma vs_lookup_tcb_update *) 203lemma vs_lookup_pages_tcb_update: 204 "kheap s p = Some (TCB t) \<Longrightarrow> 205 vs_lookup_pages (s\<lparr>kheap := kheap s(p \<mapsto> TCB t')\<rparr>) = vs_lookup_pages s" 206 by (clarsimp simp add: vs_lookup_pages_def vs_lookup_pages1_tcb_update) 207 208(* FIXME: move to CSpace_I near lemma vs_lookup1_cnode_update *) 209lemma vs_lookup_pages1_cnode_update: 210 "kheap s p = Some (CNode n cs) \<Longrightarrow> 211 vs_lookup_pages1 (s\<lparr>kheap := kheap s(p \<mapsto> CNode m cs')\<rparr>) = 212 vs_lookup_pages1 s" 213 by (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 214 intro!: set_eqI) 215 216(* FIXME: move to CSpace_I near lemma vs_lookup_cnode_update *) 217lemma vs_lookup_pages_cnode_update: 218 "kheap s p = Some (CNode n cs) \<Longrightarrow> 219 vs_lookup_pages (s\<lparr>kheap := kheap s(p \<mapsto> CNode n cs')\<rparr>) = vs_lookup_pages s" 220 by (clarsimp simp: vs_lookup_pages_def 221 dest!: vs_lookup_pages1_cnode_update[where m=n and cs'=cs']) 222 223lemma set_untyped_cap_as_full_not_reachable_pg_cap[wp]: 224 "\<lbrace>\<lambda>s. \<not> reachable_pg_cap cap' s\<rbrace> 225 set_untyped_cap_as_full src_cap cap src 226 \<lbrace>\<lambda>rv s. \<not> reachable_pg_cap cap' s\<rbrace>" 227 apply (clarsimp simp: set_untyped_cap_as_full_def set_cap_def split_def 228 set_object_def) 229 apply (wp get_object_wp | wpc)+ 230 apply (clarsimp simp: obj_at_def simp del: fun_upd_apply) 231 apply (auto simp: obj_at_def reachable_pg_cap_def is_cap_simps 232 vs_lookup_pages_cnode_update vs_lookup_pages_tcb_update) 233 done 234 235lemma table_cap_ref_eq_rewrite: 236 "\<lbrakk>cap_master_cap cap = cap_master_cap capa;(is_pg_cap cap \<or> vs_cap_ref cap = vs_cap_ref capa)\<rbrakk> 237 \<Longrightarrow> table_cap_ref cap = table_cap_ref capa" 238 apply (frule cap_master_cap_pg_cap) 239 apply (case_tac "is_pg_cap cap") 240 apply (clarsimp simp:is_cap_simps table_cap_ref_def vs_cap_ref_to_table_cap_ref cap_master_cap_pg_cap)+ 241 done 242 243lemma is_derived_cap_asid_issues: 244 "is_derived m p cap cap' 245 \<Longrightarrow> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap \<noteq> None) 246 \<and> (is_pg_cap cap \<or> (vs_cap_ref cap = vs_cap_ref cap'))" 247 unfolding is_derived_def 248 apply (cases "is_derived_arch cap cap'") 249 apply (erule is_derived_cap_arch_asid_issues) 250 apply (clarsimp split: if_split_asm)+ 251 done 252 253lemma is_derived_is_pt_pd: 254 "is_derived m p cap cap' \<Longrightarrow> (is_pt_cap cap = is_pt_cap cap') \<and> (is_pd_cap cap = is_pd_cap cap')" 255 apply (clarsimp simp: is_derived_def split: if_split_asm) 256 apply (clarsimp simp: cap_master_cap_def is_pt_cap_def is_pd_cap_def 257 split: cap.splits arch_cap.splits)+ 258 done 259 260lemma cap_insert_valid_arch_caps [CSpace_AI_assms]: 261 "\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace> 262 cap_insert cap src dest 263 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 264 apply (simp add: cap_insert_def) 265 apply (rule hoare_pre) 266 apply (wp set_cap_valid_arch_caps get_cap_wp set_untyped_cap_as_full_valid_arch_caps 267 | simp split del: if_split)+ 268 apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift set_untyped_cap_as_full_cte_wp_at_neg 269 set_untyped_cap_as_full_is_final_cap'_neg set_untyped_cap_as_full_cte_wp_at hoare_vcg_ball_lift 270 hoare_vcg_ex_lift hoare_vcg_disj_lift | wps)+ 271 apply (wp set_untyped_cap_as_full_obj_at_impossible) 272 apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift set_untyped_cap_as_full_cte_wp_at_neg 273 set_untyped_cap_as_full_is_final_cap'_neg hoare_vcg_ball_lift 274 hoare_vcg_ex_lift | wps)+ 275 apply (wp set_untyped_cap_as_full_obj_at_impossible) 276 apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift set_untyped_cap_as_full_cte_wp_at_neg 277 set_untyped_cap_as_full_is_final_cap'_neg hoare_vcg_ball_lift 278 hoare_vcg_ex_lift | wps)+ 279 apply (rule hoare_strengthen_post) 280 prefer 2 281 apply (erule iffD2[OF caps_of_state_cteD']) 282 apply (wp set_untyped_cap_as_full_cte_wp_at hoare_vcg_all_lift hoare_vcg_imp_lift 283 set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+ 284 apply (rule hoare_strengthen_post) 285 prefer 2 286 apply (erule iffD2[OF caps_of_state_cteD']) 287 apply (wp set_untyped_cap_as_full_cte_wp_at hoare_vcg_all_lift hoare_vcg_imp_lift 288 set_untyped_cap_as_full_cte_wp_at_neg hoare_vcg_ex_lift | clarsimp)+ 289 apply (wp get_cap_wp)+ 290 apply (intro conjI allI impI disj_subst) 291 apply simp 292 apply clarsimp 293 defer 294 apply (clarsimp simp:valid_arch_caps_def cte_wp_at_caps_of_state) 295 apply (drule(1) unique_table_refs_no_cap_asidD) 296 apply (frule is_derived_obj_refs) 297 apply (frule is_derived_cap_asid_issues) 298 apply (frule is_derived_is_cap) 299 apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def Ball_def 300 del:disjCI dest!: derived_cap_master_cap_eq) 301 apply (drule table_cap_ref_eq_rewrite) 302 apply clarsimp 303 apply (erule_tac x=a in allE, erule_tac x=b in allE) 304 apply simp 305 apply simp 306 apply (clarsimp simp:obj_at_def is_cap_simps valid_arch_caps_def) 307 apply (frule(1) valid_table_capsD) 308 apply (clarsimp simp:cte_wp_at_caps_of_state) 309 apply (drule is_derived_is_pt_pd) 310 apply (clarsimp simp:is_derived_def is_cap_simps) 311 apply (clarsimp simp:cte_wp_at_caps_of_state) 312 apply (frule is_derived_cap_asid_issues) 313 apply (clarsimp simp:is_cap_simps) 314 apply (clarsimp simp:cte_wp_at_caps_of_state) 315 apply (frule is_derived_obj_refs) 316 apply (drule_tac x = p in bspec) 317 apply fastforce 318 apply (clarsimp simp:obj_at_def empty_table_caps_of) 319 apply (clarsimp simp:empty_table_caps_of valid_arch_caps_def) 320 apply (frule(1) valid_table_capsD) 321 apply (clarsimp simp:cte_wp_at_caps_of_state is_derived_is_pt_pd) 322 apply (clarsimp simp:cte_wp_at_caps_of_state) 323 apply (frule is_derived_cap_asid_issues) 324 apply (clarsimp simp:is_cap_simps) 325 apply (clarsimp simp:cte_wp_at_caps_of_state) 326 apply (frule is_derived_obj_refs) 327 apply (drule_tac x = x in bspec) 328 apply fastforce 329 subgoal by (clarsimp simp:obj_at_def empty_table_caps_of) 330 apply (clarsimp simp:is_cap_simps cte_wp_at_caps_of_state) 331 apply (frule is_derived_is_pt_pd) 332 apply (frule is_derived_obj_refs) 333 apply (frule is_derived_cap_asid_issues) 334 apply (clarsimp simp:is_cap_simps valid_arch_caps_def cap_master_cap_def 335 is_derived_def is_derived_arch_def) 336 apply (drule_tac ptr = src and ptr' = "(x,xa)" in unique_table_capsD) 337 apply (simp add:is_cap_simps)+ 338 apply (clarsimp simp:is_cap_simps cte_wp_at_caps_of_state) 339 apply (frule is_derived_is_pt_pd) 340 apply (frule is_derived_obj_refs) 341 apply (frule is_derived_cap_asid_issues) 342 apply (clarsimp simp:is_cap_simps valid_arch_caps_def 343 cap_master_cap_def cap_master_arch_cap_def 344 is_derived_def is_derived_arch_def) 345 apply (drule_tac ptr = src and ptr' = "(x,xa)" in unique_table_capsD) 346 apply (simp add:is_cap_simps)+ 347 apply (auto simp:cte_wp_at_caps_of_state) 348done 349 350end 351 352 353global_interpretation cap_insert_crunches?: cap_insert_crunches . 354 355 356context Arch begin global_naming ARM 357 358lemma cap_insert_cap_refs_in_kernel_window[wp, CSpace_AI_assms]: 359 "\<lbrace>cap_refs_in_kernel_window 360 and cte_wp_at (\<lambda>c. cap_range cap \<subseteq> cap_range c) src\<rbrace> 361 cap_insert cap src dest 362 \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 363 apply (simp add: cap_insert_def set_untyped_cap_as_full_def) 364 apply (wp get_cap_wp | simp split del: if_split)+ 365 apply (clarsimp simp: cte_wp_at_caps_of_state is_derived_def) 366 apply (frule(1) cap_refs_in_kernel_windowD[where ptr=src]) 367 apply auto 368 done 369 370 371lemma mask_cap_valid[simp, CSpace_AI_assms]: 372 "s \<turnstile> c \<Longrightarrow> s \<turnstile> mask_cap R c" 373 apply (cases c, simp_all add: valid_cap_def mask_cap_def 374 cap_rights_update_def 375 cap_aligned_def 376 acap_rights_update_def) 377 using valid_validate_vm_rights[simplified valid_vm_rights_def] 378 apply (rename_tac arch_cap) 379 by (case_tac arch_cap, simp_all) 380 381lemma mask_cap_objrefs[simp, CSpace_AI_assms]: 382 "obj_refs (mask_cap rs cap) = obj_refs cap" 383 by (cases cap, simp_all add: mask_cap_def cap_rights_update_def 384 acap_rights_update_def 385 split: arch_cap.split) 386 387 388lemma mask_cap_zobjrefs[simp, CSpace_AI_assms]: 389 "zobj_refs (mask_cap rs cap) = zobj_refs cap" 390 by (cases cap, simp_all add: mask_cap_def cap_rights_update_def 391 acap_rights_update_def 392 split: arch_cap.split) 393 394 395lemma derive_cap_valid_cap [CSpace_AI_assms]: 396 "\<lbrace>valid_cap cap\<rbrace> derive_cap slot cap \<lbrace>valid_cap\<rbrace>,-" 397 apply (simp add: derive_cap_def) 398 apply (rule hoare_pre) 399 apply (wpc, (wp arch_derive_cap_valid_cap | simp)+) 400 apply auto 401 done 402 403 404lemma valid_cap_update_rights[simp, CSpace_AI_assms]: 405 "valid_cap cap s \<Longrightarrow> valid_cap (cap_rights_update cr cap) s" 406 apply (case_tac cap, 407 simp_all add: cap_rights_update_def valid_cap_def cap_aligned_def 408 acap_rights_update_def) 409 using valid_validate_vm_rights[simplified valid_vm_rights_def] 410 apply (rename_tac arch_cap) 411 apply (case_tac arch_cap, simp_all) 412 done 413 414 415lemma update_cap_data_validI [CSpace_AI_assms]: 416 "s \<turnstile> cap \<Longrightarrow> s \<turnstile> update_cap_data p d cap" 417 apply (cases cap) 418 apply (simp_all add: is_cap_defs update_cap_data_def Let_def split_def) 419 apply (simp add: valid_cap_def cap_aligned_def) 420 apply (simp add: valid_cap_def cap_aligned_def) 421 apply (simp add: the_cnode_cap_def valid_cap_def cap_aligned_def word_bits_def) 422 apply (rename_tac arch_cap) 423 apply (case_tac arch_cap) 424 apply (simp_all add: is_cap_defs arch_update_cap_data_def) 425 done 426 427 428lemma tcb_cnode_index_def2 [CSpace_AI_assms]: 429 "tcb_cnode_index n = nat_to_cref 3 n" 430 apply (simp add: tcb_cnode_index_def nat_to_cref_def) 431 apply (rule nth_equalityI) 432 apply (simp add: word_bits_def) 433 apply (clarsimp simp: to_bl_nth word_size word_bits_def) 434 apply (subst of_nat_ucast[where 'a=32 and 'b=3]) 435 apply (simp add: is_down_def target_size_def source_size_def word_size) 436 apply (simp add: nth_ucast) 437 apply fastforce 438 done 439 440 441lemma ex_nonz_tcb_cte_caps [CSpace_AI_assms]: 442 "\<lbrakk>ex_nonz_cap_to t s; tcb_at t s; valid_objs s; ref \<in> dom tcb_cap_cases\<rbrakk> 443 \<Longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cp) (t, ref) s" 444 apply (clarsimp simp: ex_nonz_cap_to_def ex_cte_cap_wp_to_def 445 cte_wp_at_caps_of_state) 446 apply (subgoal_tac "s \<turnstile> cap") 447 apply (rule_tac x=a in exI, rule_tac x=ba in exI) 448 apply (clarsimp simp: valid_cap_def obj_at_def 449 is_obj_defs dom_def 450 appropriate_cte_cap_def 451 split: cap.splits arch_cap.split_asm if_splits) 452 apply (clarsimp simp: caps_of_state_valid_cap) 453 done 454 455 456lemma no_cap_to_obj_with_diff_ref_triv: 457 "\<lbrakk> valid_objs s; valid_cap cap s; \<not> is_pt_cap cap; 458 \<not> is_pd_cap cap; table_cap_ref cap = None \<rbrakk> 459 \<Longrightarrow> no_cap_to_obj_with_diff_ref cap S s" 460 apply (clarsimp simp add: no_cap_to_obj_with_diff_ref_def) 461 apply (drule(1) cte_wp_at_valid_objs_valid_cap) 462 apply (clarsimp simp: table_cap_ref_def valid_cap_def 463 obj_at_def is_ep is_ntfn is_tcb is_cap_table 464 a_type_def is_cap_simps 465 split: cap.split_asm arch_cap.split_asm 466 if_split_asm option.split_asm) 467 done 468 469 470lemma setup_reply_master_arch_caps[wp, CSpace_AI_assms]: 471 "\<lbrace>valid_arch_caps and tcb_at t and valid_objs and pspace_aligned\<rbrace> 472 setup_reply_master t 473 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 474 apply (simp add: setup_reply_master_def) 475 apply (wp set_cap_valid_arch_caps get_cap_wp) 476 apply (clarsimp simp: cte_wp_at_caps_of_state is_pd_cap_def 477 is_pt_cap_def vs_cap_ref_def) 478 apply (rule no_cap_to_obj_with_diff_ref_triv, 479 simp_all add: is_cap_simps table_cap_ref_def) 480 apply (simp add: valid_cap_def cap_aligned_def word_bits_def) 481 apply (clarsimp simp: obj_at_def is_tcb dest!: pspace_alignedD) 482 done 483 484 485lemma setup_reply_master_cap_refs_in_kernel_window[wp, CSpace_AI_assms]: 486 "\<lbrace>cap_refs_in_kernel_window and tcb_at t and pspace_in_kernel_window\<rbrace> 487 setup_reply_master t 488 \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 489 apply (simp add: setup_reply_master_def) 490 apply (wp get_cap_wp) 491 apply (clarsimp simp: pspace_in_kernel_window_def obj_at_def 492 cap_range_def) 493 done 494 495 496(* FIXME: prove same_region_as_def2 instead or change def *) 497lemma same_region_as_Untyped2 [CSpace_AI_assms]: 498 "\<lbrakk> is_untyped_cap pcap; same_region_as pcap cap \<rbrakk> \<Longrightarrow> 499 (is_physical cap \<and> cap_range cap \<noteq> {} \<and> cap_range cap \<subseteq> cap_range pcap)" 500 by (fastforce simp: is_cap_simps cap_range_def is_physical_def arch_is_physical_def 501 split: cap.splits arch_cap.splits) 502 503 504lemma same_region_as_cap_class [CSpace_AI_assms]: 505 shows "same_region_as a b \<Longrightarrow> cap_class a = cap_class b" 506 apply (case_tac a) 507 apply (fastforce simp: cap_range_def arch_is_physical_def is_cap_simps 508 is_physical_def split:cap.splits arch_cap.splits)+ 509 apply (clarsimp split: arch_cap.splits cap.splits) 510 apply (rename_tac arch_cap arch_capa) 511 apply (case_tac arch_cap) 512 apply (case_tac arch_capa,clarsimp+)+ 513 done 514 515 516lemma cap_insert_simple_arch_caps_no_ap: 517 "\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) 518 and no_cap_to_obj_with_diff_ref cap {dest} and K (is_simple_cap cap \<and> \<not>is_ap_cap cap)\<rbrace> 519 cap_insert cap src dest 520 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 521 apply (simp add: cap_insert_def) 522 apply (wp set_cap_valid_arch_caps set_untyped_cap_as_full_valid_arch_caps get_cap_wp 523 | simp split del: if_split)+ 524 apply (wp hoare_vcg_all_lift hoare_vcg_conj_lift hoare_vcg_imp_lift hoare_vcg_ball_lift hoare_vcg_disj_lift 525 set_untyped_cap_as_full_cte_wp_at_neg set_untyped_cap_as_full_is_final_cap'_neg 526 set_untyped_cap_as_full_empty_table_at hoare_vcg_ex_lift 527 set_untyped_cap_as_full_caps_of_state_diff[where dest=dest] 528 | wps)+ 529 apply (wp get_cap_wp)+ 530 apply (clarsimp simp: cte_wp_at_caps_of_state) 531 apply (intro conjI impI allI) 532 by (auto simp:is_simple_cap_def[simplified is_simple_cap_arch_def] is_cap_simps) 533 534lemma setup_reply_master_ioports[wp, CSpace_AI_assms]: 535 "\<lbrace>valid_ioports\<rbrace> setup_reply_master c \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" 536 by wpsimp 537 538lemma cap_insert_derived_ioports[CSpace_AI_assms]: 539 "\<lbrace>valid_ioports and (\<lambda>s. cte_wp_at (is_derived (cdt s) src cap) src s)\<rbrace> 540 cap_insert cap src dest 541 \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" 542 by wpsimp 543 544end 545 546global_interpretation CSpace_AI?: CSpace_AI 547 proof goal_cases 548 interpret Arch . 549 case 1 show ?case by (unfold_locales; (fact CSpace_AI_assms)?) 550 qed 551 552 553context Arch begin global_naming ARM 554 555lemma is_cap_simps': 556 "is_cnode_cap cap = (\<exists>r bits g. cap = cap.CNodeCap r bits g)" 557 "is_thread_cap cap = (\<exists>r. cap = cap.ThreadCap r)" 558 "is_domain_cap cap = (cap = cap.DomainCap)" 559 "is_untyped_cap cap = (\<exists>dev r bits f. cap = cap.UntypedCap dev r bits f)" 560 "is_ep_cap cap = (\<exists>r b R. cap = cap.EndpointCap r b R)" 561 "is_ntfn_cap cap = (\<exists>r b R. cap = cap.NotificationCap r b R)" 562 "is_zombie cap = (\<exists>r b n. cap = cap.Zombie r b n)" 563 "is_arch_cap cap = (\<exists>a. cap = cap.ArchObjectCap a)" 564 "is_reply_cap cap = (\<exists>x. cap = cap.ReplyCap x False)" 565 "is_master_reply_cap cap = (\<exists>x. cap = cap.ReplyCap x True)" 566 "is_nondevice_page_cap cap = (\<exists> u v w x. cap = ArchObjectCap (PageCap False u v w x))" 567 by (cases cap, (auto simp: is_zombie_def is_arch_cap_def is_nondevice_page_cap_def 568 is_reply_cap_def is_master_reply_cap_def is_nondevice_page_cap_arch_def 569 split: cap.splits arch_cap.splits )+)+ 570 571lemma cap_insert_simple_invs: 572 "\<lbrace>invs and valid_cap cap and tcb_cap_valid cap dest and 573 ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and 574 cte_wp_at (\<lambda>c. is_untyped_cap c \<longrightarrow> usable_untyped_range c = {}) src and 575 cte_wp_at (\<lambda>c. c = cap.NullCap) dest and 576 no_cap_to_obj_with_diff_ref cap {dest} and 577 (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and 578 K (is_simple_cap cap \<and> \<not>is_ap_cap cap) and (\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s)\<rbrace> 579 cap_insert cap src dest \<lbrace>\<lambda>rv. invs\<rbrace>" 580 apply (simp add: invs_def valid_state_def valid_pspace_def) 581 apply (rule hoare_pre) 582 apply (wp cap_insert_simple_mdb cap_insert_iflive 583 cap_insert_zombies cap_insert_ifunsafe 584 cap_insert_valid_global_refs cap_insert_idle 585 valid_irq_node_typ cap_insert_simple_arch_caps_no_ap) 586 apply (clarsimp simp: is_simple_cap_def cte_wp_at_caps_of_state) 587 apply (frule safe_parent_cap_range) 588 apply simp 589 apply (rule conjI) 590 prefer 2 591 apply (clarsimp simp: is_cap_simps safe_parent_for_def) 592 apply (clarsimp simp: cte_wp_at_caps_of_state) 593 apply (drule_tac p="(a,b)" in caps_of_state_valid_cap, fastforce) 594 apply (clarsimp dest!: is_cap_simps' [THEN iffD1]) 595 apply (auto simp add: valid_cap_def [where c="cap.Zombie a b x" for a b x] 596 dest: obj_ref_is_tcb obj_ref_is_cap_table split: option.splits) 597 done 598 599lemmas is_derived_def = is_derived_def[simplified is_derived_arch_def] 600 601crunches arch_post_cap_deletion 602 for pred_tcb_at[wp]: "pred_tcb_at proj P t" 603 and valid_objs[wp]: valid_objs 604 and cte_wp_at[wp]: "\<lambda>s. P (cte_wp_at P' p s)" 605 and caps_of_state[wp]: "\<lambda>s. P (caps_of_state s)" 606 and irq_node[wp]: "\<lambda>s. P (interrupt_irq_node s)" 607 and invs_no_pre[wp]: invs 608 and cur_thread[wp]: "\<lambda>s. P (cur_thread s)" 609 and state_refs_of[wp]: "\<lambda>s. P (state_refs_of s)" 610 and mdb_inv[wp]: "\<lambda>s. P (cdt s)" 611 and valid_list[wp]: valid_list 612 613definition 614 "arch_post_cap_delete_pre \<equiv> \<lambda>_ _. True" 615 616lemma arch_post_cap_deletion_invs: 617 "\<lbrace>invs and (\<lambda>s. arch_post_cap_delete_pre (ArchObjectCap c) (caps_of_state s))\<rbrace> arch_post_cap_deletion c \<lbrace>\<lambda>rv. invs\<rbrace>" 618 by (wpsimp simp: arch_post_cap_delete_pre_def) 619 620end 621 622(* is this the right way? we need this fact globally but it's proven with 623 ARM defns. *) 624lemma set_cap_valid_arch_caps_simple: 625 "\<lbrace>\<lambda>s. valid_arch_caps s 626 \<and> valid_objs s 627 \<and> cte_wp_at (Not o is_arch_cap) ptr s 628 \<and> (obj_refs cap \<noteq> {} \<longrightarrow> s \<turnstile> cap) 629 \<and> \<not> (is_arch_cap cap)\<rbrace> 630 set_cap cap ptr 631 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 632 apply (wp ARM.set_cap_valid_arch_caps) 633 apply (clarsimp simp: cte_wp_at_caps_of_state) 634 apply (frule(1) caps_of_state_valid_cap) 635 apply (rename_tac cap') 636 apply (subgoal_tac "\<forall>x \<in> {cap, cap'}. \<not> ARM.is_pt_cap x \<and> \<not> ARM.is_pd_cap x") 637 apply simp 638 apply (rule conjI) 639 apply (clarsimp simp: ARM.vs_cap_ref_def is_cap_simps) 640 apply (erule impCE) 641 apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def 642 cte_wp_at_caps_of_state 643 ARM.obj_ref_none_no_asid) 644 apply (rule ARM.no_cap_to_obj_with_diff_ref_triv, simp_all) 645 apply (rule ccontr, clarsimp simp: ARM.table_cap_ref_def is_cap_simps) 646 apply (auto simp: ARM.is_cap_simps) 647 done 648 649lemma set_cap_kernel_window_simple: 650 "\<lbrace>\<lambda>s. cap_refs_in_kernel_window s 651 \<and> cte_wp_at (\<lambda>cap'. cap_range cap' = cap_range cap) ptr s\<rbrace> 652 set_cap cap ptr 653 \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 654 apply (wp ARM.set_cap_cap_refs_in_kernel_window) 655 apply (clarsimp simp: cte_wp_at_caps_of_state 656 ARM.cap_refs_in_kernel_windowD) 657 done 658 659end 660