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 ArchKHeap_AI 12imports "../KHeapPre_AI" 13begin 14 15context Arch begin global_naming ARM 16 17fun 18 non_vspace_obj :: "kernel_object \<Rightarrow> bool" 19where 20 "non_vspace_obj (ArchObj _) = False" 21| "non_vspace_obj _ = True" 22 23lemma obj_at_split: "(obj_at (P xo) p s \<and> (Q xo)) = obj_at (\<lambda>ko. P xo ko \<and> Q xo) p s" 24 by (auto simp: obj_at_def) 25 26lemma valid_vspace_objs_lift: 27 assumes x: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>" 28 assumes y: "\<And>ako p. \<lbrace>\<lambda>s. \<not> ko_at (ArchObj ako) p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not> ko_at (ArchObj ako) p s\<rbrace>" 29 assumes z: "\<And>p T. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>" 30 shows "\<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" 31 apply (simp add: valid_vspace_objs_def) 32 apply (rule hoare_vcg_all_lift, wp hoare_convert_imp[OF x]; (rule hoare_vcg_all_lift | assumption)) 33 apply (rule hoare_convert_imp[OF y]) 34 apply (rule valid_vspace_obj_typ[OF z]) 35 done 36 37lemma vspace_obj_imp: "non_arch_obj ko \<Longrightarrow> non_vspace_obj ko" 38 apply (cases ko; clarsimp) 39 apply (rename_tac ako) 40 apply (case_tac ako, auto simp: non_arch_obj_def) 41 done 42 43lemma non_vspace_objs[intro]: 44 "non_vspace_obj (Endpoint ep)" 45 "non_vspace_obj (CNode sz cnode_contents)" 46 "non_vspace_obj (TCB tcb)" 47 "non_vspace_obj (Notification notification)" 48 by (auto) 49 50definition vspace_obj_pred :: "(kernel_object \<Rightarrow> bool) \<Rightarrow> bool" where 51 "vspace_obj_pred P \<equiv> 52 \<forall>ko ko'. non_vspace_obj ko \<longrightarrow> non_vspace_obj ko' \<longrightarrow> 53 P ko = P ko'" 54 55lemma vspace_obj_predE: 56 "\<lbrakk>vspace_obj_pred P; non_vspace_obj ko; non_vspace_obj ko'\<rbrakk> \<Longrightarrow> P ko = P ko'" 57 apply (unfold vspace_obj_pred_def) 58 apply (erule allE[where ?x="ko"]) 59 apply (erule allE[where ?x="ko'"]) 60 by blast 61 62lemmas vspace_obj_pred_defs = non_vspace_objs vspace_obj_pred_def 63 64lemma vspace_pred_imp: "vspace_obj_pred P \<Longrightarrow> arch_obj_pred P" 65 apply (clarsimp simp: arch_obj_pred_def) 66 apply (rule vspace_obj_predE) 67 apply simp 68 apply (rule vspace_obj_imp, assumption)+ 69 done 70 71lemma vspace_obj_pred_a_type[intro, simp]: "vspace_obj_pred (\<lambda>ko. a_type ko = AArch T)" 72 by (auto simp add: vspace_obj_pred_defs a_type_def 73 split: kernel_object.splits arch_kernel_obj.splits) 74 75lemma 76 vspace_obj_pred_arch_obj_l[intro, simp]: 77 "vspace_obj_pred (\<lambda>ko. ArchObj ako = ko)" and 78 vspace_obj_pred_arch_obj_r[intro, simp]: 79 "vspace_obj_pred (\<lambda>ko. ko = ArchObj ako)" 80 apply (simp add: vspace_obj_pred_defs) 81 apply (rule allI[OF impI[OF allI[OF impI]]]) 82 apply (auto simp add: vspace_obj_pred_defs 83 split: kernel_object.splits arch_kernel_obj.splits) 84done 85 86lemma vspace_obj_pred_fun_lift: "vspace_obj_pred (\<lambda>ko. F (vspace_obj_fun_lift P N ko))" 87 by (auto simp: vspace_obj_pred_defs vspace_obj_fun_lift_def 88 split: kernel_object.splits arch_kernel_obj.splits) 89 90lemmas vspace_obj_pred_fun_lift_id[simp] 91 = vspace_obj_pred_fun_lift[where F=id, simplified] 92 93lemmas vspace_obj_pred_fun_lift_k[intro] 94 = vspace_obj_pred_fun_lift[where F="K R" for R, simplified] 95 96lemmas vspace_obj_pred_fun_lift_el[simp] 97 = vspace_obj_pred_fun_lift[where F="\<lambda> S. x \<in> S" for x, simplified] 98 99lemma vspace_obj_pred_const_conjI[intro]: 100 "vspace_obj_pred P \<Longrightarrow> 101 vspace_obj_pred P' \<Longrightarrow> 102 vspace_obj_pred (\<lambda>ko. P ko \<and> P' ko)" 103 apply (simp only: vspace_obj_pred_def) 104 apply blast 105 done 106 107lemma vspace_obj_pred_fI: 108 "(\<And>x. vspace_obj_pred (P x)) \<Longrightarrow> vspace_obj_pred (\<lambda>ko. f (\<lambda>x :: 'a :: type. P x ko))" 109 apply (simp only: vspace_obj_pred_def) 110 apply (intro allI impI) 111 apply (rule arg_cong[where f=f]) 112 by blast 113 114declare 115 vspace_obj_pred_fI[where f=All, intro] 116 vspace_obj_pred_fI[where f=Ex, intro] 117 118end 119 120locale vspace_only_obj_pred = Arch + 121 fixes P :: "kernel_object \<Rightarrow> bool" 122 assumes vspace_only: "vspace_obj_pred P" 123 124sublocale vspace_only_obj_pred < arch_only_obj_pred 125 using vspace_pred_imp[OF vspace_only] by unfold_locales 126 127context Arch begin global_naming ARM 128 129sublocale empty_table: vspace_only_obj_pred "empty_table S" for S 130 by unfold_locales (clarsimp simp: vspace_obj_pred_def empty_table_def 131 split: arch_kernel_obj.splits kernel_object.splits) 132 133sublocale vs_refs: vspace_only_obj_pred "\<lambda>ko. x \<in> vs_refs ko" 134 by unfold_locales (clarsimp simp: vspace_obj_pred_def vs_refs_def 135 split: arch_kernel_obj.splits kernel_object.splits) 136 137sublocale vs_refs_pages: vspace_only_obj_pred "\<lambda>ko. x \<in> vs_refs_pages ko" 138 by unfold_locales (clarsimp simp: vspace_obj_pred_def vs_refs_pages_def 139 split: arch_kernel_obj.split kernel_object.splits) 140 141lemma pspace_in_kernel_window_atyp_lift_strong: 142 assumes atyp_inv: "\<And>P p T. \<lbrace> \<lambda>s. P (typ_at T p s) \<rbrace> f \<lbrace> \<lambda>rv s. P (typ_at T p s) \<rbrace>" 143 assumes arch_inv: "\<And>P. \<lbrace>\<lambda>s. P (arm_kernel_vspace (arch_state s))\<rbrace> f \<lbrace>\<lambda>r s. P (arm_kernel_vspace (arch_state s))\<rbrace>" 144 shows "\<lbrace>\<lambda>s. pspace_in_kernel_window s\<rbrace> f \<lbrace>\<lambda>rv s. pspace_in_kernel_window s\<rbrace>" 145 apply (simp add: pspace_in_kernel_window_def) 146 apply (rule hoare_lift_Pf[where f="\<lambda>s. arm_kernel_vspace (arch_state s)", OF _ arch_inv]) 147 apply (rule hoare_vcg_all_lift) 148 apply (simp add: obj_bits_T) 149 apply (simp add: valid_def) 150 apply clarsimp 151 subgoal for _ x s _ _ ko 152 apply (cases "kheap s x") 153 apply (frule use_valid[OF _ atyp_inv, where P1= "\<lambda>x. \<not> x" and T1="a_type ko" and p1=x]; 154 simp add: obj_at_def a_type_def) 155 156 subgoal for ko' 157 apply (drule spec[of _ ko']) 158 apply (simp add: obj_bits_T) 159 apply (frule use_valid[OF _ atyp_inv, where P1= "\<lambda>x. x" and T1="a_type ko'" and p1=x]) 160 by (simp add: obj_at_def a_type_def)+ 161 done 162 done 163 164lemma pspace_in_kernel_window_atyp_lift: 165 assumes atyp_inv: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>" 166 assumes arch_inv: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>" 167 shows "\<lbrace>\<lambda>s. pspace_in_kernel_window s\<rbrace> f \<lbrace>\<lambda>rv s. pspace_in_kernel_window s\<rbrace>" 168 by (rule pspace_in_kernel_window_atyp_lift_strong[OF atyp_inv arch_inv]) 169 170lemma cap_refs_in_kernel_window_arch_update[simp]: 171 "arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s) 172 \<Longrightarrow> cap_refs_in_kernel_window (arch_state_update f s) = cap_refs_in_kernel_window s" 173 by (simp add: cap_refs_in_kernel_window_def) 174 175lemma 176 ex_ko_at_def2: 177 "(\<exists>ko. ko_at ko p s \<and> P ko) = (obj_at P p s)" 178 by (simp add: obj_at_def) 179 180lemma in_user_frame_obj_pred_lift: 181 assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow> 182 \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>" 183 shows "\<lbrace>in_user_frame p\<rbrace> f \<lbrace>\<lambda>_. in_user_frame p\<rbrace>" 184 unfolding in_user_frame_def 185 apply (wp hoare_vcg_ex_lift obj_at) 186 apply (clarsimp simp: vspace_obj_pred_def) 187 apply (auto simp: a_type_def aa_type_def split: kernel_object.splits arch_kernel_obj.splits) 188 done 189 190lemma vs_lookup_arch_obj_at_lift: 191 assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow> 192 \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>" 193 assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>" 194 shows "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup s)\<rbrace>" 195 apply (simp add: vs_lookup_def vs_lookup1_def) 196 apply (simp add: ex_ko_at_def2) 197 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state]) 198 apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P']) 199 apply (rule hoare_vcg_prop) 200 apply (clarsimp simp add: valid_def) 201 apply (erule_tac P=P in rsubst) 202 apply (rule ext)+ 203 apply (erule use_valid, rule obj_at, simp) 204 by (auto simp: vs_refs.arch_only 205 intro!: arch_obj_pred_fI[where f=Ex]) 206 207lemma vs_lookup_vspace_obj_at_lift: 208 assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow> 209 \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>" 210 assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>" 211 shows "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup s)\<rbrace>" 212 apply (simp add: vs_lookup_def vs_lookup1_def) 213 apply (simp add: ex_ko_at_def2) 214 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state]) 215 apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P']) 216 apply (rule hoare_vcg_prop) 217 apply (clarsimp simp add: valid_def) 218 apply (erule_tac P=P in rsubst) 219 apply (rule ext)+ 220 apply (erule use_valid, rule obj_at, simp) 221 by (auto simp: vs_refs.vspace_only 222 intro!: vspace_obj_pred_fI[where f=Ex]) 223 224lemma vs_lookup_pages_arch_obj_at_lift: 225 assumes obj_at: "\<And>P P' p. arch_obj_pred P' \<Longrightarrow> 226 \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>" 227 assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>" 228 shows "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup_pages s)\<rbrace>" 229 apply (simp add: vs_lookup_pages_def vs_lookup_pages1_def) 230 apply (simp add: ex_ko_at_def2) 231 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state]) 232 apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P']) 233 apply (rule hoare_vcg_prop) 234 apply (clarsimp simp add: valid_def) 235 apply (erule_tac P=P in rsubst) 236 apply (rule ext)+ 237 apply (erule use_valid, rule obj_at, simp) 238 by (auto simp: vs_refs_pages.arch_only 239 intro!: arch_obj_pred_fI[where f=Ex]) 240 241lemma vs_lookup_pages_vspace_obj_at_lift: 242 assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow> 243 \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>" 244 assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>" 245 shows "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>rv s. P (vs_lookup_pages s)\<rbrace>" 246 apply (simp add: vs_lookup_pages_def vs_lookup_pages1_def) 247 apply (simp add: ex_ko_at_def2) 248 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch_state]) 249 apply (rule hoare_lift_Pf[where f="\<lambda>s rs p rs' p'. obj_at (P' p rs rs' p') p s" for P']) 250 apply (rule hoare_vcg_prop) 251 apply (clarsimp simp add: valid_def) 252 apply (erule_tac P=P in rsubst) 253 apply (rule ext)+ 254 apply (erule use_valid, rule obj_at, simp) 255 by (auto simp: vs_refs_pages.vspace_only 256 intro!: vspace_obj_pred_fI[where f=Ex]) 257 258lemma valid_vspace_objs_lift_weak: 259 assumes obj_at: "\<And>P P' p. vspace_obj_pred P' \<Longrightarrow> 260 \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' p s)\<rbrace>" 261 assumes arch_state: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (arch_state s)\<rbrace>" 262 shows "\<lbrace>valid_vspace_objs\<rbrace> f \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 263 apply (rule valid_vspace_objs_lift) 264 apply (rule vs_lookup_vspace_obj_at_lift) 265 apply (rule obj_at arch_state vspace_pred_imp; simp)+ 266 done 267 268lemma set_object_neg_lookup: 269 "\<lbrace>\<lambda>s. \<not> (\<exists>rs. (rs \<rhd> p') s) \<and> obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p s \<rbrace> 270 set_object p ko 271 \<lbrace>\<lambda>_ s. \<not> (\<exists>rs. (rs \<rhd> p') s)\<rbrace>" 272 apply (simp add: set_object_def) 273 apply wp 274 apply clarsimp 275 apply (erule_tac x=rs in allE) 276 apply (erule notE) 277 apply (erule vs_lookup_stateI) 278 apply (clarsimp simp: obj_at_def split: if_split_asm) 279 apply simp 280 done 281 282lemma set_object_vs_lookup: 283 "\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs ko = vs_refs ko') p s \<and> P (vs_lookup s) \<rbrace> 284 set_object p ko 285 \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>" 286 apply (simp add: set_object_def) 287 apply wp 288 apply clarsimp 289 apply (erule rsubst [where P=P]) 290 apply (rule order_antisym) 291 apply (rule vs_lookup_sub) 292 apply (clarsimp simp: obj_at_def) 293 apply simp 294 apply (rule vs_lookup_sub) 295 apply (clarsimp simp: obj_at_def split: if_split_asm) 296 apply simp 297 done 298 299lemma set_object_pt_not_vs_lookup_pages: 300 "\<lbrace>\<lambda>s. \<not>(ref \<unrhd> p') s 301 \<and> ((\<exists>\<unrhd>p) s \<longrightarrow> (\<forall>x. case pte_ref_pages (pt x) of 302 Some ptr \<Rightarrow> 303 obj_at (\<lambda>ko. vs_refs_pages ko = {}) ptr s \<and> 304 ptr \<noteq> p' 305 | None \<Rightarrow> True))\<rbrace> 306 set_object p (ArchObj (PageTable pt)) 307 \<lbrace>\<lambda>_ s. \<not>(ref \<unrhd> p') s\<rbrace>" 308 apply (simp add: set_object_def) 309 apply wp 310 apply (clarsimp simp: obj_at_def) 311 apply (case_tac "(\<exists>\<unrhd>p) s") 312 apply (erule notE) 313 apply clarsimp 314 apply (subst (asm) vs_lookup_pages_def) 315 apply clarsimp 316 apply (erule vs_lookup_pagesI) 317 apply (erule converse_rtrancl_induct) 318 apply simp 319 apply (drule vs_lookup_pages1D) 320 apply (clarsimp simp: obj_at_def split:if_split_asm) 321 apply (case_tac "pa=p") 322 apply (clarsimp simp: vs_refs_pages_def graph_of_def) 323 apply (erule_tac x=ab in allE) 324 apply (drule_tac R="vs_lookup_pages1 s" in rtranclD) 325 apply clarsimp 326 apply (drule tranclD) 327 apply clarsimp 328 apply (drule vs_lookup_pages1D) 329 apply (clarsimp simp: obj_at_def vs_refs_pages_def) 330 apply clarsimp 331 apply (erule rtrancl_trans[OF r_into_rtrancl, rotated]) 332 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 333 apply clarsimp 334 apply (erule notE) 335 apply (subst (asm) vs_lookup_pages_def) 336 apply clarsimp 337 apply (rule vs_lookup_pagesI, assumption) 338 apply (erule rtrancl_induct) 339 apply simp 340 apply (drule vs_lookup_pages1D) 341 apply (clarsimp simp: obj_at_def split:if_split_asm) 342 apply (case_tac "pa=p") 343 apply (clarsimp simp: vs_refs_pages_def graph_of_def) 344 apply (erule_tac x=rs in allE) 345 apply (clarsimp simp: vs_lookup_pages_def) 346 apply (drule(1) ImageI, erule (1) notE) 347 apply clarsimp 348 apply (erule rtrancl_trans[OF _ r_into_rtrancl]) 349 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 350 done 351 352 353lemma set_object_vs_lookup_pages: 354 "\<lbrace>\<lambda>s. obj_at (\<lambda>ko'. vs_refs_pages ko = vs_refs_pages ko') p s \<and> P (vs_lookup_pages s) \<rbrace> 355 set_object p ko 356 \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>" 357 apply (simp add: set_object_def) 358 apply wp 359 apply clarsimp 360 apply (erule rsubst [where P=P]) 361 apply (rule order_antisym) 362 apply (rule vs_lookup_pages_sub) 363 apply (clarsimp simp: obj_at_def) 364 apply simp 365 apply (rule vs_lookup_pages_sub) 366 apply (clarsimp simp: obj_at_def split: if_split_asm) 367 apply simp 368 done 369 370 371lemma set_object_atyp_at: 372 "\<lbrace>\<lambda>s. typ_at (AArch (aa_type ako)) p s \<and> P (typ_at (AArch T) p' s)\<rbrace> 373 set_object p (ArchObj ako) 374 \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p' s)\<rbrace>" 375 apply (simp add: set_object_def) 376 apply wp 377 apply clarsimp 378 apply (erule rsubst [where P=P]) 379 apply (clarsimp simp: obj_at_def a_type_aa_type) 380 done 381 382lemma set_object_vspace_objs: 383 "\<lbrace>valid_vspace_objs and typ_at (a_type ko) p and 384 obj_at (\<lambda>ko'. vs_refs ko \<subseteq> vs_refs ko') p and 385 (\<lambda>s. case ko of ArchObj ao \<Rightarrow> 386 (\<exists>\<rhd>p)s \<longrightarrow> valid_vspace_obj ao s 387 | _ \<Rightarrow> True)\<rbrace> 388 set_object p ko 389 \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 390 apply (simp add: valid_vspace_objs_def) 391 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) 392 apply (subst imp_conv_disj) 393 apply (subst imp_conv_disj) 394 apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift set_object_neg_lookup set_object_neg_ko) 395 apply (wp valid_vspace_obj_typ2 [where Q="typ_at (a_type ko) p"] set_object_typ_at 396 | simp)+ 397 apply (clarsimp simp: pred_neg_def obj_at_def) 398 apply (case_tac ko; auto) 399 done 400 401lemma set_object_valid_kernel_mappings: 402 "\<lbrace>\<lambda>s. valid_kernel_mappings s 403 \<and> valid_kernel_mappings_if_pd 404 (set (arm_global_pts (arch_state s))) 405 ko\<rbrace> 406 set_object ptr ko 407 \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" 408 apply (simp add: set_object_def) 409 apply wp 410 apply (clarsimp simp: valid_kernel_mappings_def 411 elim!: ranE split: if_split_asm) 412 apply fastforce 413 done 414 415lemma valid_vs_lookup_lift: 416 assumes lookup: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>" 417 assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 418 shows "\<lbrace>valid_vs_lookup\<rbrace> f \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" 419 unfolding valid_vs_lookup_def 420 apply (rule hoare_lift_Pf [where f=vs_lookup_pages]) 421 apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"]) 422 apply (wp lookup cap)+ 423 done 424 425 426lemma valid_table_caps_lift: 427 assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 428 assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (second_level_tables (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (second_level_tables (arch_state s))\<rbrace>" 429 assumes obj: "\<And>S p. \<lbrace>obj_at (empty_table S) p\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) p\<rbrace>" 430 shows "\<lbrace>valid_table_caps\<rbrace> f \<lbrace>\<lambda>_. valid_table_caps\<rbrace>" 431 unfolding valid_table_caps_def 432 apply (rule hoare_lift_Pf [where f="\<lambda>s. (caps_of_state s)"]) 433 apply (rule hoare_lift_Pf [where f="\<lambda>s. second_level_tables (arch_state s)"]) 434 apply (wp cap pts hoare_vcg_all_lift hoare_vcg_const_imp_lift obj)+ 435 done 436 437lemma valid_arch_caps_lift: 438 assumes lookup: "\<And>P. \<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> f \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>" 439 assumes cap: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 440 assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (second_level_tables (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (second_level_tables (arch_state s))\<rbrace>" 441 assumes obj: "\<And>S p. \<lbrace>obj_at (empty_table S) p\<rbrace> f \<lbrace>\<lambda>rv. obj_at (empty_table S) p\<rbrace>" 442 shows "\<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" 443 unfolding valid_arch_caps_def 444 apply (rule hoare_pre) 445 apply (wp valid_vs_lookup_lift valid_table_caps_lift lookup cap pts obj) 446 apply simp 447 done 448 449lemma valid_global_objs_lift': 450 assumes pts: "\<And>P. \<lbrace>\<lambda>s. P (arm_global_pts (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pts (arch_state s))\<rbrace>" 451 assumes pd: "\<And>P. \<lbrace>\<lambda>s. P (arm_global_pd (arch_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (arm_global_pd (arch_state s))\<rbrace>" 452 assumes obj: "\<And>p. \<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>" 453 assumes ko: "\<And>ako p. \<lbrace>ko_at (ArchObj ako) p\<rbrace> f \<lbrace>\<lambda>_. ko_at (ArchObj ako) p\<rbrace>" 454 assumes emp: "\<And>pd S. 455 \<lbrace>\<lambda>s. (v \<longrightarrow> pd = arm_global_pd (arch_state s) \<and> S = set (second_level_tables (arch_state s)) \<and> P s) 456 \<and> obj_at (empty_table S) pd s\<rbrace> 457 f \<lbrace>\<lambda>rv. obj_at (empty_table S) pd\<rbrace>" 458 shows "\<lbrace>\<lambda>s. valid_global_objs s \<and> (v \<longrightarrow> P s)\<rbrace> f \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 459 unfolding valid_global_objs_def second_level_tables_def 460 apply (rule hoare_pre) 461 apply (rule hoare_use_eq [where f="\<lambda>s. arm_global_pts (arch_state s)", OF pts]) 462 apply (rule hoare_use_eq [where f="\<lambda>s. arm_global_pd (arch_state s)", OF pd]) 463 apply (wp obj ko emp hoare_vcg_const_Ball_lift hoare_ex_wp) 464 apply (clarsimp simp: second_level_tables_def) 465 done 466 467lemmas valid_global_objs_lift 468 = valid_global_objs_lift' [where v=False, simplified] 469 470context 471 fixes f :: "'a::state_ext state \<Rightarrow> ('b \<times> 'a state) set \<times> bool" 472 assumes arch: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>" 473begin 474 475context 476 assumes aobj_at: 477 "\<And>P P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>" 478 notes vspace_obj_fun_lift_expand[simp del] 479begin 480 481lemma valid_global_vspace_mappings_lift: 482 "\<lbrace>valid_global_vspace_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" 483 apply (simp add: valid_global_vspace_mappings_def valid_pd_kernel_mappings_def 484 del: valid_pd_kernel_mappings_arch_def) 485 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) 486 apply (rule_tac f="valid_pd_kernel_mappings_arch (arm_kernel_vspace x)" in hoare_lift_Pf) 487 apply (rule aobj_at; simp) 488 apply (subst valid_pd_kernel_mappings_arch_def valid_pde_kernel_mappings_def)+ 489 apply (clarsimp simp add: valid_def) 490 apply (erule_tac P=P in rsubst) 491 apply (rule ext) 492 apply (clarsimp intro!: iff_allI split: arch_kernel_obj.splits pde.splits) 493 apply (safe; clarsimp simp add: valid_pt_kernel_mappings_def 494 simp del: valid_pt_kernel_mappings_arch_def) 495 apply (erule use_valid[OF _ aobj_at[where P="\<lambda>x. x"]]; simp add:)+ 496 by (rule classical, 497 drule use_valid[OF _ aobj_at[where P="\<lambda>x. \<not>x", OF vspace_obj_pred_fun_lift_id]], 498 simp+)+ 499 500lemma valid_arch_caps_lift_weak: 501 "(\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>) \<Longrightarrow> 502 \<lbrace>valid_arch_caps\<rbrace> f \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" 503 apply (rule valid_arch_caps_lift[OF _ _ arch aobj_at]) 504 apply (rule vs_lookup_pages_vspace_obj_at_lift[OF aobj_at arch], assumption+) 505 apply (rule empty_table.vspace_only) 506 done 507 508lemma valid_global_objs_lift_weak: 509 "\<lbrace>valid_global_objs\<rbrace> f \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 510 apply (rule valid_global_objs_lift) 511 apply (wp arch)+ 512 apply (simp add: valid_vso_at_def) 513 apply (rule hoare_vcg_ex_lift) 514 apply (rule hoare_vcg_conj_lift) 515 apply (wp aobj_at valid_vspace_obj_typ | simp | rule empty_table.vspace_only)+ 516 done 517 518lemma valid_asid_map_lift: 519 "\<lbrace>valid_asid_map\<rbrace> f \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" 520 apply (simp add: valid_asid_map_def) 521 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) 522 apply (simp add: vspace_at_asid_def) 523 by (rule vs_lookup_vspace_obj_at_lift[OF aobj_at arch]) 524 525lemma valid_kernel_mappings_lift: 526 "\<lbrace>valid_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" 527 apply (simp add: valid_kernel_mappings_def) 528 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) 529 apply (simp add: valid_kernel_mappings_if_pd_def ran_def 530 del: valid_kernel_mappings_if_pd_arch_def) 531 apply (rule hoare_vcg_all_lift) 532 apply (case_tac "\<exists>ao. xa = ArchObj ao") 533 apply (rule hoare_convert_imp) 534 apply clarsimp 535 apply (rule hoare_vcg_all_lift) 536 subgoal for ao a 537 by (rule aobj_at[where P=Not and P'="\<lambda>x. x = ArchObj ao", simplified obj_at_def, simplified]) 538 apply clarsimp 539 apply (case_tac ao; simp add: hoare_vcg_prop) 540 apply (clarsimp simp del: valid_kernel_mappings_if_pd_arch_def) 541 apply (case_tac xa; simp add: hoare_vcg_prop) 542 done 543 544end 545 546context 547 assumes aobj_at: 548 "\<And>P P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>" 549begin 550 551lemma valid_global_pts_lift: 552 "\<lbrace>valid_global_pts\<rbrace> f \<lbrace>\<lambda>rv. valid_global_pts\<rbrace>" 553 apply (simp add: valid_global_pts_def) 554 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) 555 apply (rule hoare_vcg_ball_lift) 556 apply (rule aobj_at) 557 apply clarsimp 558 done 559 560lemma valid_arch_state_lift_aobj_at: 561 "\<lbrace>valid_arch_state\<rbrace> f \<lbrace>\<lambda>rv. valid_arch_state\<rbrace>" 562 apply (simp add: valid_arch_state_def valid_asid_table_def) 563 apply (rule hoare_lift_Pf[where f="arch_state", OF _ arch]) 564 apply (wp hoare_vcg_conj_lift hoare_vcg_ball_lift valid_global_pts_lift | (rule aobj_at, clarsimp))+ 565 apply simp 566 done 567 568end 569end 570 571lemma equal_kernel_mappings_lift: 572 assumes aobj_at: 573 "\<And>P P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>\<lambda>s. P (obj_at P' pd s)\<rbrace> f \<lbrace>\<lambda>r s. P (obj_at P' pd s)\<rbrace>" 574 shows "\<lbrace>equal_kernel_mappings\<rbrace> f \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" 575 apply (simp add: equal_kernel_mappings_def) 576 apply (rule hoare_vcg_all_lift)+ 577 apply (rule hoare_convert_imp) 578 apply simp 579 apply (rule hoare_convert_imp) 580 apply (wp aobj_at[OF vspace_obj_pred_arch_obj_l])+ 581 done 582 583lemma valid_machine_state_lift: 584 assumes memory: "\<And>P. \<lbrace>\<lambda>s. P (underlying_memory (machine_state s))\<rbrace> f \<lbrace>\<lambda>_ s. P (underlying_memory (machine_state s))\<rbrace>" 585 assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>" 586 shows "\<lbrace>valid_machine_state\<rbrace> f \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 587 unfolding valid_machine_state_def 588 apply (rule hoare_lift_Pf[where f="\<lambda>s. underlying_memory (machine_state s)", OF _ memory]) 589 apply (rule hoare_vcg_all_lift) 590 apply (rule hoare_vcg_disj_lift[OF _ hoare_vcg_prop]) 591 apply (rule in_user_frame_lift) 592 apply (wp aobj_at; simp) 593 done 594 595lemma valid_ao_at_lift: 596 assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>" 597 and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>" 598 shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>" 599 unfolding valid_ao_at_def 600 by (wp hoare_vcg_ex_lift y valid_vspace_obj_typ z) 601 602lemma valid_ao_at_lift_aobj_at: 603 assumes aobj_at: "\<And>P' pd. arch_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>" 604 shows "\<lbrace>valid_ao_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_ao_at p\<rbrace>" 605 unfolding valid_ao_at_def 606 by (wp hoare_vcg_ex_lift valid_vspace_obj_typ aobj_at | clarsimp)+ 607 608lemma valid_vso_at_lift: 609 assumes z: "\<And>P p T. \<lbrace>\<lambda>s. P (typ_at (AArch T) p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at (AArch T) p s)\<rbrace>" 610 and y: "\<And>ao. \<lbrace>\<lambda>s. ko_at (ArchObj ao) p s\<rbrace> f \<lbrace>\<lambda>rv s. ko_at (ArchObj ao) p s\<rbrace>" 611 shows "\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>" 612 unfolding valid_vso_at_def 613 by (wpsimp wp: hoare_vcg_ex_lift y valid_vspace_obj_typ z)+ 614 615lemma valid_vso_at_lift_aobj_at: 616 assumes aobj_at: "\<And>P' pd. vspace_obj_pred P' \<Longrightarrow> \<lbrace>obj_at P' pd\<rbrace> f \<lbrace>\<lambda>r s. obj_at P' pd s\<rbrace>" 617 shows "\<lbrace>valid_vso_at p\<rbrace> f \<lbrace>\<lambda>rv. valid_vso_at p\<rbrace>" 618 unfolding valid_vso_at_def 619 apply (rule hoare_vcg_ex_lift) 620 apply (rule hoare_vcg_conj_lift aobj_at)+ 621 apply (clarsimp simp: vspace_obj_pred_def) 622 apply (rule iffI) 623 apply ((case_tac ao; clarsimp)+)[2] 624 apply (wpsimp wp: valid_vspace_obj_typ) 625 apply (wpsimp wp: aobj_at) 626 apply assumption 627 done 628 629lemmas set_object_v_ker_map 630 = set_object_valid_kernel_mappings 631 [unfolded valid_kernel_mappings_if_pd_def] 632 633lemma set_object_asid_map: 634 "\<lbrace>valid_asid_map and 635 obj_at (\<lambda>ko'. vs_refs ko' \<subseteq> vs_refs ko) p\<rbrace> 636 set_object p ko 637 \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 638 apply (simp add: valid_asid_map_def set_object_def) 639 apply wp 640 apply (clarsimp simp: vspace_at_asid_def simp del: fun_upd_apply) 641 apply (drule bspec, blast) 642 apply clarsimp 643 apply (rule vs_lookup_stateI, assumption) 644 apply (clarsimp simp: obj_at_def) 645 apply blast 646 apply simp 647 done 648 649lemma set_object_equal_mappings: 650 "\<lbrace>\<lambda>s. equal_kernel_mappings s 651 \<and> (\<forall>pd. ko = ArchObj (PageDirectory pd) 652 \<longrightarrow> (\<forall>x pd'. ko_at (ArchObj (PageDirectory pd')) x s 653 \<longrightarrow> (\<forall>w \<in> kernel_mapping_slots. pd w = pd' w)))\<rbrace> 654 set_object p ko 655 \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" 656 apply (simp add: set_object_def, wp) 657 apply (clarsimp simp: equal_kernel_mappings_def obj_at_def 658 split del: if_split) 659 apply (simp split: if_split_asm) 660 done 661 662lemma valid_global_vspace_mappings_pres: 663 "\<lbrakk> valid_global_vspace_mappings s; 664 \<And>pd. ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s 665 \<Longrightarrow> ko_at (ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s'; 666 \<And>pt p. \<lbrakk> ko_at (ArchObj (PageTable pt)) p s; 667 valid_global_objs s \<Longrightarrow> p \<in> set (arm_global_pts (arch_state s)) \<rbrakk> 668 \<Longrightarrow> ko_at (ArchObj (PageTable pt)) p s'; 669 arm_global_pd (arch_state s') = arm_global_pd (arch_state s); 670 arm_kernel_vspace (arch_state s') = arm_kernel_vspace (arch_state s) \<rbrakk> 671 \<Longrightarrow> valid_global_vspace_mappings s'" 672 apply atomize 673 apply (clarsimp simp: valid_global_vspace_mappings_def obj_at_def) 674 apply (clarsimp simp: valid_pd_kernel_mappings_def 675 split: kernel_object.split_asm arch_kernel_obj.split_asm) 676 apply (drule_tac x=x in spec) 677 apply (clarsimp simp: valid_pde_kernel_mappings_def obj_at_def 678 valid_pt_kernel_mappings_def pde_ref_def 679 split: pde.split_asm) 680 apply (simp split: kernel_object.split_asm 681 arch_kernel_obj.split_asm) 682 apply (drule spec, drule spec, drule(1) mp) 683 apply (drule mp) 684 apply (clarsimp simp: valid_global_objs_def obj_at_def empty_table_def) 685 apply (drule_tac x=x in spec) 686 apply (simp add: pde_ref_def second_level_tables_def)[1] 687 apply clarsimp 688 done 689 690lemma valid_global_vspace_mappings_arch_update[simp]: 691 "arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s) 692 \<and> arm_kernel_vspace (f (arch_state s)) = arm_kernel_vspace (arch_state s) 693 \<Longrightarrow> valid_global_vspace_mappings (arch_state_update f s) = valid_global_vspace_mappings s" 694 by (simp add: valid_global_vspace_mappings_def) 695 696lemma set_object_global_vspace_mappings: 697 "\<lbrace>valid_global_vspace_mappings 698 and (\<lambda>s. (page_directory_at p s \<or> page_table_at p s) 699 \<longrightarrow> valid_global_objs s \<and> p \<notin> global_refs s)\<rbrace> 700 set_object p ko 701 \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" 702 apply (simp add: set_object_def, wp) 703 apply clarsimp 704 apply (erule valid_global_vspace_mappings_pres) 705 apply (clarsimp simp: obj_at_def a_type_def global_refs_def second_level_tables_def)+ 706 done 707 708 709lemma valid_table_caps_ptD: 710 "\<lbrakk> (caps_of_state s) p = Some (ArchObjectCap (arch_cap.PageTableCap p' None)); 711 page_table_at p' s; valid_table_caps s \<rbrakk> \<Longrightarrow> 712 \<exists>pt. ko_at (ArchObj (PageTable pt)) p' s \<and> valid_vspace_obj (PageTable pt) s" 713 apply (clarsimp simp: valid_table_caps_def simp del: split_paired_All) 714 apply (erule allE)+ 715 apply (erule (1) impE) 716 apply (clarsimp simp add: is_pt_cap_def cap_asid_def) 717 apply (erule impE, rule refl) 718 apply (clarsimp simp: obj_at_def empty_table_def) 719 done 720 721lemma store_pde_pred_tcb_at: 722 "\<lbrace>pred_tcb_at proj P t\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. pred_tcb_at proj P t\<rbrace>" 723 apply (simp add: store_pde_def set_pd_def set_object_def 724 get_pd_def bind_assoc) 725 apply (rule hoare_seq_ext [OF _ get_object_sp]) 726 apply (case_tac x, simp_all) 727 apply (rename_tac arch_kernel_obj) 728 apply (case_tac arch_kernel_obj, simp_all) 729 apply (rule hoare_seq_ext [OF _ get_object_sp]) 730 apply wp 731 apply (clarsimp simp: pred_tcb_at_def obj_at_def) 732 done 733 734lemma empty_table_lift: 735 assumes S: "\<And>P. \<lbrace>\<lambda>s. P (S s)\<rbrace> f \<lbrace>\<lambda>_ s. P (S s)\<rbrace>" 736 assumes o: "\<And>P. \<lbrace>obj_at P p and Q\<rbrace> f \<lbrace>\<lambda>_. obj_at P p\<rbrace>" 737 shows "\<lbrace>\<lambda>s. obj_at (empty_table (S s)) p s \<and> Q s\<rbrace> 738 f \<lbrace>\<lambda>_ s. obj_at (empty_table (S s)) p s\<rbrace>" 739 apply (rule hoare_lift_Pf2 [where f="S"]) 740 apply (wp o S|simp)+ 741 done 742 743lemma in_user_frame_obj_upd: 744 "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> 745 in_user_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) 746 = in_user_frame x s" 747 apply (rule iffI) 748 apply (clarsimp simp: in_user_frame_def obj_at_def split: if_split_asm) 749 apply (elim disjE) 750 apply clarsimp 751 apply (intro exI) 752 apply (rule conjI,assumption) 753 apply (simp add: a_type_def) 754 apply (fastforce simp: a_type_def) 755 apply (clarsimp simp: in_user_frame_def obj_at_def split: if_split_asm) 756 apply (rule_tac x = sz in exI) 757 apply (intro conjI impI) 758 apply (fastforce simp: a_type_def)+ 759 done 760 761lemma user_mem_obj_upd_dom: 762 "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> 763 dom (user_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)) 764 = dom (user_mem s)" 765 by (clarsimp simp: user_mem_def in_user_frame_obj_upd dom_def) 766 767lemma in_device_frame_obj_upd: 768 "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> 769 in_device_frame x (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>) 770 = in_device_frame x s" 771 apply (rule iffI) 772 apply (clarsimp simp: in_device_frame_def obj_at_def split: if_split_asm) 773 apply (elim disjE) 774 apply clarsimp 775 apply (intro exI) 776 apply (rule conjI,assumption) 777 apply (simp add: a_type_def) 778 apply (fastforce simp: a_type_def) 779 apply (clarsimp simp: in_device_frame_def obj_at_def split: if_split_asm) 780 apply (rule_tac x = sz in exI) 781 apply (intro conjI impI) 782 apply (fastforce simp: a_type_def)+ 783 done 784 785lemma device_mem_obj_upd_dom: 786 "\<lbrakk>kheap s p = Some ko; a_type k = a_type ko\<rbrakk> \<Longrightarrow> 787 dom (device_mem (s\<lparr>kheap := \<lambda>a. if a = p then Some k else kheap s a\<rparr>)) 788 = dom (device_mem s)" 789 by (clarsimp simp: device_mem_def in_device_frame_obj_upd dom_def) 790 791lemma pspace_respects_region_cong[cong]: 792 "\<lbrakk>kheap a = kheap b; device_state (machine_state a) = device_state (machine_state b)\<rbrakk> 793 \<Longrightarrow> pspace_respects_device_region a = pspace_respects_device_region b" 794 by (simp add: pspace_respects_device_region_def device_mem_def user_mem_def in_device_frame_def 795 in_user_frame_def obj_at_def dom_def) 796 797definition "obj_is_device tp dev \<equiv> 798 case tp of Untyped \<Rightarrow> dev 799 | _ \<Rightarrow>(case (default_object tp dev 0) of (ArchObj (DataPage dev _)) \<Rightarrow> dev 800 | _ \<Rightarrow> False)" 801 802lemma cap_is_device_obj_is_device[simp]: 803 "cap_is_device (default_cap tp a sz dev) = obj_is_device tp dev" 804 by (simp add: default_cap_def arch_default_cap_def obj_is_device_def 805 default_object_def default_arch_object_def 806 split: apiobject_type.splits aobject_type.splits) 807 808crunch device_state_inv: storeWord "\<lambda>ms. P (device_state ms)" 809 810(* some hyp_ref invariants *) 811 812lemma state_hyp_refs_of_ep_update: "\<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow> 813 state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s" 814 apply (rule all_ext) 815 apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def) 816 done 817 818lemma state_hyp_refs_of_ntfn_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow> 819 state_hyp_refs_of (s\<lparr>kheap := kheap s(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s" 820 apply (rule all_ext) 821 apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def) 822 done 823 824lemma state_hyp_refs_of_tcb_bound_ntfn_update: 825 "kheap s t = Some (TCB tcb) \<Longrightarrow> 826 state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>) 827 = state_hyp_refs_of s" 828 apply (rule all_ext) 829 apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits) 830 done 831 832lemma state_hyp_refs_of_tcb_state_update: 833 "kheap s t = Some (TCB tcb) \<Longrightarrow> 834 state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>) 835 = state_hyp_refs_of s" 836 apply (rule all_ext) 837 apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits) 838 done 839 840lemma arch_valid_obj_same_type: 841 "\<lbrakk> arch_valid_obj ao s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk> 842 \<Longrightarrow> arch_valid_obj ao (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)" 843 by (induction ao rule: arch_kernel_obj.induct; 844 clarsimp simp: typ_at_same_type) 845 846 847lemma default_arch_object_not_live: "\<not> live (ArchObj (default_arch_object aty dev us))" 848 by (clarsimp simp: default_arch_object_def live_def hyp_live_def arch_live_def 849 split: aobject_type.splits) 850 851lemma default_tcb_not_live: "\<not> live (TCB default_tcb)" 852 by (clarsimp simp: default_tcb_def default_arch_tcb_def live_def hyp_live_def) 853 854lemma valid_arch_tcb_same_type: 855 "\<lbrakk> valid_arch_tcb t s; valid_obj p k s; kheap s p = Some ko; a_type k = a_type ko \<rbrakk> 856 \<Longrightarrow> valid_arch_tcb t (s\<lparr>kheap := kheap s(p \<mapsto> k)\<rparr>)" 857 by (auto simp: valid_arch_tcb_def obj_at_def) 858 859lemma valid_ioports_lift: 860 assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" 861 assumes y: "\<And>P. \<lbrace>\<lambda>s. P (arch_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>" 862 shows "\<lbrace>valid_ioports\<rbrace> f \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" 863 apply (simp add: valid_ioports_def) 864 apply (rule hoare_use_eq [where f=caps_of_state, OF x y]) 865 done 866 867lemma valid_arch_mdb_lift: 868 assumes c: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. P (caps_of_state s)\<rbrace>" 869 assumes r: "\<And>P. \<lbrace>\<lambda>s. P (is_original_cap s)\<rbrace> f \<lbrace>\<lambda>r s. P (is_original_cap s)\<rbrace>" 870 shows "\<lbrace>\<lambda>s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>r s. valid_arch_mdb (is_original_cap s) (caps_of_state s)\<rbrace>" 871 apply (clarsimp simp: valid_arch_mdb_def valid_def) 872 done 873 874 875end 876end 877