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 Detype_C 12imports Ctac_lemmas_C TcbQueue_C 13begin 14 15lemma typ_clear_region_out: 16 "x \<notin> {p..+2 ^ bits} \<Longrightarrow> typ_clear_region p bits d x = d x" 17 unfolding typ_clear_region_def 18 by simp 19 20lemma typ_bytes_region_out: 21 "x \<notin> {p..+2 ^ bits} \<Longrightarrow> typ_region_bytes p bits d x = d x" 22 unfolding typ_region_bytes_def 23 by simp 24 25lemma h_t_valid_ptr_clear_region: 26 fixes p :: "'a :: c_type ptr" 27 shows "typ_clear_region ptr bits hp,g \<Turnstile>\<^sub>t p = 28 ({ptr_val p ..+ size_of (TYPE ('a))} \<inter> {ptr ..+ 2 ^ bits} = {} \<and> hp,g \<Turnstile>\<^sub>t p)" 29 unfolding h_t_valid_def 30 apply (clarsimp simp: valid_footprint_def Let_def) 31 apply (rule iffI) 32 apply clarsimp 33 apply (rule conjI) 34 apply (clarsimp simp: disjoint_iff_not_equal) 35 apply (drule intvlD) 36 apply (clarsimp simp: size_of_def) 37 apply (drule spec, drule (1) mp) 38 apply (clarsimp simp: typ_clear_region_def) 39 apply clarsimp 40 apply (drule spec, drule (1) mp) 41 apply (clarsimp simp: typ_clear_region_def split: if_split_asm) 42 apply clarsimp 43 apply (drule spec, drule (1) mp) 44 apply (subgoal_tac "ptr_val p + of_nat y \<notin> {ptr..+2 ^ bits}") 45 apply (simp add: typ_clear_region_out) 46 apply clarsimp 47 apply (drule intvlD) 48 apply (clarsimp simp: disjoint_iff_not_equal ) 49 apply (drule_tac x = "ptr_val p + of_nat y" in bspec) 50 apply (rule intvlI) 51 apply (simp add: size_of_def) 52 apply (drule_tac x = "ptr + of_nat k" in bspec) 53 apply (erule intvlI) 54 apply simp 55 done 56 57lemma map_of_le: 58 "map_le (map_of xs) m \<Longrightarrow> distinct (map fst xs) \<Longrightarrow> \<forall>(x, v) \<in> set xs. m x = Some v" 59 apply (induct xs) 60 apply simp 61 apply clarsimp 62 apply (clarsimp simp: map_le_def dom_map_of_conv_image_fst) 63 apply (drule(1) bspec, simp) 64 apply (simp(no_asm_use) split: if_split_asm) 65 apply (fastforce simp: image_def) 66 apply simp 67 done 68 69lemma list_map_le_singleton: 70 "map_le (list_map xs) [n \<mapsto> x] 71 = (xs = [] \<or> n = 0 \<and> xs = [x])" 72 apply (simp add: list_map_def) 73 apply (rule iffI) 74 apply (drule map_of_le) 75 apply simp 76 apply (cases xs, simp_all add: list_map_def upt_conv_Cons 77 split: if_split_asm del: upt.simps) 78 apply (case_tac list, simp_all add: upt_conv_Cons del: upt.simps) 79 apply auto 80 done 81 82lemma neq_types_not_typ_slice_eq: 83 "\<lbrakk> s \<noteq> t \<rbrakk> \<Longrightarrow> typ_slice_t s k \<noteq> [(t, v)]" 84 using ladder_set_self[where s=s and n=k] 85 by clarsimp 86 87lemma valid_footprint_typ_region_bytes: 88 assumes neq_byte: "td \<noteq> typ_uinfo_t TYPE (word8)" 89 shows "valid_footprint (typ_region_bytes ptr bits hp) p td = 90 ({p ..+ size_td td} \<inter> {ptr ..+ 2 ^ bits} = {} \<and> valid_footprint hp p td)" 91 apply (clarsimp simp: valid_footprint_def Let_def) 92 apply (rule iffI) 93 apply clarsimp 94 apply (rule conjI) 95 apply (clarsimp simp: disjoint_iff_not_equal) 96 apply (drule intvlD) 97 apply (clarsimp simp: size_of_def) 98 apply (drule spec, drule (1) mp) 99 apply (clarsimp simp: typ_region_bytes_def list_map_le_singleton neq_byte 100 neq_types_not_typ_slice_eq) 101 apply clarsimp 102 apply (drule spec, drule (1) mp) 103 apply (clarsimp simp: typ_region_bytes_def list_map_le_singleton neq_byte 104 neq_types_not_typ_slice_eq 105 split: if_split_asm) 106 apply clarsimp 107 apply (drule spec, drule (1) mp) 108 apply (subgoal_tac "p + of_nat y \<notin> {ptr..+2 ^ bits}") 109 apply (simp add: typ_bytes_region_out) 110 apply clarsimp 111 apply (drule intvlD) 112 apply (clarsimp simp: disjoint_iff_not_equal ) 113 apply (drule_tac x = "p + of_nat y" in bspec) 114 apply (rule intvlI) 115 apply (simp add: size_of_def) 116 apply (drule_tac x = "ptr + of_nat k" in bspec) 117 apply (erule intvlI) 118 apply simp 119 done 120 121lemma h_t_valid_typ_region_bytes: 122 fixes p :: "'a :: c_type ptr" 123 assumes neq_byte: "typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE (word8)" 124 shows "typ_region_bytes ptr bits hp,g \<Turnstile>\<^sub>t p = 125 ({ptr_val p ..+ size_of (TYPE ('a))} \<inter> {ptr ..+ 2 ^ bits} = {} \<and> hp,g \<Turnstile>\<^sub>t p)" 126 unfolding h_t_valid_def 127 by (simp add: valid_footprint_typ_region_bytes[OF neq_byte] 128 size_of_def) 129 130lemma proj_d_lift_state_hrs_htd_update [simp]: 131 "proj_d (lift_state (hrs_htd_update f hp)) = f (hrs_htd hp)" 132 by (cases hp) (simp add: hrs_htd_update_def proj_d_lift_state hrs_htd_def) 133 134lemma proj_d_lift_state_hrs_htd [simp]: 135 "proj_d (lift_state hp), g \<Turnstile>\<^sub>t x = hrs_htd hp, g \<Turnstile>\<^sub>t x" 136 apply (cases hp) 137 apply (simp add: proj_d_lift_state hrs_htd_def) 138 done 139 140lemma heap_list_s_heap_list': 141 fixes p :: "'a :: c_type ptr" 142 shows "hrs_htd hp,\<top> \<Turnstile>\<^sub>t p \<Longrightarrow> 143 heap_list_s (lift_state hp) (size_of TYPE('a)) (ptr_val p) = 144 heap_list (hrs_mem hp) (size_of TYPE('a)) (ptr_val p)" 145 apply (cases hp) 146 apply (simp add: hrs_htd_def hrs_mem_def heap_list_s_heap_list) 147 done 148 149lemma lift_t_typ_clear_region: 150 assumes doms: "\<And>x :: 'a :: mem_type ptr. \<lbrakk> hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<in> - (Ptr ` {ptr ..+2 ^ bits}) \<rbrakk> 151 \<Longrightarrow> {ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}" 152 shows "(lift_t g (hrs_htd_update (typ_clear_region ptr bits) hp) :: 'a :: mem_type typ_heap) = 153 lift_t g hp |` (- Ptr ` {ptr ..+2 ^ bits})" 154 apply (rule ext) 155 apply (case_tac "({ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x)") 156 apply (clarsimp simp add: lift_t_def lift_typ_heap_if s_valid_def h_t_valid_ptr_clear_region) 157 apply (subgoal_tac "x \<in> - Ptr ` {ptr..+2 ^ bits}") 158 apply clarsimp 159 apply (subst heap_list_s_heap_list') 160 apply (clarsimp simp add: hrs_htd_update h_t_valid_ptr_clear_region) 161 apply (erule h_t_valid_taut) 162 apply (subst heap_list_s_heap_list') 163 apply (clarsimp elim!: h_t_valid_taut) 164 apply simp 165 apply clarsimp 166 apply (drule (1) orthD2) 167 apply (erule contrapos_np, rule intvl_self) 168 apply (simp add: size_of_def wf_size_desc_gt) 169 apply (simp add: lift_t_def lift_typ_heap_if s_valid_def h_t_valid_ptr_clear_region del: disj_not1 split del: if_split) 170 apply (subst if_not_P) 171 apply simp 172 apply (case_tac "x \<in> (- Ptr ` {ptr..+2 ^ bits})") 173 apply (simp del: disj_not1) 174 apply (erule contrapos_pn) 175 apply simp 176 apply (erule doms) 177 apply simp 178 apply simp 179 done 180 181lemma image_Ptr: 182 "Ptr ` S = {x. ptr_val x \<in> S}" 183 apply (safe, simp_all) 184 apply (case_tac x, simp_all) 185 done 186 187lemma lift_t_typ_region_bytes: 188 assumes doms: "\<And>x :: 'a :: mem_type ptr. \<lbrakk> hrs_htd hp,g \<Turnstile>\<^sub>t x; x \<in> - (Ptr ` {ptr ..+2 ^ bits}) \<rbrakk> 189 \<Longrightarrow> {ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {}" 190 assumes neq_byte: "typ_uinfo_t TYPE('a) \<noteq> typ_uinfo_t TYPE (word8)" 191 shows "(lift_t g (hrs_htd_update (typ_region_bytes ptr bits) hp) :: 'a :: mem_type typ_heap) = 192 lift_t g hp |` (- Ptr ` {ptr ..+2 ^ bits})" 193 apply (rule ext) 194 apply (case_tac "({ptr_val x..+size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} \<and> hrs_htd hp,g \<Turnstile>\<^sub>t x)") 195 apply (clarsimp simp add: lift_t_def lift_typ_heap_if s_valid_def 196 h_t_valid_typ_region_bytes neq_byte) 197 apply (subgoal_tac "x \<in> - Ptr ` {ptr..+2 ^ bits}") 198 apply clarsimp 199 apply (subst heap_list_s_heap_list') 200 apply (clarsimp simp add: hrs_htd_update h_t_valid_typ_region_bytes neq_byte) 201 apply (erule h_t_valid_taut) 202 apply (subst heap_list_s_heap_list') 203 apply (clarsimp elim!: h_t_valid_taut) 204 apply simp 205 apply (simp add: image_Ptr) 206 apply (cut_tac p=x in mem_type_self) 207 apply blast 208 apply (simp add: lift_t_def lift_typ_heap_if s_valid_def neq_byte 209 h_t_valid_typ_region_bytes del: disj_not1 split del: if_split) 210 apply (clarsimp simp add: restrict_map_def) 211 apply (blast dest: doms) 212 done 213 214context kernel 215begin 216 217lemma cmap_relation_h_t_valid: 218 fixes p :: "'a :: c_type ptr" 219 shows "\<lbrakk>cmap_relation am (cslift s' :: 'a typ_heap) f rel; s' \<Turnstile>\<^sub>c p; 220 \<And>v v' x. \<lbrakk>f x = p; am x = Some v; cslift s' p = Some v'; rel v v'\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 221 unfolding cmap_relation_def 222 apply (clarsimp simp: h_t_valid_clift_Some_iff) 223 apply (drule equalityD2) 224 apply (drule (1) subsetD [OF _ domI]) 225 apply clarsimp 226 apply (drule (1) bspec [OF _ domI]) 227 apply clarsimp 228 done 229 230lemma valid_untyped_capE: 231 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 232 and rl: "\<lbrakk>is_aligned ptr bits; valid_untyped' d ptr bits idx s; ptr \<noteq> 0; bits < word_bits \<rbrakk> \<Longrightarrow> P" 233 shows P 234proof (rule rl) 235 from vuc show al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 236 unfolding valid_cap'_def capAligned_def by auto 237 238 from al p0 show wb: "bits < word_bits" 239 by (clarsimp elim!: is_aligned_get_word_bits[where 'a=32, folded word_bits_def]) 240qed 241(*FIX me: move *) 242 243lemma valid_untyped_pspace_no_overlap': 244 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 245 and idx: "idx< 2^ bits" 246 and psp_al: "pspace_aligned' s" "pspace_distinct' s" 247 shows "pspace_no_overlap' (ptr + of_nat idx) bits s" 248 249proof - 250 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 251 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 252 253 from vuc have al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 254 and wb: "bits < word_bits" 255 by (auto elim!: valid_untyped_capE) 256 257 from vuc idx 258 have [simp]: "(ptr + (of_nat idx) && ~~ mask bits) = ptr" 259 apply - 260 apply (rule is_aligned_add_helper[THEN conjunct2]) 261 apply (clarsimp simp:valid_cap'_def capAligned_def)+ 262 apply (rule word_of_nat_less) 263 apply simp 264 done 265 266 show "pspace_no_overlap' (ptr + of_nat idx) bits s" 267 using vuc idx psp_al 268 apply - 269 apply (clarsimp simp:valid_cap'_def valid_untyped'_def pspace_no_overlap'_def) 270 apply (drule_tac x = x in spec) 271 apply (frule(1) pspace_alignedD') 272 apply (frule(1) pspace_distinctD') 273 apply (clarsimp simp:ko_wp_at'_def obj_range'_def p_assoc_help) 274 done 275 qed 276 277lemma cmap_relation_disjoint: 278 fixes rel :: "'a :: pspace_storable \<Rightarrow> 'b :: mem_type \<Rightarrow> bool" and x :: "'b :: mem_type ptr" 279 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 280 and invs: "invs' s" 281 and cm: "cmap_relation (proj \<circ>\<^sub>m (ksPSpace s)) (cslift s') Ptr rel" 282 and ht: "s' \<Turnstile>\<^sub>c x" 283 and tp: "\<And>ko v. proj ko = Some v \<Longrightarrow> koType TYPE('a) = koTypeOf ko" 284 and xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}" 285 and sof: "size_td (typ_info_t TYPE('b)) \<le> 2 ^ objBits (undefined :: 'a)" 286 shows "{ptr_val x..+size_of TYPE('b)} \<inter> {ptr..+2 ^ bits} = {}" 287proof - 288 from vuc have al: "is_aligned ptr bits" 289 and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 290 and wb: "bits < word_bits" 291 and [simp]: "(ptr && ~~ mask bits) = ptr" 292 by (auto elim!: valid_untyped_capE) 293 294 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 295 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 296 297 let ?ran = "{ptr..ptr + 2 ^ bits - 1}" 298 let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" 299 from cm ht obtain ko and v :: 'a where ks: "ksPSpace s (ptr_val x) = Some ko" and po: "proj ko = Some v" 300 apply (rule cmap_relation_h_t_valid) 301 apply (clarsimp simp: map_comp_Some_iff) 302 done 303 304 let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBitsKO ko - 1}" 305 let ?ran' = "{ptr..+2 ^ bits}" 306 let ?oran' = "{ptr_val x..+2 ^ objBitsKO ko}" 307 308 have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by blast 309 310 have oran' [simp]: "?oran' = ?oran" 311 proof (rule upto_intvl_eq) 312 from invs have "pspace_aligned' s" .. 313 with ks show "is_aligned (ptr_val x) (objBitsKO ko)" .. 314 qed 315 316 from xv have "ptr_val x \<in> (- ?ran)" apply (simp only: ran' Compl_iff) 317 apply (erule contrapos_nn) 318 apply (erule image_eqI [rotated]) 319 apply simp 320 done 321 322 hence "ksPSpace ?s (ptr_val x) = Some ko" using ks by auto 323 hence "?oran \<inter> ?ran = {}" 324 proof (rule pspace_no_overlapD'[where p = ptr and bits = bits,simplified]) 325 from invs have "valid_pspace' s" .. 326 with vu al show "pspace_no_overlap' ptr bits ?s" by (rule valid_untyped_no_overlap) 327 qed 328 329 hence "?oran' \<inter> ?ran' = {}" by simp 330 thus "{ptr_val x..+size_of TYPE('b)} \<inter> ?ran' = {}" 331 proof (rule disjoint_subset [rotated]) 332 have "objBits (undefined :: 'a) = objBitsKO ko" using po 333 apply (simp add: objBits_def) 334 apply (rule objBits_type) 335 apply (subst iffD1 [OF project_koType]) 336 apply (fastforce simp add: project_inject) 337 apply (erule tp) 338 done 339 thus "{ptr_val x..+size_of TYPE('b)} \<subseteq> ?oran'" using sof 340 apply - 341 apply (rule intvl_start_le) 342 apply (simp add: size_of_def) 343 done 344 qed 345qed 346 347lemma vut_subseteq: 348notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 349 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 350shows "\<lbrakk>s \<turnstile>' UntypedCap d ptr bits idx;idx < 2 ^ bits\<rbrakk> 351 \<Longrightarrow> Ptr ` {ptr + of_nat idx..ptr + 2 ^ bits - 1} \<subseteq> Ptr ` {ptr ..+ 2^bits}" (is "\<lbrakk>?a1;?a2\<rbrakk> \<Longrightarrow> ?b \<subseteq> ?c") 352 apply (subgoal_tac "?c = Ptr ` {ptr ..ptr + 2 ^ bits - 1}") 353 apply (simp add:inj_image_subset_iff) 354 apply (clarsimp simp:blah valid_cap'_def capAligned_def) 355 apply (rule is_aligned_no_wrap') 356 apply simp+ 357 apply (rule word_of_nat_less) 358 apply simp 359 apply (rule arg_cong[where f = "\<lambda>x. Ptr ` x"]) 360 apply (rule upto_intvl_eq) 361 apply (clarsimp simp:valid_cap'_def capAligned_def)+ 362 done 363 364(* CLAG : IpcCancel_C *) 365lemma tcb_ptr_to_ctcb_ptr_imageD: 366 "x \<in> tcb_ptr_to_ctcb_ptr ` S \<Longrightarrow> ctcb_ptr_to_tcb_ptr x \<in> S" 367 apply (erule imageE) 368 apply simp 369 done 370 371lemma ctcb_ptr_to_tcb_ptr_imageI: 372 "ctcb_ptr_to_tcb_ptr x \<in> S \<Longrightarrow> x \<in> tcb_ptr_to_ctcb_ptr ` S" 373 apply (drule imageI [where f = tcb_ptr_to_ctcb_ptr]) 374 apply simp 375 done 376 377lemma aligned_ranges_subset_or_disjointE [consumes 2, case_names disjoint subset1 subset2]: 378 "\<lbrakk>is_aligned p n; is_aligned p' n'; 379 {p..p + 2 ^ n - 1} \<inter> {p'..p' + 2 ^ n' - 1} = {} \<Longrightarrow> P; 380 {p..p + 2 ^ n - 1} \<subseteq> {p'..p' + 2 ^ n' - 1} \<Longrightarrow> P; 381 {p'..p' + 2 ^ n' - 1} \<subseteq> {p..p + 2 ^ n - 1} \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 382 apply (drule (1) aligned_ranges_subset_or_disjoint) 383 apply blast 384 done 385 386lemma valid_untyped_cap_ko_at_disjoint: 387 assumes vu: "s \<turnstile>' UntypedCap d ptr bits idx" 388 and koat: "ko_at' ko x s" 389 and pv: "{x .. x + 2 ^ objBits ko - 1} \<inter> {ptr .. ptr + 2 ^ bits - 1} \<noteq> {}" 390 shows "{x .. x + 2 ^ objBits ko - 1} \<subseteq> {ptr .. ptr + 2 ^ bits - 1}" 391 392proof - 393 from vu have "is_aligned ptr bits" 394 unfolding valid_cap'_def capAligned_def by simp 395 396 moreover from koat have "is_aligned x (objBits ko)" 397 by (rule obj_atE') (simp add: projectKOs objBits_def project_inject) 398 399 ultimately show ?thesis 400 proof (cases rule: aligned_ranges_subset_or_disjointE) 401 case disjoint 402 thus ?thesis using pv by auto 403 next 404 case subset2 thus ?thesis . 405 next 406 case subset1 407 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 408 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 409 have "\<not> ko_wp_at' (\<lambda>ko. {ptr..ptr + 2 ^ bits - 1} \<subset> obj_range' x ko) x s" 410 using vu unfolding valid_cap'_def valid_untyped'_def 411 apply clarsimp 412 apply (drule_tac x = x in spec) 413 apply (clarsimp simp:ko_wp_at'_def) 414 done 415 416 with koat have "\<not> {ptr..ptr + 2 ^ bits - 1} \<subset> {x..x + 2 ^ objBits ko - 1}" 417 apply - 418 apply (erule obj_atE')+ 419 apply (simp add: ko_wp_at'_def projectKOs obj_range'_def not_less objBits_def project_inject) 420 done 421 422 thus ?thesis using subset1 423 by (simp add: psubset_eq del: Icc_eq_Icc) 424 qed 425qed 426 427lemma tcb_ptr_to_ctcb_ptr_in_range: 428 fixes tcb :: tcb 429 assumes tat: "ko_at' tcb x s" 430 shows "ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}" 431proof - 432 from tat have al: "is_aligned x tcbBlockSizeBits" 433 by (clarsimp elim!: obj_atE' simp: projectKOs objBits_simps) 434 hence "x \<le> x + 2 ^ tcbBlockSizeBits - 1" 435 by (rule is_aligned_no_overflow) 436 437 moreover from al have "x \<le> x + 2 ^ ctcb_size_bits" 438 by (rule is_aligned_no_wrap') (simp add: ctcb_size_bits_def objBits_defs) 439 440 ultimately show ?thesis 441 unfolding tcb_ptr_to_ctcb_ptr_def 442 by (simp add: ctcb_offset_defs objBits_simps' field_simps word_plus_mono_right) 443qed 444 445lemma tcb_ptr_to_ctcb_ptr_in_range': 446 fixes tcb :: tcb 447 assumes al: "is_aligned (ctcb_ptr_to_tcb_ptr x) tcbBlockSizeBits" 448 shows "{ptr_val x ..+ size_of TYPE (tcb_C)} 449 \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}" 450proof - 451 from al have "ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ tcbBlockSizeBits - 1" 452 by (rule is_aligned_no_overflow) 453 454 moreover from al have "ctcb_ptr_to_tcb_ptr x \<le> ctcb_ptr_to_tcb_ptr x + 2 ^ ctcb_size_bits" 455 by (rule is_aligned_no_wrap') (simp add: ctcb_size_bits_def objBits_defs) 456 457 moreover from al have "is_aligned (ptr_val x) ctcb_size_bits" by (rule ctcb_ptr_to_tcb_ptr_aligned) 458 moreover from al have "{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} = {ctcb_ptr_to_tcb_ptr x.. ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}" 459 apply - 460 apply (rule upto_intvl_eq) 461 apply (simp add: objBits_simps') 462 done 463 464 ultimately show ?thesis 465 unfolding ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs 466 apply - 467 apply (clarsimp simp: field_simps objBits_simps' size_of_def) 468 apply (drule intvlD) 469 apply clarsimp 470 apply (rule conjI) 471 apply (erule order_trans, erule is_aligned_no_wrap') 472 apply (rule of_nat_power) 473 apply simp 474 apply simp 475 apply (rule word_plus_mono_right) 476 apply (simp add: word_le_nat_alt unat_of_nat) 477 apply (erule is_aligned_no_wrap') 478 apply simp 479 done 480qed 481 482lemma valid_untyped_cap_ctcb_member: 483 fixes tcb :: tcb 484 assumes vu: "s \<turnstile>' UntypedCap d ptr bits idx" 485 and koat: "ko_at' tcb x s" 486 and pv: "ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr .. ptr + 2 ^ bits - 1}" 487 shows "x \<in> {ptr .. ptr + 2 ^ bits - 1}" 488 using vu 489proof - 490 from vu koat have "{x..x + 2 ^ objBits tcb - 1} \<subseteq> {ptr..ptr + 2 ^ bits - 1}" 491 proof (rule valid_untyped_cap_ko_at_disjoint) 492 from koat have "ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {x..x + 2 ^ objBits tcb - 1}" 493 by (rule tcb_ptr_to_ctcb_ptr_in_range) 494 thus "{x..x + 2 ^ objBits tcb - 1} \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}" using pv 495 apply - 496 apply rule 497 apply (drule (1) orthD1) 498 apply simp 499 done 500 qed 501 502 thus ?thesis 503 proof (rule set_mp) 504 from koat have "is_aligned x (objBits tcb)" by (clarsimp elim!: obj_atE' simp: objBits_simps projectKOs) 505 thus "x \<in> {x..x + 2 ^ objBits tcb - 1}" 506 apply (rule base_member_set [simplified field_simps]) 507 apply (simp add: objBits_simps' word_bits_conv) 508 done 509 qed 510qed 511 512lemma ko_at_is_aligned' [intro?]: 513 "ko_at' ko p s \<Longrightarrow> is_aligned p (objBits ko)" 514 apply (erule obj_atE') 515 apply (simp add: objBits_def projectKOs project_inject) 516 done 517 518lemma cmap_relation_disjoint_tcb: 519 fixes x :: "tcb_C ptr" 520 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 521 and invs: "invs' s" 522 and cm: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') tcb_ptr_to_ctcb_ptr ctcb_relation" 523 and ht: "s' \<Turnstile>\<^sub>c x" 524 and xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}" 525 shows "{ptr_val x..+size_of TYPE(tcb_C)} \<inter> {ptr..+2 ^ bits} = {}" 526proof - 527 let ?ran = "{ptr..ptr + 2 ^ bits - 1}" 528 let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" 529 from cm ht invs obtain tcb :: tcb where koat: "ko_at' tcb (ctcb_ptr_to_tcb_ptr x) s" 530 apply - 531 apply (erule (1) cmap_relation_h_t_valid) 532 apply (drule (1) map_to_ko_atI') 533 apply clarsimp 534 done 535 536 let ?oran = "{ctcb_ptr_to_tcb_ptr x .. ctcb_ptr_to_tcb_ptr x + 2 ^ objBits tcb - 1}" 537 let ?ran' = "{ptr..+2 ^ bits}" 538 let ?oran' = "{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}" 539 540 from vuc have al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 541 and wb: "bits < word_bits" 542 by (auto elim!: valid_untyped_capE) 543 544 have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by blast 545 546 have oran' [simp]: "?oran' = ?oran" 547 proof (rule upto_intvl_eq) 548 from koat show "is_aligned (ctcb_ptr_to_tcb_ptr x) (objBits tcb)" .. 549 qed 550 551 show ?thesis 552 proof (rule disjoint_subset) 553 from xv koat have "\<not> ?oran \<subseteq> ?ran" 554 apply - 555 apply (erule contrapos_nn) 556 apply (drule tcb_ptr_to_ctcb_ptr_in_range) 557 apply (rule image_eqI [where x = "ptr_val x"]) 558 apply simp 559 apply (drule (1) subsetD) 560 apply simp 561 done 562 563 thus "{ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb} \<inter> {ptr..+2 ^ bits} = {}" 564 apply (rule contrapos_np) 565 apply (rule valid_untyped_cap_ko_at_disjoint [OF vuc koat]) 566 apply simp 567 done 568 569 from koat show "{ptr_val x..+size_of TYPE(tcb_C)} \<subseteq> {ctcb_ptr_to_tcb_ptr x..+2 ^ objBits tcb}" 570 by (metis tcb_ptr_to_ctcb_ptr_in_range' tcb_aligned' obj_at'_weakenE) 571 qed 572qed 573 574lemma ctes_of_is_aligned: 575 fixes s :: "kernel_state" 576 assumes ks: "ctes_of s p = Some cte" 577 shows "is_aligned p (objBits cte)" 578proof - 579 have "cte_wp_at' ((=) cte) p s" using ks by (clarsimp simp: cte_wp_at_ctes_of) 580 thus ?thesis 581 apply (simp add: cte_wp_at_cases' objBits_simps' cte_level_bits_def) 582 apply (erule disjE) 583 apply simp 584 apply clarsimp 585 apply (drule_tac y = n in aligned_add_aligned [where m = 4]) 586 apply (simp add: tcb_cte_cases_def is_aligned_def split: if_split_asm) 587 apply (simp add: word_bits_conv) 588 apply simp 589 done 590qed 591 592lemma cte_wp_at_casesE' [consumes 1, case_names cte tcb]: 593 "\<lbrakk>cte_wp_at' P p s; 594 \<And>cte. \<lbrakk> ksPSpace s p = Some (KOCTE cte); is_aligned p cte_level_bits; P cte; ps_clear p cteSizeBits s \<rbrakk> \<Longrightarrow> R; 595 \<And>n tcb getF setF. \<lbrakk> 596 ksPSpace s (p - n) = Some (KOTCB tcb); 597 is_aligned (p - n) tcbBlockSizeBits; 598 tcb_cte_cases n = Some (getF, setF); 599 P (getF tcb); ps_clear (p - n) tcbBlockSizeBits s\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 600 by (fastforce simp: cte_wp_at_cases') 601 602 603(* FIXME: MOVE *) 604lemma tcb_cte_cases_in_range3: 605 assumes tc: "tcb_cte_cases (y - x) = Some v" 606 and al: "is_aligned x tcbBlockSizeBits" 607 shows "y + 2 ^ cteSizeBits - 1 \<le> x + 2 ^ tcbBlockSizeBits - 1" 608proof - 609 note [simp] = objBits_defs ctcb_size_bits_def 610 from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ ctcb_size_bits - 1" 611 unfolding tcb_cte_cases_def 612 by (simp add: diff_eq_eq split: if_split_asm) 613 614 have "q + (2 ^ cteSizeBits - 1) \<le> (2 ^ ctcb_size_bits - 1) + (2 ^ cteSizeBits - 1)" using qv 615 by (rule word_plus_mcs_3) simp 616 also have "\<dots> \<le> 2 ^ tcbBlockSizeBits - 1" by simp 617 finally have "x + (q + (2 ^ cteSizeBits - 1)) \<le> x + (2 ^ tcbBlockSizeBits - 1)" 618 apply (rule word_plus_mono_right) 619 apply (rule is_aligned_no_overflow' [OF al]) 620 done 621 622 thus ?thesis using yq by (simp add: field_simps) 623qed 624 625 626lemma tcb_cte_in_range: 627 "\<lbrakk> ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; 628 tcb_cte_cases n = Some (getF, setF) \<rbrakk> 629 \<Longrightarrow> {p + n.. (p + n) + 2 ^ objBits (cte :: cte) - 1} \<subseteq> {p .. p + 2 ^ objBits tcb - 1}" 630 apply (rule range_subsetI) 631 apply (erule (1) tcb_cte_cases_in_range1 [where y = "p + n" and x = p, simplified]) 632 apply (frule (1) tcb_cte_cases_in_range3 [where y = "p + n" and x = p, simplified]) 633 apply (simp add: objBits_simps') 634 done 635 636lemma tcb_cte_cases_aligned: 637 "\<lbrakk>is_aligned p tcbBlockSizeBits; tcb_cte_cases n = Some (getF, setF)\<rbrakk> 638 \<Longrightarrow> is_aligned (p + n) (objBits (cte :: cte))" 639 apply (erule aligned_add_aligned) 640 apply (simp add: tcb_cte_cases_def is_aligned_def objBits_simps' split: if_split_asm) 641 apply (simp add: objBits_simps') 642 done 643 644lemma tcb_cte_in_range': 645 "\<lbrakk> ksPSpace s p = Some (KOTCB tcb); is_aligned p tcbBlockSizeBits; 646 tcb_cte_cases n = Some (getF, setF) \<rbrakk> 647 \<Longrightarrow> {p + n..+2 ^ objBits (cte :: cte)} \<subseteq> {p ..+ 2 ^ objBits tcb}" 648 apply (subst upto_intvl_eq) 649 apply (erule (1) tcb_cte_cases_aligned) 650 apply (subst upto_intvl_eq) 651 apply (simp add: objBits_simps') 652 apply (erule (2) tcb_cte_in_range) 653 done 654 655(* clagged from above :( Were I smarter or if I cared more I could probably factor out more \<dots>*) 656lemma cmap_relation_disjoint_cte: 657 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 658 and invs: "invs' s" 659 and cm: "cmap_relation (ctes_of s) (cslift s') Ptr ccte_relation" 660 and ht: "s' \<Turnstile>\<^sub>c (x :: cte_C ptr)" 661 and xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}" 662 shows "{ptr_val x..+size_of TYPE(cte_C)} \<inter> {ptr..+2 ^ bits} = {}" 663proof - 664 from vuc have al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 665 and wb: "bits < word_bits" and [simp]: "(ptr && ~~ mask bits) = ptr" 666 by (auto elim!: valid_untyped_capE) 667 668 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 669 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 670 671 let ?ran = "{ptr..ptr + 2 ^ bits - 1}" 672 let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" 673 from cm ht obtain cte where ks: "ctes_of s (ptr_val x) = Some cte" 674 apply (rule cmap_relation_h_t_valid) 675 apply (clarsimp simp: map_comp_Some_iff) 676 done 677 678 let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBits cte - 1}" 679 680 let ?ran' = "{ptr..+2 ^ bits}" 681 let ?oran' = "{ptr_val x..+2 ^ objBits cte}" 682 683 have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by auto 684 685 have oran' [simp]: "?oran' = ?oran" 686 proof (rule upto_intvl_eq) 687 from ks show "is_aligned (ptr_val x) (objBits cte)" 688 by (rule ctes_of_is_aligned) 689 qed 690 691 from xv have px: "ptr_val x \<in> (- ?ran)" 692 apply (simp only: ran' Compl_iff) 693 apply (erule contrapos_nn) 694 apply (erule image_eqI [rotated]) 695 apply simp 696 done 697 698 from ks have "cte_wp_at' ((=) cte) (ptr_val x) s" by (clarsimp simp: cte_wp_at_ctes_of) 699 thus ?thesis 700 proof (cases rule: cte_wp_at_casesE') 701 case (cte cte') 702 703 hence "ksPSpace ?s (ptr_val x) = Some (injectKOS cte)" using px by simp 704 hence "?oran \<inter> ?ran = {}" 705 unfolding objBits_def 706 proof (rule pspace_no_overlapD'[where p = ptr and bits = bits,simplified]) 707 from invs have "valid_pspace' s" .. 708 with vu al show "pspace_no_overlap' ptr bits ?s" by (rule valid_untyped_no_overlap) 709 qed 710 hence "?oran' \<inter> ?ran' = {}" by simp 711 thus ?thesis by (simp add: objBits_simps' size_of_def) 712 next 713 case (tcb n tcb _ _) 714 715 hence koat: "ko_at' tcb (ptr_val x - n) s" 716 apply - 717 apply (erule obj_atI', simp_all add: objBits_simps' projectKOs) 718 done 719 720 let ?tran = "{ptr_val x - n .. (ptr_val x - n) + 2 ^ objBits tcb - 1}" 721 have ot: "?oran \<subseteq> ?tran" 722 by (rule tcb_cte_in_range[where p = "ptr_val x - n" and n = "n", 723 simplified diff_add_cancel]) fact+ 724 725 also 726 from xv have "\<not> \<dots> \<subseteq> ?ran" 727 proof (rule contrapos_nn) 728 assume "?tran \<subseteq> ?ran" 729 with ot have "?oran \<subseteq> ?ran" by (rule order_trans) 730 hence "ptr_val x \<in> ?ran" 731 proof (rule subsetD) 732 from tcb have "is_aligned (ptr_val x) (objBits cte)" 733 apply - 734 apply (drule (1) tcb_cte_cases_aligned) 735 apply simp 736 done 737 hence "ptr_val x \<le> ptr_val x + 2 ^ objBits cte - 1" 738 by (rule is_aligned_no_overflow) 739 thus "ptr_val x \<in> ?oran" by (rule first_in_uptoD) 740 qed 741 thus "x \<in> Ptr ` {ptr..+2 ^ bits}" 742 unfolding ran' 743 by (rule image_eqI [where x = "ptr_val x", rotated]) simp 744 qed 745 746 hence "?tran \<inter> ?ran' = {}" 747 apply (rule contrapos_np) 748 apply (rule valid_untyped_cap_ko_at_disjoint [OF vuc koat]) 749 apply simp 750 done 751 752 finally have "{ptr_val x..+2 ^ objBits cte} \<inter> ?ran' = {}" 753 using ot unfolding oran' 754 by blast 755 thus ?thesis by (simp add: objBits_simps' size_of_def) 756 qed 757qed 758 759lemma cmap_relation_disjoint_user_data: 760 fixes x :: "user_data_C ptr" 761 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 762 and invs: "invs' s" 763 and cm: "cmap_relation (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') Ptr cuser_user_data_relation" 764 and ht: "s' \<Turnstile>\<^sub>c x" 765 and xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}" 766 shows "{ptr_val x..+size_of TYPE(user_data_C)} \<inter> {ptr..+2 ^ bits} = {}" 767proof - 768 from vuc have al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 769 and wb: "bits < word_bits" and [simp]:"ptr && ~~ mask bits = ptr" 770 by (auto elim!: valid_untyped_capE) 771 772 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 773 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 774 775 let ?ran = "{ptr..ptr + 2 ^ bits - 1}" 776 let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" 777 from cm ht have ks: "ksPSpace s (ptr_val x) = Some KOUserData" 778 apply (rule cmap_relation_h_t_valid) 779 apply (clarsimp simp: map_comp_Some_iff heap_to_user_data_def Let_def projectKO_opts_defs) 780 apply (case_tac k') 781 apply simp_all 782 done 783 784 let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBitsKO KOUserData - 1}" 785 786 let ?ran' = "{ptr..+2 ^ bits}" 787 let ?oran' = "{ptr_val x..+2 ^ objBitsKO KOUserData}" 788 789 have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by auto 790 791 have oran' [simp]: "?oran' = ?oran" 792 proof (rule upto_intvl_eq) 793 from invs have "pspace_aligned' s" .. 794 with ks show "is_aligned (ptr_val x) (objBitsKO KOUserData)" .. 795 qed 796 797 from xv have "ptr_val x \<in> (- ?ran)" 798 apply (simp only: ran' Compl_iff) 799 apply (erule contrapos_nn) 800 apply (erule image_eqI [rotated]) 801 apply simp 802 done 803 804 hence "ksPSpace ?s (ptr_val x) = Some KOUserData" using ks by simp 805 hence "?oran \<inter> ?ran = {}" 806 proof (rule pspace_no_overlapD'[where p = ptr and bits = bits,simplified]) 807 from invs have "valid_pspace' s" .. 808 with vu al show "pspace_no_overlap' ptr bits ?s" by (rule valid_untyped_no_overlap) 809 qed 810 811 hence "?oran' \<inter> ?ran' = {}" by simp 812 thus "{ptr_val x..+size_of TYPE(user_data_C)} \<inter> ?ran' = {}" 813 proof (rule disjoint_subset [rotated]) 814 show "{ptr_val x..+size_of TYPE(user_data_C)} \<subseteq> ?oran'" 815 apply - 816 apply (rule intvl_start_le) 817 apply (simp add: size_of_def objBits_simps pageBits_def) 818 done 819 qed 820qed 821 822lemma cmap_relation_disjoint_device_data: 823 fixes x :: "user_data_device_C ptr" 824 assumes vuc: "s \<turnstile>' UntypedCap d ptr bits idx" 825 and invs: "invs' s" 826 and cm: "cmap_relation (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) (cslift s') Ptr cuser_user_data_device_relation" 827 and ht: "s' \<Turnstile>\<^sub>c x" 828 and xv: "x \<notin> Ptr ` {ptr..+2 ^ bits}" 829 shows "{ptr_val x..+size_of TYPE(user_data_device_C)} \<inter> {ptr..+2 ^ bits} = {}" 830proof - 831 from vuc have al: "is_aligned ptr bits" and vu: "valid_untyped' d ptr bits idx s" and p0: "ptr \<noteq> 0" 832 and wb: "bits < word_bits" and [simp]:"ptr && ~~ mask bits = ptr" 833 by (auto elim!: valid_untyped_capE) 834 835 note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 836 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 837 838 let ?ran = "{ptr..ptr + 2 ^ bits - 1}" 839 let ?s = "(s\<lparr>ksPSpace := (ksPSpace s) |` (- ?ran)\<rparr>)" 840 from cm ht have ks: "ksPSpace s (ptr_val x) = Some KOUserDataDevice" 841 apply (rule cmap_relation_h_t_valid) 842 apply (clarsimp simp: map_comp_Some_iff heap_to_device_data_def Let_def projectKO_opts_defs) 843 apply (case_tac k') 844 apply simp_all 845 done 846 847 let ?oran = "{ptr_val x .. ptr_val x + 2 ^ objBitsKO KOUserDataDevice - 1}" 848 849 let ?ran' = "{ptr..+2 ^ bits}" 850 let ?oran' = "{ptr_val x..+2 ^ objBitsKO KOUserDataDevice}" 851 852 have ran' [simp]: "?ran' = ?ran" using al wb upto_intvl_eq by auto 853 854 have oran' [simp]: "?oran' = ?oran" 855 proof (rule upto_intvl_eq) 856 from invs have "pspace_aligned' s" .. 857 with ks show "is_aligned (ptr_val x) (objBitsKO KOUserDataDevice)" .. 858 qed 859 860 from xv have "ptr_val x \<in> (- ?ran)" 861 apply (simp only: ran' Compl_iff) 862 apply (erule contrapos_nn) 863 apply (erule image_eqI [rotated]) 864 apply simp 865 done 866 867 hence "ksPSpace ?s (ptr_val x) = Some KOUserDataDevice" using ks by simp 868 hence "?oran \<inter> ?ran = {}" 869 proof (rule pspace_no_overlapD'[where p = ptr and bits = bits,simplified]) 870 from invs have "valid_pspace' s" .. 871 with vu al show "pspace_no_overlap' ptr bits ?s" by (rule valid_untyped_no_overlap) 872 qed 873 874 hence "?oran' \<inter> ?ran' = {}" by simp 875 thus "{ptr_val x..+size_of TYPE(user_data_device_C)} \<inter> ?ran' = {}" 876 proof (rule disjoint_subset [rotated]) 877 show "{ptr_val x..+size_of TYPE(user_data_device_C)} \<subseteq> ?oran'" 878 apply - 879 apply (rule intvl_start_le) 880 apply (simp add: size_of_def objBits_simps pageBits_def) 881 done 882 qed 883qed 884 885 886lemma tcb_queue_relation_live_restrict: 887 assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx" 888 and rel: "\<forall>t \<in> set q. tcb_at' t s" 889 and live: "\<forall>t \<in> set q. ko_wp_at' live' t s" 890 and rl: "\<forall>(p :: word32) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}" 891 shows "tcb_queue_relation' getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q cend chead = 892 tcb_queue_relation' getNext getPrev cm q cend chead" 893proof (rule tcb_queue_relation'_cong [OF refl refl refl]) 894 fix p 895 assume "p \<in> tcb_ptr_to_ctcb_ptr ` set q" 896 897 hence pin: "ctcb_ptr_to_tcb_ptr p \<in> set q" by (rule tcb_ptr_to_ctcb_ptr_imageD) 898 899 with rel have "tcb_at' (ctcb_ptr_to_tcb_ptr p) s" .. 900 then obtain tcb :: tcb where koat: "ko_at' tcb (ctcb_ptr_to_tcb_ptr p) s" 901 by (clarsimp simp: obj_at'_real_def ko_wp_at'_def) 902 903 from live pin have "ko_wp_at' live' (ctcb_ptr_to_tcb_ptr p) s" .. 904 hence notin: "(ctcb_ptr_to_tcb_ptr p) \<notin> {ptr..ptr + 2 ^ bits - 1}" 905 by (fastforce intro!: rl [rule_format]) 906 907 from vuc have al: "is_aligned ptr bits" and wb: "bits < word_bits" 908 by (auto elim!: valid_untyped_capE) 909 910 hence ran': " {ptr..+2 ^ bits} = {ptr..ptr + 2 ^ bits - 1}" by (simp add: upto_intvl_eq) 911 912 hence "p \<in> - Ptr ` {ptr..+2 ^ bits}" using vuc koat notin 913 apply - 914 apply (erule contrapos_np) 915 apply (erule (1) valid_untyped_cap_ctcb_member) 916 apply (clarsimp elim!: imageE simp: ran') 917 done 918 919 thus "(cm |` (- Ptr ` {ptr..+2 ^ bits})) p = cm p" by simp 920qed 921 922fun 923 epQ :: "endpoint \<Rightarrow> word32 list" 924 where 925 "epQ IdleEP = []" 926 | "epQ (RecvEP ts) = ts" 927 | "epQ (SendEP ts) = ts" 928 929lemma ep_queue_live: 930 assumes invs: "invs' s" 931 and koat: "ko_at' ep p s" 932 shows "\<forall>t \<in> set (epQ ep). ko_wp_at' live' t s" 933proof 934 fix t 935 assume tin: "t \<in> set (epQ ep)" 936 937 from invs koat tin show "ko_wp_at' live' t s" 938 apply - 939 apply (drule sym_refs_ko_atD') 940 apply clarsimp 941 apply (cases ep) 942 by (auto elim!: ko_wp_at'_weakenE [OF _ refs_of_live']) 943qed 944 945fun 946 ntfnQ :: "ntfn \<Rightarrow> word32 list" 947 where 948 "ntfnQ (WaitingNtfn ts) = ts" 949 | "ntfnQ _ = []" 950 951lemma ntfn_queue_live: 952 assumes invs: "invs' s" 953 and koat: "ko_at' ntfn p s" 954 shows "\<forall>t \<in> set (ntfnQ (ntfnObj ntfn)). ko_wp_at' live' t s" 955proof 956 fix t 957 assume tin: "t \<in> set (ntfnQ (ntfnObj ntfn))" 958 959 from invs koat tin show "ko_wp_at' live' t s" 960 apply - 961 apply (drule sym_refs_ko_atD') 962 apply clarsimp 963 apply (cases "ntfnObj ntfn") 964 apply (auto elim!: ko_wp_at'_weakenE [OF _ refs_of_live'] 965 dest!: bspec) 966 done 967qed 968 969lemma cendpoint_relation_restrict: 970 assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx" 971 and invs: "invs' s" 972 and rl: "\<forall>(p :: word32) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}" 973 and meps: "map_to_eps (ksPSpace s) p = Some ep" 974 shows "cendpoint_relation (cslift s' |` (- Ptr ` {ptr..+2 ^ bits})) ep b = cendpoint_relation (cslift s') ep b" 975proof - 976 from invs have "valid_objs' s" .. 977 with meps have vep: "valid_ep' ep s" 978 apply - 979 apply (clarsimp simp add: map_comp_Some_iff projectKOs) 980 apply (erule (1) valid_objsE') 981 apply (simp add: valid_obj'_def) 982 done 983 984 from meps have koat: "ko_at' ep p s" by (rule map_to_ko_atI') fact+ 985 986 show ?thesis 987 proof (cases ep) 988 case (RecvEP ts) 989 990 from vep RecvEP have tats: "\<forall>t \<in> set ts. tcb_at' t s" 991 by (simp add: valid_ep'_def) 992 993 have tlive: "\<forall>t\<in>set ts. ko_wp_at' live' t s" using RecvEP invs koat 994 apply - 995 apply (drule (1) ep_queue_live) 996 apply simp 997 done 998 999 show ?thesis using RecvEP 1000 unfolding cendpoint_relation_def Let_def 1001 by (simp add: tcb_queue_relation_live_restrict [OF vuc tats tlive rl]) 1002 next 1003 case (SendEP ts) 1004 1005 from vep SendEP have tats: "\<forall>t \<in> set ts. tcb_at' t s" 1006 by (simp add: valid_ep'_def) 1007 1008 have tlive: "\<forall>t\<in>set ts. ko_wp_at' live' t s" using SendEP invs koat 1009 apply - 1010 apply (drule (1) ep_queue_live) 1011 apply simp 1012 done 1013 1014 show ?thesis using SendEP 1015 unfolding cendpoint_relation_def Let_def 1016 by (simp add: tcb_queue_relation_live_restrict [OF vuc tats tlive rl]) 1017 next 1018 case IdleEP 1019 thus ?thesis unfolding cendpoint_relation_def Let_def by simp 1020 qed 1021qed 1022 1023lemma cnotification_relation_restrict: 1024 assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx" 1025 and invs: "invs' s" 1026 and rl: "\<forall>(p :: word32) P. ko_wp_at' P p s \<and> (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}" 1027 and meps: "map_to_ntfns (ksPSpace s) p = Some ntfn" 1028 shows "cnotification_relation (cslift s' |` (- Ptr ` {ptr..+2 ^ bits})) ntfn b = cnotification_relation (cslift s') ntfn b" 1029proof - 1030 from invs have "valid_objs' s" .. 1031 with meps have vep: "valid_ntfn' ntfn s" 1032 apply - 1033 apply (clarsimp simp add: map_comp_Some_iff projectKOs) 1034 apply (erule (1) valid_objsE') 1035 apply (simp add: valid_obj'_def) 1036 done 1037 1038 from meps have koat: "ko_at' ntfn p s" by (rule map_to_ko_atI') fact+ 1039 1040 show ?thesis 1041 proof (cases "ntfnObj ntfn") 1042 case (WaitingNtfn ts) 1043 1044 with vep have tats: "\<forall>t \<in> set ts. tcb_at' t s" 1045 by (simp add: valid_ntfn'_def) 1046 1047 have tlive: "\<forall>t\<in>set ts. ko_wp_at' live' t s" using WaitingNtfn invs koat 1048 apply - 1049 apply (drule (1) ntfn_queue_live) 1050 apply simp 1051 done 1052 1053 show ?thesis using WaitingNtfn 1054 unfolding cnotification_relation_def Let_def 1055 by (simp add: tcb_queue_relation_live_restrict [OF vuc tats tlive rl]) 1056 qed (simp_all add: cnotification_relation_def Let_def) 1057qed 1058 1059declare surj_Ptr[simp] 1060 1061declare bij_Ptr[simp] 1062 1063lemma surj_tcb_ptr_to_ctcb_ptr [simp]: 1064 "surj tcb_ptr_to_ctcb_ptr" 1065 by (rule surjI [where f = "ctcb_ptr_to_tcb_ptr"], simp) 1066 1067lemma bij_tcb_ptr_to_ctcb_ptr [simp]: 1068 "bij tcb_ptr_to_ctcb_ptr" by (simp add: bijI) 1069 1070 1071lemma inj_ctcb_ptr_to_tcb_ptr [simp]: 1072 "inj ctcb_ptr_to_tcb_ptr" 1073 apply (rule injI) 1074 apply (simp add: ctcb_ptr_to_tcb_ptr_def) 1075 done 1076 1077lemma surj_ctcb_ptr_to_tcb_ptr [simp]: 1078 "surj ctcb_ptr_to_tcb_ptr" 1079 by (rule surjI [where f = "tcb_ptr_to_ctcb_ptr"], simp) 1080 1081lemma bij_ctcb_ptr_to_tcb_ptr [simp]: 1082 "bij ctcb_ptr_to_tcb_ptr" by (simp add: bijI) 1083 1084lemma cmap_relation_restrict_both: 1085 "\<lbrakk> cmap_relation am cm f rel; bij f\<rbrakk> \<Longrightarrow> cmap_relation (am |` (- S)) (cm |` (- f ` S)) f rel" 1086 unfolding cmap_relation_def 1087 apply (rule conjI) 1088 apply (clarsimp simp: image_Int bij_image_Compl_eq bij_def) 1089 apply (rule ballI) 1090 apply (clarsimp simp: image_iff2 bij_def) 1091 done 1092 1093lemma cmap_relation_restrict_both_proj: 1094 "\<lbrakk> cmap_relation (projectKO_opt \<circ>\<^sub>m am) cm f rel; bij f\<rbrakk> 1095 \<Longrightarrow> cmap_relation (projectKO_opt \<circ>\<^sub>m (am |` (- S))) (cm |` (- f ` S)) f rel" 1096 unfolding cmap_relation_def 1097 apply (rule conjI) 1098 apply (rule equalityI) 1099 apply rule 1100 apply (clarsimp simp: map_comp_restrict_map_Some_iff image_iff2 bij_def) 1101 apply (erule (1) cmap_domE1) 1102 apply simp 1103 apply (clarsimp simp: image_Int bij_image_Compl_eq bij_def) 1104 apply (erule (1) cmap_domE2) 1105 apply (clarsimp simp: image_Int bij_image_Compl_eq bij_def map_comp_restrict_map_Some_iff intro!: imageI) 1106 apply clarsimp 1107 apply (subst restrict_in) 1108 apply (clarsimp simp add: image_iff map_comp_restrict_map_Some_iff inj_eq bij_def) 1109 apply (clarsimp simp add: map_comp_restrict_map_Some_iff) 1110 apply (drule (1) bspec [OF _ domI]) 1111 apply simp 1112 done 1113 1114declare not_snd_assert[simp] 1115 1116lemma ccorres_stateAssert_fwd: 1117 "ccorres r xf (P and R) P' hs b c \<Longrightarrow> ccorres r xf P P' hs (stateAssert R vs >>= (\<lambda>_. b)) c" 1118 apply (rule ccorresI') 1119 apply (simp add: stateAssert_def bind_assoc) 1120 apply (drule not_snd_bindD) 1121 apply (fastforce simp add: in_monad) 1122 apply clarsimp 1123 apply (frule not_snd_bindI1) 1124 apply simp 1125 apply (erule (1) ccorresE) 1126 apply simp 1127 apply assumption 1128 apply assumption 1129 apply assumption 1130 apply (fastforce simp: in_monad') 1131 done 1132 1133(* FIXME: generalise to above *) 1134lemma tcb_ptr_to_ctcb_ptr_comp: 1135 "tcb_ptr_to_ctcb_ptr = Ptr o (\<lambda>p. p + ctcb_offset)" 1136 apply (rule ext) 1137 apply (simp add: tcb_ptr_to_ctcb_ptr_def) 1138 done 1139 1140lemma tcb_ptr_to_ctcb_ptr_to_Ptr: 1141 "tcb_ptr_to_ctcb_ptr ` {p..+b} = Ptr ` {p + ctcb_offset..+b}" 1142 apply (simp add: tcb_ptr_to_ctcb_ptr_comp image_comp [symmetric]) 1143 apply (rule equalityI) 1144 apply clarsimp 1145 apply (rule imageI) 1146 apply (drule intvlD) 1147 apply clarsimp 1148 apply (subgoal_tac "p + ctcb_offset + of_nat k \<in> {p + ctcb_offset..+b}") 1149 apply (simp add: field_simps) 1150 apply (erule intvlI) 1151 apply (rule image_mono) 1152 apply clarsimp 1153 apply (drule intvlD) 1154 apply clarsimp 1155 apply (rule image_eqI) 1156 apply simp 1157 apply (erule intvlI) 1158 done 1159 1160 1161lemma valid_untyped_cap_ctcb_member': 1162 fixes tcb :: tcb 1163 shows "\<lbrakk>s \<turnstile>' capability.UntypedCap d ptr bits idx; ko_at' tcb x s; 1164 ptr_val (tcb_ptr_to_ctcb_ptr x) \<in> {ptr..+2 ^ bits}\<rbrakk> 1165 \<Longrightarrow> x \<in> {ptr..+ 2 ^ bits}" 1166 apply (rule valid_untyped_capE, assumption) 1167 apply (simp only: upto_intvl_eq) 1168 apply (erule (2) valid_untyped_cap_ctcb_member) 1169 done 1170 1171lemma cpspace_tcb_relation_address_subset: 1172 assumes vuc: "s \<turnstile>' capability.UntypedCap d ptr bits idx" 1173 and invs: "invs' s" 1174 and ctcbrel: "cpspace_tcb_relation (ksPSpace s) (t_hrs_' (globals s'))" 1175 shows "cmap_relation (map_to_tcbs (ksPSpace s |` (- {ptr..+2 ^ bits - unat ctcb_offset}))) 1176 (cslift s' |` (- tcb_ptr_to_ctcb_ptr ` {ptr..+2 ^ bits - unat ctcb_offset})) tcb_ptr_to_ctcb_ptr 1177 ctcb_relation 1178 = cmap_relation (map_to_tcbs (ksPSpace s |` (- {ptr..+2 ^ bits}))) 1179 (cslift s' |` (- Ptr ` {ptr..+2 ^ bits})) tcb_ptr_to_ctcb_ptr 1180 ctcb_relation" (is "cmap_relation ?am ?cm tcb_ptr_to_ctcb_ptr ctcb_relation 1181 = cmap_relation ?am' ?cm' tcb_ptr_to_ctcb_ptr ctcb_relation") 1182proof (rule cmap_relation_cong) 1183 from vuc have al: "is_aligned ptr bits" and wb: "bits < word_bits" by (auto elim: valid_untyped_capE) 1184 1185 have r1: "\<And>x tcb. \<lbrakk> (map_to_tcbs (ksPSpace s) x) = Some tcb; x \<in> {ptr..+2 ^ bits}\<rbrakk> 1186 \<Longrightarrow> x \<in> {ptr..+2 ^ bits - unat ctcb_offset}" 1187 proof (subst intvl_aligned_top [where 'a=32, folded word_bits_def, OF _ al _ _ wb]) 1188 fix x tcb 1189 assume mtcb: "map_to_tcbs (ksPSpace s) x = Some tcb" and xin: "x \<in> {ptr..+2 ^ bits}" 1190 1191 from mtcb invs have koat: "ko_at' tcb x s" 1192 by (fastforce simp: map_comp_Some_iff projectKOs intro: aligned_distinct_obj_atI') 1193 1194 thus "is_aligned x (objBits tcb)" 1195 by (clarsimp elim!: obj_atE' simp: projectKOs objBits_def) 1196 1197 (* FIXME: generalise *) 1198 with xin koat show "objBits tcb \<le> bits" using wb 1199 apply - 1200 apply (frule is_aligned_no_overflow) 1201 apply (drule valid_untyped_cap_ko_at_disjoint [OF vuc]) 1202 apply (erule contrapos_pn) 1203 apply (subst upto_intvl_eq [OF al]) 1204 apply (erule orthD1) 1205 apply simp 1206 apply (drule (1) range_subsetD) 1207 apply clarsimp 1208 apply (drule (1) word_sub_mono2 [where b = "(2 :: word32) ^ objBits tcb - 1" 1209 and d = "2 ^ bits - 1", simplified field_simps]) 1210 apply (subst field_simps [symmetric], subst olen_add_eqv [symmetric]) 1211 apply (simp add: field_simps) 1212 apply (subst field_simps [symmetric], subst olen_add_eqv [symmetric]) 1213 apply (rule is_aligned_no_overflow' [OF al]) 1214 apply (subgoal_tac "(2 :: word32) ^ objBits tcb \<noteq> 0") 1215 apply (simp add: word_le_nat_alt unat_minus_one le_diff_iff word_bits_def) 1216 apply (simp add: objBits_simps) 1217 done 1218 1219 show "unat ctcb_offset < 2 ^ objBits tcb" 1220 by (fastforce simp add: ctcb_offset_defs objBits_simps' project_inject) 1221 1222 show "x \<in> {ptr..+2 ^ bits}" by fact 1223 qed 1224 1225 show "dom ?am = dom ?am'" 1226 apply (rule dom_eqI) 1227 apply (clarsimp dest!: r1 simp: map_comp_restrict_map_Some_iff) 1228 apply (clarsimp dest!: intvl_mem_weaken simp: map_comp_restrict_map_Some_iff) 1229 done 1230 1231 let ?ran = "{ptr..+2 ^ bits}" 1232 let ?small_ran = "{ptr..+2 ^ bits - unat ctcb_offset}" 1233 1234 show "dom ?cm = dom ?cm'" 1235 proof (rule dom_eqI) 1236 fix x y 1237 assume "?cm' x = Some y" 1238 hence cl: "cslift s' x = Some y" and xni: "x \<notin> Ptr ` ?ran" 1239 by (auto simp: restrict_map_Some_iff) 1240 1241 with ctcbrel obtain x' tcb where mt: "map_to_tcbs (ksPSpace s) x' = Some tcb" 1242 and xv: "x = tcb_ptr_to_ctcb_ptr x'" 1243 by (fastforce elim!: cmap_relation_h_t_valid simp add: h_t_valid_clift_Some_iff) 1244 1245 have "(cslift s' |` (- tcb_ptr_to_ctcb_ptr ` ?small_ran)) x = Some y" 1246 proof (subst restrict_in) 1247 show "x \<in> - tcb_ptr_to_ctcb_ptr ` ?small_ran" using xni 1248 proof (rule contrapos_np) 1249 assume "x \<notin> - tcb_ptr_to_ctcb_ptr ` ?small_ran" 1250 hence "x \<in> tcb_ptr_to_ctcb_ptr ` ?small_ran" by simp 1251 hence "x \<in> Ptr ` {ptr + ctcb_offset ..+ 2 ^ bits - unat ctcb_offset}" by (simp add: tcb_ptr_to_ctcb_ptr_to_Ptr) 1252 thus "x \<in> Ptr ` ?ran" 1253 by (clarsimp intro!: imageI elim!: intvl_plus_sub_offset) 1254 qed 1255 qed fact 1256 thus "\<exists>y. (cslift s' |` (- tcb_ptr_to_ctcb_ptr ` ?small_ran)) x = Some y" .. 1257 next 1258 fix x y 1259 assume "?cm x = Some y" 1260 hence cl: "cslift s' x = Some y" and xni: "x \<notin> tcb_ptr_to_ctcb_ptr ` ?small_ran" 1261 by (auto simp: restrict_map_Some_iff) 1262 1263 with ctcbrel obtain x' tcb where mt: "map_to_tcbs (ksPSpace s) x' = Some tcb" and xv: "x = tcb_ptr_to_ctcb_ptr x'" 1264 by (fastforce elim!: cmap_relation_h_t_valid simp add: h_t_valid_clift_Some_iff) 1265 1266 from mt invs have koat: "ko_at' tcb x' s" by (rule map_to_ko_atI') 1267 1268 have "(cslift s' |` (- Ptr ` ?ran)) x = Some y" 1269 proof (subst restrict_in) 1270 show "x \<in> - Ptr ` ?ran" using xni 1271 apply (rule contrapos_np) 1272 apply (simp add: xv) 1273 apply (rule imageI) 1274 apply (rule r1 [OF mt]) 1275 apply (rule valid_untyped_cap_ctcb_member' [OF vuc koat]) 1276 apply (erule imageE) 1277 apply simp 1278 done 1279 qed fact 1280 thus "\<exists>y. (cslift s' |` (- Ptr ` ?ran)) x = Some y" .. 1281 qed 1282qed (clarsimp simp: map_comp_Some_iff restrict_map_Some_iff) 1283 1284lemma heap_to_user_data_restrict: 1285 "heap_to_user_data (mp |` S) bhp = (heap_to_user_data mp bhp |` S)" 1286 unfolding heap_to_user_data_def 1287 apply (rule ext) 1288 apply (case_tac "p \<in> S") 1289 apply (simp_all add: Let_def map_comp_def split: option.splits) 1290 done 1291 1292lemma heap_to_device_data_restrict: 1293 "heap_to_device_data (mp |` S) bhp = (heap_to_device_data mp bhp |` S)" 1294 unfolding heap_to_device_data_def 1295 apply (rule ext) 1296 apply (case_tac "p \<in> S") 1297 apply (simp_all add: Let_def map_comp_def split: option.splits) 1298 done 1299 1300lemma ccorres_stateAssert_after: 1301 assumes "ccorres r xf (P and (\<lambda>s. (\<forall>(rv,s') \<in> fst (f s). R s'))) P' hs f c" 1302 shows "ccorres r xf P P' hs (do _ \<leftarrow> f; stateAssert R vs od) c" using assms 1303 apply (clarsimp simp: ccorres_underlying_def split: xstate.splits) 1304 apply (drule snd_stateAssert_after) 1305 apply clarsimp 1306 apply (drule (1) bspec) 1307 apply (clarsimp simp: split_def) 1308 apply (rule conjI) 1309 apply clarsimp 1310 apply (rename_tac s) 1311 apply (erule_tac x=n in allE) 1312 apply (erule_tac x="Normal s" in allE) 1313 apply clarsimp 1314 apply (simp add: bind_def stateAssert_def get_def assert_def) 1315 apply (rule bexI) 1316 prefer 2 1317 apply assumption 1318 apply (clarsimp simp: return_def fail_def) 1319 apply fastforce 1320 apply fastforce 1321 done 1322 1323lemma heap_to_user_data_update_region: 1324 assumes foo: "\<And>x y v. \<lbrakk> map_to_user_data psp x = Some y; 1325 v < 2 ^ pageBits \<rbrakk> \<Longrightarrow> (x + v \<in> S) = (x \<in> S)" 1326 shows 1327 "heap_to_user_data psp (\<lambda>x. if x \<in> S then v else f x) 1328 = (\<lambda>x. if x \<in> S \<inter> dom (map_to_user_data psp) then Some (K (word_rcat [v, v, v, v])) 1329 else heap_to_user_data psp f x)" 1330 apply (rule ext) 1331 apply (simp add: heap_to_user_data_def Let_def 1332 split: if_split) 1333 apply (rule conjI) 1334 apply (clarsimp simp: byte_to_word_heap_def Let_def add.assoc 1335 intro!: ext) 1336 apply (subst foo, assumption+, 1337 (rule word_add_offset_less[where n=2, simplified] 1338 word_add_offset_less[where n=2 and y=0, simplified], 1339 simp_all, rule ucast_less, 1340 simp_all add: word_bits_def pageBits_def 1341 order_less_le_trans[OF ucast_less])[1])+ 1342 apply simp 1343 apply clarsimp 1344 apply (case_tac "map_to_user_data psp x") 1345 apply simp 1346 apply (clarsimp simp: dom_def byte_to_word_heap_def Let_def add.assoc 1347 intro!: ext) 1348 apply (subst foo, assumption, 1349 (rule word_add_offset_less[where n=2, simplified] 1350 word_add_offset_less[where n=2 and y=0, simplified], 1351 simp_all, rule ucast_less, 1352 simp_all add: word_bits_def pageBits_def 1353 order_less_le_trans[OF ucast_less])[1])+ 1354 apply (simp add: field_simps) 1355 done 1356 1357lemma heap_to_device_data_update_region: 1358 assumes foo: "\<And>x y v. \<lbrakk> map_to_user_data_device psp x = Some y; 1359 v < 2 ^ pageBits \<rbrakk> \<Longrightarrow> (x + v \<in> S) = (x \<in> S)" 1360 shows 1361 "heap_to_device_data psp (\<lambda>x. if x \<in> S then v else f x) 1362 = (\<lambda>x. if x \<in> S \<inter> dom (map_to_user_data_device psp) then Some (K (word_rcat [v, v, v, v])) 1363 else heap_to_device_data psp f x)" 1364 apply (rule ext) 1365 apply (simp add: heap_to_device_data_def Let_def 1366 split: if_split) 1367 apply (rule conjI) 1368 apply (clarsimp simp: byte_to_word_heap_def Let_def add.assoc 1369 intro!: ext) 1370 apply (subst foo, assumption+, 1371 (rule word_add_offset_less[where n=2, simplified] 1372 word_add_offset_less[where n=2 and y=0, simplified], 1373 simp_all, rule ucast_less, 1374 simp_all add: word_bits_def pageBits_def 1375 order_less_le_trans[OF ucast_less])[1])+ 1376 apply simp 1377 apply clarsimp 1378 apply (case_tac "map_to_user_data_device psp x") 1379 apply simp 1380 apply (clarsimp simp: dom_def byte_to_word_heap_def Let_def add.assoc 1381 intro!: ext) 1382 apply (subst foo, assumption, 1383 (rule word_add_offset_less[where n=2, simplified] 1384 word_add_offset_less[where n=2 and y=0, simplified], 1385 simp_all, rule ucast_less, 1386 simp_all add: word_bits_def pageBits_def 1387 order_less_le_trans[OF ucast_less])[1])+ 1388 apply (simp add: field_simps) 1389 done 1390 1391(* FIXME: move *) 1392lemma ccorres_grab_asm: 1393 "(Q \<Longrightarrow> ccorres_underlying sr G rr xf ar ax P P' hs f g) \<Longrightarrow> 1394 ccorres_underlying sr G rr xf ar ax (P and K Q) P' hs f g" 1395 by (fastforce simp: ccorres_underlying_def) 1396 1397lemma ksPSpace_ksMSu_comm: 1398 "ksPSpace_update f (ksMachineState_update g s) = 1399 ksMachineState_update g (ksPSpace_update f s)" 1400 by simp 1401 1402lemma ksPSpace_update_ext: 1403 "(\<lambda>s. s\<lparr>ksPSpace := f (ksPSpace s)\<rparr>) = (ksPSpace_update f)" 1404 by (rule ext) simp 1405 1406(* FIXME: move *) 1407lemma valid_untyped': 1408 notes usableUntypedRange.simps[simp del] 1409 assumes pspace_distinct': "pspace_distinct' s" and 1410 pspace_aligned': "pspace_aligned' s" and 1411 al: "is_aligned ptr bits" 1412 shows "valid_untyped' d ptr bits idx s = 1413 (\<forall>p ko. ksPSpace s p = Some ko \<longrightarrow> 1414 obj_range' p ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {} \<longrightarrow> 1415 obj_range' p ko \<subseteq> {ptr..ptr + 2 ^ bits - 1} \<and> 1416 obj_range' p ko \<inter> 1417 usableUntypedRange (UntypedCap d ptr bits idx) = {})" 1418 apply (simp add: valid_untyped'_def) 1419 apply (simp add: ko_wp_at'_def) 1420 apply (rule arg_cong[where f=All]) 1421 apply (rule ext) 1422 apply (rule arg_cong[where f=All]) 1423 apply (rule ext) 1424 apply (case_tac "ksPSpace s ptr' = Some ko", simp_all) 1425 apply (frule pspace_alignedD'[OF _ pspace_aligned']) 1426 apply (frule pspace_distinctD'[OF _ pspace_distinct']) 1427 apply simp 1428 apply (frule aligned_ranges_subset_or_disjoint[OF al]) 1429 apply (fold obj_range'_def) 1430 apply (rule iffI) 1431 apply auto[1] 1432 apply (rule conjI) 1433 apply (rule ccontr, simp) 1434 apply (simp add: Set.psubset_eq) 1435 apply (erule conjE) 1436 apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp) 1437 apply (cut_tac is_aligned_no_overflow[OF al]) 1438 apply (auto simp add: obj_range'_def)[1] 1439 apply (clarsimp simp add: usableUntypedRange.simps Int_commute) 1440 apply (case_tac "obj_range' ptr' ko \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}", simp+) 1441 apply (cut_tac is_aligned_no_overflow[OF al]) 1442 apply (clarsimp simp add: obj_range'_def) 1443 apply (frule is_aligned_no_overflow) 1444 by (metis al intvl_range_conv' le_m1_iff_lt less_is_non_zero_p1 1445 nat_le_linear power_overflow sub_wrap add_0 1446 add_0_right word_add_increasing word_less_1 word_less_sub_1) 1447 1448lemma hrs_ghost_update_comm: 1449 "(t_hrs_'_update f \<circ> ghost'state_'_update g) = 1450 (ghost'state_'_update g \<circ> t_hrs_'_update f)" 1451 by (rule ext) simp 1452 1453lemma htd_safe_typ_clear_region: 1454 "htd_safe S htd \<Longrightarrow> htd_safe S (typ_clear_region ptr bits htd)" 1455 apply (clarsimp simp: htd_safe_def dom_s_def typ_clear_region_def) 1456 apply (simp add: subset_iff) 1457 apply blast 1458 done 1459 1460lemma htd_safe_typ_region_bytes: 1461 "htd_safe S htd \<Longrightarrow> {ptr ..+ 2 ^ bits} \<subseteq> S \<Longrightarrow> htd_safe S (typ_region_bytes ptr bits htd)" 1462 apply (clarsimp simp: htd_safe_def dom_s_def typ_region_bytes_def) 1463 apply (simp add: subset_iff) 1464 apply blast 1465 done 1466 1467lemma untyped_cap_rf_sr_ptr_bits_domain: 1468 "cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p s 1469 \<Longrightarrow> invs' s \<Longrightarrow> (s, s') \<in> rf_sr 1470 \<Longrightarrow> {ptr..+2 ^ bits} \<subseteq> domain" 1471 apply (clarsimp simp: cte_wp_at_ctes_of) 1472 apply (frule ctes_of_valid', clarsimp) 1473 apply (drule valid_global_refsD', clarsimp) 1474 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 1475 valid_cap'_def capAligned_def) 1476 apply (simp only: upto_intvl_eq) 1477 apply blast 1478 done 1479 1480lemma offs_in_intvl_iff: 1481 "(p + x \<in> {p ..+ n}) = (unat x < n)" 1482 apply (simp add: intvl_def, safe) 1483 apply (erule order_le_less_trans[rotated], simp add: unat_of_nat) 1484 apply (rule exI, erule conjI[rotated]) 1485 apply simp 1486 done 1487 1488lemma objBits_koTypeOf: 1489 fixes v :: "'a :: pspace_storable" shows 1490 "objBits v = objBitsT (koType TYPE('a))" 1491 using project_inject[where v=v, THEN iffD2, OF refl] 1492 project_koType[THEN iffD1, OF exI[where x=v]] 1493 by (simp add: objBits_def objBitsT_koTypeOf[symmetric]) 1494 1495lemma cmap_array_typ_region_bytes: 1496 "ptrf = (Ptr :: _ \<Rightarrow> 'b ptr) 1497 \<Longrightarrow> carray_map_relation bits' amap (h_t_valid htd c_guard) ptrf 1498 \<Longrightarrow> is_aligned ptr bits 1499 \<Longrightarrow> typ_uinfo_t TYPE('b :: c_type) \<noteq> typ_uinfo_t TYPE(8 word) 1500 \<Longrightarrow> size_of TYPE('b) = 2 ^ bits' 1501 \<Longrightarrow> objBitsT (koType TYPE('a :: pspace_storable)) \<le> bits 1502 \<Longrightarrow> objBitsT (koType TYPE('a :: pspace_storable)) \<le> bits' 1503 \<Longrightarrow> bits' < word_bits 1504 \<Longrightarrow> carray_map_relation bits' (restrict_map (amap :: _ \<Rightarrow> 'a option) (- {ptr ..+ 2 ^ bits})) 1505 (h_t_valid (typ_region_bytes ptr bits htd) c_guard) ptrf" 1506 apply (clarsimp simp: carray_map_relation_def h_t_valid_typ_region_bytes) 1507 apply (case_tac "h_t_valid htd c_guard (ptrf p)", simp_all) 1508 apply (clarsimp simp: objBits_koTypeOf) 1509 apply (drule spec, drule(1) iffD2, clarsimp) 1510 apply (rule iffI[rotated]) 1511 apply clarsimp 1512 apply (drule equals0D, erule notE, erule IntI[rotated]) 1513 apply (simp only: upto_intvl_eq is_aligned_neg_mask2 mask_in_range[symmetric]) 1514 apply (simp only: upto_intvl_eq, rule distinct_aligned_addresses_accumulate, 1515 simp_all add: upto_intvl_eq[symmetric] word_size word_bits_def) 1516 apply clarsimp 1517 apply (drule_tac x="p + (y << objBitsT (koType TYPE('a)))" in spec)+ 1518 apply (simp add: is_aligned_add[OF is_aligned_weaken is_aligned_shiftl]) 1519 apply (simp add: is_aligned_add_helper shiftl_less_t2n word_bits_def) 1520 apply clarsimp 1521 apply (drule_tac x=p in spec) 1522 apply (clarsimp simp: objBits_koTypeOf) 1523 apply auto 1524 done 1525 1526lemma map_comp_restrict_map: 1527 "(f \<circ>\<^sub>m (restrict_map m S)) = (restrict_map (f \<circ>\<^sub>m m) S)" 1528 by (rule ext, simp add: restrict_map_def map_comp_def) 1529 1530lemma size_td_uinfo_array_tag_n_m[simp]: 1531 "size_td (uinfo_array_tag_n_m (ta :: ('a :: c_type) itself) n m) 1532 = size_of (TYPE('a)) * n" 1533 apply (induct n) 1534 apply (simp add: uinfo_array_tag_n_m_def) 1535 apply (simp add: uinfo_array_tag_n_m_def size_of_def) 1536 done 1537 1538lemma modify_machinestate_assert_cnodes_swap: 1539 "do x \<leftarrow> modify (ksMachineState_update f); 1540 y \<leftarrow> stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) S) []; g od 1541 = do y \<leftarrow> stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) S) []; 1542 x \<leftarrow> modify (ksMachineState_update f); g od" 1543 by (simp add: fun_eq_iff exec_modify stateAssert_def 1544 bind_assoc exec_get assert_def) 1545 1546lemma h_t_array_valid_typ_region_bytes: 1547 "h_t_array_valid htd (p :: ('a :: c_type) ptr) n 1548 \<Longrightarrow> {ptr_val p..+n * size_of TYPE('a)} \<inter> {ptr..+2 ^ bits} = {} 1549 \<Longrightarrow> h_t_array_valid (typ_region_bytes ptr bits htd) p n" 1550 apply (clarsimp simp: h_t_array_valid_def) 1551 apply (subst valid_footprint_typ_region_bytes) 1552 apply (simp add: uinfo_array_tag_n_m_def typ_uinfo_t_def typ_info_word) 1553 apply (simp add: field_simps) 1554 done 1555 1556lemma cvariable_array_map_relation_detype: 1557 "cvariable_array_map_relation mp szs ptrfun htd 1558 \<Longrightarrow> ptrfun = (Ptr :: _ \<Rightarrow> ('a :: c_type ptr)) 1559 \<Longrightarrow> \<forall>p v. mp p = Some v \<longrightarrow> p \<notin> {ptr ..+ 2 ^ bits} 1560 \<longrightarrow> {p ..+ szs v * size_of TYPE('a)} \<inter> {ptr ..+ 2 ^ bits} = {} 1561 \<Longrightarrow> cvariable_array_map_relation (mp |` (- {ptr..+2 ^ bits})) 1562 szs ptrfun (typ_region_bytes ptr bits htd)" 1563 apply (clarsimp simp: cvariable_array_map_relation_def restrict_map_def) 1564 apply (elim allE, (drule(1) mp)+) 1565 apply (simp add: h_t_array_valid_typ_region_bytes) 1566 done 1567 1568lemma zero_ranges_are_zero_typ_region_bytes: 1569 "zero_ranges_are_zero rs hrs 1570 \<Longrightarrow> zero_ranges_are_zero rs (hrs_htd_update (typ_region_bytes ptr bits) hrs)" 1571 apply (clarsimp simp: zero_ranges_are_zero_def) 1572 apply (drule(1) bspec) 1573 apply (clarsimp simp: region_actually_is_bytes'_def typ_region_bytes_def hrs_htd_update) 1574 done 1575 1576lemma deleteObjects_ccorres': 1577 notes if_cong[cong] 1578 shows 1579 "ccorres dc xfdc 1580 (cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) p and 1581 (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and 1582 invs' and ct_active' and sch_act_simple and 1583 K ( 2 \<le> bits \<and> bits < word_bits)) 1584 UNIV hs 1585 (deleteObjects ptr bits) 1586 (Basic (\<lambda>s. globals_update 1587 (t_hrs_'_update (hrs_htd_update (typ_region_bytes ptr bits)) \<circ> 1588 ghost'state_'_update (gs_clear_region ptr bits)) s))" 1589 apply (rule ccorres_grab_asm) 1590 apply (rule ccorres_name_pre) 1591 apply (simp add: deleteObjects_def3 hrs_ghost_update_comm) 1592 apply (rule ccorres_assert) 1593 apply (rule ccorres_stateAssert_fwd) 1594 apply (subst bind_assoc[symmetric]) 1595 apply (unfold freeMemory_def) 1596 apply (subst ksPSpace_update_ext) 1597 apply (subgoal_tac "bits \<le> word_bits") 1598 prefer 2 1599 apply (clarsimp simp:cte_wp_at_ctes_of) 1600 apply (clarsimp simp: mapM_x_storeWord_step[simplified word_size_bits_def] 1601 intvl_range_conv intvl_range_conv[where 'a=32, folded word_bits_def] 1602 doMachineOp_modify modify_modify o_def ksPSpace_ksMSu_comm 1603 bind_assoc modify_machinestate_assert_cnodes_swap 1604 modify_modify_bind) 1605 apply (rule ccorres_stateAssert_fwd) 1606 apply (rule ccorres_stateAssert_after) 1607 apply (rule ccorres_from_vcg) 1608 apply (rule allI, rule conseqPre, vcg) 1609 apply (clarsimp simp: in_monad) 1610 apply (rule bexI [rotated]) 1611 apply (rule iffD2 [OF in_monad(20)]) 1612 apply (rule conjI [OF refl refl]) 1613 apply (clarsimp simp: simpler_modify_def) 1614proof - 1615 let ?mmu = "(\<lambda>h x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then 0 else h x)" 1616 let ?psu = "(\<lambda>h x. if ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1 then None else h x)" 1617 1618 fix s s' 1619 assume al: "is_aligned ptr bits" 1620 and cte: "cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d ptr bits idx) p s" 1621 and desc_range: "descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)" 1622 and invs: "invs' s" and "ct_active' s" 1623 and "sch_act_simple s" and wb: "bits < word_bits" and b2: "2 \<le> bits" 1624 and "deletionIsSafe ptr bits s" 1625 and cNodePartial: "\<not> cNodePartialOverlap (gsCNodes s) 1626 (\<lambda>x. ptr \<le> x \<and> x \<le> ptr + 2 ^ bits - 1)" 1627 and sr: "(s, s') \<in> rf_sr" 1628 and safe_asids: 1629 "ksASIDMapSafe 1630 (gsCNodes_update (\<lambda>_. ?psu (gsCNodes s)) 1631 (gsUserPages_update 1632 (\<lambda>_. ?psu (gsUserPages s)) 1633 (ksMachineState_update 1634 (underlying_memory_update ?mmu) 1635 (s\<lparr>ksPSpace := ?psu (ksPSpace s) \<rparr>))))" (is "ksASIDMapSafe ?t") 1636 1637 interpret D: delete_locale s ptr bits p 1638 apply (unfold_locales) 1639 apply fact+ 1640 done 1641 1642 1643 let ?ks = "?psu (ksPSpace s)" 1644 let ?ks' = "ksPSpace s |` (- {ptr..+2 ^ bits})" 1645 1646 have psu_restrict: "\<forall>h. ?psu h = h |` (- {ptr..+2 ^ bits})" 1647 apply (intro allI ext) 1648 apply (subst upto_intvl_eq [OF al]) 1649 apply (clarsimp) 1650 done 1651 1652 have ks': "?ks = ?ks'" by (simp add: psu_restrict) 1653 1654 let ?th = "hrs_htd_update (typ_region_bytes ptr bits)" 1655 let ?th_s = "?th (t_hrs_' (globals s'))" 1656 1657 have map_to_ctes_delete': 1658 "map_to_ctes ?ks' = ctes_of s |` (- {ptr..+2 ^ bits})" using invs 1659 apply (subst ks' [symmetric]) 1660 apply (subst map_to_ctes_delete [OF D.valid_untyped, simplified field_simps]) 1661 apply clarsimp 1662 apply (rule ext) 1663 apply (subst upto_intvl_eq [OF al]) 1664 apply clarsimp 1665 done 1666 1667 note cm_disj = cmap_relation_disjoint [OF D.valid_untyped invs, atomize] 1668 note cm_disj_tcb = cmap_relation_disjoint_tcb [OF D.valid_untyped invs] 1669 note cm_disj_cte = cmap_relation_disjoint_cte [OF D.valid_untyped invs] 1670 note cm_disj_user = cmap_relation_disjoint_user_data [OF D.valid_untyped invs] 1671 note cm_disj_device = cmap_relation_disjoint_device_data [OF D.valid_untyped invs] 1672 1673 have rl: "\<forall>(p :: word32) P. ko_wp_at' P p s \<and> 1674 (\<forall>ko. P ko \<longrightarrow> live' ko) \<longrightarrow> p \<notin> {ptr..ptr + 2 ^ bits - 1}" 1675 apply (intro allI impI conjI) 1676 apply (elim conjE) 1677 apply (erule D.live_notRange [simplified field_simps]) 1678 apply clarsimp 1679 done 1680 1681 note cmaptcb = cmap_relation_tcb [OF sr] 1682 note cmap_array_helper = arg_cong2[where f=carray_map_relation, OF refl map_comp_restrict_map] 1683 have trivia: "size_of TYPE(pte_C[256]) = 2 ^ ptBits" 1684 "size_of TYPE(pde_C[4096]) = 2 ^ pdBits" 1685 by (auto simp: ptBits_def pageBits_def pdBits_def pdeBits_def pteBits_def) 1686 note cmap_array = cmap_array_typ_region_bytes[where 'a=pte, OF refl _ al _ trivia(1)] 1687 cmap_array_typ_region_bytes[where 'a=pde, OF refl _ al _ trivia(2)] 1688 note cmap_array = cmap_array[simplified, simplified objBitsT_simps b2 1689 ptBits_def pdBits_def pageBits_def word_bits_def, simplified] 1690 1691 note pspace_distinct' = invs_pspace_distinct'[OF invs] and 1692 pspace_aligned' = invs_pspace_aligned'[OF invs] and 1693 valid_objs' = invs_valid_objs'[OF invs] and 1694 valid_untyped'_def2 = 1695 valid_untyped'[OF pspace_distinct' pspace_aligned' al] 1696 1697 have s_ksPSpace_adjust: "ksPSpace_update ?psu s = s\<lparr>ksPSpace := ?psu (ksPSpace s)\<rparr>" 1698 by simp 1699 1700 from invs have "valid_global_refs' s" by fastforce 1701 with cte 1702 have ptr_refs: "kernel_data_refs \<inter> {ptr..ptr + 2 ^ bits - 1} = {}" 1703 by (fastforce simp: valid_global_refs'_def valid_refs'_def cte_wp_at_ctes_of ran_def) 1704 1705 (* calculation starts here *) 1706 have cs: "cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) 1707 (t_hrs_' (globals s'))" 1708 using sr 1709 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 1710 hence "cpspace_relation ?ks' (underlying_memory (ksMachineState s)) ?th_s" 1711 unfolding cpspace_relation_def 1712 using cendpoint_relation_restrict [OF D.valid_untyped invs rl] 1713 cnotification_relation_restrict [OF D.valid_untyped invs rl] 1714 apply - 1715 apply (elim conjE) 1716 apply ((subst lift_t_typ_region_bytes, 1717 rule cm_disj cm_disj_tcb cm_disj_cte cm_disj_user cm_disj_device 1718 , assumption +, 1719 simp_all add: objBits_simps' archObjSize_def pageBits_def projectKOs 1720 pteBits_def pdeBits_def 1721 heap_to_user_data_restrict heap_to_device_data_restrict)[1])+ \<comment> \<open>waiting ...\<close> 1722 apply (simp add: map_to_ctes_delete' cmap_relation_restrict_both_proj 1723 cmap_relation_restrict_both cmap_array_helper hrs_htd_update 1724 ptBits_def pdBits_def pageBits_def cmap_array) 1725 apply (intro conjI) 1726 apply (frule cmap_relation_restrict_both_proj 1727 [where f = tcb_ptr_to_ctcb_ptr]) 1728 apply simp 1729 apply (erule iffD1[OF cpspace_tcb_relation_address_subset, 1730 OF D.valid_untyped invs cmaptcb]) 1731 apply (subst cmap_relation_cong [OF refl refl, 1732 where rel' = "cendpoint_relation (cslift s')"]) 1733 apply (clarsimp simp: restrict_map_Some_iff image_iff 1734 map_comp_restrict_map_Some_iff) 1735 apply (simp add: cmap_relation_restrict_both_proj) 1736 apply (subst cmap_relation_cong[OF refl refl, 1737 where rel' = "cnotification_relation (cslift s')"]) 1738 apply (clarsimp simp: restrict_map_Some_iff image_iff 1739 map_comp_restrict_map_Some_iff) 1740 apply (simp add: cmap_relation_restrict_both_proj) 1741 apply (rule cmap_array; simp add: pdeBits_def) 1742 apply (rule cmap_array; simp add: pteBits_def) 1743 done 1744 moreover 1745 from invs have "valid_queues s" .. 1746 hence "\<And>p. \<forall>t \<in> set (ksReadyQueues s p). tcb_at' t s \<and> ko_wp_at' live' t s" 1747 apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def) 1748 apply (drule spec, drule spec) 1749 apply clarsimp 1750 apply (drule (1) bspec) 1751 apply (rule conjI) 1752 apply (erule obj_at'_weakenE) 1753 apply simp 1754 apply (simp add: obj_at'_real_def) 1755 apply (erule ko_wp_at'_weakenE) 1756 apply (clarsimp simp: projectKOs inQ_def) 1757 done 1758 hence tat: "\<And>p. \<forall>t \<in> set (ksReadyQueues s p). tcb_at' t s" 1759 and tlive: "\<And>p. \<forall>t \<in> set (ksReadyQueues s p). ko_wp_at' live' t s" 1760 by auto 1761 from sr have 1762 "cready_queues_relation (clift ?th_s) 1763 (ksReadyQueues_' (globals s')) (ksReadyQueues s)" 1764 unfolding cready_queues_relation_def rf_sr_def cstate_relation_def 1765 cpspace_relation_def 1766 apply (clarsimp simp: Let_def all_conj_distrib) 1767 apply (drule spec, drule spec, drule mp) 1768 apply fastforce 1769 apply ((subst lift_t_typ_region_bytes, rule cm_disj_tcb, assumption+, 1770 simp_all add: objBits_simps archObjSize_def pageBits_def projectKOs)[1])+ 1771 \<comment> \<open>waiting ...\<close> 1772 apply (simp add: tcb_queue_relation_live_restrict 1773 [OF D.valid_untyped tat tlive rl]) 1774 done 1775 1776 moreover 1777 1778 { assume asid_map: 1779 "asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) = 1780 set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot)" 1781 1782 hence asid: 1783 "\<And>p pd_ptr pde. \<lbrakk> cslift s' (pde_Ptr p) = Some pde; 1784 pd_pointer_to_asid_slot pd_ptr = Some (pde_Ptr p); 1785 pde_stored_asid pde \<noteq> None \<rbrakk> \<Longrightarrow> 1786 \<exists>asid. (asid, pd_ptr) \<in> ran (armKSASIDMap (ksArchState s))" 1787 apply - 1788 apply (drule_tac x=pd_ptr in fun_cong) 1789 apply (clarsimp simp: map_comp_def) 1790 apply (clarsimp simp: asid_map_pd_to_hwasids_def) 1791 apply (drule equalityD2) 1792 apply fastforce 1793 done 1794 1795 from safe_asids 1796 have pds: 1797 "\<And>p asid pd_ptr. armKSASIDMap (ksArchState (s\<lparr>ksPSpace := ?ks\<rparr>)) p = 1798 Some (asid, pd_ptr) \<Longrightarrow> 1799 page_directory_at' pd_ptr (s\<lparr>ksPSpace := ?ks\<rparr>)" 1800 by (clarsimp simp: ksASIDMapSafe_def) 1801 1802 from cs 1803 have clift: 1804 "\<And>p. clift (hrs_htd_update (typ_region_bytes ptr bits) 1805 (t_hrs_' (globals s'))) (p::pde_C ptr) = 1806 (if p \<in> pde_Ptr ` {ptr..+2 ^ bits} then None else cslift s' p)" 1807 apply (subst lift_t_typ_region_bytes[OF cm_disj], simp_all) 1808 apply (fastforce simp: cpspace_relation_def) 1809 apply (simp add: projectKOs) 1810 apply (simp add: objBits_simps archObjSize_def pdeBits_def) 1811 done 1812 1813 have "set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot) = 1814 set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift ?th_s \<circ>\<^sub>m 1815 pd_pointer_to_asid_slot)" 1816 apply - 1817 apply (rule ext) 1818 apply (rename_tac pd_ptr) 1819 apply (clarsimp simp: map_comp_def) 1820 apply (simp add: clift split: option.splits) 1821 apply clarsimp 1822 apply (rule ccontr) 1823 apply (drule (2) asid) 1824 apply (clarsimp simp: ran_def pd_pointer_to_asid_slot_def split: if_split_asm) 1825 apply (subgoal_tac "armKSASIDMap (ksArchState (s\<lparr>ksPSpace := ?ks\<rparr>)) a = Some (asid, pd_ptr)") 1826 prefer 2 1827 apply simp 1828 apply (drule pds) 1829 apply (subgoal_tac "pde_at' (pd_ptr + 0x3FC0) (s\<lparr>ksPSpace := ?ks\<rparr>)") 1830 apply (cut_tac p="pd_ptr + 0x3FC0" in D.typ_at' [of "ArchT PDET", simplified field_simps]) 1831 apply (simp add: upto_intvl_eq [OF al]) 1832 apply (clarsimp simp: page_directory_at'_def) 1833 apply (erule_tac x="0xFF0" in allE) 1834 apply simp 1835 done 1836 } 1837 moreover 1838 { 1839 assume "s' \<Turnstile>\<^sub>c (Ptr::(32 word \<Rightarrow> (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD'')" 1840 moreover 1841 from sr ptr_refs have "ptr_span (pd_Ptr (symbol_table ''armKSGlobalPD'')) 1842 \<inter> {ptr..ptr + 2 ^ bits - 1} = {}" 1843 by (fastforce simp: rf_sr_def cstate_relation_def Let_def) 1844 ultimately 1845 have "hrs_htd (hrs_htd_update (typ_region_bytes ptr bits) (t_hrs_' (globals s'))) 1846 \<Turnstile>\<^sub>t (Ptr::(32 word \<Rightarrow> (pde_C[4096]) ptr)) (symbol_table ''armKSGlobalPD'')" 1847 using al wb 1848 apply (cases "t_hrs_' (globals s')") 1849 apply (simp add: hrs_htd_update_def hrs_htd_def h_t_valid_typ_region_bytes upto_intvl_eq) 1850 done 1851 } 1852 1853 moreover 1854 have h2ud_eq: 1855 "heap_to_user_data (?psu (ksPSpace s)) 1856 (?mmu (underlying_memory (ksMachineState s))) = 1857 heap_to_user_data (?psu (ksPSpace s)) 1858 (underlying_memory (ksMachineState s))" 1859 apply (subst heap_to_user_data_update_region 1860 [where S="{ptr..ptr + 2 ^ bits - 1}", simplified]) 1861 prefer 2 1862 apply (rule ext) 1863 apply clarsimp 1864 apply (simp add: map_option_def map_comp_def 1865 split: if_split_asm option.splits) 1866 apply (frule pspace_alignedD'[OF _ pspace_aligned']) 1867 apply (case_tac "pageBits \<le> bits") 1868 apply (simp add: objBitsKO_def projectKOs split: kernel_object.splits) 1869 apply clarsimp 1870 apply (rule aligned_range_offset_mem 1871 [where 'a=32, folded word_bits_def, simplified, OF _ _ al _ wb]) 1872 apply assumption+ 1873 apply (rule iffI[rotated], simp) 1874 apply (simp add: objBits_simps projectKOs) 1875 apply (rule FalseE) 1876 apply (case_tac "ptr \<le> x", simp) 1877 apply clarsimp 1878 apply (frule_tac y="ptr + 2 ^ bits - 1" in le_less_trans) 1879 apply (simp only: not_le) 1880 apply (drule (1) is_aligned_no_wrap') 1881 apply simp 1882 apply (cut_tac cte[simplified cte_wp_at_ctes_of]) 1883 apply clarsimp 1884 apply (frule ctes_of_valid'[OF _ valid_objs']) 1885 apply (frule pspace_distinctD'[OF _ pspace_distinct']) 1886 apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def) 1887 apply (drule_tac x=x in spec) 1888 apply (simp add: obj_range'_def objBitsKO_def) 1889 apply (simp only: not_le) 1890 apply (cut_tac is_aligned_no_overflow[OF al]) 1891 apply (case_tac "ptr \<le> x + 2 ^ pageBits - 1", 1892 simp_all only: simp_thms not_le) 1893 apply clarsimp 1894 apply (thin_tac "psp = Some ko" for psp ko)+ 1895 apply (thin_tac "ps_clear x y z" for x y z) 1896 apply (thin_tac "cteCap x = y" for x y)+ 1897 apply (frule is_aligned_no_overflow) 1898 apply (simp only: x_power_minus_1) 1899 apply (frule_tac x=x in word_plus_strict_mono_right[of _ "2^pageBits"]) 1900 apply (rule ccontr) 1901 apply (simp only: not_le) 1902 apply (frule_tac y="x" in less_le_trans, assumption) 1903 apply (simp add: field_simps word_sub_less_iff) 1904 apply simp 1905 done 1906 moreover 1907 have h2dd_eq: 1908 "heap_to_device_data (?psu (ksPSpace s)) 1909 (?mmu (underlying_memory (ksMachineState s))) = 1910 heap_to_device_data (?psu (ksPSpace s)) 1911 (underlying_memory (ksMachineState s))" 1912 apply (subst heap_to_device_data_update_region 1913 [where S="{ptr..ptr + 2 ^ bits - 1}", simplified]) 1914 prefer 2 1915 apply (rule ext) 1916 apply clarsimp 1917 apply (simp add: map_option_def map_comp_def 1918 split: if_split_asm option.splits) 1919 apply (frule pspace_alignedD'[OF _ pspace_aligned']) 1920 apply (case_tac "pageBits \<le> bits") 1921 apply (simp add: objBitsKO_def projectKOs split: kernel_object.splits) 1922 apply clarsimp 1923 apply (rule aligned_range_offset_mem 1924 [where 'a=32, folded word_bits_def, simplified, OF _ _ al _ wb]) 1925 apply assumption+ 1926 apply (rule iffI[rotated], simp) 1927 apply (simp add: objBits_simps projectKOs) 1928 apply (rule FalseE) 1929 apply (case_tac "ptr \<le> x", simp) 1930 apply clarsimp 1931 apply (frule_tac y="ptr + 2 ^ bits - 1" in le_less_trans) 1932 apply (simp only: not_le) 1933 apply (drule (1) is_aligned_no_wrap') 1934 apply simp 1935 apply (cut_tac cte[simplified cte_wp_at_ctes_of]) 1936 apply clarsimp 1937 apply (frule ctes_of_valid'[OF _ valid_objs']) 1938 apply (frule pspace_distinctD'[OF _ pspace_distinct']) 1939 apply (clarsimp simp add: valid_cap'_def valid_untyped'_def2 capAligned_def) 1940 apply (drule_tac x=x in spec) 1941 apply (simp add: obj_range'_def objBitsKO_def) 1942 apply (simp only: not_le) 1943 apply (cut_tac is_aligned_no_overflow[OF al]) 1944 apply (case_tac "ptr \<le> x + 2 ^ pageBits - 1", 1945 simp_all only: simp_thms not_le) 1946 apply clarsimp 1947 apply (thin_tac "psp = Some ko" for psp ko)+ 1948 apply (thin_tac "ps_clear x y z" for x y z) 1949 apply (thin_tac "cteCap x = y" for x y)+ 1950 apply (frule is_aligned_no_overflow) 1951 apply (simp only: x_power_minus_1) 1952 apply (frule_tac x=x in word_plus_strict_mono_right[of _ "2^pageBits"]) 1953 apply (rule ccontr) 1954 apply (simp only: not_le) 1955 apply (frule_tac y="x" in less_le_trans, assumption) 1956 apply (simp add: field_simps word_sub_less_iff) 1957 apply simp 1958 done 1959 1960 moreover { 1961 from D.valid_untyped invs have tcb_no_overlap: 1962 "\<And>p v. map_to_tcbs (ksPSpace s) p = Some v 1963 \<Longrightarrow> p \<notin> {ptr..+2 ^ bits} 1964 \<Longrightarrow> {p ..+ 2 ^ objBitsT TCBT} \<inter> {ptr..+2 ^ bits} = {}" 1965 apply (clarsimp simp: valid_cap'_def) 1966 apply (drule(1) map_to_ko_atI') 1967 apply (clarsimp simp: obj_at'_def valid_untyped'_def2) 1968 apply (elim allE, drule(1) mp) 1969 apply (clarsimp simp only: obj_range'_def upto_intvl_eq[symmetric] al) 1970 apply (subgoal_tac "objBitsKO ko = objBitsT TCBT") 1971 apply (subgoal_tac "p \<in> {p ..+ 2 ^ objBitsT TCBT}") 1972 apply simp 1973 apply blast 1974 apply (simp add: upto_intvl_eq) 1975 apply (clarsimp simp: objBits_simps projectKOs objBitsT_simps) 1976 done 1977 1978 note upto_rew = upto_intvl_eq[OF al, THEN eqset_imp_iff, symmetric, simplified] 1979 1980 from cNodePartial[simplified upto_rew] have cn_no_overlap: 1981 "\<And>p n. gsCNodes s p = Some n \<Longrightarrow> p \<notin> {ptr..+2 ^ bits} 1982 \<Longrightarrow> {p ..+ 2 ^ (n + cte_level_bits)} \<inter> {ptr..+2 ^ bits} = {}" 1983 apply (simp add: cNodePartialOverlap_def) 1984 apply (elim allE, drule(1) mp) 1985 apply clarsimp 1986 apply (frule base_member_set, simp add: word_bits_def) 1987 apply (clarsimp simp only: upto_intvl_eq[symmetric] field_simps) 1988 apply blast 1989 done 1990 1991 from sr have "cvariable_array_map_relation (gsCNodes s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) ((^) 2) cte_Ptr 1992 (typ_region_bytes ptr bits (hrs_htd (t_hrs_' (globals s'))))" 1993 "cvariable_array_map_relation (map_to_tcbs (ksPSpace s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>)) (\<lambda>x. 5) cte_Ptr 1994 (typ_region_bytes ptr bits (hrs_htd (t_hrs_' (globals s'))))" 1995 apply (simp_all add: map_comp_restrict_map rf_sr_def cstate_relation_def Let_def) 1996 apply (rule cvariable_array_map_relation_detype, clarsimp+) 1997 apply (drule(1) cn_no_overlap) 1998 apply (simp add: cte_level_bits_def power_add) 1999 apply (rule cvariable_array_map_relation_detype, clarsimp+) 2000 apply (drule(1) tcb_no_overlap) 2001 apply (erule disjoint_subset[rotated]) 2002 apply (rule intvl_start_le) 2003 apply (simp add: objBitsT_simps objBits_defs) 2004 done 2005 } 2006 2007 moreover from sr 2008 have "apsnd fst (gs_clear_region ptr bits (ghost'state_' (globals s'))) = 2009 (gsUserPages s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>, gsCNodes s|\<^bsub>(- {ptr..+2 ^ bits})\<^esub>) 2010 \<and> ghost_size_rel (gs_clear_region ptr bits (ghost'state_' (globals s'))) 2011 (gsMaxObjectSize s)" 2012 apply (case_tac "ghost'state_' (globals s')") 2013 apply (simp add: rf_sr_def cstate_relation_def Let_def gs_clear_region_def 2014 upto_intvl_eq[OF al] carch_state_relation_def 2015 cmachine_state_relation_def ghost_size_rel_def 2016 ghost_assertion_data_get_def restrict_map_def 2017 if_flip[symmetric, where F=None]) 2018 done 2019 2020 moreover from sr have 2021 "h_t_valid (typ_region_bytes ptr bits (hrs_htd (t_hrs_' (globals s')))) 2022 c_guard (ptr_coerce (intStateIRQNode_' (globals s')) :: (cte_C[256]) ptr)" 2023 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 2024 apply (simp add: h_t_valid_typ_region_bytes) 2025 apply (simp add: upto_intvl_eq al) 2026 apply (rule disjoint_subset[OF _ ptr_refs]) 2027 apply (simp add: cinterrupt_relation_def cte_level_bits_def) 2028 done 2029 2030 ultimately 2031 show "(?t, globals_update 2032 (%x. ghost'state_'_update (gs_clear_region ptr bits) 2033 (t_hrs_'_update ?th x)) s') \<in> rf_sr" 2034 using sr untyped_cap_rf_sr_ptr_bits_domain[OF cte invs sr] 2035 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2036 psu_restrict cpspace_relation_def 2037 carch_state_relation_def cmachine_state_relation_def 2038 hrs_htd_update htd_safe_typ_region_bytes 2039 zero_ranges_are_zero_typ_region_bytes) 2040qed 2041 2042abbreviation (input) 2043 "global_htd_update f == Guard MemorySafety \<lbrace>htd_safe domain (hrs_htd \<acute>t_hrs) 2044 \<and> htd_safe domain (\<acute>(\<lambda>s. f s) (hrs_htd \<acute>t_hrs))\<rbrace> 2045 (Basic (\<lambda>s. globals_update (t_hrs_'_update (hrs_htd_update (f s))) s))" 2046 2047lemma kernel_data_refs_domain_eq_rotate: 2048 "(kernel_data_refs = - domain) = (domain = - kernel_data_refs)" 2049 by blast 2050 2051lemma deleteObjects_ccorres[corres]: 2052 "ccorres dc xfdc 2053 (cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d ptr bits idx) p and 2054 (\<lambda>s. descendants_range' (UntypedCap d ptr bits idx) p (ctes_of s)) and 2055 invs' and ct_active' and sch_act_simple and 2056 K ( 2 \<le> bits \<and> bits < word_bits)) 2057 UNIV hs 2058 (deleteObjects ptr bits) 2059 (Seq (global_htd_update (\<lambda>_. typ_region_bytes ptr bits)) 2060 (Basic (\<lambda>s. globals_update 2061 (ghost'state_'_update (gs_clear_region ptr bits)) s)))" 2062 apply (rule ccorres_guard_imp2) 2063 apply (rule ccorres_Guard_Seq) 2064 apply (rule Corres_UL_C.ccorres_exec_cong 2065 [THEN iffD2, OF _ deleteObjects_ccorres'[where idx=idx and p=p and d=d]]) 2066 apply (simp add: exec_Basic_Seq_Basic o_def 2067 hrs_ghost_update_comm[simplified o_def]) 2068 apply clarsimp 2069 apply (frule(2) untyped_cap_rf_sr_ptr_bits_domain) 2070 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2071 kernel_data_refs_domain_eq_rotate htd_safe_typ_region_bytes 2072 untyped_cap_rf_sr_ptr_bits_domain) 2073 2074end 2075end 2076