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 ArchUntyped_AI 12imports "../Untyped_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems Untyped_AI_assms 18 19lemma of_bl_nat_to_cref[Untyped_AI_assms]: 20 "\<lbrakk> x < 2 ^ bits; bits < word_bits \<rbrakk> 21 \<Longrightarrow> (of_bl (nat_to_cref bits x) :: machine_word) = of_nat x" 22 apply (clarsimp intro!: less_mask_eq 23 simp: nat_to_cref_def of_drop_to_bl 24 word_size word_less_nat_alt word_bits_def) 25 apply (subst unat_of_nat) 26 apply (erule order_le_less_trans [OF mod_less_eq_dividend]) 27 done 28 29 30lemma cnode_cap_ex_cte[Untyped_AI_assms]: 31 "\<lbrakk> is_cnode_cap cap; cte_wp_at (\<lambda>c. \<exists>m. cap = mask_cap m c) p s; 32 (s::'state_ext::state_ext state) \<turnstile> cap; valid_objs s; pspace_aligned s \<rbrakk> \<Longrightarrow> 33 ex_cte_cap_wp_to is_cnode_cap (obj_ref_of cap, nat_to_cref (bits_of cap) x) s" 34 apply (simp only: ex_cte_cap_wp_to_def) 35 apply (rule exI, erule cte_wp_at_weakenE) 36 apply (clarsimp simp: is_cap_simps bits_of_def) 37 apply (case_tac c, simp_all add: mask_cap_def cap_rights_update_def) 38 apply (clarsimp simp: nat_to_cref_def word_bits_def) 39 apply (erule(2) valid_CNodeCapE) 40 apply (simp add: word_bits_def cte_level_bits_def) 41 done 42 43 44 45lemma inj_on_nat_to_cref[Untyped_AI_assms]: 46 "bits < 32 \<Longrightarrow> inj_on (nat_to_cref bits) {..< 2 ^ bits}" 47 apply (rule inj_onI) 48 apply (drule arg_cong[where f="\<lambda>x. replicate (32 - bits) False @ x"]) 49 apply (subst(asm) word_bl.Abs_inject[where 'a=32, symmetric]) 50 apply (simp add: nat_to_cref_def word_bits_def) 51 apply (simp add: nat_to_cref_def word_bits_def) 52 apply (simp add: of_bl_rep_False of_bl_nat_to_cref[simplified word_bits_def]) 53 apply (erule word_unat.Abs_eqD) 54 apply (simp only: unats_def mem_simps) 55 apply (erule order_less_le_trans) 56 apply (rule power_increasing, simp+) 57 apply (simp only: unats_def mem_simps) 58 apply (erule order_less_le_trans) 59 apply (rule power_increasing, simp+) 60 done 61 62 63lemma data_to_obj_type_sp[Untyped_AI_assms]: 64 "\<lbrace>P\<rbrace> data_to_obj_type x \<lbrace>\<lambda>ts (s::'state_ext::state_ext state). ts \<noteq> ArchObject ASIDPoolObj \<and> P s\<rbrace>, -" 65 unfolding data_to_obj_type_def 66 apply (rule hoare_pre) 67 apply (wp|wpc)+ 68 apply clarsimp 69 apply (simp add: arch_data_to_obj_type_def split: if_split_asm) 70 done 71 72lemma dui_inv_wf[wp, Untyped_AI_assms]: 73 "\<lbrace>invs and cte_wp_at ((=) (cap.UntypedCap dev w sz idx)) slot 74 and (\<lambda>s. \<forall>cap \<in> set cs. is_cnode_cap cap 75 \<longrightarrow> (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s)) 76 and (\<lambda>s. \<forall>x \<in> set cs. s \<turnstile> x)\<rbrace> 77 decode_untyped_invocation label args slot (cap.UntypedCap dev w sz idx) cs 78 \<lbrace>valid_untyped_inv\<rbrace>,-" 79proof - 80 have inj: "\<And>node_cap s. \<lbrakk>is_cnode_cap node_cap; 81 unat (args ! 5) \<le> 2 ^ bits_of node_cap - unat (args ! 4);valid_cap node_cap s\<rbrakk> \<Longrightarrow> 82 inj_on (Pair (obj_ref_of node_cap) \<circ> nat_to_cref (bits_of node_cap)) 83 {unat (args ! 4)..<unat (args ! 4) + unat (args ! 5)}" 84 apply (simp add:comp_def) 85 apply (rule inj_on_split) 86 apply (rule subset_inj_on [OF inj_on_nat_to_cref]) 87 apply (clarsimp simp: is_cap_simps bits_of_def valid_cap_def 88 word_bits_def cap_aligned_def) 89 apply clarsimp 90 apply (rule less_le_trans) 91 apply assumption 92 apply (simp add:le_diff_conv2) 93 done 94 have nasty_strengthen: 95 "\<And>S a f s. (\<forall>x\<in>S. cte_wp_at ((=) cap.NullCap) (a, f x) s) 96 \<Longrightarrow> cte_wp_at (\<lambda>c. c \<noteq> cap.NullCap) slot s 97 \<longrightarrow> slot \<notin> (Pair a \<circ> f) ` S" 98 by (auto simp:cte_wp_at_caps_of_state) 99 show ?thesis 100 apply (simp add: decode_untyped_invocation_def unlessE_def[symmetric] 101 unlessE_whenE 102 split del: if_split) 103 apply (rule validE_R_sp[OF whenE_throwError_sp] 104 validE_R_sp[OF data_to_obj_type_sp] 105 validE_R_sp[OF dui_sp_helper] validE_R_sp[OF map_ensure_empty])+ 106 apply clarsimp 107 apply (rule hoare_pre) 108 apply (wp whenE_throwError_wp[THEN validE_validE_R] check_children_wp 109 map_ensure_empty_wp) 110 apply (clarsimp simp: distinct_map cases_imp_eq) 111 apply (subgoal_tac "s \<turnstile> node_cap") 112 prefer 2 113 apply (erule disjE) 114 apply (drule bspec [where x = "cs ! 0"],clarsimp)+ 115 apply fastforce 116 apply clarsimp 117 apply (clarsimp simp:cte_wp_at_caps_of_state) 118 apply (drule(1) caps_of_state_valid[rotated])+ 119 apply (clarsimp simp: is_cap_simps diminished_def mask_cap_def 120 cap_rights_update_def, 121 simp split: cap.splits) 122 apply (subgoal_tac "\<forall>r\<in>cte_refs node_cap (interrupt_irq_node s). ex_cte_cap_wp_to is_cnode_cap r s") 123 apply (clarsimp simp:cte_wp_at_caps_of_state) 124 apply (frule(1) caps_of_state_valid[rotated]) 125 apply (clarsimp simp:not_less) 126 apply (frule(2) inj) 127 apply (clarsimp simp:comp_def) 128 apply (frule(1) caps_of_state_valid) 129 apply (simp add: nasty_strengthen[unfolded o_def] cte_wp_at_caps_of_state) 130 apply (intro conjI) 131 apply (intro impI) 132 apply (frule range_cover_stuff[where w=w and rv = 0 and sz = sz], simp_all)[1] 133 apply (clarsimp simp: valid_cap_simps cap_aligned_def)+ 134 apply (frule alignUp_idem[OF is_aligned_weaken,where a = w]) 135 apply (erule range_cover.sz) 136 apply (simp add:range_cover_def) 137 apply (clarsimp simp:get_free_ref_def is_aligned_neg_mask_eq empty_descendants_range_in) 138 apply (rule conjI[rotated], blast, clarsimp) 139 apply (drule_tac x = "(obj_ref_of node_cap,nat_to_cref (bits_of node_cap) slota)" in bspec) 140 apply (clarsimp simp:is_cap_simps nat_to_cref_def word_bits_def 141 bits_of_def valid_cap_simps cap_aligned_def)+ 142 apply (simp add: free_index_of_def) 143 apply (frule(1) range_cover_stuff[where sz = sz]) 144 apply (clarsimp dest!:valid_cap_aligned simp:cap_aligned_def word_bits_def)+ 145 apply simp+ 146 apply (clarsimp simp:get_free_ref_def) 147 apply (erule disjE) 148 apply (drule_tac x= "cs!0" in bspec) 149 subgoal by clarsimp 150 subgoal by simp 151 apply (clarsimp simp: cte_wp_at_caps_of_state ex_cte_cap_wp_to_def) 152 apply (rule_tac x=aa in exI,rule exI,rule exI) 153 apply (rule conjI, assumption) 154 apply (clarsimp simp: diminished_def is_cap_simps mask_cap_def 155 cap_rights_update_def, 156 simp split: cap.splits ) 157 done 158qed 159 160lemma asid_bits_ge_0: 161 "(0::word32) < 2 ^ asid_bits" by (simp add: asid_bits_def) 162 163lemma retype_ret_valid_caps_captable[Untyped_AI_assms]: 164 "\<lbrakk>pspace_no_overlap_range_cover ptr sz (s::'state_ext::state_ext state) \<and> 0 < us 165 \<and> range_cover ptr sz (obj_bits_api CapTableObject us) n \<and> ptr \<noteq> 0 166 \<rbrakk> 167 \<Longrightarrow> \<forall>y\<in>{0..<n}. s 168 \<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object CapTableObject dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api CapTableObject us)) [0..<n]) 169 (kheap s)\<rparr> \<turnstile> CNodeCap (ptr_add ptr (y * 2 ^ obj_bits_api CapTableObject us)) us []" 170by ((clarsimp simp:valid_cap_def default_object_def cap_aligned_def 171 cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def 172 dom_def arch_default_cap_def ptr_add_def | rule conjI | intro conjI obj_at_foldr_intro imageI 173 | rule is_aligned_add_multI[OF _ le_refl], 174 (simp add:range_cover_def word_bits_def obj_bits_api_def slot_bits_def)+)+)[1] 175 176lemma retype_ret_valid_caps_aobj[Untyped_AI_assms]: 177 "\<And>ptr sz (s::'state_ext::state_ext state) x6 us n. 178 \<lbrakk>pspace_no_overlap_range_cover ptr sz s \<and> x6 \<noteq> ASIDPoolObj \<and> 179 range_cover ptr sz (obj_bits_api (ArchObject x6) us) n \<and> ptr \<noteq> 0\<rbrakk> 180 \<Longrightarrow> \<forall>y\<in>{0..<n}. s 181 \<lparr>kheap := foldr (\<lambda>p kh. kh(p \<mapsto> default_object (ArchObject x6) dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api (ArchObject x6) us)) [0..<n]) 182 (kheap s)\<rparr> \<turnstile> ArchObjectCap (ARM_A.arch_default_cap x6 (ptr_add ptr (y * 2 ^ obj_bits_api (ArchObject x6) us)) us dev)" 183 apply (rename_tac aobject_type us n) 184 apply (case_tac aobject_type) 185 by (clarsimp simp: valid_cap_def default_object_def cap_aligned_def 186 cte_level_bits_def is_obj_defs well_formed_cnode_n_def empty_cnode_def 187 dom_def arch_default_cap_def ptr_add_def 188 | intro conjI obj_at_foldr_intro 189 imageI valid_vm_rights_def 190 | rule is_aligned_add_multI[OF _ le_refl] 191 | fastforce simp:range_cover_def obj_bits_api_def 192 default_arch_object_def valid_vm_rights_def word_bits_def a_type_def)+ 193 194 195 196lemma copy_global_mappings_hoare_lift:(*FIXME: arch_split \<rightarrow> these do not seem to be used globally *) 197 assumes wp: "\<And>ptr val. \<lbrace>Q\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. Q\<rbrace>" 198 shows "\<lbrace>Q\<rbrace> copy_global_mappings pd \<lbrace>\<lambda>rv. Q\<rbrace>" 199 apply (simp add: copy_global_mappings_def) 200 apply (wp mapM_x_wp' wp) 201 done 202 203lemma init_arch_objects_hoare_lift: 204 assumes wp: "\<And>oper. \<lbrace>(P::'state_ext::state_ext state\<Rightarrow>bool)\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv :: unit. Q\<rbrace>" 205 "\<And>ptr val. \<lbrace>P\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv. P\<rbrace>" 206 shows "\<lbrace>P and Q\<rbrace> init_arch_objects tp ptr sz us adds \<lbrace>\<lambda>rv. Q\<rbrace>" 207proof - 208 have pres: "\<And>oper. \<lbrace>P and Q\<rbrace> do_machine_op oper \<lbrace>\<lambda>rv :: unit. Q\<rbrace>" 209 "\<lbrace>P and Q\<rbrace> return () \<lbrace>\<lambda>rv. Q\<rbrace>" 210 by (wp wp | simp)+ 211 show ?thesis 212 apply (simp add: init_arch_objects_def 213 pres reserve_region_def unless_def when_def 214 split: Structures_A.apiobject_type.split 215 aobject_type.split) 216 apply clarsimp 217 apply (rule hoare_pre) 218 apply (wp mapM_x_wp' copy_global_mappings_hoare_lift wp) 219 apply simp 220 done 221qed 222 223crunch pdistinct[wp]: do_machine_op "pspace_distinct" 224crunch vmdb[wp]: do_machine_op "valid_mdb" 225crunch mdb[wp]: do_machine_op "\<lambda>s. P (cdt s)" 226crunch cte_wp_at[wp]: do_machine_op "\<lambda>s. P (cte_wp_at P' p s)" 227 228lemma cap_refs_in_kernel_windowD2: 229 "\<lbrakk> cte_wp_at P p (s::'state_ext::state_ext state); cap_refs_in_kernel_window s \<rbrakk> 230 \<Longrightarrow> \<exists>cap. P cap \<and> region_in_kernel_window (cap_range cap) s" 231 apply (clarsimp simp: cte_wp_at_caps_of_state region_in_kernel_window_def) 232 apply (drule(1) cap_refs_in_kernel_windowD) 233 apply fastforce 234 done 235 236lemma init_arch_objects_descendants_range[wp,Untyped_AI_assms]: 237 "\<lbrace>\<lambda>(s::'state_ext::state_ext state). descendants_range x cref s \<rbrace> init_arch_objects ty ptr n us y 238 \<lbrace>\<lambda>rv s. descendants_range x cref s\<rbrace>" 239 apply (simp add:descendants_range_def) 240 apply (rule hoare_pre) 241 apply (wp retype_region_mdb init_arch_objects_hoare_lift) 242 apply (wps do_machine_op_mdb) 243 apply (wp hoare_vcg_ball_lift) 244 apply (rule hoare_pre) 245 apply (wps store_pde_mdb_inv) 246 apply wp 247 apply simp 248 apply fastforce 249 done 250 251 252 253lemma init_arch_objects_caps_overlap_reserved[wp,Untyped_AI_assms]: 254 "\<lbrace>\<lambda>(s::'state_ext::state_ext state). caps_overlap_reserved S s\<rbrace> 255 init_arch_objects ty ptr n us y 256 \<lbrace>\<lambda>rv s. caps_overlap_reserved S s\<rbrace>" 257 apply (simp add:caps_overlap_reserved_def) 258 apply (rule hoare_pre) 259 apply (wp retype_region_mdb init_arch_objects_hoare_lift) 260 apply fastforce 261 done 262 263lemma set_untyped_cap_invs_simple[Untyped_AI_assms]: 264 "\<lbrace>\<lambda>s. descendants_range_in {ptr .. ptr+2^sz - 1} cref s \<and> pspace_no_overlap_range_cover ptr sz s \<and> invs s 265 \<and> cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr \<and> cap_is_device c = dev) cref s \<and> idx \<le> 2^ sz\<rbrace> 266 set_cap (cap.UntypedCap dev ptr sz idx) cref 267 \<lbrace>\<lambda>rv s. invs s\<rbrace>" 268 apply (rule hoare_name_pre_state) 269 apply (clarsimp simp: cte_wp_at_caps_of_state invs_def valid_state_def) 270 apply (rule hoare_pre) 271 apply (wp set_free_index_valid_pspace_simple set_cap_valid_mdb_simple 272 set_cap_idle update_cap_ifunsafe) 273 apply (simp add:valid_irq_node_def) 274 apply wps 275 apply (wp hoare_vcg_all_lift set_cap_irq_handlers set_cap_valid_arch_caps 276 set_cap_irq_handlers cap_table_at_lift_valid set_cap_typ_at 277 set_untyped_cap_refs_respects_device_simple) 278 apply (clarsimp simp:cte_wp_at_caps_of_state is_cap_simps) 279 apply (intro conjI,clarsimp) 280 apply (rule ext,clarsimp simp:is_cap_simps) 281 apply (clarsimp split:cap.splits simp:is_cap_simps appropriate_cte_cap_def) 282 apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD]) 283 apply clarsimp 284 apply (clarsimp simp:is_cap_simps ex_cte_cap_wp_to_def appropriate_cte_cap_def cte_wp_at_caps_of_state) 285 apply (clarsimp dest!:valid_global_refsD2 simp:cap_range_def) 286 apply (simp add:valid_irq_node_def) 287 apply (clarsimp simp:valid_irq_node_def) 288 apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state vs_cap_ref_def) 289 apply (case_tac cap) 290 apply (simp_all add:vs_cap_ref_def table_cap_ref_def) 291 apply (rename_tac arch_cap) 292 apply (case_tac arch_cap) 293 apply simp_all 294 apply (clarsimp simp:cap_refs_in_kernel_window_def 295 valid_refs_def simp del:split_paired_All) 296 apply (drule_tac x = cref in spec) 297 apply (clarsimp simp:cte_wp_at_caps_of_state) 298 apply fastforce 299 done 300 301 302lemma pbfs_atleast_pageBits': 303 "pageBits \<le> pageBitsForSize sz"by (cases sz, simp_all add: pageBits_def) 304 305 306lemma pbfs_less_wb': 307 "pageBitsForSize sz < word_bits"by (cases sz, simp_all add: word_bits_conv pageBits_def) 308 309lemma delete_objects_rewrite[Untyped_AI_assms]: 310 "\<lbrakk> word_size_bits \<le> sz; sz\<le> word_bits; ptr && ~~ mask sz = ptr \<rbrakk> 311 \<Longrightarrow> delete_objects ptr sz = 312 do y \<leftarrow> modify (clear_um {ptr + of_nat k |k. k < 2 ^ sz}); 313 modify (detype {ptr && ~~ mask sz..ptr + 2 ^ sz - 1}) 314 od" 315 apply (clarsimp simp: delete_objects_def freeMemory_def word_size_def word_size_bits_def) 316 apply (subgoal_tac "is_aligned (ptr &&~~ mask sz) sz") 317 apply (subst mapM_storeWord_clear_um[simplified word_size_def word_size_bits_def]) 318 apply (simp) 319 apply simp 320 apply (simp add:range_cover_def) 321 apply clarsimp 322 apply (rule is_aligned_neg_mask) 323 apply simp 324 done 325 326declare store_pde_pred_tcb_at [wp] 327 328(* nonempty_table *) 329definition 330 nonempty_table :: "machine_word set \<Rightarrow> Structures_A.kernel_object \<Rightarrow> bool" 331where 332 "nonempty_table S ko \<equiv> 333 (a_type ko = AArch APageTable \<or> a_type ko = AArch APageDirectory) 334 \<and> \<not> empty_table S ko" 335 336lemma reachable_pg_cap_exst_update[simp]: 337 "reachable_pg_cap x (trans_state f (s::'state_ext::state_ext state)) = reachable_pg_cap x s" 338 by (simp add: reachable_pg_cap_def vs_lookup_pages_def 339 vs_lookup_pages1_def obj_at_def) 340 341lemma create_cap_valid_arch_caps[wp, Untyped_AI_assms]: 342 "\<lbrace>valid_arch_caps 343 and valid_cap (default_cap tp oref sz dev) 344 and (\<lambda>(s::'state_ext::state_ext state). \<forall>r\<in>obj_refs (default_cap tp oref sz dev). 345 (\<forall>p'. \<not> cte_wp_at (\<lambda>cap. r \<in> obj_refs cap) p' s) 346 \<and> \<not> obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) 347 and cte_wp_at ((=) cap.NullCap) cref 348 and K (tp \<noteq> ArchObject ASIDPoolObj)\<rbrace> 349 create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 350 apply (simp add: create_cap_def set_cdt_def) 351 apply (wp set_cap_valid_arch_caps) 352 apply (simp add: trans_state_update[symmetric] del: trans_state_update) 353 apply (wp hoare_vcg_disj_lift hoare_vcg_conj_lift hoare_vcg_all_lift hoare_vcg_imp_lift | simp)+ 354 apply (clarsimp simp del: split_paired_All split_paired_Ex 355 imp_disjL 356 simp: cte_wp_at_caps_of_state) 357 apply (rule conjI) 358 apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def 359 cte_wp_at_caps_of_state) 360 apply (case_tac "\<exists>x. x \<in> obj_refs cap") 361 apply (clarsimp dest!: obj_ref_elemD) 362 apply (case_tac cref, fastforce) 363 apply (simp add: obj_ref_none_no_asid) 364 apply (rule conjI) 365 apply (auto simp: is_cap_simps valid_cap_def second_level_tables_def 366 obj_at_def nonempty_table_def a_type_simps)[1] 367 apply (clarsimp simp del: imp_disjL) 368 apply (case_tac "\<exists>x. x \<in> obj_refs cap") 369 apply (clarsimp dest!: obj_ref_elemD) 370 apply fastforce 371 apply (auto simp: is_cap_simps)[1] 372 done 373 374lemma create_cap_cap_refs_in_kernel_window[wp, Untyped_AI_assms]: 375 "\<lbrace>cap_refs_in_kernel_window and cte_wp_at (\<lambda>c. cap_range (default_cap tp oref sz dev) \<subseteq> cap_range c) p\<rbrace> 376 create_cap tp sz p dev (cref, oref) \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 377 apply (simp add: create_cap_def) 378 apply (wp | simp)+ 379 apply (clarsimp simp: cte_wp_at_caps_of_state) 380 apply (drule(1) cap_refs_in_kernel_windowD) 381 apply blast 382 done 383 384crunch irq_node[wp]: store_pde "\<lambda>s. P (interrupt_irq_node s)" 385 (wp: crunch_wps) 386 387(* make these available in the generic theory? *) 388lemma init_arch_objects_irq_node[wp]: 389 "\<lbrace>\<lambda>s. P (interrupt_irq_node s)\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv s. P (interrupt_irq_node s)\<rbrace>" 390 by (wp init_arch_objects_hoare_lift, simp) 391 392lemma init_arch_objects_excap[wp]: 393 "\<lbrace>ex_cte_cap_wp_to P p\<rbrace> init_arch_objects tp ptr bits us refs \<lbrace>\<lambda>rv. ex_cte_cap_wp_to P p\<rbrace>" 394 by (wp ex_cte_cap_to_pres init_arch_objects_irq_node init_arch_objects_cte_wp_at) 395 396crunch nonempty_table[wp]: do_machine_op 397 "\<lambda>s. P' (obj_at (nonempty_table (set (arm_global_pts (arch_state s)))) r s)" 398 399lemma store_pde_weaken: 400 "\<lbrace>\<lambda>s. page_directory_at (p && ~~ mask pd_bits) s \<longrightarrow> P s\<rbrace> store_pde p e \<lbrace>Q\<rbrace> = 401 \<lbrace>P\<rbrace> store_pde p e \<lbrace>Q\<rbrace>" 402 apply (rule iffI) 403 apply (simp add: valid_def) 404 apply (erule allEI) 405 apply clarsimp 406 apply (simp add: valid_def) 407 apply (erule allEI) 408 apply clarsimp 409 apply (rule use_valid, assumption) 410 apply (simp add: store_pde_def set_pd_def set_object_def) 411 apply (wp get_object_wp) 412 apply (clarsimp simp: obj_at_def a_type_simps) 413 apply (drule bspec, assumption) 414 apply (simp add: simpler_store_pde_def obj_at_def fun_upd_def 415 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 416 done 417 418lemma store_pde_nonempty_table: 419 "\<lbrace>\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) 420 \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow> 421 rf \<in> set (arm_global_pts (arch_state s))) 422 \<and> ucast (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots 423 \<and> valid_pde_mappings pde\<rbrace> 424 store_pde pde_ptr pde 425 \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>" 426 apply (simp add: store_pde_def set_pd_def set_object_def) 427 apply (wp get_object_wp) 428 apply (clarsimp simp: obj_at_def nonempty_table_def a_type_def) 429 apply (clarsimp simp add: empty_table_def second_level_tables_def) 430 done 431 432lemma store_pde_global_global_objs: 433 "\<lbrace>\<lambda>s. valid_global_objs s 434 \<and> (\<forall>rf. pde_ref pde = Some rf \<longrightarrow> 435 rf \<in> set (arm_global_pts (arch_state s))) 436 \<and> ucast (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots 437 \<and> valid_pde_mappings pde\<rbrace> 438 store_pde pde_ptr pde 439 \<lbrace>\<lambda>rv s. valid_global_objs s\<rbrace>" 440 apply (simp add: store_pde_def set_pd_def set_object_def) 441 apply (wp get_object_wp) 442 apply (clarsimp simp: obj_at_def fun_upd_def[symmetric]) 443proof - 444 fix s pd 445 assume vg: "valid_global_objs s" 446 and gr: "\<forall>rf. pde_ref pde = Some rf \<longrightarrow> 447 rf \<in> set (arm_global_pts (arch_state s))" 448 and uc: "ucast (pde_ptr && mask pd_bits >> 2) \<in> kernel_mapping_slots" 449 and vp: "valid_pde_mappings pde" 450 and pd: "kheap s (pde_ptr && ~~ mask pd_bits) = 451 Some (ArchObj (PageDirectory pd))" 452 let ?ko' = "ArchObj (PageDirectory 453 (pd(ucast (pde_ptr && mask pd_bits >> 2) := pde)))" 454 let ?s' = "s\<lparr>kheap := kheap s(pde_ptr && ~~ mask pd_bits \<mapsto> ?ko')\<rparr>" 455 have typ_at: "\<And>T p. typ_at T p s \<Longrightarrow> typ_at T p ?s'" 456 using pd 457 by (clarsimp simp: obj_at_def a_type_def) 458 have valid_pde: "\<And>pde. valid_pde pde s \<Longrightarrow> valid_pde pde ?s'" 459 by (case_tac pdea, auto simp add: typ_at data_at_def) 460 have valid_pte: "\<And>pte. valid_pte pte s \<Longrightarrow> valid_pte pte ?s'" 461 by (case_tac pte, auto simp add: typ_at data_at_def) 462 have valid_ao_at: "\<And>p. valid_ao_at p s \<Longrightarrow> valid_ao_at p ?s'" 463 using pd uc 464 apply (clarsimp simp: valid_ao_at_def obj_at_def) 465 apply (intro conjI impI allI) 466 apply (clarsimp simp: valid_pde vp) 467 apply (case_tac ao, simp_all add: typ_at valid_pde valid_pte) 468 done 469 have valid_vso_at: "\<And>p. valid_vso_at p s \<Longrightarrow> valid_vso_at p ?s'" 470 using pd uc 471 apply (clarsimp simp: valid_vso_at_def obj_at_def) 472 apply (intro conjI impI allI) 473 apply (clarsimp simp: valid_pde vp) 474 apply (case_tac ao, simp_all add: typ_at valid_pde valid_pte) 475 done 476 have empty: 477 "\<And>p. obj_at (empty_table (set (second_level_tables (arch_state s)))) p s 478 \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) p ?s'" 479 using pd gr vp uc 480 by (clarsimp simp: obj_at_def empty_table_def second_level_tables_def) 481 show "valid_global_objs ?s'" 482 using vg pd 483 apply (clarsimp simp add: valid_global_objs_def valid_ao_at valid_vso_at empty) 484 apply (fastforce simp add: obj_at_def) 485 done 486qed 487 488lemma valid_arch_state_global_pd: 489 "\<lbrakk> valid_arch_state s; pspace_aligned s \<rbrakk> 490 \<Longrightarrow> obj_at (\<lambda>ko. \<exists>pd. ko = ArchObj (PageDirectory pd)) (arm_global_pd (arch_state s)) s 491 \<and> is_aligned (arm_global_pd (arch_state s)) pd_bits" 492 apply (clarsimp simp: valid_arch_state_def a_type_def 493 pd_aligned pd_bits_def pageBits_def 494 elim!: obj_at_weakenE) 495 apply (clarsimp split: Structures_A.kernel_object.split_asm 496 arch_kernel_obj.split_asm if_split_asm) 497 done 498 499lemma pd_shifting': 500 "is_aligned (pd :: word32) pd_bits \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits = pd" 501 by (rule pd_shifting, simp add: pd_bits_def pageBits_def) 502 503lemma copy_global_mappings_nonempty_table: 504 "is_aligned pd pd_bits \<Longrightarrow> 505 \<lbrace>\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) \<and> 506 valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace> 507 copy_global_mappings pd 508 \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table 509 (set (second_level_tables (arch_state s)))) r s) \<and> 510 valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s\<rbrace>" 511 apply (simp add: copy_global_mappings_def) 512 apply (rule hoare_seq_ext [OF _ gets_sp]) 513 apply (rule hoare_strengthen_post) 514 apply (rule mapM_x_wp[where S="{x. kernel_base >> 20 \<le> x \<and> 515 x < 2 ^ (pd_bits - 2)}"]) 516 apply (wp get_pde_wp hoare_vcg_ball_lift 517 store_pde_weaken[THEN iffD2,OF store_pde_nonempty_table] 518 store_pde_weaken[THEN iffD2,OF store_pde_global_global_objs] 519 | simp)+ 520 apply clarsimp 521 apply (subst (asm) is_aligned_add_helper[THEN conjunct2]) 522 apply (clarsimp simp: valid_arch_state_def pspace_aligned_def dom_def 523 obj_at_def) 524 apply (drule_tac x="arm_global_pd (arch_state s)" in spec, erule impE, 525 fastforce) 526 apply (simp add: pd_bits_def pageBits_def) 527 apply (erule shiftl_less_t2n) 528 apply (simp add: pd_bits_def pageBits_def) 529 apply (clarsimp simp: valid_arch_state_def valid_global_objs_def obj_at_def 530 empty_table_def second_level_tables_def) 531 apply (simp add: kernel_mapping_slots_def) 532 apply (subst is_aligned_add_helper[THEN conjunct1], assumption) 533 apply (erule shiftl_less_t2n) 534 apply (simp add: pd_bits_def pageBits_def) 535 apply (simp add: kernel_base_shift_cast_le[symmetric] ucast_ucast_mask) 536 apply (subst shiftl_shiftr_id) 537 apply simp 538 apply (simp add: word_less_nat_alt pd_bits_def pageBits_def) 539 apply (subst less_mask_eq) 540 apply (simp add: pd_bits_def pageBits_def) 541 apply assumption 542 apply (clarsimp simp: pd_bits_def) 543 apply simp 544 done 545 546 547lemma mapM_copy_global_mappings_nonempty_table[wp]: 548 "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) 549 \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and 550 K (\<forall>pd\<in>set pds. is_aligned pd pd_bits)\<rbrace> 551 mapM_x copy_global_mappings pds 552 \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>" 553 apply (rule hoare_gen_asm) 554 apply (rule hoare_strengthen_post) 555 apply (rule mapM_x_wp', rule copy_global_mappings_nonempty_table) 556 apply simp_all 557 done 558 559lemma init_arch_objects_nonempty_table[Untyped_AI_assms, wp]: 560 "\<lbrace>(\<lambda>s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s) 561 \<and> valid_global_objs s \<and> valid_arch_state s \<and> pspace_aligned s) and 562 K (\<forall>ref\<in>set refs. is_aligned ref (obj_bits_api tp us))\<rbrace> 563 init_arch_objects tp ptr bits us refs 564 \<lbrace>\<lambda>rv s. \<not> (obj_at (nonempty_table (set (second_level_tables (arch_state s)))) r s)\<rbrace>" 565 apply (rule hoare_gen_asm) 566 apply (simp add: init_arch_objects_def split del: if_split) 567 apply (rule hoare_pre) 568 apply (wp hoare_unless_wp | wpc | simp add: reserve_region_def second_level_tables_def)+ 569 apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def) 570 done 571 572lemma nonempty_table_caps_of[Untyped_AI_assms]: 573 "nonempty_table S ko \<Longrightarrow> caps_of ko = {}" 574 by (auto simp: caps_of_def cap_of_def nonempty_table_def a_type_def 575 split: Structures_A.kernel_object.split if_split_asm) 576 577 578lemma nonempty_default[simp, Untyped_AI_assms]: 579 "tp \<noteq> Untyped \<Longrightarrow> \<not> nonempty_table S (default_object tp dev us)" 580 apply (case_tac tp, simp_all add: default_object_def nonempty_table_def 581 a_type_def) 582 apply (rename_tac aobject_type) 583 apply (case_tac aobject_type, simp_all add: default_arch_object_def) 584 apply (simp_all add: empty_table_def pde_ref_def valid_pde_mappings_def) 585 done 586 587lemma set_pd_cte_wp_at_iin[wp]: 588 "\<lbrace>\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace> 589 set_pd q pd 590 \<lbrace>\<lambda>_ s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)\<rbrace>" 591 apply (simp add: set_pd_def set_object_def) 592 apply (wp get_object_wp) 593 apply (clarsimp simp: obj_at_def cte_wp_at_caps_of_state 594 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 595 apply (subst caps_of_state_after_update) 596 apply (simp add: obj_at_def)+ 597 done 598 599crunch cte_wp_at_iin[wp]: init_arch_objects 600 "\<lambda>s. P (cte_wp_at (P' (interrupt_irq_node s)) p s)" 601 (ignore: clearMemory wp: crunch_wps hoare_unless_wp) 602 603lemmas init_arch_objects_ex_cte_cap_wp_to 604 = init_arch_objects_excap 605 606lemma obj_is_device_vui_eq[Untyped_AI_assms]: 607 "valid_untyped_inv ui s 608 \<Longrightarrow> case ui of Retype slot reset ptr_base ptr tp us slots dev 609 \<Rightarrow> obj_is_device tp dev = dev" 610 apply (cases ui, clarsimp) 611 apply (clarsimp simp: obj_is_device_def 612 split: apiobject_type.split) 613 apply (intro impI conjI allI, simp_all add: is_frame_type_def default_object_def) 614 apply (simp add: default_arch_object_def split: aobject_type.split) 615 apply (auto simp: arch_is_frame_type_def) 616 done 617 618lemma create_cap_ioports[wp, Untyped_AI_assms]: 619 "\<lbrace>valid_ioports and cte_wp_at (\<lambda>_. True) cref\<rbrace> create_cap tp sz p dev (cref,oref) \<lbrace>\<lambda>rv. valid_ioports\<rbrace>" 620 by wpsimp 621 622end 623 624global_interpretation Untyped_AI? : Untyped_AI 625 where nonempty_table = ARM.nonempty_table 626 proof goal_cases 627 interpret Arch . 628 case 1 show ?case 629 by (unfold_locales; (fact Untyped_AI_assms)?) 630 qed 631 632end 633