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 ArchVSpaceEntries_AI 12imports "../VSpaceEntries_AI" 13begin 14 15 16context Arch begin global_naming ARM (*FIXME: arch_split*) 17 18lemma a_type_pdD: 19 "a_type ko = AArch APageDirectory \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)" 20 by (clarsimp) 21 22primrec 23 pde_range_sz :: "pde \<Rightarrow> nat" 24where 25 "pde_range_sz (InvalidPDE) = 0" 26 | "pde_range_sz (SectionPDE ptr x y z) = 0" 27 | "pde_range_sz (SuperSectionPDE ptr x z) = 4" 28 | "pde_range_sz (PageTablePDE ptr x z) = 0" 29 30primrec 31 pte_range_sz :: "pte \<Rightarrow> nat" 32where 33 "pte_range_sz (InvalidPTE) = 0" 34 | "pte_range_sz (LargePagePTE ptr x y) = 4" 35 | "pte_range_sz (SmallPagePTE ptr x y) = 0" 36 37primrec 38 pde_range :: "pde \<Rightarrow> 12 word \<Rightarrow> 12 word set" 39where 40 "pde_range (InvalidPDE) p = {}" 41 | "pde_range (SectionPDE ptr x y z) p = {p}" 42 | "pde_range (SuperSectionPDE ptr x z) p = 43 (if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})" 44 | "pde_range (PageTablePDE ptr x z) p = {p}" 45 46primrec 47 pte_range :: "pte \<Rightarrow> word8 \<Rightarrow> word8 set" 48where 49 "pte_range (InvalidPTE) p = {}" 50 | "pte_range (LargePagePTE ptr x y) p = 51 (if is_aligned p 4 then {x. x && ~~ mask 4 = p && ~~ mask 4} else {p})" 52 | "pte_range (SmallPagePTE ptr x y) p = {p}" 53 54abbreviation "valid_pt_entries \<equiv> \<lambda>pt. valid_entries pte_range pt" 55 56abbreviation "valid_pd_entries \<equiv> \<lambda>pd. valid_entries pde_range pd" 57 58definition 59 obj_valid_pdpt :: "kernel_object \<Rightarrow> bool" 60where 61 "obj_valid_pdpt obj \<equiv> case obj of 62 ArchObj (PageTable pt) \<Rightarrow> valid_pt_entries pt \<and> entries_align pte_range_sz pt 63 | ArchObj (PageDirectory pd) \<Rightarrow> valid_pd_entries pd \<and> entries_align pde_range_sz pd 64 | _ \<Rightarrow> True" 65 66lemmas obj_valid_pdpt_simps[simp] 67 = obj_valid_pdpt_def 68 [split_simps Structures_A.kernel_object.split 69 arch_kernel_obj.split] 70 71abbreviation 72 valid_pdpt_objs :: "'z state \<Rightarrow> bool" 73where 74 "valid_pdpt_objs s \<equiv> \<forall>x \<in> ran (kheap s). obj_valid_pdpt x" 75 76lemma valid_pdpt_init[iff]: 77 "valid_pdpt_objs init_A_st" 78proof - 79 have P: "valid_pd_entries (global_pd :: 12 word \<Rightarrow> _)" 80 by (clarsimp simp: valid_entries_def) 81 also have Q: "entries_align pde_range_sz (global_pd :: 12 word \<Rightarrow> _)" 82 by (clarsimp simp: entries_align_def) 83 thus ?thesis using P 84 by (auto simp: init_A_st_def init_kheap_def 85 elim!: ranE split: if_split_asm) 86qed 87 88lemma set_object_valid_pdpt[wp]: 89 "\<lbrace>valid_pdpt_objs and K (obj_valid_pdpt obj)\<rbrace> 90 set_object ptr obj 91 \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 92 apply (simp add: set_object_def, wp) 93 apply (auto simp: fun_upd_def[symmetric] del: ballI elim: ball_ran_updI) 94 done 95 96crunch valid_pdpt_objs[wp]: cap_insert, cap_swap_for_delete,empty_slot "valid_pdpt_objs" 97 (wp: crunch_wps simp: crunch_simps ignore:set_object) 98 99crunch valid_pdpt_objs[wp]: flush_page "valid_pdpt_objs" 100 (wp: crunch_wps simp: crunch_simps) 101 102lemma shift_0x3C_set: 103 "\<lbrakk> is_aligned p 6; 8 \<le> bits; bits < 32; len_of TYPE('a) = bits - 2 \<rbrakk> \<Longrightarrow> 104 (\<lambda>x. ucast (x + p && mask bits >> 2) :: ('a :: len) word) ` set [0 :: word32 , 4 .e. 0x3C] 105 = {x. x && ~~ mask 4 = ucast (p && mask bits >> 2)}" 106 apply (clarsimp simp: upto_enum_step_def word_shift_by_2 image_image) 107 apply (subst image_cong[where N="{x. x < 2 ^ 4}"]) 108 apply (safe, simp_all)[1] 109 apply (drule plus_one_helper2, simp_all)[1] 110 apply (drule minus_one_helper3, simp_all)[1] 111 apply (rule_tac f="\<lambda>x. ucast (x && mask bits >> 2)" in arg_cong) 112 apply (rule trans[OF add.commute is_aligned_add_or], assumption) 113 apply (rule shiftl_less_t2n, simp_all)[1] 114 apply safe 115 apply (frule upper_bits_unset_is_l2p_32[THEN iffD2, rotated]) 116 apply (simp add: word_bits_conv) 117 apply (rule word_eqI) 118 apply (simp add: word_ops_nth_size word_size nth_ucast nth_shiftr 119 nth_shiftl neg_mask_bang 120 word_bits_conv) 121 apply (safe, simp_all add: is_aligned_nth)[1] 122 apply (drule_tac x="Suc (Suc n)" in spec) 123 apply simp 124 apply (rule_tac x="ucast x && mask 4" in image_eqI) 125 apply (rule word_eqI[rule_format]) 126 apply (drule_tac x=n in word_eqD) 127 apply (simp add: word_ops_nth_size word_size nth_ucast nth_shiftr 128 nth_shiftl) 129 apply (safe, simp_all) 130 apply (rule order_less_le_trans, rule and_mask_less_size) 131 apply (simp_all add: word_size) 132 done 133 134lemma mapM_x_store_pte_updates: 135 "\<forall>x \<in> set xs. f x && ~~ mask pt_bits = p \<Longrightarrow> 136 \<lbrace>\<lambda>s. (\<not> page_table_at p s \<longrightarrow> Q s) \<and> 137 (\<forall>pt. ko_at (ArchObj (PageTable pt)) p s 138 \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p := Some (ArchObj (PageTable (\<lambda>y. if y \<in> (\<lambda>x. 139 ucast (f x && mask pt_bits >> 2)) ` set xs then pte else pt y)))) \<rparr>))\<rbrace> 140 mapM_x (\<lambda>x. store_pte (f x) pte) xs 141 \<lbrace>\<lambda>_. Q\<rbrace>" 142 apply (induct xs) 143 apply (simp add: mapM_x_Nil) 144 apply wp 145 apply (clarsimp simp: obj_at_def fun_upd_idem) 146 apply (simp add: mapM_x_Cons) 147 apply (rule hoare_seq_ext, assumption) 148 apply (thin_tac "valid P f Q" for P f Q) 149 apply (simp add: store_pte_def set_pt_def set_object_def) 150 apply (wp get_pt_wp get_object_wp) 151 apply (clarsimp simp: obj_at_def a_type_simps) 152 apply (erule rsubst[where P=Q]) 153 apply (rule abstract_state.fold_congs[OF refl refl]) 154 apply (rule ext, clarsimp) 155 apply (rule ext, clarsimp) 156 done 157 158lemma valid_pt_entries_invalid[simp]: 159 "valid_pt_entries (\<lambda>x. InvalidPTE)" 160 by (simp add:valid_entries_def) 161 162lemma valid_pd_entries_invalid[simp]: 163 "valid_pd_entries (\<lambda>x. InvalidPDE)" 164 by (simp add:valid_entries_def) 165 166lemma entries_align_pte_update: 167 "\<lbrakk>entries_align pte_range_sz pt; 168 (\<forall>y. (P y) \<longrightarrow> is_aligned y (pte_range_sz pte))\<rbrakk> 169 \<Longrightarrow> entries_align pte_range_sz (\<lambda>y. if (P y) then pte else pt y)" 170 by (simp add:entries_align_def) 171 172lemma entries_align_pde_update: 173 "\<lbrakk>entries_align pde_range_sz pd; 174 (\<forall>y. (P y) \<longrightarrow> is_aligned y (pde_range_sz pde))\<rbrakk> 175 \<Longrightarrow> entries_align pde_range_sz (\<lambda>y. if (P y) then pde else pd y)" 176 by (simp add:entries_align_def) 177 178 179lemma valid_pdpt_objs_pdD: 180 "\<lbrakk>valid_pdpt_objs s; 181 kheap s ptr = Some (ArchObj (arch_kernel_obj.PageDirectory pd))\<rbrakk> 182 \<Longrightarrow> valid_pd_entries pd \<and> entries_align pde_range_sz pd" 183 by (fastforce simp:ran_def) 184 185lemma valid_pdpt_objs_ptD: 186 "\<lbrakk>valid_pdpt_objs s; 187 kheap s ptr = Some (ArchObj (arch_kernel_obj.PageTable pt))\<rbrakk> 188 \<Longrightarrow> valid_pt_entries pt \<and> entries_align pte_range_sz pt" 189 by (fastforce simp:ran_def) 190 191lemma mapM_x_store_invalid_pte_valid_pdpt: 192 "\<lbrace>valid_pdpt_objs and K (is_aligned p 6) \<rbrace> 193 mapM_x (\<lambda>x. store_pte (x + p) InvalidPTE) [0, 4 .e. 0x3C] 194 \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" 195 apply (rule hoare_gen_asm)+ 196 apply (rule hoare_pre, rule_tac p="p && ~~ mask pt_bits" in mapM_x_store_pte_updates) 197 apply clarsimp 198 apply (rule mask_out_first_mask_some[where n=6]) 199 apply (drule_tac d=x in is_aligned_add_helper) 200 apply (drule subsetD[OF upto_enum_step_subset]) 201 apply simp 202 apply (erule order_le_less_trans, simp) 203 apply (simp add: field_simps) 204 apply (simp add: pt_bits_def pageBits_def) 205 apply (clarsimp simp: ranI elim!: ranE split: if_split_asm) 206 apply (intro conjI) 207 apply (simp add: shift_0x3C_set pt_bits_def pageBits_def) 208 apply (rule valid_entries_overwrite_groups 209 [where S = "{x. x && ~~ mask 4 = ucast (p && mask 10 >> 2)}"]) 210 apply (fastforce simp add: obj_at_def ran_def) 211 apply simp 212 apply clarsimp 213 apply (case_tac v) 214 apply (simp split:if_splits)+ 215 apply (clarsimp) 216 apply (case_tac v, simp_all split:if_splits) 217 apply (intro conjI impI) 218 apply (rule disjointI) 219 apply (clarsimp)+ 220 apply (rule entries_align_pte_update) 221 apply (clarsimp simp:obj_at_def) 222 apply (drule(1) valid_pdpt_objs_ptD) 223 apply simp 224 apply (simp) 225 done 226 227lemma mapM_x_store_pde_updates: 228 "\<forall>x \<in> set xs. f x && ~~ mask pd_bits = p \<Longrightarrow> 229 \<lbrace>\<lambda>s. (\<not> page_directory_at p s \<longrightarrow> Q s) \<and> 230 (\<forall>pd. ko_at (ArchObj (PageDirectory pd)) p s 231 \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p := Some (ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. 232 ucast (f x && mask pd_bits >> 2)) ` set xs then pde else pd y)))) \<rparr>))\<rbrace> 233 mapM_x (\<lambda>x. store_pde (f x) pde) xs 234 \<lbrace>\<lambda>_. Q\<rbrace>" 235 apply (induct xs) 236 apply (simp add: mapM_x_Nil) 237 apply wp 238 apply (clarsimp simp: obj_at_def fun_upd_idem) 239 apply (simp add: mapM_x_Cons) 240 apply (rule hoare_seq_ext, assumption) 241 apply (thin_tac "valid P f Q" for P f Q) 242 apply (simp add: store_pde_def set_pd_def set_object_def) 243 apply (wp get_pd_wp get_object_wp) 244 apply (clarsimp simp: obj_at_def a_type_simps) 245 apply (erule rsubst[where P=Q]) 246 apply (rule abstract_state.fold_congs[OF refl refl]) 247 apply (rule ext, clarsimp) 248 apply (rule ext, clarsimp) 249 done 250 251lemma mapM_x_store_pde_valid_pdpt_objs: 252 "\<lbrace>valid_pdpt_objs and K (is_aligned p 6)\<rbrace> 253 mapM_x (\<lambda>x. store_pde (x + p) InvalidPDE) [0, 4 .e. 0x3C] 254 \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" 255 apply (rule hoare_gen_asm)+ 256 apply (rule hoare_pre, rule_tac p="p && ~~ mask pd_bits" in mapM_x_store_pde_updates) 257 apply clarsimp 258 apply (rule mask_out_first_mask_some[where n=6]) 259 apply (drule_tac d=x in is_aligned_add_helper) 260 apply (drule subsetD[OF upto_enum_step_subset]) 261 apply simp 262 apply (erule order_le_less_trans, simp) 263 apply (simp add: field_simps) 264 apply (simp add: pd_bits_def pageBits_def) 265 apply (clarsimp simp: ranI elim!: ranE split: if_split_asm) 266 apply (simp add: shift_0x3C_set pd_bits_def pageBits_def) 267 apply (rule conjI) 268 apply (rule_tac valid_entries_overwrite_groups 269 [where S = "{x. x && ~~ mask 4 = ucast (p && mask 14 >> 2)}"]) 270 apply (fastforce simp add: obj_at_def ran_def) 271 apply fastforce 272 apply clarsimp 273 apply (case_tac v, simp_all split:if_splits) 274 apply clarsimp 275 apply (case_tac v, simp_all split:if_splits) 276 apply (intro conjI impI allI) 277 apply (rule disjointI) 278 apply clarsimp 279 apply (rule entries_align_pde_update) 280 apply (clarsimp simp:obj_at_def) 281 apply (drule valid_pdpt_objs_pdD) 282 apply (simp add:pd_bits_def pageBits_def) 283 apply simp 284 apply simp 285 done 286 287lemma store_invalid_pde_valid_pdpt: 288 "\<lbrace>valid_pdpt_objs and 289 (\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s 290 \<longrightarrow> pde = InvalidPDE)\<rbrace> 291 store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 292 apply (simp add: store_pde_def set_pd_def, wp get_object_wp) 293 apply (clarsimp simp: obj_at_def) 294 apply (intro conjI) 295 apply (rule valid_entries_overwrite_0, simp_all) 296 apply (fastforce simp: ran_def) 297 apply (simp add:fun_upd_def) 298 apply (rule entries_align_pde_update) 299 apply (drule(1) valid_pdpt_objs_pdD) 300 apply simp 301 apply simp 302 done 303 304lemma store_pde_non_master_valid_pdpt: 305 "\<lbrace>valid_pdpt_objs and 306 (\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s 307 \<longrightarrow> (pde_range_sz (pd (ucast (p && mask pd_bits >> 2) && ~~ mask 4)) = 0 308 \<and> pde_range_sz pde = 0))\<rbrace> 309 store_pde p pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 310 apply (simp add: store_pde_def set_pd_def, wp get_object_wp) 311 apply (clarsimp simp: obj_at_def) 312 apply (intro conjI) 313 apply (rule valid_entries_overwrite_0) 314 apply (fastforce simp:ran_def) 315 apply (drule bspec) 316 apply fastforce 317 apply (case_tac "pd pa") 318 apply simp_all 319 apply (case_tac pde,simp_all) 320 apply (case_tac pde,simp_all) 321 apply (case_tac pde,simp_all) 322 apply (clarsimp simp: is_aligned_neg_mask_eq)+ 323 apply (simp add:fun_upd_def) 324 apply (rule entries_align_pde_update) 325 apply (drule(1) valid_pdpt_objs_pdD,simp) 326 apply simp 327 done 328 329lemma store_invalid_pte_valid_pdpt: 330 "\<lbrace>valid_pdpt_objs and 331 (\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s 332 \<longrightarrow> pte = InvalidPTE)\<rbrace> 333 store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 334 apply (simp add: store_pte_def set_pt_def, wp get_object_wp) 335 apply (clarsimp simp: obj_at_def) 336 apply (intro conjI) 337 apply (rule valid_entries_overwrite_0, simp_all) 338 apply (fastforce simp: ran_def) 339 apply (simp add:fun_upd_def) 340 apply (rule entries_align_pte_update) 341 apply (drule (1) valid_pdpt_objs_ptD,simp) 342 apply simp 343 done 344 345lemma store_pte_non_master_valid_pdpt: 346 "\<lbrace>valid_pdpt_objs and 347 (\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s 348 \<longrightarrow> (pte_range_sz (pt (ucast (p && mask pt_bits >> 2) && ~~ mask 4)) = 0 349 \<and> pte_range_sz pte = 0))\<rbrace> 350 store_pte p pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 351 apply (simp add: store_pte_def set_pt_def, wp get_object_wp) 352 apply (clarsimp simp: obj_at_def) 353 apply (intro conjI) 354 apply (rule valid_entries_overwrite_0) 355 apply (fastforce simp:ran_def) 356 apply (drule bspec) 357 apply fastforce 358 apply (case_tac "pt pa") 359 apply simp 360 apply (case_tac pte,simp_all) 361 apply (clarsimp simp: is_aligned_neg_mask_eq) 362 apply (case_tac pte,simp_all) 363 apply (simp add:fun_upd_def) 364 apply (rule entries_align_pte_update) 365 apply (drule (1) valid_pdpt_objs_ptD,simp) 366 apply simp 367 done 368 369lemma unmap_page_valid_pdpt[wp]: 370 "\<lbrace>valid_pdpt_objs\<rbrace> unmap_page sz asid vptr pptr \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 371 apply (simp add: unmap_page_def mapM_discarded 372 cong: vmpage_size.case_cong) 373 apply (wp) 374 prefer 2 375 apply (rule valid_validE[OF find_pd_for_asid_inv]) 376 apply (rule hoare_pre) 377 apply (wp get_object_wp get_pte_wp get_pde_wp lookup_pt_slot_inv_any 378 store_invalid_pte_valid_pdpt 379 store_invalid_pde_valid_pdpt 380 mapM_x_store_invalid_pte_valid_pdpt mapM_x_store_pde_valid_pdpt_objs 381 | simp add: mapM_x_map 382 | wpc | simp add: check_mapping_pptr_def)+ 383 apply (simp add: fun_upd_def[symmetric] is_aligned_mask[symmetric]) 384 apply assumption 385 done 386 387crunch valid_pdpt_objs[wp]: flush_table "valid_pdpt_objs" 388 (wp: crunch_wps simp: crunch_simps) 389 390crunch kheap[wp]: flush_table "\<lambda>s. P (kheap s)" 391 (wp: crunch_wps simp: crunch_simps) 392 393lemma unmap_page_table_valid_pdpt_objs[wp]: 394 notes hoare_pre [wp_pre del] 395 shows "\<lbrace>valid_pdpt_objs\<rbrace> unmap_page_table asid vptr pt \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 396 apply (simp add: unmap_page_table_def) 397 apply (wp get_object_wp store_invalid_pde_valid_pdpt | wpc)+ 398 apply (simp add: obj_at_def) 399 apply (simp add: page_table_mapped_def) 400 apply (wp get_pde_wp | wpc)+ 401 apply simp 402 apply (rule hoare_post_impErr, rule valid_validE, 403 rule find_pd_for_asid_inv, simp_all) 404 done 405 406lemma set_simple_ko_valid_pdpt_objs[wp]: 407 "\<lbrace>\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> 408 set_simple_ko param_a param_b param_c \<lbrace>\<lambda>_ s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x\<rbrace> " 409 by (set_simple_ko_method wp_thm: set_object_valid_pdpt simp_thm: get_object_def) 410 411crunch valid_pdpt_objs[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_pdpt_objs" 412 (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object) 413 414lemma preemption_point_valid_pdpt_objs[wp]: 415 "\<lbrace>valid_pdpt_objs\<rbrace> preemption_point \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 416 by (wp preemption_point_inv | simp)+ 417 418lemmas cap_revoke_preservation_valid_pdpt_objs = cap_revoke_preservation[OF _, 419 where E=valid_pdpt_objs, 420 simplified, THEN validE_valid] 421 422lemmas rec_del_preservation_valid_pdpt_objs = rec_del_preservation[OF _ _ _ _, 423 where P=valid_pdpt_objs, simplified] 424 425crunch valid_pdpt_objs[wp]: cap_delete, cap_revoke "valid_pdpt_objs" 426 (rule: rec_del_preservation_valid_pdpt_objs cap_revoke_preservation_valid_pdpt_objs) 427 428crunch valid_pdpt_objs[wp]: invalidate_tlb_by_asid, page_table_mapped 429 "valid_pdpt_objs" 430 431lemma mapM_x_copy_pde_updates: 432 "\<lbrakk> \<forall>x \<in> set xs. f x && ~~ mask pd_bits = 0; is_aligned p pd_bits; 433 is_aligned p' pd_bits \<rbrakk> \<Longrightarrow> 434 \<lbrace>\<lambda>s. (\<not> page_directory_at p s \<longrightarrow> Q s) \<and> (\<not> page_directory_at p' s \<longrightarrow> Q s) \<and> 435 (\<forall>pd pd'. ko_at (ArchObj (PageDirectory pd)) p s 436 \<and> ko_at (ArchObj (PageDirectory pd')) p' s 437 \<longrightarrow> Q (s \<lparr> kheap := (kheap s) (p' := Some (ArchObj (PageDirectory (\<lambda>y. if y \<in> (\<lambda>x. 438 ucast (f x && mask pd_bits >> 2)) ` set xs then pd y else pd' y)))) \<rparr>))\<rbrace> 439 mapM_x (\<lambda>x. get_pde (p + f x) >>= store_pde (p' + f x)) xs 440 \<lbrace>\<lambda>_. Q\<rbrace>" 441 apply (induct xs) 442 apply (simp add: mapM_x_Nil) 443 apply wp 444 apply (clarsimp simp: obj_at_def fun_upd_idem dest!: a_type_pdD) 445 apply (simp add: mapM_x_Cons) 446 apply wp 447 apply (thin_tac "valid P f Q" for P f Q) 448 apply (simp add: store_pde_def set_pd_def set_object_def 449 cong: bind_cong split del: if_split) 450 apply (wp get_object_wp get_pde_wp) 451 apply (clarsimp simp: obj_at_def a_type_simps mask_out_add_aligned[symmetric] 452 split del: if_split) 453 apply (simp add: a_type_simps, safe) 454 apply (erule rsubst[where P=Q]) 455 apply (rule abstract_state.fold_congs[OF refl refl]) 456 apply (rule ext, clarsimp) 457 apply (rule ext, simp) 458 apply (erule rsubst[where P=Q]) 459 apply (rule abstract_state.fold_congs[OF refl refl]) 460 apply (rule ext, clarsimp) 461 apply (rule ext, simp add: mask_add_aligned) 462 done 463 464lemma copy_global_mappings_valid_pdpt_objs[wp]: 465 notes hoare_pre [wp_pre del] 466 shows 467 "\<lbrace>valid_pdpt_objs and valid_arch_state and pspace_aligned 468 and K (is_aligned p pd_bits)\<rbrace> 469 copy_global_mappings p \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 470 apply (rule hoare_gen_asm) 471 apply (simp add: copy_global_mappings_def) 472 apply wp 473 apply (rule_tac P="is_aligned global_pd pd_bits" in hoare_gen_asm) 474 apply (rule mapM_x_copy_pde_updates, simp_all) 475 apply (clarsimp simp: mask_eq_x_eq_0[symmetric]) 476 apply (rule less_mask_eq, rule shiftl_less_t2n, 477 simp_all add: pd_bits_def pageBits_def)[1] 478 apply (drule plus_one_helper2, simp+) 479 apply wp 480 apply (clarsimp simp: invs_aligned_pdD ranI 481 elim!: ranE split: if_split_asm) 482 apply (intro conjI) 483 apply (rule_tac S="{x. ucast x \<ge> (kernel_base >> 20)}" 484 in valid_entries_partial_copy) 485 apply (fastforce simp: obj_at_def ran_def) 486 apply (fastforce simp: obj_at_def ran_def) 487 apply (clarsimp simp:image_def) 488 apply (subst (asm) less_mask_eq) 489 apply (rule shiftl_less_t2n) 490 apply (simp add:pd_bits_def pageBits_def word_le_make_less) 491 apply (simp add:pd_bits_def pageBits_def) 492 apply (subst (asm) shiftl_shiftr1) 493 apply simp 494 apply (simp add:word_size) 495 apply (subst (asm) less_mask_eq) 496 apply (simp add:pd_bits_def pageBits_def le_less_trans) 497 apply (case_tac v) 498 apply (simp add:ucast_ucast_len pd_bits_def pageBits_def le_less_trans)+ 499 apply (clarsimp split:if_splits) 500 apply (simp add:kernel_base_shift_cast_le) 501 apply (simp add:kernel_base_def) 502 apply (cut_tac y1 = xb and x1 = "0xE00::12 word" in ucast_le_migrate[THEN iffD1,rotated -1]) 503 apply simp 504 apply (simp add:word_size le_less_trans) 505 apply (simp add:word_size) 506 apply (drule aligned_le_sharp[where n = 4 and a = "0xE00::12 word"]) 507 apply (simp add:kernel_base_def is_aligned_def) 508 apply (erule order_trans) 509 apply (erule subst) 510 apply (simp add:word_and_le2) 511 apply (subst ucast_ucast_len) 512 apply (simp,word_bitwise) 513 apply simp 514 apply (clarsimp simp:image_def) 515 apply (rule disjointI) 516 apply clarsimp 517 apply (drule_tac x = "ucast x" in spec) 518 apply (erule impE) 519 apply (simp add:pd_bits_def pageBits_def) 520 apply word_bitwise 521 apply (subgoal_tac "kernel_base >> 20 \<le> ucast x") 522 apply simp 523 apply (subst (asm) less_mask_eq) 524 apply (rule shiftl_less_t2n) 525 apply (simp add:pd_bits_def pageBits_def word_le_make_less) 526 apply word_bitwise 527 apply (simp add:pd_bits_def pageBits_def) 528 apply (subst (asm) shiftl_shiftr1) 529 apply simp 530 apply (simp add:word_size) 531 apply (subst (asm) less_mask_eq) 532 apply (rule less_le_trans[OF ucast_less]) 533 apply simp 534 apply simp 535 apply word_bitwise 536 apply (case_tac v,simp_all) 537 apply (clarsimp split:if_splits) 538 apply (drule aligned_le_sharp[where n = 4]) 539 apply (simp add:kernel_base_def is_aligned_def) 540 apply (simp add:word_size kernel_base_def pd_bits_def pageBits_def) 541 apply word_bitwise 542 apply simp 543 apply (clarsimp simp:obj_at_def) 544 apply (subst (asm) is_aligned_neg_mask_eq 545 [where p = p and n = pd_bits,symmetric]) 546 apply simp 547 apply (drule(1) valid_pdpt_objs_pdD[rotated])+ 548 apply (clarsimp simp:entries_align_def) 549 done 550 551lemma in_pte_rangeD: 552 "x \<in> pte_range v y \<Longrightarrow> x && ~~ mask 4 = y && ~~ mask 4" 553 by (case_tac v,simp_all split:if_splits) 554 555lemma in_pde_rangeD: 556 "x \<in> pde_range v y \<Longrightarrow> x && ~~ mask 4 = y && ~~ mask 4" 557 by (case_tac v,simp_all split:if_splits) 558 559lemma mapM_x_store_pte_valid_pdpt2: 560 "\<lbrace>valid_pdpt_objs and K (is_aligned ptr pt_bits)\<rbrace> 561 mapM_x (\<lambda>x. store_pte x InvalidPTE) [ptr, ptr + 4 .e. ptr + 2 ^ pt_bits - 1] 562 \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" 563 apply (rule hoare_gen_asm)+ 564 apply (rule mapM_x_wp') 565 apply (simp add:store_pte_def set_pt_def) 566 apply (wp get_pt_wp get_object_wp) 567 apply (clarsimp simp: mask_in_range 568 split:Structures_A.kernel_object.splits 569 arch_kernel_obj.splits) 570 apply (rule conjI) 571 apply (rule valid_entries_overwrite_0) 572 apply (fastforce simp:ran_def obj_at_def) 573 apply simp 574 apply (simp add:fun_upd_def obj_at_def) 575 apply (rule entries_align_pte_update) 576 apply (drule (1) valid_pdpt_objs_ptD,simp) 577 apply simp 578 done 579 580lemma mapM_x_store_pde_valid_pdpt2: 581 "\<lbrace>valid_pdpt_objs and K (is_aligned pd pd_bits)\<rbrace> 582 mapM_x (\<lambda>x. store_pde ((x << 2) + pd) pde.InvalidPDE) 583 [0.e.(kernel_base >> 20) - 1] 584 \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 585 apply (rule hoare_gen_asm) 586 apply (rule mapM_x_wp') 587 apply (simp add:store_pde_def set_pd_def) 588 apply (wp get_pd_wp get_object_wp) 589 apply (clarsimp simp: mask_in_range 590 split:Structures_A.kernel_object.splits 591 arch_kernel_obj.splits) 592 apply (rule conjI) 593 apply (rule valid_entries_overwrite_0) 594 apply (fastforce simp:ran_def obj_at_def) 595 apply simp 596 apply (simp add:fun_upd_def obj_at_def) 597 apply (rule entries_align_pde_update) 598 apply (drule (1) valid_pdpt_objs_pdD,simp) 599 apply simp 600 done 601 602lemma non_invalid_in_pde_range: 603 "pde \<noteq> InvalidPDE 604 \<Longrightarrow> x \<in> pde_range pde x" 605 by (case_tac pde,simp_all) 606 607lemma non_invalid_in_pte_range: 608 "pte \<noteq> InvalidPTE 609 \<Longrightarrow> x \<in> pte_range pte x" 610 by (case_tac pte,simp_all) 611 612crunch valid_pdpt_objs[wp]: cancel_badged_sends "valid_pdpt_objs" 613 (simp: crunch_simps filterM_mapM wp: crunch_wps) 614 615crunch valid_pdpt_objs[wp]: cap_move, cap_insert "valid_pdpt_objs" 616 617lemma invoke_cnode_valid_pdpt_objs[wp]: 618 "\<lbrace>valid_pdpt_objs and invs and valid_cnode_inv i\<rbrace> invoke_cnode i \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 619 apply (simp add: invoke_cnode_def) 620 apply (rule hoare_pre) 621 apply (wp get_cap_wp | wpc | simp split del: if_split)+ 622 done 623 624lemma as_user_valid_pdpt_objs[wp]: 625 "\<lbrace>valid_pdpt_objs\<rbrace> as_user t m \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 626 apply (simp add: as_user_def split_def) 627 apply wp 628 apply simp 629 done 630 631crunch valid_pdpt_objs[wp]: invoke_tcb "valid_pdpt_objs" 632 (wp: check_cap_inv crunch_wps simp: crunch_simps 633 ignore: check_cap_at) 634 635lemma invoke_domain_valid_pdpt_objs[wp]: 636 "\<lbrace>valid_pdpt_objs\<rbrace> invoke_domain t d \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 637 by (simp add: invoke_domain_def | wp)+ 638 639crunch valid_pdpt_objs[wp]: set_extra_badge, transfer_caps_loop "valid_pdpt_objs" 640 (rule: transfer_caps_loop_pres) 641 642crunch valid_pdpt_objs[wp]: send_ipc, send_signal, 643 do_reply_transfer, invoke_irq_control, invoke_irq_handler "valid_pdpt_objs" 644 (wp: crunch_wps simp: crunch_simps 645 ignore: clearMemory const_on_failure set_object) 646 647lemma valid_pdpt_objs_trans_state[simp]: "valid_pdpt_objs (trans_state f s) = valid_pdpt_objs s" 648 apply (simp add: obj_valid_pdpt_def) 649 done 650 651lemma retype_region_valid_pdpt[wp]: 652 "\<lbrace>valid_pdpt_objs\<rbrace> retype_region ptr bits o_bits type dev \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 653 apply (simp add: retype_region_def split del: if_split) 654 apply (wp | simp only: valid_pdpt_objs_trans_state trans_state_update[symmetric])+ 655 apply (clarsimp simp: retype_addrs_fold foldr_upd_app_if ranI 656 elim!: ranE split: if_split_asm simp del:fun_upd_apply) 657 apply (simp add: default_object_def default_arch_object_def 658 split: Structures_A.kernel_object.splits 659 Structures_A.apiobject_type.split aobject_type.split)+ 660 apply (simp add:entries_align_def) 661 done 662 663lemma detype_valid_pdpt[elim!]: 664 "valid_pdpt_objs s \<Longrightarrow> valid_pdpt_objs (detype S s)" 665 by (auto simp add: detype_def ran_def) 666 667crunch valid_pdpt_objs[wp]: create_cap "valid_pdpt_objs" 668 (ignore: clearMemory simp: crunch_simps unless_def) 669 670lemma init_arch_objects_valid_pdpt: 671 "\<lbrace>valid_pdpt_objs and pspace_aligned and valid_arch_state 672 and K (\<exists>us sz. orefs = retype_addrs ptr type n us 673 \<and> range_cover ptr sz (obj_bits_api type us) n)\<rbrace> 674 init_arch_objects type ptr n obj_sz orefs 675 \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 676 apply (rule hoare_gen_asm)+ 677 apply (clarsimp simp: init_arch_objects_def 678 split del: if_split) 679 apply (rule hoare_pre) 680 apply (wp | wpc)+ 681 apply (rule_tac Q="\<lambda>rv. valid_pdpt_objs and pspace_aligned and valid_arch_state" 682 in hoare_post_imp, simp) 683 apply (rule mapM_x_wp') 684 apply (rule hoare_pre, wp copy_global_mappings_valid_pdpt_objs) 685 apply clarsimp 686 apply (drule_tac sz=sz in retype_addrs_aligned) 687 apply (simp add:range_cover_def) 688 apply (drule range_cover.sz,simp add:word_bits_def) 689 apply (simp add:range_cover_def) 690 apply (clarsimp simp:obj_bits_api_def pd_bits_def pageBits_def 691 arch_kobj_size_def default_arch_object_def range_cover_def)+ 692 apply wp 693 apply simp 694 done 695 696lemma delete_objects_valid_pdpt: 697 "\<lbrace>valid_pdpt_objs\<rbrace> delete_objects ptr bits \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 698 by (rule delete_objects_reduct) (wp detype_valid_pdpt) 699 700crunch valid_pdpt[wp]: reset_untyped_cap "valid_pdpt_objs" 701 (wp: mapME_x_inv_wp crunch_wps simp: crunch_simps unless_def) 702 703lemma invoke_untyped_valid_pdpt[wp]: 704 "\<lbrace>valid_pdpt_objs and invs and ct_active 705 and valid_untyped_inv ui\<rbrace> 706 invoke_untyped ui 707 \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 708 apply (rule hoare_pre, rule invoke_untyped_Q) 709 apply (wp init_arch_objects_valid_pdpt | simp)+ 710 apply (auto simp: post_retype_invs_def split: if_split_asm)[1] 711 apply (wp | simp)+ 712 done 713 714crunch valid_pdpt_objs[wp]: perform_asid_pool_invocation, 715 perform_asid_control_invocation "valid_pdpt_objs" 716 (ignore: delete_objects wp: delete_objects_valid_pdpt static_imp_wp) 717 718abbreviation (input) 719 "safe_pt_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) 720 \<and> (\<forall>x\<in>set (tl slots). pt (ucast (x && mask pt_bits >> 2)) 721 = pte.InvalidPTE)) 722 (hd slots && ~~ mask pt_bits) s" 723 724abbreviation (input) 725 "safe_pd_range \<equiv> \<lambda>slots s. obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) 726 \<and> (\<forall>x\<in>set (tl slots). pd (ucast (x && mask pd_bits >> 2)) 727 = pde.InvalidPDE)) 728 (hd slots && ~~ mask pd_bits) s" 729 730definition 731 "page_inv_entries_pre entries \<equiv> 732 let slots = (case entries of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots) 733 in (if \<exists>sl. slots = [sl] 734 then case entries of 735 Inl (pte, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) 736 \<and> pt (ucast (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte 737 \<and> pte_range_sz pte = 0) 738 (hd slots && ~~ mask pt_bits) 739 and K (pte_range_sz pte = 0) 740 | Inr (pde, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) 741 \<and> pd (ucast (head slots && mask pd_bits >> 2) && ~~ mask 4) 742 = pde \<and> pde_range_sz pde = 0) 743 (hd slots && ~~ mask pd_bits) 744 and K (pde_range_sz pde = 0) 745 else (\<lambda>s. (\<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0, 4 .e. 0x3C]))) 746 and K (case entries of Inl (pte,slots) \<Rightarrow> pte \<noteq> InvalidPTE 747 | Inr (pde,slots) \<Rightarrow> pde \<noteq> InvalidPDE)" 748 749definition 750 "page_inv_entries_safe entries \<equiv> 751 let slots = (case entries of Inl (pte, slots) \<Rightarrow> slots | Inr (pde, slots) \<Rightarrow> slots) 752 in if \<exists>sl. slots = [sl] 753 then case entries of 754 Inl (pte, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pt pte. ko = ArchObj (PageTable pt) 755 \<and> pt (ucast (hd slots && mask pt_bits >> 2) && ~~ mask 4) = pte 756 \<and> pte_range_sz pte = 0) 757 (hd slots && ~~ mask pt_bits) 758 and K (pte_range_sz pte = 0) 759 | Inr (pde, _) \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) 760 \<and> pd (ucast (head slots && mask pd_bits >> 2) && ~~ mask 4) 761 = pde \<and> pde_range_sz pde = 0) 762 (hd slots && ~~ mask pd_bits) 763 and K (pde_range_sz pde = 0) 764 else (\<lambda>s. (\<exists>p. is_aligned p 6 \<and> slots = map (\<lambda>x. x + p) [0, 4 .e. 0x3C] 765 \<and> (case entries of 766 Inl (pte, _) \<Rightarrow> safe_pt_range slots s 767 | Inr (pde, _) \<Rightarrow> safe_pd_range slots s 768 )))" 769 770definition 771 "page_inv_duplicates_valid iv \<equiv> case iv of 772 PageMap asid cap ct_slot entries \<Rightarrow> 773 page_inv_entries_safe entries 774 | PageRemap asid entries \<Rightarrow> 775 page_inv_entries_safe entries 776 | _ \<Rightarrow> \<top>" 777 778lemma pte_range_interD: 779 "pte_range pte p \<inter> pte_range pte' p' \<noteq> {} 780 \<Longrightarrow> pte \<noteq> InvalidPTE \<and> pte' \<noteq> InvalidPTE 781 \<and> p && ~~ mask 4 = p' && ~~ mask 4" 782 apply (drule int_not_emptyD) 783 apply (case_tac pte,simp_all split:if_splits) 784 apply (case_tac pte',simp_all split:if_splits) 785 apply clarsimp 786 apply (case_tac pte',simp_all split:if_splits) 787 apply (case_tac pte', simp_all split:if_splits) 788 done 789 790lemma pde_range_interD: 791 "pde_range pde p \<inter> pde_range pde' p' \<noteq> {} 792 \<Longrightarrow> pde \<noteq> InvalidPDE \<and> pde' \<noteq> InvalidPDE 793 \<and> p && ~~ mask 4 = p' && ~~ mask 4" 794 apply (drule int_not_emptyD) 795 apply (case_tac pde,simp_all split:if_splits) 796 apply (case_tac pde',simp_all split:if_splits) 797 apply (case_tac pde',simp_all split:if_splits) 798 apply clarsimp 799 apply (case_tac pde', simp_all split:if_splits) 800 apply (case_tac pde', simp_all split:if_splits) 801 done 802 803lemma pte_range_sz_le: 804 "(pte_range_sz pte) \<le> 4" 805 by (case_tac pte,simp_all) 806 807lemma pde_range_sz_le: 808 "(pde_range_sz pde) \<le> 4" 809 by (case_tac pde,simp_all) 810 811(* BUG , revisit the following lemmas , moved from ArchAcc_R.thy *) 812lemma mask_pd_bits_shift_ucast_align[simp]: 813 "is_aligned (ucast (p && mask pd_bits >> 2)::12 word) 4 = 814 is_aligned ((p::word32) >> 2) 4" 815 by (clarsimp simp: is_aligned_mask mask_def pd_bits) word_bitwise 816 817lemma mask_pt_bits_shift_ucast_align[simp]: 818 "is_aligned (ucast (p && mask pt_bits >> 2)::word8) 4 = 819 is_aligned ((p::word32) >> 2) 4" 820 by (clarsimp simp: is_aligned_mask mask_def pt_bits_def pageBits_def) 821 word_bitwise 822 823lemma ucast_pt_index: 824 "\<lbrakk>is_aligned (p::word32) 6\<rbrakk> 825 \<Longrightarrow> ucast ((pa && mask 4) + (ucast (p && mask pt_bits >> 2)::8 word)) 826 = ucast (pa && mask 4) + (p && mask pt_bits >> 2)" 827 apply (simp add:is_aligned_mask mask_def pt_bits_def pageBits_def) 828 apply word_bitwise 829 apply (auto simp: carry_def) 830 done 831 832lemma store_pte_valid_pdpt: 833 "\<lbrace>valid_pdpt_objs and page_inv_entries_safe (Inl (pte, slots))\<rbrace> 834 store_pte (hd slots) pte \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 835 apply (rule hoare_name_pre_state) 836 apply (clarsimp simp:page_inv_entries_safe_def split:if_splits) 837 apply (clarsimp simp:store_pte_def set_pt_def) 838 apply (wp get_pt_wp get_object_wp) 839 apply (clarsimp simp:obj_at_def 840 split:pte.splits arch_kernel_obj.splits) 841 apply (rule conjI) 842 apply (drule(1) valid_pdpt_objs_ptD) 843 apply (rule valid_entries_overwrite_0) 844 apply simp 845 apply (case_tac pte) 846 apply simp+ 847 apply (case_tac "pta p",simp_all) 848 apply (clarsimp simp: is_aligned_neg_mask_eq) 849 apply (simp add:fun_upd_def) 850 apply (rule entries_align_pte_update) 851 apply (drule (1) valid_pdpt_objs_ptD,simp) 852 apply simp 853 apply (simp add:hd_map_simp upto_enum_def upto_enum_step_def) 854 apply (clarsimp simp:store_pte_def set_pt_def) 855 apply (wp get_pt_wp get_object_wp) 856 apply (clarsimp simp:obj_at_def 857 split:pte.splits arch_kernel_obj.splits) 858 apply (drule(1) valid_pdpt_objs_ptD) 859 apply (rule conjI) 860 apply (rule valid_entries_overwrite_0) 861 apply simp 862 apply (rule ccontr) 863 apply (drule pte_range_interD) 864 apply clarsimp 865 apply (simp add:ucast_neg_mask) 866 apply (subst (asm) is_aligned_neg_mask_eq[where n = 4]) 867 apply (rule is_aligned_shiftr[OF is_aligned_andI1]) 868 apply simp 869 apply (drule_tac x = "((p && ~~ mask pt_bits) + ((ucast pa) << 2))" in bspec) 870 apply (clarsimp simp: tl_map_simp upto_0_to_n2 image_def) 871 apply (rule_tac x = "unat (((ucast pa)::word32) - (p && mask pt_bits >> 2))" in bexI) 872 apply (simp add:ucast_nat_def shiftl_t2n mask_out_sub_mask) 873 apply (subst shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric]) 874 apply (subst shiftr_shiftl1) 875 apply simp+ 876 apply (subst is_aligned_neg_mask_eq) 877 apply (erule is_aligned_andI1[OF is_aligned_weaken]) 878 apply simp 879 apply simp 880 apply simp 881 apply (drule_tac s = "ucast (p && mask pt_bits >> 2)" in sym) 882 apply (simp add:mask_out_sub_mask field_simps) 883 apply (drule_tac f = "ucast::(word8\<Rightarrow>word32)" in arg_cong) 884 apply (simp add:ucast_pt_index) 885 apply (simp add:unat_ucast_8_32) 886 apply (rule conjI) 887 apply (subgoal_tac "unat (pa && mask 4)\<noteq> 0") 888 apply simp 889 apply (simp add:unat_gt_0) 890 apply (rule unat_less_helper) 891 apply (rule le_less_trans[OF word_and_le1]) 892 apply (simp add:mask_def) 893 apply (simp add:field_simps neg_mask_add_mask) 894 apply (thin_tac "ucast y = x" for y x) 895 apply (subst (asm) less_mask_eq[where n = pt_bits]) 896 apply (rule shiftl_less_t2n) 897 apply (simp add:pt_bits_def pageBits_def) 898 apply word_bitwise 899 apply (simp add:pt_bits_def pageBits_def) 900 apply (subst (asm) shiftl_shiftr_id) 901 apply simp 902 apply (simp,word_bitwise) 903 apply (simp add:ucast_ucast_id) 904 apply (simp add:fun_upd_def entries_align_def) 905 apply (rule is_aligned_weaken[OF _ pte_range_sz_le]) 906 apply (simp add:is_aligned_shiftr) 907 done 908 909 910lemma ucast_pd_index: 911 "\<lbrakk>is_aligned (p::word32) 6\<rbrakk> 912 \<Longrightarrow> ucast ((pa && mask 4) + (ucast (p && mask pd_bits >> 2)::12 word)) 913 = ucast (pa && mask 4) + (p && mask pd_bits >> 2)" 914 apply (simp add:is_aligned_mask mask_def pd_bits_def pageBits_def) 915 apply word_bitwise 916 apply (auto simp:carry_def) 917 done 918 919lemma unat_ucast_12_32: 920 "unat (ucast (x::(12 word))::word32) = unat x" 921 apply (subst unat_ucast) 922 apply (rule mod_less) 923 apply (rule less_le_trans[OF unat_lt2p]) 924 apply simp 925 done 926 927lemma store_pde_valid_pdpt: 928 "\<lbrace>valid_pdpt_objs and page_inv_entries_safe (Inr (pde, slots))\<rbrace> 929 store_pde (hd slots) pde \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 930 apply (rule hoare_name_pre_state) 931 apply (clarsimp simp:page_inv_entries_safe_def split:if_splits) 932 apply (clarsimp simp:store_pde_def set_pd_def) 933 apply (wp get_pd_wp get_object_wp) 934 apply (clarsimp simp:obj_at_def 935 split:pde.splits arch_kernel_obj.splits) 936 apply (drule(1) valid_pdpt_objs_pdD) 937 apply (rule conjI) 938 apply (rule valid_entries_overwrite_0) 939 apply simp 940 apply (case_tac pde,simp_all) 941 apply (case_tac "pda p",simp_all) 942 apply (clarsimp simp: is_aligned_neg_mask_eq) 943 apply (case_tac "pda p",simp_all) 944 apply (clarsimp simp: is_aligned_neg_mask_eq) 945 apply (simp add:fun_upd_def) 946 apply (rule entries_align_pde_update) 947 apply simp+ 948 apply (simp add:hd_map_simp upto_enum_def upto_enum_step_def) 949 apply (clarsimp simp:store_pde_def set_pd_def) 950 apply (wp get_pd_wp get_object_wp) 951 apply (clarsimp simp:obj_at_def 952 split:pde.splits arch_kernel_obj.splits) 953 apply (drule(1) valid_pdpt_objs_pdD) 954 apply (rule conjI) 955 apply (rule valid_entries_overwrite_0) 956 apply simp 957 apply (rule ccontr) 958 apply (drule pde_range_interD) 959 apply clarsimp 960 apply (simp add:ucast_neg_mask) 961 apply (subst (asm) is_aligned_neg_mask_eq[where n = 4]) 962 apply (rule is_aligned_shiftr[OF is_aligned_andI1]) 963 apply simp 964 apply (drule_tac x = "((p && ~~ mask pd_bits) + ((ucast pa) << 2))" in bspec) 965 apply (clarsimp simp: tl_map_simp upto_0_to_n2 image_def) 966 apply (rule_tac x = "unat (((ucast pa)::word32) - (p && mask pd_bits >> 2))" in bexI) 967 apply (simp add:ucast_nat_def shiftl_t2n mask_out_sub_mask) 968 apply (subst shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric]) 969 apply (subst shiftr_shiftl1) 970 apply simp+ 971 apply (subst is_aligned_neg_mask_eq) 972 apply (erule is_aligned_andI1[OF is_aligned_weaken]) 973 apply simp 974 apply simp 975 apply simp 976 apply (drule_tac s = "ucast (p && mask pd_bits >> 2)" in sym) 977 apply (simp add:mask_out_sub_mask field_simps) 978 apply (drule_tac f = "ucast::(12 word\<Rightarrow>word32)" in arg_cong) 979 apply (simp add:ucast_pd_index) 980 apply (simp add:unat_ucast_12_32) 981 apply (rule conjI) 982 apply (subgoal_tac "unat (pa && mask 4)\<noteq> 0") 983 apply simp 984 apply (simp add:unat_gt_0) 985 apply (rule unat_less_helper) 986 apply (rule le_less_trans[OF word_and_le1]) 987 apply (simp add:mask_def) 988 apply (simp add:field_simps neg_mask_add_mask) 989 apply (thin_tac "ucast y = x" for y x) 990 apply (subst (asm) less_mask_eq[where n = pd_bits]) 991 apply (rule shiftl_less_t2n) 992 apply (simp add:pd_bits_def pageBits_def) 993 apply word_bitwise 994 apply (simp add:pd_bits_def pageBits_def) 995 apply (subst (asm) shiftl_shiftr_id) 996 apply simp 997 apply (simp,word_bitwise) 998 apply (simp add:ucast_ucast_id) 999 apply (simp add:entries_align_def) 1000 apply (rule is_aligned_weaken[OF _ pde_range_sz_le]) 1001 apply (simp add:is_aligned_shiftr) 1002 done 1003 1004lemma set_cap_page_inv_entries_safe: 1005 "\<lbrace>page_inv_entries_safe x\<rbrace> set_cap y z \<lbrace>\<lambda>_. page_inv_entries_safe x\<rbrace>" 1006 apply (simp add:page_inv_entries_safe_def set_cap_def split_def 1007 get_object_def set_object_def) 1008 apply (wp | wpc)+ 1009 apply (case_tac x) 1010 apply (auto simp:obj_at_def 1011 Let_def split:if_splits option.splits) 1012 done 1013 1014crunch inv[wp]: pte_check_if_mapped, pde_check_if_mapped "\<lambda>s. P s" 1015 1016lemma perform_page_valid_pdpt[wp]: 1017 "\<lbrace>valid_pdpt_objs and valid_page_inv pinv and page_inv_duplicates_valid pinv\<rbrace> 1018 perform_page_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 1019 apply (simp add: perform_page_invocation_def page_inv_duplicates_valid_def) 1020 apply (cases pinv, 1021 simp_all add: mapM_discarded page_inv_entries_safe_def 1022 split: sum.split arch_cap.split option.split, 1023 safe intro!: hoare_gen_asm hoare_gen_asm[unfolded K_def], 1024 simp_all add: mapM_x_Nil mapM_x_Cons mapM_x_map) 1025 apply (wp store_pte_valid_pdpt store_pde_valid_pdpt get_master_pte_wp get_master_pde_wp 1026 store_pte_non_master_valid_pdpt store_pde_non_master_valid_pdpt 1027 mapM_x_wp'[OF store_invalid_pte_valid_pdpt 1028 [where pte=pte.InvalidPTE, simplified]] 1029 mapM_x_wp'[OF store_invalid_pde_valid_pdpt 1030 [where pde=pde.InvalidPDE, simplified]] 1031 set_cap_page_inv_entries_safe 1032 hoare_vcg_imp_lift[OF set_cap_arch_obj_neg] hoare_vcg_all_lift 1033 | clarsimp simp: cte_wp_at_weakenE[OF _ TrueI] obj_at_def 1034 pte_range_sz_def pde_range_sz_def swp_def valid_page_inv_def 1035 valid_slots_def page_inv_entries_safe_def pte_check_if_mapped_def 1036 pde_check_if_mapped_def 1037 split: pte.splits pde.splits 1038 | wp_once hoare_drop_imps)+ 1039 done 1040 1041definition 1042 "pti_duplicates_valid iv \<equiv> 1043 case iv of PageTableMap cap ct_slot pde pd_slot 1044 \<Rightarrow> obj_at (\<lambda>ko. \<exists>pd pde. ko = ArchObj (PageDirectory pd) 1045 \<and> pd (ucast (pd_slot && mask pd_bits >> 2) && ~~ mask 4) 1046 = pde \<and> pde_range_sz pde = 0) 1047 (pd_slot && ~~ mask pd_bits) 1048 1049 and K (pde_range_sz pde = 0) 1050 | _ \<Rightarrow> \<top>" 1051 1052 1053definition 1054 "invocation_duplicates_valid i \<equiv> 1055 case i of 1056 InvokeArchObject (InvokePage pgi) \<Rightarrow> page_inv_duplicates_valid pgi 1057 | InvokeArchObject (InvokePageTable pti) \<Rightarrow> pti_duplicates_valid pti 1058 | _ \<Rightarrow> \<top>" 1059 1060lemma perform_page_table_valid_pdpt[wp]: 1061 "\<lbrace>valid_pdpt_objs and valid_pti pinv and pti_duplicates_valid pinv\<rbrace> 1062 perform_page_table_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 1063 apply (simp add: perform_page_table_invocation_def split_def 1064 cong: page_table_invocation.case_cong 1065 option.case_cong cap.case_cong arch_cap.case_cong) 1066 apply (rule hoare_pre) 1067 apply (wp store_pde_non_master_valid_pdpt hoare_vcg_ex_lift 1068 set_cap_arch_obj mapM_x_store_pte_valid_pdpt2 1069 | wpc 1070 | simp add: swp_def 1071 | strengthen all_imp_ko_at_from_ex_strg)+ 1072 apply (clarsimp simp: pti_duplicates_valid_def valid_pti_def) 1073 apply (auto simp: obj_at_def cte_wp_at_caps_of_state valid_cap_simps 1074 cap_aligned_def pt_bits_def pageBits_def 1075 intro!: inj_onI) 1076 done 1077 1078lemma perform_page_directory_valid_pdpt[wp]: 1079 "\<lbrace>valid_pdpt_objs and valid_pdi pinv\<rbrace> 1080 perform_page_directory_invocation pinv \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 1081 apply (simp add: perform_page_directory_invocation_def split_def) 1082 apply (rule hoare_pre) 1083 apply (wp | wpc | simp)+ 1084 done 1085 1086lemma perform_invocation_valid_pdpt[wp]: 1087 "\<lbrace>invs and ct_active and valid_invocation i and valid_pdpt_objs 1088 and invocation_duplicates_valid i\<rbrace> 1089 perform_invocation blocking call i 1090 \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 1091 apply (cases i, simp_all) 1092 apply (wp send_signal_interrupt_states | simp)+ 1093 apply (clarsimp simp: invocation_duplicates_valid_def) 1094 apply (wp | wpc | simp)+ 1095 apply (simp add: arch_perform_invocation_def) 1096 apply (rule hoare_pre) 1097 apply (wp | wpc | simp)+ 1098 apply (auto simp: valid_arch_inv_def invocation_duplicates_valid_def) 1099 done 1100 1101lemma neg_mask_pt_6_4: 1102 "(ptr && mask pt_bits >> 2) && ~~ mask 4 = 1103 (ptr::word32) && ~~ mask 6 && mask pt_bits >> 2" 1104 apply (simp add:pt_bits_def pageBits_def) 1105 apply word_bitwise 1106 apply (simp add:word_size) 1107 done 1108 1109lemma neg_mask_pd_6_4: 1110 "(ptr && mask pd_bits >> 2) && ~~ mask 4 = 1111 (ptr::word32) && ~~ mask 6 && mask pd_bits >> 2" 1112 apply (simp add:pd_bits_def pageBits_def) 1113 apply word_bitwise 1114 apply (simp add:word_size) 1115 done 1116 1117lemma mask_out_same_pt: 1118 "\<lbrakk>is_aligned p 6; x < 2 ^ 6 \<rbrakk> \<Longrightarrow> p + x && ~~ mask pt_bits = p && ~~ mask pt_bits" 1119 apply (subst mask_lower_twice[symmetric,where n = 6]) 1120 apply (simp add:pt_bits_def pageBits_def) 1121 apply (simp add:is_aligned_add_helper) 1122 done 1123 1124lemma mask_out_same_pd: 1125 "\<lbrakk>is_aligned p 6; x < 2 ^ 6 \<rbrakk> \<Longrightarrow> p + x && ~~ mask pd_bits = p && ~~ mask pd_bits" 1126 apply (subst mask_lower_twice[symmetric,where n = 6]) 1127 apply (simp add:pd_bits_def pageBits_def) 1128 apply (simp add:is_aligned_add_helper) 1129 done 1130 1131lemma ensure_safe_mapping_ensures[wp]: 1132 "\<lbrace>valid_pdpt_objs and (case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top> 1133 | (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom> 1134 | (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom> 1135 | (Inr (SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top> 1136 | (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom> 1137 | (Inr (SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom> 1138 | _ \<Rightarrow> page_inv_entries_pre entries)\<rbrace> 1139 ensure_safe_mapping entries 1140 \<lbrace>\<lambda>rv. page_inv_entries_safe entries\<rbrace>,-" 1141 proof - 1142 have [simp]: 1143 "\<And>s a. page_inv_entries_pre (Inl (pte.InvalidPTE, a)) s \<Longrightarrow> 1144 page_inv_entries_safe (Inl (pte.InvalidPTE, a)) s" 1145 apply (clarsimp simp:page_inv_entries_pre_def page_inv_entries_safe_def 1146 split:if_splits) 1147 done 1148 have name_pre: 1149 "\<And>F P Q. (\<And>s. P s \<Longrightarrow> \<lbrace>(=) s \<rbrace> F \<lbrace>Q\<rbrace>, -) \<Longrightarrow> \<lbrace>P\<rbrace> F \<lbrace>Q\<rbrace>,-" 1150 apply (simp add:validE_R_def validE_def) 1151 apply (rule hoare_name_pre_state) 1152 apply assumption 1153 done 1154 have mask_neg_mask_order[simp]: 1155 "\<And>a m n. a && ~~ mask m && mask n = a && mask n && ~~ mask m" 1156 by (simp add:word_bw_comms word_bw_lcs) 1157 have align_entry_ptD: 1158 "\<And>pt m x xb xc. \<lbrakk>pt m = pte.LargePagePTE x xb xc; entries_align pte_range_sz pt\<rbrakk> 1159 \<Longrightarrow> is_aligned m 4" 1160 apply (simp add:entries_align_def) 1161 apply (drule_tac x = m in spec,simp) 1162 done 1163 have align_entry_pdD: 1164 "\<And>pd m x xb xc. \<lbrakk>pd m = pde.SuperSectionPDE x xb xc; entries_align pde_range_sz pd\<rbrakk> 1165 \<Longrightarrow> is_aligned m 4" 1166 apply (simp add:entries_align_def) 1167 apply (drule_tac x = m in spec,simp) 1168 done 1169 have pt_offset_bitwise[simp]:"\<And>a. (ucast ((a::word32) && mask pt_bits && ~~ mask 6 >> 2)::word8) 1170 = (ucast (a && mask pt_bits >> 2)::word8) && ~~ mask 4" 1171 apply (simp add:pt_bits_def pageBits_def mask_def) 1172 apply word_bitwise 1173 done 1174 have pd_offset_bitwise[simp]:"\<And>a. (ucast ((a::word32) && mask pd_bits && ~~ mask 6 >> 2)::12 word) 1175 = (ucast (a && mask pd_bits >> 2)::12 word) && ~~ mask 4" 1176 apply (simp add:pt_bits_def pageBits_def mask_def pd_bits_def) 1177 apply word_bitwise 1178 done 1179 have mask_neq_0: 1180 "\<And>z zs xa p g. \<lbrakk>[0 :: word32, 4 .e. 0x3C] = z # zs; xa \<in> set zs; is_aligned p 6; 6 \<le> g\<rbrakk> 1181 \<Longrightarrow> (p + xa && mask g >> 2) && mask 4 \<noteq> 0" 1182 apply (rule ccontr) 1183 apply (simp add:is_aligned_mask[symmetric]) 1184 apply (drule is_aligned_shiftl[where n = 6 and m = 2,simplified]) 1185 apply (subst (asm) shiftr_shiftl1) 1186 apply simp+ 1187 apply (subst (asm) is_aligned_neg_mask_eq) 1188 apply (rule is_aligned_andI1) 1189 apply (erule aligned_add_aligned) 1190 apply (clarsimp simp :upto_enum_def upto_enum_step_def 1191 Fun.comp_def upto_0_to_n2 is_aligned_mult_triv2[where n = 2,simplified]) 1192 apply simp 1193 apply (simp add:is_aligned_mask mask_twice 1194 pt_bits_def pageBits_def min_def) 1195 apply (subst (asm) is_aligned_mask[symmetric]) 1196 apply (subst (asm) is_aligned_add_helper) 1197 apply simp 1198 apply (clarsimp simp :upto_enum_def upto_enum_step_def 1199 Fun.comp_def upto_0_to_n2) 1200 apply (subst shiftl_t2n 1201 [where n = 2,simplified field_simps,simplified,symmetric])+ 1202 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1203 apply (rule word_of_nat_less) 1204 apply simp 1205 apply simp 1206 apply (clarsimp simp :upto_enum_def upto_enum_step_def 1207 Fun.comp_def upto_0_to_n2) 1208 apply (cut_tac x = "of_nat x" and n = 2 in word_power_nonzero_32) 1209 apply (simp add:word_of_nat_less word_bits_def)+ 1210 apply (simp add: of_nat_neq_0) 1211 apply simp 1212 done 1213 have neq_pt_offset: "\<And>z zs xa (p::word32). \<lbrakk>[0 , 4 .e. 0x3C] = z # zs; 1214 xa \<in> set zs;is_aligned p 6 \<rbrakk> \<Longrightarrow> 1215 ucast (p + xa && mask pt_bits >> 2) && ~~ mask 4 \<noteq> ((ucast (p + xa && mask pt_bits >> 2))::word8)" 1216 apply (rule ccontr) 1217 apply (simp add:mask_out_sub_mask ucast_and_mask[symmetric]) 1218 apply (drule arg_cong[where f = unat]) 1219 apply (simp add:unat_ucast) 1220 apply (subst (asm) mod_less) 1221 apply (rule unat_less_helper) 1222 apply (rule le_less_trans[OF word_and_le1]) 1223 apply (simp add:mask_def) 1224 apply (simp add:unat_eq_0) 1225 apply (drule(2) mask_neq_0[of _ _ _ _ pt_bits]) 1226 apply (simp add:pt_bits_def pageBits_def)+ 1227 done 1228 have neq_pd_offset: "\<And>z zs xa (p::word32). \<lbrakk>[0 , 4 .e. 0x3C] = z # zs; 1229 xa \<in> set zs;is_aligned p 6 \<rbrakk> \<Longrightarrow> 1230 ucast (p + xa && mask pd_bits >> 2) && ~~ mask 4 \<noteq> ((ucast (p + xa && mask pd_bits >> 2)) :: 12 word)" 1231 apply (simp add:mask_out_sub_mask) 1232 apply (rule ccontr) 1233 apply (simp add:mask_out_sub_mask ucast_and_mask[symmetric]) 1234 apply (drule arg_cong[where f = unat]) 1235 apply (simp add:unat_ucast) 1236 apply (subst (asm) mod_less) 1237 apply (rule unat_less_helper) 1238 apply (rule le_less_trans[OF word_and_le1]) 1239 apply (simp add:mask_def) 1240 apply (simp add:unat_eq_0) 1241 apply (drule(2) mask_neq_0[of _ _ _ _ pd_bits]) 1242 apply (simp add:pd_bits_def pageBits_def)+ 1243 done 1244 have invalid_pteI: 1245 "\<And>a pt x y z. \<lbrakk>valid_pt_entries pt; (a && ~~ mask 4) \<noteq> a; 1246 pt (a && ~~ mask 4) = pte.LargePagePTE x y z \<rbrakk> 1247 \<Longrightarrow> pt a = pte.InvalidPTE" 1248 apply (drule(1) valid_entriesD[rotated]) 1249 apply (case_tac "pt a"; simp add:mask_lower_twice is_aligned_neg_mask split:if_splits) 1250 done 1251 have invalid_pdeI: 1252 "\<And>a pd x y z. \<lbrakk>valid_pd_entries pd; (a && ~~ mask 4) \<noteq> a; 1253 pd (a && ~~ mask 4) = pde.SuperSectionPDE x y z \<rbrakk> 1254 \<Longrightarrow> pd a = pde.InvalidPDE" 1255 apply (drule(1) valid_entriesD[rotated]) 1256 apply (case_tac "pd a", 1257 simp_all add:mask_lower_twice is_aligned_neg_mask 1258 split:if_splits) 1259 done 1260 have inj[simp]: 1261 "\<And>p. is_aligned (p::word32) 6 \<Longrightarrow> inj_on (\<lambda>x. toEnum x * 4 + p) {Suc 0..<16}" 1262 apply (clarsimp simp:inj_on_def) 1263 apply (subst (asm) shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric])+ 1264 apply (drule arg_cong[where f = "\<lambda>x. x >> 2"]) 1265 apply (simp add:shiftl_shiftr_id word_of_nat_less) 1266 apply (simp add:of_nat_inj) 1267 done 1268 1269 show ?thesis 1270 apply (rule name_pre) 1271 apply (case_tac entries) 1272 apply (case_tac a, case_tac aa) 1273 apply (simp add:page_inv_entries_pre_def page_inv_entries_safe_def 1274 | wp | intro conjI impI)+ 1275 apply (simp split:list.splits add:page_inv_entries_pre_def)+ 1276 apply (rename_tac obj_ref vm_attributes cap_rights slot slots) 1277 apply (elim conjE exE) 1278 apply (subst mapME_x_Cons) 1279 apply simp 1280 apply wp 1281 apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set slots. obj_at 1282 (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) \<and> 1283 pt (ucast (x && mask pt_bits >> 2)) = pte.InvalidPTE) 1284 (hd (slot # slots) && ~~ mask pt_bits) s" in hoare_post_imp_R) 1285 apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] ) 1286 apply (wp get_master_pte_wp| wpc | simp)+ 1287 apply clarsimp 1288 apply (frule_tac x = xa in mask_out_same_pt) 1289 apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2) 1290 apply (erule notE) 1291 apply (subst shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric]) 1292 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1293 apply (simp add:word_of_nat_less) 1294 apply simp 1295 apply (frule_tac x = z in mask_out_same_pt) 1296 apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2) 1297 apply (clarsimp simp:field_simps obj_at_def 1298 split:pte.splits) 1299 apply (intro conjI impI) 1300 apply (clarsimp) 1301 apply (drule(1) valid_pdpt_objs_ptD) 1302 apply (frule align_entry_ptD,simp) 1303 apply (simp add:is_aligned_neg_mask_eq) 1304 apply clarsimp 1305 apply (drule(1) valid_pdpt_objs_ptD,clarify) 1306 apply (erule(4) invalid_pteI[OF _ neq_pt_offset]) 1307 apply clarsimp 1308 apply (drule(1) valid_pdpt_objs_ptD,clarify) 1309 apply (frule align_entry_ptD,simp) 1310 apply (simp add:is_aligned_neg_mask_eq) 1311 apply (wp hoare_drop_imps |wpc|simp)+ 1312 apply (clarsimp simp:upto_enum_def upto_enum_step_def 1313 upto_0_to_n2 Fun.comp_def distinct_map) 1314 apply (intro exI conjI,fastforce+) 1315 apply (simp add:obj_at_def hd_map_simp 1316 upto_0_to_n2 upto_enum_def upto_enum_step_def) 1317 apply (frule_tac x = 1 in bspec,fastforce+) 1318 apply ((wp hoare_drop_imps |wpc|simp)+)[1] 1319 apply (simp add:page_inv_entries_pre_def page_inv_entries_safe_def 1320 | wp | intro conjI impI)+ 1321 apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton) 1322 apply (wp get_master_pte_wp |wpc | simp)+ 1323 apply (clarsimp simp:obj_at_def split:pte.splits) 1324 apply (clarsimp simp:page_inv_entries_safe_def split:list.splits) 1325 apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton) 1326 apply (case_tac b,case_tac a) 1327 apply ((simp add:page_inv_entries_pre_def page_inv_entries_safe_def 1328 | wp | intro conjI impI)+)[1] 1329 apply simp 1330 apply wp[1] 1331 apply (simp split:list.splits add:page_inv_entries_pre_def mapME_singleton) 1332 apply (wp get_master_pde_wp | wpc | simp)+ 1333 apply (clarsimp simp:obj_at_def page_inv_entries_safe_def 1334 split:pde.splits) 1335 apply (simp split:list.splits if_splits 1336 add:page_inv_entries_pre_def Let_def page_inv_entries_safe_def) 1337 apply (elim conjE exE) 1338 apply (subst mapME_x_Cons) 1339 apply simp 1340 apply wp 1341 apply (rule_tac Q' = "\<lambda>r s. \<forall>x \<in> set x22. obj_at 1342 (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd) \<and> 1343 pd (ucast (x && mask pd_bits >> 2)) = pde.InvalidPDE) 1344 (hd (x21 # x22) && ~~ mask pd_bits) s" in hoare_post_imp_R) 1345 apply (wp mapME_x_accumulate_checks[where Q = "\<lambda>s. valid_pdpt_objs s"] ) 1346 apply (wp get_master_pde_wp| wpc | simp)+ 1347 apply clarsimp 1348 apply (frule_tac x = xa in mask_out_same_pd) 1349 apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2) 1350 apply (erule notE) 1351 apply (subst shiftl_t2n[where n = 2,simplified field_simps,simplified,symmetric]) 1352 apply (rule shiftl_less_t2n[where m = 6,simplified]) 1353 apply (simp add:word_of_nat_less) 1354 apply simp 1355 apply (frule_tac x = z in mask_out_same_pd) 1356 apply (clarsimp simp:upto_enum_def upto_enum_step_def upto_0_to_n2) 1357 apply (clarsimp simp:field_simps obj_at_def 1358 split:pde.splits) 1359 apply (drule(1) valid_pdpt_objs_pdD) 1360 apply (intro conjI impI) 1361 apply clarsimp 1362 apply (frule(1) align_entry_pdD) 1363 apply (simp add:is_aligned_neg_mask_eq) 1364 apply clarsimp 1365 apply (frule(1) align_entry_pdD) 1366 apply (simp add:is_aligned_neg_mask_eq) 1367 apply clarsimp 1368 apply (frule(1) align_entry_pdD) 1369 apply (simp add:is_aligned_neg_mask_eq) 1370 apply clarsimp 1371 apply (erule(4) invalid_pdeI[OF _ neq_pd_offset]) 1372 apply (wp hoare_drop_imps |wpc|simp)+ 1373 apply (clarsimp simp:upto_enum_def upto_enum_step_def 1374 upto_0_to_n2 Fun.comp_def distinct_map) 1375 apply (intro exI conjI,fastforce+) 1376 apply (simp add:obj_at_def hd_map_simp 1377 upto_0_to_n2 upto_enum_def upto_enum_step_def) 1378 apply (frule_tac x = 1 in bspec,fastforce+) 1379 apply (wp get_master_pde_wp | simp | wpc)+ 1380 done 1381qed 1382 1383lemma create_mapping_entries_safe[wp]: 1384 "\<lbrace>\<exists>\<rhd>pd and K (vmsz_aligned vptr sz) and K (is_aligned pd pd_bits) 1385 and K (vptr < kernel_base) 1386 and valid_vspace_objs and pspace_aligned and 1387 (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))\<rbrace> 1388 create_mapping_entries ptr vptr sz rights attrib pd 1389 \<lbrace>\<lambda>entries. case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top> 1390 | (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom> 1391 | (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom> 1392 | (Inr (SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top> 1393 | (Inr (SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom> 1394 | (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom> 1395 | _ \<Rightarrow> page_inv_entries_pre entries\<rbrace>,-" 1396 apply (cases sz, simp_all add: largePagePTE_offsets_def superSectionPDE_offsets_def) 1397 defer 2 1398 apply (wp | simp)+ 1399 apply (simp split:list.split) 1400 apply (subgoal_tac "lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C") 1401 apply (clarsimp simp:upto_enum_def not_less upto_enum_step_def 1402 page_inv_entries_pre_def Let_def) 1403 apply (clarsimp simp:upto_enum_step_def upto_enum_def 1404 map_eq_Cons_conv upt_eq_Cons_conv) 1405 apply (drule_tac x = "lookup_pd_slot pd vptr" in spec) 1406 apply (subst (asm) upto_0_to_n2) 1407 apply simp 1408 apply clarsimp 1409 apply (drule lookup_pd_slot_aligned_6) 1410 apply (simp add:pd_bits_def pageBits_def) 1411 apply simp 1412 apply clarsimp 1413 apply (erule is_aligned_no_wrap'[OF lookup_pd_slot_aligned_6]) 1414 apply (simp add:pd_bits pageBits_def) 1415 apply simp 1416 apply (wp get_pde_wp | simp add:lookup_pt_slot_def | wpc)+ 1417 apply (clarsimp simp:upto_enum_def upto_enum_step_def 1418 page_inv_entries_pre_def Let_def ) 1419 apply (drule_tac ref = refa in valid_vspace_objsD) 1420 apply (simp add:obj_at_def) 1421 apply simp 1422 apply (simp) 1423 apply (drule_tac x = "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2)" 1424 in bspec) 1425 apply simp 1426 apply (erule(1) less_kernel_base_mapping_slots) 1427 apply (clarsimp simp:not_less[symmetric] split:list.splits) 1428 apply (clarsimp simp:page_inv_entries_pre_def 1429 Let_def upto_enum_step_def upto_enum_def) 1430 apply (subst (asm) upto_0_to_n2) 1431 apply simp 1432 apply (clarsimp simp:not_less[symmetric]) 1433 apply (subgoal_tac 1434 "(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2)) 1435 = pde.PageTablePDE x xa xb) 1436 \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6") 1437 apply clarsimp 1438 apply clarsimp 1439 apply (rule aligned_add_aligned) 1440 apply (erule(1) pt_aligned) 1441 apply (rule is_aligned_shiftl[OF is_aligned_andI1]) 1442 apply (rule is_aligned_shiftr) 1443 apply (simp add:vmsz_aligned_def) 1444 apply simp 1445 done 1446 1447crunch vspace_objs[wp]: find_pd_for_asid valid_vspace_objs 1448 1449lemma arch_decode_invocation_valid_pdpt[wp]: 1450 "\<lbrace>invs and valid_cap (cap.ArchObjectCap cap) and valid_pdpt_objs \<rbrace> 1451 arch_decode_invocation label args cap_index slot cap excaps 1452 \<lbrace>invocation_duplicates_valid o Invocations_A.InvokeArchObject\<rbrace>,-" 1453 proof - 1454 have bitwise:"\<And>a. (ucast (((a::word32) && ~~ mask 6) && mask 14 >> 2)::12 word) 1455 = (ucast (a && mask 14 >> 2)::12 word) && ~~ mask 4" 1456 apply (simp add:mask_def) 1457 apply word_bitwise 1458 done 1459 have sz: 1460 "\<And>vmpage_size. \<lbrakk>args ! 0 + 2 ^ pageBitsForSize vmpage_size - 1 < kernel_base; 1461 vmsz_aligned (args ! 0) vmpage_size\<rbrakk> 1462 \<Longrightarrow> args ! 0 < kernel_base" 1463 apply (rule le_less_trans[OF is_aligned_no_overflow]) 1464 apply (simp add:vmsz_aligned_def) 1465 apply simp 1466 done 1467 show ?thesis 1468 apply (simp add: arch_decode_invocation_def 1469 Let_def split_def get_master_pde_def 1470 split del: if_split 1471 cong: arch_cap.case_cong if_cong cap.case_cong 1472 option.case_cong) 1473 apply (rule hoare_pre) 1474 apply ((wp get_pde_wp 1475 ensure_safe_mapping_ensures[THEN hoare_post_imp_R] 1476 create_mapping_entries_safe check_vp_wpR 1477 find_pd_for_asid_aligned_pd_bits 1478 [unfolded pd_bits_def pageBits_def,simplified] 1479 | wpc 1480 | simp add: invocation_duplicates_valid_def unlessE_def whenE_def 1481 pti_duplicates_valid_def page_inv_duplicates_valid_def 1482 mask_lower_twice pd_bits_def bitwise pageBits_def 1483 not_le sz if_apply_def2 1484 del: hoare_True_E_R 1485 split del: if_split 1486 | simp only: obj_at_def)+) 1487 apply (rule_tac Q'="\<lambda>rv. \<exists>\<rhd> rv and K (is_aligned rv pd_bits) and 1488 (\<exists>\<rhd> (lookup_pd_slot rv (args ! 0) && ~~ mask pd_bits)) and 1489 valid_vspace_objs and pspace_aligned and valid_pdpt_objs" 1490 and f="find_pd_for_asid p" for p 1491 in hoare_post_imp_R) 1492 apply (wp | simp)+ 1493 apply (fastforce simp:pd_bits_def pageBits_def) 1494 apply ((wp get_pde_wp 1495 ensure_safe_mapping_ensures[THEN hoare_post_imp_R] 1496 create_mapping_entries_safe check_vp_wpR 1497 find_pd_for_asid_aligned_pd_bits 1498 [unfolded pd_bits_def pageBits_def,simplified] 1499 | wpc 1500 | simp add: invocation_duplicates_valid_def unlessE_def whenE_def 1501 pti_duplicates_valid_def page_inv_duplicates_valid_def 1502 mask_lower_twice pd_bits_def bitwise pageBits_def 1503 not_le sz if_apply_def2 1504 del: hoare_True_E_R 1505 split del: if_split 1506 | simp only: obj_at_def)+) 1507 apply (rule_tac Q'="\<lambda>rv. \<exists>\<rhd> rv and K (is_aligned rv pd_bits) and 1508 (\<exists>\<rhd> (lookup_pd_slot rv (snd pa) && ~~ mask pd_bits)) and 1509 valid_vspace_objs and pspace_aligned and valid_pdpt_objs and 1510 K ((snd pa) < kernel_base)" 1511 and f="find_pd_for_asid p" for p 1512 in hoare_post_imp_R) 1513 apply (wp| simp)+ 1514 apply (auto simp:pd_bits_def pageBits_def)[1] 1515 apply ((wp get_pde_wp 1516 ensure_safe_mapping_ensures[THEN hoare_post_imp_R] 1517 create_mapping_entries_safe check_vp_wpR 1518 find_pd_for_asid_aligned_pd_bits 1519 [unfolded pd_bits_def pageBits_def,simplified] 1520 | wpc 1521 | simp add: invocation_duplicates_valid_def unlessE_def whenE_def 1522 pti_duplicates_valid_def page_inv_duplicates_valid_def 1523 mask_lower_twice pd_bits_def bitwise pageBits_def 1524 not_le sz if_apply_def2 1525 del: hoare_True_E_R 1526 split del: if_split 1527 | simp only: obj_at_def)+) 1528 apply (rule hoare_post_imp_R[where P=\<top>]) 1529 apply (rule hoare_True_E_R) 1530 apply auto[1] 1531 apply ((wp 1532 | wpc 1533 | simp add: invocation_duplicates_valid_def unlessE_def whenE_def 1534 pti_duplicates_valid_def page_inv_duplicates_valid_def 1535 if_apply_def2 1536 del: hoare_True_E_R 1537 split del: if_split 1538 | simp only: obj_at_def)+) 1539 apply (auto simp:valid_cap_simps) 1540 done 1541qed 1542 1543lemma decode_invocation_valid_pdpt[wp]: 1544 "\<lbrace>invs and valid_cap cap and valid_pdpt_objs\<rbrace> decode_invocation label args cap_index slot cap excaps 1545 \<lbrace>invocation_duplicates_valid\<rbrace>,-" 1546 apply (simp add: decode_invocation_def split del: if_split) 1547 apply (rule hoare_pre) 1548 apply (wp | wpc 1549 | simp only: invocation_duplicates_valid_def o_def uncurry_def split_def 1550 Invocations_A.invocation.simps)+ 1551 apply clarsimp 1552 done 1553 1554crunch valid_pdpt_objs[wp]: handle_fault, reply_from_kernel "valid_pdpt_objs" 1555 (simp: crunch_simps wp: crunch_wps) 1556 1557 1558lemma invocation_duplicates_valid_exst_update[simp]: 1559 "invocation_duplicates_valid i (trans_state f s) = invocation_duplicates_valid i s" 1560 apply (clarsimp simp add: invocation_duplicates_valid_def pti_duplicates_valid_def page_inv_duplicates_valid_def page_inv_entries_safe_def split: sum.splits invocation.splits arch_invocation.splits kernel_object.splits page_table_invocation.splits page_invocation.splits)+ 1561 done 1562 1563 1564lemma set_thread_state_duplicates_valid[wp]: 1565 "\<lbrace>invocation_duplicates_valid i\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. invocation_duplicates_valid i\<rbrace>" 1566 apply (simp add: set_thread_state_def set_object_def) 1567 apply (wp|simp)+ 1568 apply (clarsimp simp: invocation_duplicates_valid_def pti_duplicates_valid_def 1569 page_inv_duplicates_valid_def page_inv_entries_safe_def 1570 Let_def 1571 dest!: get_tcb_SomeD 1572 split: Invocations_A.invocation.split arch_invocation.split_asm 1573 page_table_invocation.split 1574 page_invocation.split sum.split 1575 ) 1576 apply (auto simp add: obj_at_def page_inv_entries_safe_def) 1577 done 1578 1579lemma handle_invocation_valid_pdpt[wp]: 1580 "\<lbrace>valid_pdpt_objs and invs and ct_active\<rbrace> 1581 handle_invocation calling blocking \<lbrace>\<lambda>rv. valid_pdpt_objs\<rbrace>" 1582 apply (simp add: handle_invocation_def) 1583 apply (wp syscall_valid set_thread_state_ct_st 1584 | simp add: split_def | wpc 1585 | wp_once hoare_drop_imps)+ 1586 apply (auto simp: ct_in_state_def elim: st_tcb_ex_cap) 1587 done 1588 1589 1590crunch valid_pdpt[wp]: handle_event, activate_thread,switch_to_thread, 1591 switch_to_idle_thread "valid_pdpt_objs" 1592 (simp: crunch_simps wp: crunch_wps alternative_valid select_wp OR_choice_weak_wp select_ext_weak_wp 1593 ignore: without_preemption getActiveIRQ resetTimer ackInterrupt 1594 getFAR getDFSR getIFSR OR_choice set_scheduler_action 1595 clearExMonitor) 1596 1597lemma schedule_valid_pdpt[wp]: "\<lbrace>valid_pdpt_objs\<rbrace> schedule :: (unit,unit) s_monad \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" 1598 apply (simp add: schedule_def allActiveTCBs_def) 1599 apply (wp alternative_wp select_wp) 1600 apply simp 1601 done 1602 1603lemma call_kernel_valid_pdpt[wp]: 1604 "\<lbrace>invs and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running s) and valid_pdpt_objs\<rbrace> 1605 (call_kernel e) :: (unit,unit) s_monad 1606 \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>" 1607 apply (cases e, simp_all add: call_kernel_def) 1608 apply (rule hoare_pre) 1609 apply (wp | simp add: if_apply_def2 | wpc 1610 | rule conjI | clarsimp simp: ct_in_state_def 1611 | erule pred_tcb_weakenE 1612 | wp_once hoare_drop_imps)+ 1613 done 1614 1615end 1616 1617end 1618