1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11(* 12 Arch-specific retype invariants 13*) 14 15theory ArchRetype_AI 16imports "../Retype_AI" 17begin 18 19context Arch begin global_naming ARM 20 21named_theorems Retype_AI_assms 22 23lemma arch_kobj_size_cong[Retype_AI_assms]: 24"\<lbrakk>a = a1; c=c1\<rbrakk> \<Longrightarrow> arch_kobj_size (default_arch_object a b c) 25 = arch_kobj_size (default_arch_object a1 b1 c1)" 26 by (simp add: default_arch_object_def split: aobject_type.splits) 27 28lemma clearMemoryVM_return[simp, Retype_AI_assms]: 29 "clearMemoryVM a b = return ()" 30 by (simp add: clearMemoryVM_def) 31 32lemma slot_bits_def2 [Retype_AI_assms]: "slot_bits = cte_level_bits" 33 by (simp add: slot_bits_def cte_level_bits_def) 34 35definition 36 "no_gs_types \<equiv> UNIV - {Structures_A.CapTableObject, 37 ArchObject SmallPageObj, ArchObject LargePageObj, 38 ArchObject SectionObj, ArchObject SuperSectionObj}" 39 40lemma no_gs_types_simps [simp, Retype_AI_assms]: 41 "Untyped \<in> no_gs_types" 42 "TCBObject \<in> no_gs_types" 43 "EndpointObject \<in> no_gs_types" 44 "NotificationObject \<in> no_gs_types" 45 "ArchObject PageTableObj \<in> no_gs_types" 46 "ArchObject PageDirectoryObj \<in> no_gs_types" 47 "ArchObject ASIDPoolObj \<in> no_gs_types" 48 by (simp_all add: no_gs_types_def) 49 50lemma retype_region_ret_folded [Retype_AI_assms]: 51 "\<lbrace>\<top>\<rbrace> retype_region y n bits ty dev 52 \<lbrace>\<lambda>r s. r = retype_addrs y ty n bits\<rbrace>" 53 unfolding retype_region_def 54 apply (simp add: pageBits_def) 55 apply wp 56 apply (simp add: retype_addrs_def) 57 done 58 59declare store_pde_state_refs_of [wp] 60declare store_pde_state_hyp_refs_of [wp] 61 62(* These also prove facts about copy_global_mappings *) 63crunch pspace_aligned[wp]: init_arch_objects "pspace_aligned" 64 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 65crunch pspace_distinct[wp]: init_arch_objects "pspace_distinct" 66 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 67crunch mdb_inv[wp]: init_arch_objects "\<lambda>s. P (cdt s)" 68 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 69crunch valid_mdb[wp]: init_arch_objects "valid_mdb" 70 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 71crunch cte_wp_at[wp]: init_arch_objects "\<lambda>s. P (cte_wp_at P' p s)" 72 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 73crunch typ_at[wp]: init_arch_objects "\<lambda>s. P (typ_at T p s)" 74 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 75 76lemma mdb_cte_at_store_pde[wp]: 77 "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> 78 store_pde y pde 79 \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" 80 apply (clarsimp simp: mdb_cte_at_def) 81 apply (simp only: imp_conv_disj) 82 apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) 83done 84 85lemma get_pde_valid[wp]: 86 "\<lbrace>valid_vspace_objs 87 and \<exists>\<rhd> (x && ~~mask pd_bits) 88 and K (ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> 89 get_pde x 90 \<lbrace>valid_pde\<rbrace>" 91 apply (simp add: get_pde_def) 92 apply wp 93 apply clarsimp 94 apply (drule (2) valid_vspace_objsD) 95 apply simp 96 done 97 98lemma get_master_pde_valid[wp]: 99 "\<lbrace>valid_vspace_objs 100 and \<exists>\<rhd> (x && ~~mask pd_bits) 101 and K (ucast (x && mask pd_bits >> 2) \<notin> kernel_mapping_slots)\<rbrace> 102 get_master_pde x 103 \<lbrace>valid_pde\<rbrace>" 104 apply (simp add: get_master_pde_def get_pde_def) 105 apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift | wpc)+ 106 defer 107 apply (clarsimp simp: mask_lower_twice pd_bits_def pageBits_def)+ 108 apply (drule sym) 109 apply (drule (1) ko_at_obj_congD, clarsimp) 110 apply (drule (2) valid_vspace_objsD) 111 apply simp 112 apply (erule notE, erule bspec) 113 apply (clarsimp simp: kernel_mapping_slots_def not_le) 114 apply (erule le_less_trans[rotated]) 115 apply (rule ucast_mono_le) 116 apply (rule le_shiftr) 117 apply (clarsimp simp: word_bw_comms) 118 apply (clarsimp simp: word_bool_alg.conj_assoc[symmetric]) 119 apply (subst word_bw_comms, rule word_and_le2) 120 apply (rule shiftr_less_t2n) 121 apply (clarsimp simp: pd_bits_def pageBits_def and_mask_less'[where n=14, simplified]) 122 done 123 124 125lemma get_pde_wellformed[wp]: 126 "\<lbrace>valid_objs\<rbrace> get_pde x \<lbrace>\<lambda>rv _. wellformed_pde rv\<rbrace>" 127 apply (simp add: get_pde_def) 128 apply wp 129 apply (fastforce simp add: valid_objs_def dom_def obj_at_def valid_obj_def) 130 done 131 132crunch valid_objs[wp]: init_arch_objects "valid_objs" 133 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 134 135lemma set_pd_arch_state[wp]: 136 "\<lbrace>valid_arch_state\<rbrace> set_pd ptr val \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>" 137 by (rule set_pd_valid_arch) 138 139crunch valid_arch_state[wp]: init_arch_objects "valid_arch_state" 140 (ignore: clearMemory set_object wp: crunch_wps hoare_unless_wp) 141 142lemmas init_arch_objects_valid_cap[wp] = valid_cap_typ [OF init_arch_objects_typ_at] 143 144lemmas init_arch_objects_cap_table[wp] = cap_table_at_lift_valid [OF init_arch_objects_typ_at] 145 146crunch device_state_inv[wp]: clearMemory "\<lambda>ms. P (device_state ms)" 147 (wp: mapM_x_wp) 148 149crunch pspace_respects_device_region[wp]: reserve_region pspace_respects_device_region 150crunch cap_refs_respects_device_region[wp]: reserve_region cap_refs_respects_device_region 151 152crunch invs [wp]: reserve_region "invs" 153 154crunch iflive[wp]: copy_global_mappings "if_live_then_nonz_cap" 155 (wp: crunch_wps) 156 157crunch zombies[wp]: copy_global_mappings "zombies_final" 158 (wp: crunch_wps) 159 160crunch state_refs_of[wp]: copy_global_mappings "\<lambda>s. P (state_refs_of s)" 161 (wp: crunch_wps) 162 163crunch state_hyp_refs_of[wp]: copy_global_mappings "\<lambda>s. P (state_hyp_refs_of s)" 164 (wp: crunch_wps) 165 166crunch valid_idle[wp]: copy_global_mappings "valid_idle" 167 (wp: crunch_wps) 168 169crunch only_idle[wp]: copy_global_mappings "only_idle" 170 (wp: crunch_wps) 171 172crunch ifunsafe[wp]: copy_global_mappings "if_unsafe_then_cap" 173 (wp: crunch_wps) 174 175crunch reply_caps[wp]: copy_global_mappings "valid_reply_caps" 176 (wp: crunch_wps) 177 178crunch reply_masters[wp]: copy_global_mappings "valid_reply_masters" 179 (wp: crunch_wps) 180 181crunch valid_global[wp]: copy_global_mappings "valid_global_refs" 182 (wp: crunch_wps) 183 184crunch irq_node[wp]: copy_global_mappings "\<lambda>s. P (interrupt_irq_node s)" 185 (wp: crunch_wps) 186 187crunch irq_states[wp]: copy_global_mappings "\<lambda>s. P (interrupt_states s)" 188 (wp: crunch_wps) 189 190crunch caps_of_state[wp]: copy_global_mappings "\<lambda>s. P (caps_of_state s)" 191 (wp: crunch_wps) 192 193crunch pspace_in_kernel_window[wp]: copy_global_mappings "pspace_in_kernel_window" 194 (wp: crunch_wps) 195 196crunch cap_refs_in_kernel_window[wp]: copy_global_mappings "cap_refs_in_kernel_window" 197 (wp: crunch_wps) 198 199crunch pspace_respects_device_region[wp]: copy_global_mappings "pspace_respects_device_region" 200 (wp: crunch_wps) 201 202crunch cap_refs_respects_device_region[wp]: copy_global_mappings "cap_refs_respects_device_region" 203 (wp: crunch_wps) 204 205(* FIXME: move to VSpace_R *) 206lemma vs_refs_add_one'': 207 "p \<in> kernel_mapping_slots \<Longrightarrow> 208 vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = 209 vs_refs (ArchObj (PageDirectory pd))" 210 by (auto simp: vs_refs_def graph_of_def split: if_split_asm) 211 212 213lemma glob_vs_refs_add_one': 214 "glob_vs_refs (ArchObj (PageDirectory (pd(p := pde)))) = 215 glob_vs_refs (ArchObj (PageDirectory pd)) 216 - Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) 217 \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref pde)" 218 apply (simp add: glob_vs_refs_def) 219 apply (rule set_eqI) 220 apply clarsimp 221 apply (rule iffI) 222 apply (clarsimp del: disjCI dest!: graph_ofD split: if_split_asm) 223 apply (rule disjI1) 224 apply (rule conjI) 225 apply (rule_tac x="(aa, ba)" in image_eqI) 226 apply simp 227 apply (simp add: graph_of_def) 228 apply clarsimp 229 apply (erule disjE) 230 apply (clarsimp dest!: graph_ofD) 231 apply (rule_tac x="(aa,ba)" in image_eqI) 232 apply simp 233 apply (clarsimp simp: graph_of_def) 234 apply clarsimp 235 apply (rule_tac x="(p,x)" in image_eqI) 236 apply simp 237 apply (clarsimp simp: graph_of_def) 238 done 239 240 241lemma store_pde_map_global_valid_arch_caps: 242 "\<lbrace>valid_arch_caps and valid_objs and valid_vspace_objs 243 and valid_arch_state and valid_global_objs 244 and K (valid_pde_mappings pde) 245 and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) 246 \<in> kernel_vsrefs) 247 and (\<lambda>s. \<forall>p. pde_ref pde = Some p 248 \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace> 249 store_pde p pde 250 \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" 251 apply (simp add: store_pde_def) 252 apply (wp set_pd_valid_arch_caps 253 [where T="{}" and S="{}" and T'="{}" and S'="{}"]) 254 apply (clarsimp simp: obj_at_def kernel_vsrefs_kernel_mapping_slots[symmetric]) 255 apply (intro conjI) 256 apply (erule vs_refs_add_one'') 257 apply (rule set_eqI) 258 apply (clarsimp simp add: vs_refs_pages_def graph_of_def image_def) 259 apply (rule arg_cong[where f=Ex], rule ext, fastforce) 260 apply clarsimp 261 apply (rule conjI, clarsimp) 262 apply (drule valid_vspace_objsD, simp add: obj_at_def, simp+)[1] 263 apply (rule impI, rule disjI2) 264 apply (simp add: empty_table_def second_level_tables_def) 265 apply clarsimp 266 apply (rule conjI, clarsimp) 267 apply (thin_tac "All P" for P) 268 apply clarsimp 269 apply (frule_tac ref'="VSRef (ucast c) (Some APageDirectory) # r" and 270 p'=q in vs_lookup_pages_step) 271 apply (clarsimp simp: vs_lookup_pages1_def vs_refs_pages_def 272 obj_at_def graph_of_def image_def) 273 apply (clarsimp simp: valid_arch_caps_def valid_vs_lookup_def) 274 apply clarsimp 275 apply (rule conjI, clarsimp) 276 apply (thin_tac "All P" for P) 277 apply clarsimp 278 apply (drule_tac ref'="VSRef (ucast c) (Some APageDirectory) # r" and 279 p'=q in vs_lookup_pages_step) 280 apply (clarsimp simp: vs_lookup_pages1_def vs_refs_pages_def 281 obj_at_def graph_of_def image_def) 282 apply (drule_tac ref'="VSRef (ucast d) (Some APageTable) # 283 VSRef (ucast c) (Some APageDirectory) # r" and 284 p'=q' in vs_lookup_pages_step) 285 apply (fastforce simp: vs_lookup_pages1_def vs_refs_pages_def 286 obj_at_def graph_of_def image_def) 287 apply (clarsimp simp: valid_arch_caps_def valid_vs_lookup_def) 288 done 289 290 291lemma store_pde_map_global_valid_vspace_objs: 292 "\<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs 293 and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)\<rbrace> 294 store_pde p pde 295 \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" 296 apply (simp add: store_pde_def) 297 apply (wp set_pd_vspace_objs_map[where T="{}" and S="{}"]) 298 apply (clarsimp simp: obj_at_def kernel_vsrefs_kernel_mapping_slots[symmetric]) 299 apply (intro conjI) 300 apply (erule vs_refs_add_one'') 301 apply clarsimp 302 apply (drule valid_vspace_objsD, simp add: obj_at_def, simp+) 303 apply clarsimp 304 done 305 306 307lemma store_pde_global_objs[wp]: 308 "\<lbrace>valid_global_objs and valid_global_refs and 309 valid_arch_state and 310 (\<lambda>s. (\<forall>pd. (obj_at (empty_table (set (second_level_tables (arch_state s)))) 311 (p && ~~ mask pd_bits) s 312 \<and> ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s 313 \<longrightarrow> empty_table (set (second_level_tables (arch_state s))) 314 (ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde)))))) 315 \<or> (\<exists>slot. cte_wp_at (\<lambda>cap. p && ~~ mask pd_bits \<in> obj_refs cap) slot s))\<rbrace> 316 store_pde p pde \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 317 apply (simp add: store_pde_def) 318 apply wp 319 apply clarsimp 320 done 321 322 323lemma store_pde_valid_kernel_mappings_map_global: 324 "\<lbrace>valid_kernel_mappings and valid_arch_state and valid_global_objs 325 and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) 326 \<in> kernel_vsrefs) 327 and (\<lambda>s. \<forall>p. pde_ref pde = Some p 328 \<longrightarrow> p \<in> set (arm_global_pts (arch_state s)))\<rbrace> 329 store_pde p pde 330 \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" 331 apply (simp add: store_pde_def) 332 apply (wp set_pd_valid_kernel_mappings_map) 333 apply (clarsimp simp: obj_at_def) 334 apply (rule conjI, rule glob_vs_refs_add_one') 335 apply (clarsimp simp: ucast_ucast_mask_shift_helper) 336 done 337 338 339crunch valid_asid_map[wp]: store_pde "valid_asid_map" 340 341crunch cur[wp]: store_pde "cur_tcb" 342 343lemma mapM_x_store_pde_eq_kernel_mappings_restr: 344 "pd \<in> S \<and> is_aligned pd pd_bits \<and> is_aligned pd' pd_bits 345 \<and> set xs \<subseteq> {..< 2 ^ (pd_bits - 2)} 346 \<Longrightarrow> 347 \<lbrace>\<lambda>s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>)\<rbrace> 348 mapM_x (\<lambda>idx. get_pde (pd' + (idx << 2)) >>= 349 store_pde (pd + (idx << 2))) xs 350 \<lbrace>\<lambda>rv s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>) 351 \<and> (\<forall>x \<in> set xs. 352 (\<exists>pdv pdv'. ko_at (ArchObj (PageDirectory pdv)) pd s 353 \<and> ko_at (ArchObj (PageDirectory pdv')) pd' s 354 \<and> pdv (ucast x) = pdv' (ucast x)))\<rbrace>" 355 apply (induct xs rule: rev_induct, simp_all add: mapM_x_Nil mapM_x_append mapM_x_singleton) 356 apply (erule hoare_seq_ext[rotated]) 357 apply (simp add: store_pde_def set_pd_def set_object_def cong: bind_cong) 358 apply (wp get_object_wp get_pde_wp) 359 apply (clarsimp simp: obj_at_def split del: if_split) 360 apply (frule shiftl_less_t2n) 361 apply (simp add: pd_bits_def pageBits_def) 362 apply (simp add: is_aligned_add_helper split del: if_split) 363 apply (cut_tac x=x and n=2 in shiftl_shiftr_id) 364 apply (simp add: word_bits_def) 365 apply (simp add: word_bits_def pd_bits_def pageBits_def) 366 apply (erule order_less_le_trans, simp) 367 apply (clarsimp simp: fun_upd_def[symmetric] is_aligned_add_helper) 368 done 369 370 371lemma equal_kernel_mappings_specific_def: 372 "ko_at (ArchObj (PageDirectory pd)) p s 373 \<Longrightarrow> equal_kernel_mappings s 374 = (\<forall>p' pd'. ko_at (ArchObj (PageDirectory pd')) p' s 375 \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd' w = pd w))" 376 apply (rule iffI) 377 apply (clarsimp simp: equal_kernel_mappings_def) 378 apply (clarsimp simp: equal_kernel_mappings_def) 379 apply (subgoal_tac "pda w = pd w \<and> pd' w = pd w") 380 apply (erule conjE, erule(1) trans[OF _ sym]) 381 apply blast 382 done 383 384lemma copy_global_equal_kernel_mappings_restricted: 385 "is_aligned pd pd_bits \<Longrightarrow> 386 \<lbrace>\<lambda>s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- (insert pd S)) \<rparr>) 387 \<and> arm_global_pd (arch_state s) \<notin> (insert pd S) 388 \<and> pspace_aligned s \<and> valid_arch_state s\<rbrace> 389 copy_global_mappings pd 390 \<lbrace>\<lambda>rv s. equal_kernel_mappings (s \<lparr> kheap := restrict_map (kheap s) (- S) \<rparr>)\<rbrace>" 391 apply (simp add: copy_global_mappings_def) 392 apply (rule hoare_seq_ext [OF _ gets_sp]) 393 apply (rule hoare_chain) 394 apply (rule hoare_vcg_conj_lift) 395 apply (rule_tac P="global_pd \<notin> (insert pd S)" in hoare_vcg_prop) 396 apply (rule_tac P="is_aligned global_pd pd_bits" 397 in hoare_gen_asm(1)) 398 apply (rule_tac S="insert pd S" in mapM_x_store_pde_eq_kernel_mappings_restr) 399 apply clarsimp 400 apply (erule order_le_less_trans) 401 apply (simp add: pd_bits_def pageBits_def) 402 apply (clarsimp simp: invs_aligned_pdD) 403 apply clarsimp 404 apply (frule_tac x="kernel_base >> 20" in spec) 405 apply (drule mp) 406 apply (simp add: kernel_base_def pd_bits_def pageBits_def) 407 apply (clarsimp simp: obj_at_def) 408 apply (subst equal_kernel_mappings_specific_def) 409 apply (fastforce simp add: obj_at_def restrict_map_def) 410 apply (subst(asm) equal_kernel_mappings_specific_def) 411 apply (fastforce simp add: obj_at_def restrict_map_def) 412 apply (clarsimp simp: restrict_map_def obj_at_def) 413 apply (drule_tac x="ucast w" in spec, drule mp) 414 apply (clarsimp simp: kernel_mapping_slots_def) 415 apply (rule conjI) 416 apply (simp add: word_le_nat_alt unat_ucast_kernel_base_rshift) 417 apply (simp only: unat_ucast, subst mod_less) 418 apply (rule order_less_le_trans, rule unat_lt2p) 419 apply simp 420 apply simp 421 apply (rule minus_one_helper3) 422 apply (rule order_less_le_trans, rule ucast_less) 423 apply simp 424 apply (simp add: pd_bits_def pageBits_def) 425 apply (simp add: ucast_down_ucast_id word_size source_size_def 426 target_size_def is_down_def) 427 apply (drule_tac x=p' in spec) 428 apply (simp split: if_split_asm) 429 done 430 431lemma store_pde_valid_global_pd_mappings[wp]: 432 "\<lbrace>valid_global_objs and valid_global_vspace_mappings 433 and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s)\<rbrace> 434 store_pde p pde 435 \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" 436 apply (simp add: store_pde_def set_pd_def) 437 apply (wp set_object_global_vspace_mappings get_object_wp) 438 apply simp 439 done 440 441lemma store_pde_valid_ioc[wp]: 442 "\<lbrace>valid_ioc\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. valid_ioc\<rbrace>" 443 by (simp add: store_pde_def, wp) simp 444 445 446lemma store_pde_vms[wp]: 447 "\<lbrace>valid_machine_state\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 448 by (simp add: store_pde_def, wp) clarsimp 449 450crunch valid_irq_states[wp]: store_pde "valid_irq_states" 451 452lemma copy_global_invs_mappings_restricted: 453 "\<lbrace>(\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (insert pd S) s) 454 and (\<lambda>s. insert pd S \<inter> global_refs s = {}) 455 and K (is_aligned pd pd_bits)\<rbrace> 456 copy_global_mappings pd 457 \<lbrace>\<lambda>rv. all_invs_but_equal_kernel_mappings_restricted S\<rbrace>" 458 apply (rule hoare_gen_asm) 459 apply (simp add: valid_pspace_def pred_conj_def) 460 apply (rule hoare_conjI, wp copy_global_equal_kernel_mappings_restricted) 461 apply (clarsimp simp: global_refs_def) 462 apply (rule valid_prove_more, rule hoare_vcg_conj_lift, rule hoare_TrueI) 463 apply (simp add: copy_global_mappings_def valid_pspace_def) 464 apply (rule hoare_seq_ext [OF _ gets_sp]) 465 apply (rule hoare_strengthen_post) 466 apply (rule mapM_x_wp[where S="{x. kernel_base >> 20 \<le> x 467 \<and> x < 2 ^ (pd_bits - 2)}"]) 468 apply simp_all 469 apply (rule hoare_pre) 470 apply (wp valid_irq_node_typ valid_irq_handlers_lift 471 store_pde_map_global_valid_arch_caps 472 store_pde_map_global_valid_vspace_objs 473 store_pde_valid_kernel_mappings_map_global 474 get_pde_wp) 475 apply (clarsimp simp: valid_global_objs_def) 476 apply (frule(1) invs_aligned_pdD) 477 apply (frule shiftl_less_t2n) 478 apply (simp add: pd_bits_def pageBits_def) 479 apply (clarsimp simp: is_aligned_add_helper) 480 apply (cut_tac x=x and n=2 in shiftl_shiftr_id) 481 apply (simp add: word_bits_def) 482 apply (erule order_less_le_trans) 483 apply (simp add: word_bits_def pd_bits_def pageBits_def) 484 apply (rule conjI) 485 apply (simp add: valid_objs_def dom_def obj_at_def valid_obj_def) 486 apply (drule spec, erule impE, fastforce, clarsimp) 487 apply (clarsimp simp: obj_at_def empty_table_def kernel_vsrefs_def second_level_tables_def) 488 apply clarsimp 489 apply (erule minus_one_helper5[rotated]) 490 apply (simp add: pd_bits_def pageBits_def) 491 done 492 493lemma copy_global_mappings_valid_ioc[wp]: 494 "\<lbrace>valid_ioc\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_ioc\<rbrace>" 495 by (wpsimp wp: mapM_x_wp[of UNIV] simp: copy_global_mappings_def) 496 497lemma copy_global_mappings_vms[wp]: 498 "\<lbrace>valid_machine_state\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 499 by (wpsimp wp: mapM_x_wp[of UNIV] simp: copy_global_mappings_def) 500 501lemma copy_global_mappings_invs: 502 "\<lbrace>invs and (\<lambda>s. pd \<notin> global_refs s) 503 and K (is_aligned pd pd_bits)\<rbrace> 504 copy_global_mappings pd \<lbrace>\<lambda>rv. invs\<rbrace>" 505 apply (fold all_invs_but_equal_kernel_mappings_restricted_eq) 506 apply (wp copy_global_invs_mappings_restricted) 507 apply (clarsimp simp: equal_kernel_mappings_def obj_at_def 508 restrict_map_def) 509 done 510 511crunch global_refs_inv[wp]: copy_global_mappings "\<lambda>s. P (global_refs s)" 512 (wp: crunch_wps) 513 514lemma mapM_copy_global_invs_mappings_restricted: 515 "\<lbrace>\<lambda>s. all_invs_but_equal_kernel_mappings_restricted (set pds) s 516 \<and> (set pds \<inter> global_refs s = {}) 517 \<and> (\<forall>pd \<in> set pds. is_aligned pd pd_bits)\<rbrace> 518 mapM_x copy_global_mappings pds 519 \<lbrace>\<lambda>rv. invs\<rbrace>" 520 apply (fold all_invs_but_equal_kernel_mappings_restricted_eq) 521 apply (induct pds, simp_all only: mapM_x_Nil mapM_x_Cons K_bind_def) 522 apply wpsimp 523 apply (rule hoare_seq_ext, assumption, thin_tac "P" for P) 524 apply (wpsimp wp: copy_global_invs_mappings_restricted) 525 done 526 527 528lemma dmo_eq_kernel_restricted [wp, Retype_AI_assms]: 529 "\<lbrace>\<lambda>s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace> 530 do_machine_op m 531 \<lbrace>\<lambda>rv s. equal_kernel_mappings (kheap_update (f (kheap s)) s)\<rbrace>" 532 apply (simp add: do_machine_op_def split_def) 533 apply wp 534 apply (simp add: equal_kernel_mappings_def obj_at_def) 535 done 536 537 538definition 539 "post_retype_invs_check tp \<equiv> tp = ArchObject PageDirectoryObj" 540 541declare post_retype_invs_check_def[simp] 542 543end 544 545 546context begin interpretation Arch . 547requalify_consts post_retype_invs_check 548end 549 550definition 551 post_retype_invs :: "apiobject_type \<Rightarrow> machine_word list \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" 552where 553 "post_retype_invs tp refs \<equiv> 554 if post_retype_invs_check tp 555 then all_invs_but_equal_kernel_mappings_restricted (set refs) 556 else invs" 557 558global_interpretation Retype_AI_post_retype_invs?: Retype_AI_post_retype_invs 559 where post_retype_invs_check = post_retype_invs_check 560 and post_retype_invs = post_retype_invs 561 by (unfold_locales; fact post_retype_invs_def) 562 563 564context Arch begin global_naming ARM 565 566lemma dmo_mapM_x_ccr_invs[wp]: 567 "\<lbrace>invs\<rbrace> 568 do_machine_op (mapM_x (\<lambda>ptr. cleanCacheRange_PoU ptr (w ptr) (addrFromPPtr ptr)) xs) 569 \<lbrace>\<lambda>rv. invs\<rbrace>" 570 apply (clarsimp simp: mapM_x_mapM do_machine_op_return_foo) 571 apply (rule hoare_pre) 572 apply (subst dom_mapM) 573 apply ((simp add: clearMemory_def 574 | wp empty_fail_cleanCacheRange_PoU ef_storeWord 575 empty_fail_mapM_x empty_fail_bind)+)[1] 576 apply (wp mapM_wp' | clarsimp)+ 577 done 578 579lemma init_arch_objects_invs_from_restricted: 580 "\<lbrace>post_retype_invs new_type refs 581 and (\<lambda>s. global_refs s \<inter> set refs = {}) 582 and K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace> 583 init_arch_objects new_type ptr bits obj_sz refs 584 \<lbrace>\<lambda>_. invs\<rbrace>" 585 apply (simp add: init_arch_objects_def split del: if_split) 586 apply (rule hoare_pre) 587 apply (wp mapM_copy_global_invs_mappings_restricted 588 hoare_vcg_const_Ball_lift 589 valid_irq_node_typ 590 | wpc)+ 591 apply (auto simp: post_retype_invs_def default_arch_object_def 592 pd_bits_def pageBits_def obj_bits_api_def 593 global_refs_def) 594 done 595 596 597lemma obj_bits_api_neq_0 [Retype_AI_assms]: 598 "ty \<noteq> Untyped \<Longrightarrow> 0 < obj_bits_api ty us" 599 unfolding obj_bits_api_def 600 by (clarsimp simp: slot_bits_def default_arch_object_def pageBits_def 601 split: Structures_A.apiobject_type.splits aobject_type.splits) 602 603 604lemma vs_lookup_sub2: 605 assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s'" 606 assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))" 607 shows "vs_lookup s \<subseteq> vs_lookup s'" 608 unfolding vs_lookup_def 609 apply (rule Image_mono) 610 apply (rule vs_lookup_trans_sub2) 611 apply (erule (1) ko) 612 apply (unfold vs_asid_refs_def) 613 apply (rule image_mono) 614 apply (rule table) 615 done 616 617 618lemma vs_lookup_pages_sub2: 619 assumes ko: "\<And>ko p. \<lbrakk> ko_at ko p s; vs_refs_pages ko \<noteq> {} \<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'" 620 assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))" 621 shows "vs_lookup_pages s \<subseteq> vs_lookup_pages s'" 622 unfolding vs_lookup_pages_def 623 apply (rule Image_mono) 624 apply (rule vs_lookup_pages_trans_sub2) 625 apply (erule (1) ko) 626 apply (unfold vs_asid_refs_def) 627 apply (rule image_mono) 628 apply (rule table) 629 done 630 631end 632 633 634global_interpretation Retype_AI_slot_bits?: Retype_AI_slot_bits 635 proof goal_cases 636 interpret Arch . 637 case 1 show ?case 638 by (unfold_locales; fact Retype_AI_assms) 639 qed 640 641 642context Arch begin global_naming ARM 643 644lemma valid_untyped_helper [Retype_AI_assms]: 645 assumes valid_c : "s \<turnstile> c" 646 and cte_at : "cte_wp_at ((=) c) q s" 647 and tyunt: "ty \<noteq> Untyped" 648 and cover : "range_cover ptr sz (obj_bits_api ty us) n" 649 and range : "is_untyped_cap c \<Longrightarrow> usable_untyped_range c \<inter> {ptr..ptr + of_nat (n * 2 ^ (obj_bits_api ty us)) - 1} = {}" 650 and pn : "pspace_no_overlap_range_cover ptr sz s" 651 and cn : "caps_no_overlap ptr sz s" 652 and vp : "valid_pspace s" 653 shows "valid_cap c 654 (s\<lparr>kheap := \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) then Some (default_object ty dev us) else kheap s x\<rparr>)" 655 (is "valid_cap c ?ns") 656 proof - 657 have obj_at_pres: "\<And>P x. obj_at P x s \<Longrightarrow> obj_at P x ?ns" 658 by (clarsimp simp: obj_at_def dest: domI) 659 (erule pspace_no_overlapC [OF pn _ _ cover vp]) 660 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 661 Int_atLeastAtMost atLeastatMost_empty_iff 662 have cover':"range_cover ptr sz (obj_bits (default_object ty dev us)) n" 663 using cover tyunt 664 by (clarsimp simp: obj_bits_dev_irr) 665 666 show ?thesis 667 using cover valid_c range usable_range_emptyD[where cap = c] cte_at 668 apply (clarsimp simp: valid_cap_def elim!: obj_at_pres 669 split: cap.splits option.splits arch_cap.splits) 670 defer 671 apply (fastforce elim!: obj_at_pres) 672 apply (fastforce elim!: obj_at_pres) 673 apply (fastforce elim!: obj_at_pres) 674 apply (rename_tac word nat1 nat2) 675 apply (clarsimp simp: valid_untyped_def is_cap_simps obj_at_def split: if_split_asm) 676 apply (thin_tac "\<forall>x. Q x" for Q) 677 apply (frule retype_addrs_obj_range_subset_strong[where dev = dev,OF _ _ tyunt]) 678 apply (simp add: obj_bits_dev_irr tyunt) 679 apply (frule usable_range_subseteq) 680 apply (simp add: is_cap_simps) 681 apply (clarsimp simp: cap_aligned_def split: if_split_asm) 682 apply (frule aligned_ranges_subset_or_disjoint) 683 apply (erule retype_addrs_aligned[where sz = sz]) 684 apply (simp add: range_cover_def) 685 apply (simp add: range_cover_def word_bits_def) 686 apply (simp add: range_cover_def) 687 apply (clarsimp simp: default_obj_range Int_ac tyunt 688 split: if_split_asm) 689 apply (elim disjE) 690 apply (drule(2) subset_trans[THEN disjoint_subset2]) 691 apply (drule Int_absorb2)+ 692 apply (simp add: is_cap_simps free_index_of_def) 693 apply simp 694 apply (drule(1) disjoint_subset2[rotated]) 695 apply (simp add: Int_ac) 696 apply (thin_tac "\<forall>x. Q x" for Q) 697 apply (frule retype_addrs_obj_range_subset[OF _ cover' tyunt]) 698 apply (clarsimp simp: cap_aligned_def) 699 apply (frule aligned_ranges_subset_or_disjoint) 700 apply (erule retype_addrs_aligned[where sz = sz]) 701 apply (simp add: range_cover_def) 702 apply (simp add: range_cover_def word_bits_def) 703 apply (simp add: range_cover_def) 704 apply (clarsimp simp: default_obj_range Int_ac tyunt 705 split: if_split_asm) 706 apply (erule disjE) 707 apply (simp add: cte_wp_at_caps_of_state) 708 apply (drule cn[unfolded caps_no_overlap_def,THEN bspec,OF ranI]) 709 apply (simp add: p_assoc_help[symmetric]) 710 apply (erule impE) 711 apply blast (* set arith *) 712 apply blast (* set arith *) 713 apply blast (* set arith *) 714 done 715 qed 716 717lemma valid_default_arch_tcb: 718 "\<And>s. valid_arch_tcb default_arch_tcb s" 719 by (simp add: default_arch_tcb_def valid_arch_tcb_def) 720 721end 722 723 724global_interpretation Retype_AI_valid_untyped_helper?: Retype_AI_valid_untyped_helper 725 proof goal_cases 726 interpret Arch . 727 case 1 show ?case by (unfold_locales; fact Retype_AI_assms) 728 qed 729 730 731locale retype_region_proofs_arch 732 = retype_region_proofs s ty us ptr sz n ps s' dev 733 + Arch 734 for s :: "'state_ext :: state_ext state" 735 and ty us ptr sz n ps s' dev 736 737 738context retype_region_proofs begin 739 740interpretation Arch . 741 742lemma valid_cap: 743 assumes cap: 744 "(s::'state_ext state) \<turnstile> cap \<and> untyped_range cap \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} = {}" 745 shows "s' \<turnstile> cap" 746 proof - 747 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 748 Int_atLeastAtMost atLeastatMost_empty_iff 749 have cover':"range_cover ptr sz (obj_bits (default_object ty dev us)) n" 750 using cover tyunt 751 by (clarsimp simp: obj_bits_dev_irr) 752 show ?thesis 753 using cap 754 apply (case_tac cap) 755 unfolding valid_cap_def 756 apply (simp_all add: valid_cap_def obj_at_pres cte_at_pres 757 split: option.split_asm arch_cap.split_asm 758 option.splits) 759 apply (clarsimp simp add: valid_untyped_def ps_def s'_def) 760 apply (intro conjI) 761 apply clarsimp 762 apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) 763 apply (simp add: Int_ac p_assoc_help[symmetric]) 764 apply simp 765 apply clarsimp 766 apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) 767 apply (simp add: Int_ac p_assoc_help[symmetric]) 768 apply simp 769 using cover tyunt 770 apply (simp add: obj_bits_api_def2 split: Structures_A.apiobject_type.splits) 771 apply clarsimp+ 772 apply (fastforce elim!: obj_at_pres)+ 773 done 774 qed 775 776 777lemma valid_global_refs: 778 "valid_global_refs s \<Longrightarrow> valid_global_refs s'" 779 apply (simp add: valid_global_refs_def valid_refs_def global_refs_def idle_s') 780 apply (simp add: cte_retype cap_range_def) 781 done 782 783lemma valid_arch_state: 784 "valid_arch_state s \<Longrightarrow> valid_arch_state s'" 785 by (clarsimp simp: valid_arch_state_def obj_at_pres 786 valid_asid_table_def valid_global_pts_def) 787 788lemma vs_refs_default [simp]: 789 "vs_refs (default_object ty dev us) = {}" 790 by (simp add: default_object_def default_arch_object_def tyunt vs_refs_def 791 o_def pde_ref_def graph_of_def 792 split: Structures_A.apiobject_type.splits aobject_type.splits) 793 794lemma vs_refs_pages_default [simp]: 795 "vs_refs_pages (default_object ty dev us) = {}" 796 by (simp add: default_object_def default_arch_object_def tyunt vs_refs_pages_def 797 o_def pde_ref_pages_def pte_ref_pages_def graph_of_def 798 split: Structures_A.apiobject_type.splits aobject_type.splits) 799 800lemma vs_lookup': 801 "vs_lookup s' = vs_lookup s" 802 apply (rule order_antisym) 803 apply (rule vs_lookup_sub2) 804 apply (clarsimp simp: obj_at_def s'_def ps_def split: if_split_asm) 805 apply simp 806 apply (rule vs_lookup_sub) 807 apply (clarsimp simp: obj_at_def s'_def ps_def split: if_split_asm dest!: orthr) 808 apply simp 809 done 810 811lemma vs_lookup_pages': 812 "vs_lookup_pages s' = vs_lookup_pages s" 813 apply (rule order_antisym) 814 apply (rule vs_lookup_pages_sub2) 815 apply (clarsimp simp: obj_at_def s'_def ps_def split: if_split_asm) 816 apply simp 817 apply (rule vs_lookup_pages_sub) 818 apply (clarsimp simp: obj_at_def s'_def ps_def split: if_split_asm dest!: orthr) 819 apply simp 820 done 821 822lemma hyp_refs_eq: 823 "ARM.state_hyp_refs_of s' = ARM.state_hyp_refs_of s" 824 unfolding s'_def ps_def 825 apply (clarsimp intro!: ext simp: state_hyp_refs_of_def 826 simp: orthr 827 split: option.splits) 828 apply (cases ty, simp_all add: tyunt default_object_def default_tcb_def 829 hyp_refs_of_def tcb_hyp_refs_def 830 default_arch_tcb_def) 831 done 832 833end 834 835 836context retype_region_proofs_arch begin 837 838lemma valid_vspace_obj_pres: 839 "valid_vspace_obj ao s \<Longrightarrow> valid_vspace_obj ao s'" 840 apply (cases ao; simp add: valid_vspace_obj_def obj_at_pres) 841 apply (erule allEI ballEI; rename_tac t i; case_tac "t i"; fastforce simp: data_at_def obj_at_pres)+ 842 done 843 844end 845 846 847context retype_region_proofs begin 848 849interpretation retype_region_proofs_arch .. 850 851lemma valid_vspace_objs': 852 assumes va: "valid_vspace_objs s" 853 shows "valid_vspace_objs s'" 854proof 855 fix p ao 856 assume p: "(\<exists>\<rhd> p) s'" 857 assume "ko_at (ArchObj ao) p s'" 858 hence "ko_at (ArchObj ao) p s \<or> ArchObj ao = default_object ty dev us" 859 by (simp add: ps_def obj_at_def s'_def split: if_split_asm) 860 moreover 861 { assume "ArchObj ao = default_object ty dev us" with tyunt 862 have "valid_vspace_obj ao s'" by (rule valid_vspace_obj_default) 863 } 864 moreover 865 { assume "ko_at (ArchObj ao) p s" 866 with va p 867 have "valid_vspace_obj ao s" 868 by (auto simp: vs_lookup' elim: valid_vspace_objsD) 869 hence "valid_vspace_obj ao s'" 870 by (rule valid_vspace_obj_pres) 871 } 872 ultimately 873 show "valid_vspace_obj ao s'" by blast 874qed 875 876 877(* ML \<open>val pre_ctxt_0 = @{context}\<close> *) 878sublocale retype_region_proofs_gen?: retype_region_proofs_gen 879 by (unfold_locales, 880 auto simp: hyp_refs_eq[simplified s'_def ps_def] 881 valid_default_arch_tcb) 882(* local_setup \<open>note_new_facts pre_ctxt_0\<close> *) 883 884end 885 886 887context Arch begin global_naming ARM (*FIXME: arch_split*) 888 889definition 890 valid_vs_lookup2 :: "(vs_ref list \<times> word32) set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool" 891where 892 "valid_vs_lookup2 lookup caps \<equiv> 893 \<forall>p ref. (ref, p) \<in> lookup \<longrightarrow> 894 ref \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None] \<and> 895 (\<exists>p' cap. caps p' = Some cap \<and> p \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref)" 896 897 898lemma valid_vs_lookup_def2: 899 "valid_vs_lookup s = valid_vs_lookup2 (vs_lookup_pages s) (null_filter (caps_of_state s))" 900 apply (simp add: valid_vs_lookup_def valid_vs_lookup2_def) 901 apply (intro iff_allI imp_cong[OF refl] disj_cong[OF refl] 902 iff_exI conj_cong[OF refl]) 903 apply (auto simp: null_filter_def) 904 done 905 906 907lemma unique_table_caps_null: 908 "unique_table_caps (null_filter s) 909 = unique_table_caps s" 910 apply (simp add: unique_table_caps_def) 911 apply (intro iff_allI) 912 apply (clarsimp simp: null_filter_def) 913 done 914 915 916lemma unique_table_refs_null: 917 "unique_table_refs (null_filter s) 918 = unique_table_refs s" 919 apply (simp only: unique_table_refs_def) 920 apply (intro iff_allI) 921 apply (clarsimp simp: null_filter_def) 922 apply (auto dest!: obj_ref_none_no_asid[rule_format] 923 simp: table_cap_ref_def) 924 done 925 926 927lemma pspace_respects_device_regionI: 928 assumes uat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz)) 929 \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - device_region s" 930 and dat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage True sz)) 931 \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> device_region s" 932 and inv: "pspace_aligned s" "valid_objs s" 933 shows "pspace_respects_device_region s" 934 935 apply (simp add: pspace_respects_device_region_def,intro conjI) 936 apply (rule subsetI) 937 apply (clarsimp simp: dom_def user_mem_def obj_at_def in_user_frame_def split: if_split_asm) 938 apply (frule uat) 939 apply (cut_tac ko = "(ArchObj (DataPage False sz))" in p_in_obj_range_internal[OF _ inv]) 940 prefer 2 941 apply (fastforce simp: obj_bits_def) 942 apply simp 943 apply (rule subsetI) 944 apply (clarsimp simp: dom_def device_mem_def obj_at_def in_device_frame_def split: if_split_asm) 945 apply (frule dat) 946 apply (cut_tac ko = "(ArchObj (DataPage True sz))" in p_in_obj_range_internal[OF _ inv]) 947 prefer 2 948 apply (fastforce simp: obj_bits_def) 949 apply simp 950 done 951 952lemma obj_range_respect_device_range: 953 "\<lbrakk>kheap s ptr = Some (ArchObj (DataPage dev sz));pspace_aligned s\<rbrakk> \<Longrightarrow> 954 obj_range ptr (ArchObj $ DataPage dev sz) \<subseteq> (if dev then dom (device_mem s) else dom (user_mem s))" 955 apply (drule(1) pspace_alignedD[rotated]) 956 apply (clarsimp simp: user_mem_def in_user_frame_def obj_at_def obj_range_def device_mem_def in_device_frame_def) 957 apply (intro impI conjI) 958 apply clarsimp 959 apply (rule exI[where x = sz]) 960 apply (simp add: mask_in_range[symmetric,THEN iffD1] a_type_def) 961 apply clarsimp 962 apply (rule exI[where x = sz]) 963 apply (simp add: mask_in_range[symmetric,THEN iffD1] a_type_def) 964 done 965 966lemma pspace_respects_device_regionD: 967 assumes inv: "pspace_aligned s" "valid_objs s" "pspace_respects_device_region s" 968 shows uat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage False sz)) 969 \<Longrightarrow> obj_range ptr (ArchObj $ DataPage False sz) \<subseteq> - device_region s" 970 and dat: "\<And>ptr sz. kheap s ptr = Some (ArchObj (DataPage True sz)) 971 \<Longrightarrow> obj_range ptr (ArchObj $ DataPage True sz) \<subseteq> device_region s" 972 using inv 973 apply (simp_all add: pspace_respects_device_region_def) 974 apply (rule subsetI) 975 apply (drule obj_range_respect_device_range[OF _ inv(1)]) 976 apply (clarsimp split: if_splits) 977 apply (drule(1) subsetD[rotated]) 978 apply (drule(1) subsetD[rotated]) 979 apply (simp add: dom_def) 980 apply (rule subsetI) 981 apply (drule obj_range_respect_device_range[OF _ inv(1)]) 982 apply (clarsimp split: if_splits) 983 apply (drule(1) subsetD[rotated]) 984 apply (drule(1) subsetD[rotated]) 985 apply (simp add: dom_def) 986 done 987 988 989lemma default_obj_dev: 990 "\<lbrakk>ty \<noteq> Untyped;default_object ty dev us = ArchObj (DataPage dev' sz)\<rbrakk> \<Longrightarrow> dev = dev'" 991 by (clarsimp simp: default_object_def default_arch_object_def 992 split: apiobject_type.split_asm aobject_type.split_asm) 993 994 995definition 996 region_in_kernel_window :: "word32 set \<Rightarrow> 'z state \<Rightarrow> bool" 997where 998 "region_in_kernel_window S \<equiv> 999 \<lambda>s. \<forall>x \<in> S. arm_kernel_vspace (arch_state s) x = ArmVSpaceKernelWindow" 1000 1001end 1002 1003context begin interpretation Arch . 1004requalify_consts region_in_kernel_window 1005end 1006 1007 1008lemma cap_range_respects_device_region_cong[cong]: 1009 "device_state (machine_state s) = device_state (machine_state s') 1010 \<Longrightarrow> cap_range_respects_device_region cap s = cap_range_respects_device_region cap s'" 1011 by (clarsimp simp: cap_range_respects_device_region_def) 1012 1013 1014context retype_region_proofs_arch begin 1015 1016lemmas unique_table_caps_eq 1017 = arg_cong[where f=unique_table_caps, OF null_filter, 1018 simplified unique_table_caps_null] 1019 1020lemmas unique_table_refs_eq 1021 = arg_cong[where f=unique_table_refs, OF null_filter, 1022 simplified unique_table_refs_null] 1023 1024lemma valid_table_caps: 1025 "valid_table_caps s \<Longrightarrow> valid_table_caps s'" 1026 apply (simp add: valid_table_caps_def 1027 del: imp_disjL) 1028 apply (elim allEI, intro impI, simp) 1029 apply (frule caps_retype[rotated]) 1030 apply clarsimp 1031 apply (rule obj_at_pres) 1032 apply simp 1033 done 1034 1035lemma valid_arch_caps: 1036 "valid_arch_caps s \<Longrightarrow> valid_arch_caps s'" 1037 by (clarsimp simp add: valid_arch_caps_def null_filter 1038 valid_vs_lookup_def2 vs_lookup_pages' 1039 unique_table_caps_eq 1040 unique_table_refs_eq 1041 valid_table_caps) 1042 1043lemma valid_global_objs: 1044 "valid_global_objs s \<Longrightarrow> valid_global_objs s'" 1045 apply (simp add: valid_global_objs_def valid_vso_at_def) 1046 apply (elim conjE, intro conjI ballI) 1047 apply (erule exEI) 1048 apply (simp add: obj_at_pres valid_vspace_obj_pres) 1049 apply (simp add: obj_at_pres) 1050 apply (rule exEI, erule(1) bspec) 1051 apply (simp add: obj_at_pres) 1052 done 1053 1054lemma valid_kernel_mappings: 1055 "valid_kernel_mappings s \<Longrightarrow> valid_kernel_mappings s'" 1056 apply (simp add: valid_kernel_mappings_def s'_def 1057 ball_ran_eq ps_def) 1058 apply (simp add: default_object_def valid_kernel_mappings_if_pd_def 1059 tyunt default_arch_object_def pde_ref_def 1060 split: Structures_A.apiobject_type.split 1061 aobject_type.split) 1062 done 1063 1064lemma valid_asid_map: 1065 "valid_asid_map s \<Longrightarrow> valid_asid_map s'" 1066 apply (clarsimp simp: valid_asid_map_def) 1067 apply (drule bspec, blast) 1068 apply (clarsimp simp: vspace_at_asid_def) 1069 apply (drule vs_lookup_2ConsD) 1070 apply clarsimp 1071 apply (erule vs_lookup_atE) 1072 apply (drule vs_lookup1D) 1073 apply clarsimp 1074 apply (drule obj_at_pres) 1075 apply (fastforce simp: vs_asid_refs_def graph_of_def 1076 intro: vs_lookupI vs_lookup1I) 1077 done 1078 1079lemma equal_kernel_mappings: 1080 "equal_kernel_mappings s \<Longrightarrow> 1081 if ty = ArchObject PageDirectoryObj 1082 then equal_kernel_mappings 1083 (s'\<lparr>kheap := kheap s' |` (- set (retype_addrs ptr ty n us))\<rparr>) 1084 else equal_kernel_mappings s'" 1085 apply (simp add: equal_kernel_mappings_def) 1086 apply (intro conjI impI) 1087 apply (elim allEI) 1088 apply (simp add: obj_at_def restrict_map_def) 1089 apply (simp add: s'_def ps_def) 1090 apply (elim allEI) 1091 apply (simp add: obj_at_def restrict_map_def) 1092 apply (simp add: s'_def ps_def) 1093 apply (simp add: default_object_def default_arch_object_def tyunt 1094 split: Structures_A.apiobject_type.split 1095 aobject_type.split) 1096 done 1097 1098lemma valid_global_vspace_mappings: 1099 "valid_global_vspace_mappings s 1100 \<Longrightarrow> valid_global_vspace_mappings s'" 1101 apply (erule valid_global_vspace_mappings_pres) 1102 apply (simp | erule obj_at_pres)+ 1103 done 1104 1105lemma pspace_in_kernel_window: 1106 "\<lbrakk> pspace_in_kernel_window (s :: 'state_ext state); 1107 region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1} s \<rbrakk> 1108 \<Longrightarrow> pspace_in_kernel_window s'" 1109 apply (simp add: pspace_in_kernel_window_def s'_def ps_def) 1110 apply (clarsimp simp: region_in_kernel_window_def 1111 del: ballI) 1112 apply (drule retype_addrs_mem_subset_ptr_bits[OF cover tyunt]) 1113 apply (fastforce simp: field_simps obj_bits_dev_irr tyunt) 1114 done 1115 1116lemma pspace_respects_device_region: 1117 assumes psp_resp_dev: "pspace_respects_device_region s" 1118 and cap_refs_resp_dev: "cap_refs_respects_device_region s" 1119 shows "pspace_respects_device_region s'" 1120 proof - 1121 note blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff 1122 atLeastatMost_subset_iff atLeastLessThan_iff 1123 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 1124 show ?thesis 1125 apply (cut_tac vp) 1126 apply (rule pspace_respects_device_regionI) 1127 apply (clarsimp simp add: pspace_respects_device_region_def s'_def ps_def 1128 split: if_split_asm ) 1129 apply (drule retype_addrs_obj_range_subset[OF _ _ tyunt]) 1130 using cover tyunt 1131 apply (simp add: obj_bits_api_def3 split: if_splits) 1132 apply (frule default_obj_dev[OF tyunt],simp) 1133 apply (drule(1) subsetD) 1134 apply (rule exE[OF dev]) 1135 apply (drule cap_refs_respects_device_region_cap_range[OF _ cap_refs_resp_dev]) 1136 apply (fastforce split: if_splits) 1137 apply (drule pspace_respects_device_regionD[OF _ _ psp_resp_dev, rotated -1]) 1138 apply fastforce 1139 apply fastforce 1140 apply fastforce 1141 apply (clarsimp simp add: pspace_respects_device_region_def s'_def ps_def 1142 split: if_split_asm ) 1143 apply (drule retype_addrs_obj_range_subset[OF _ _ tyunt]) 1144 using cover tyunt 1145 apply (simp add: obj_bits_api_def4 split: if_splits) 1146 apply (frule default_obj_dev[OF tyunt],simp) 1147 apply (drule(1) subsetD) 1148 apply (rule exE[OF dev]) 1149 apply (drule cap_refs_respects_device_region_cap_range[OF _ cap_refs_resp_dev]) 1150 apply (fastforce split: if_splits) 1151 apply (drule pspace_respects_device_regionD[OF _ _ psp_resp_dev, rotated -1]) 1152 apply fastforce 1153 apply fastforce 1154 apply fastforce 1155 using valid_pspace 1156 apply fastforce+ 1157 done 1158qed 1159 1160 1161 1162lemma cap_refs_respects_device_region: 1163 assumes psp_resp_dev: "pspace_respects_device_region s" 1164 and cap_refs_resp_dev: "cap_refs_respects_device_region s" 1165 shows "cap_refs_respects_device_region s'" 1166 using cap_refs_resp_dev 1167 apply (clarsimp simp: cap_refs_respects_device_region_def 1168 simp del: split_paired_All split_paired_Ex) 1169 apply (drule_tac x = "(a,b)" in spec) 1170 apply (erule notE) 1171 apply (subst(asm) cte_retype) 1172 apply (simp add: cap_range_respects_device_region_def cap_range_def) 1173 apply (clarsimp simp: cte_wp_at_caps_of_state s'_def dom_def) 1174 done 1175 1176 1177lemma vms: 1178 "valid_machine_state s \<Longrightarrow> valid_machine_state s'" 1179 apply (simp add: s'_def ps_def valid_machine_state_def in_user_frame_def) 1180 apply (rule allI, erule_tac x=p in allE, clarsimp) 1181 apply (rule_tac x=sz in exI, clarsimp simp: obj_at_def orthr) 1182 done 1183 1184end 1185 1186 1187context retype_region_proofs begin 1188 1189interpretation retype_region_proofs_arch .. 1190 1191lemma post_retype_invs: 1192 "\<lbrakk> invs s; region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} s \<rbrakk> 1193 \<Longrightarrow> post_retype_invs ty (retype_addrs ptr ty n us) s'" 1194 using equal_kernel_mappings 1195 by (clarsimp simp: invs_def post_retype_invs_def valid_state_def 1196 unsafe_rep2 null_filter valid_idle 1197 valid_reply_caps valid_reply_masters 1198 valid_global_refs valid_arch_state 1199 valid_irq_node_def obj_at_pres 1200 valid_arch_caps valid_global_objs 1201 valid_vspace_objs' valid_irq_handlers 1202 valid_mdb_rep2 mdb_and_revokable 1203 valid_pspace cur_tcb only_idle 1204 valid_kernel_mappings valid_asid_map 1205 valid_global_vspace_mappings valid_ioc vms 1206 pspace_in_kernel_window pspace_respects_device_region 1207 cap_refs_respects_device_region 1208 cap_refs_in_kernel_window valid_irq_states 1209 split: if_split_asm) 1210 1211(* ML \<open>val pre_ctxt_1 = @{context}\<close> *) 1212 1213sublocale retype_region_proofs_invs?: retype_region_proofs_invs 1214 where region_in_kernel_window = region_in_kernel_window 1215 and post_retype_invs_check = post_retype_invs_check 1216 and post_retype_invs = post_retype_invs 1217 using post_retype_invs valid_cap valid_global_refs valid_arch_state valid_vspace_objs' 1218 by unfold_locales (auto simp: s'_def ps_def) 1219 1220(* local_setup \<open>note_new_facts pre_ctxt_1\<close> *) 1221 1222lemmas post_retype_invs_axioms = retype_region_proofs_invs_axioms 1223 1224end 1225 1226 1227context Arch begin global_naming ARM 1228 1229named_theorems Retype_AI_assms' 1230 1231lemma invs_post_retype_invs [Retype_AI_assms']: 1232 "invs s \<Longrightarrow> post_retype_invs ty refs s" 1233 apply (clarsimp simp: post_retype_invs_def invs_def valid_state_def) 1234 apply (clarsimp simp: equal_kernel_mappings_def obj_at_def 1235 restrict_map_def) 1236 done 1237 1238lemmas equal_kernel_mappings_trans_state 1239 = more_update.equal_kernel_mappings_update 1240 1241lemmas retype_region_proofs_assms [Retype_AI_assms'] 1242 = retype_region_proofs.post_retype_invs_axioms 1243 1244end 1245 1246 1247global_interpretation Retype_AI?: Retype_AI 1248 where no_gs_types = ARM.no_gs_types 1249 and post_retype_invs_check = post_retype_invs_check 1250 and post_retype_invs = post_retype_invs 1251 and region_in_kernel_window = region_in_kernel_window 1252 proof goal_cases 1253 interpret Arch . 1254 case 1 show ?case 1255 by (intro_locales; (unfold_locales; fact Retype_AI_assms)?) 1256 (simp add: Retype_AI_axioms_def Retype_AI_assms') 1257 qed 1258 1259 1260context Arch begin global_naming ARM 1261 1262lemma retype_region_plain_invs: 1263 "\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz 1264 and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} 1265 and region_in_kernel_window {ptr .. (ptr &&~~ mask sz) + 2 ^ sz - 1} 1266 and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. {ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)} \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) 1267 and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us) 1268 and K (range_cover ptr sz (obj_bits_api ty us) n) 1269 and K (ty \<noteq> ArchObject PageDirectoryObj)\<rbrace> 1270 retype_region ptr n us ty dev\<lbrace>\<lambda>rv. invs\<rbrace>" 1271 apply (rule hoare_gen_asm) 1272 apply (rule hoare_strengthen_post[OF retype_region_post_retype_invs]) 1273 apply (simp add: post_retype_invs_def) 1274 done 1275 1276 1277lemma storeWord_um_eq_0: 1278 "\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace> 1279 storeWord x 0 1280 \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>" 1281 by (simp add: storeWord_def word_rsplit_0 | wp)+ 1282 1283lemma clearMemory_um_eq_0: 1284 "\<lbrace>\<lambda>m. underlying_memory m p = 0\<rbrace> 1285 clearMemory ptr bits 1286 \<lbrace>\<lambda>_ m. underlying_memory m p = 0\<rbrace>" 1287 apply (clarsimp simp: clearMemory_def) 1288 apply (wp mapM_x_wp_inv | simp)+ 1289 apply (wp hoare_drop_imps storeWord_um_eq_0) 1290 apply (fastforce simp: ignore_failure_def split: if_split_asm) 1291 done 1292 1293lemma cleanCacheRange_PoU_um_inv[wp]: 1294 "\<lbrace>\<lambda>m. P (underlying_memory m)\<rbrace> 1295 cleanCacheRange_PoU ptr w p 1296 \<lbrace>\<lambda>_ m. P (underlying_memory m)\<rbrace>" 1297 by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def 1298 split_def | wp)+ 1299 1300lemma invs_irq_state_independent: 1301 "invs (s\<lparr>machine_state := machine_state s\<lparr>irq_state := f (irq_state (machine_state s))\<rparr>\<rparr>) 1302 = invs s" 1303 by (clarsimp simp: irq_state_independent_A_def invs_def 1304 valid_state_def valid_pspace_def valid_mdb_def valid_ioc_def valid_idle_def 1305 only_idle_def if_unsafe_then_cap_def valid_reply_caps_def 1306 valid_reply_masters_def valid_global_refs_def valid_arch_state_def 1307 valid_irq_node_def valid_irq_handlers_def valid_machine_state_def 1308 valid_arch_caps_def valid_global_objs_def 1309 valid_kernel_mappings_def equal_kernel_mappings_def 1310 valid_asid_map_def vspace_at_asid_def 1311 pspace_in_kernel_window_def cap_refs_in_kernel_window_def 1312 cur_tcb_def sym_refs_def state_refs_of_def 1313 swp_def valid_irq_states_def) 1314 1315crunch irq_masks_inv[wp]: cleanByVA_PoU, storeWord, clearMemory "\<lambda>s. P (irq_masks s)" 1316 (ignore: cacheRangeOp wp: crunch_wps) 1317 1318crunch underlying_mem_0[wp]: cleanByVA_PoU, clearMemory 1319 "\<lambda>s. underlying_memory s p = 0" 1320 (ignore: cacheRangeOp wp: crunch_wps storeWord_um_eq_0) 1321 1322lemma clearMemory_invs: 1323 "\<lbrace>invs\<rbrace> do_machine_op (clearMemory w sz) \<lbrace>\<lambda>_. invs\<rbrace>" 1324 apply (wp dmo_invs1) 1325 apply clarsimp 1326 apply (intro conjI impI allI) 1327 apply (clarsimp simp: invs_def valid_state_def) 1328 apply (erule_tac p=p in valid_machine_stateE) 1329 apply (clarsimp simp: use_valid[OF _ clearMemory_underlying_mem_0]) 1330 apply (clarsimp simp: use_valid[OF _ clearMemory_irq_masks_inv[where P="(=) v" for v], OF _ refl]) 1331 done 1332 1333lemma caps_region_kernel_window_imp: 1334 "caps_of_state s p = Some cap 1335 \<Longrightarrow> cap_refs_in_kernel_window s 1336 \<Longrightarrow> S \<subseteq> cap_range cap 1337 \<Longrightarrow> region_in_kernel_window S s" 1338 apply (simp add: region_in_kernel_window_def) 1339 apply (drule(1) cap_refs_in_kernel_windowD) 1340 apply blast 1341 done 1342 1343crunch irq_node[wp]: init_arch_objects "\<lambda>s. P (interrupt_irq_node s)" 1344 (wp: crunch_wps) 1345 1346lemma init_arch_objects_excap: 1347 "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> 1348 init_arch_objects tp ptr bits us refs 1349 \<lbrace>\<lambda>rv s. ex_cte_cap_wp_to P p s\<rbrace>" 1350 by (wp ex_cte_cap_to_pres) 1351 1352crunch st_tcb_at[wp]: init_arch_objects "st_tcb_at P t" 1353 (wp: crunch_wps) 1354 1355lemma valid_arch_mdb_detype: 1356 "valid_arch_mdb (is_original_cap s) (caps_of_state s) \<Longrightarrow> 1357 valid_arch_mdb (is_original_cap (detype (untyped_range cap) s)) 1358 (\<lambda>p. if fst p \<in> untyped_range cap then None else caps_of_state s p)" 1359 by auto 1360 1361end 1362 1363lemmas clearMemory_invs[wp] = ARM.clearMemory_invs 1364 1365lemmas invs_irq_state_independent[intro!, simp] 1366 = ARM.invs_irq_state_independent 1367 1368lemmas init_arch_objects_invs_from_restricted 1369 = ARM.init_arch_objects_invs_from_restricted 1370 1371lemmas caps_region_kernel_window_imp 1372 = ARM.caps_region_kernel_window_imp 1373 1374lemmas init_arch_objects_wps 1375 = ARM.init_arch_objects_cte_wp_at 1376 ARM.init_arch_objects_valid_cap 1377 ARM.init_arch_objects_cap_table 1378 ARM.init_arch_objects_excap 1379 ARM.init_arch_objects_st_tcb_at 1380 1381end 1382