1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11(* 12CSpace invariants 13*) 14 15theory ArchCSpaceInvPre_AI 16imports "../CSpaceInvPre_AI" 17begin 18context Arch begin global_naming ARM 19 20lemma aobj_ref_acap_rights_update[simp]: 21 "aobj_ref (acap_rights_update f x) = aobj_ref x" 22 by (cases x; simp add: acap_rights_update_def) 23 24lemma arch_obj_size_acap_rights_update[simp]: 25 "arch_obj_size (acap_rights_update f x) = arch_obj_size x" 26 by (cases x; simp add: acap_rights_update_def) 27 28lemma valid_arch_cap_acap_rights_update[intro]: 29 "valid_arch_cap x s \<Longrightarrow> valid_arch_cap (acap_rights_update f x) s" 30 by (cases x; simp add: acap_rights_update_def valid_arch_cap_def) 31 32definition 33 cap_master_arch_cap where 34 "cap_master_arch_cap acap \<equiv> 35 (case acap of 36 arch_cap.PageCap dev ref rghts sz mapdata \<Rightarrow> 37 arch_cap.PageCap dev ref UNIV sz None 38 | arch_cap.ASIDPoolCap pool asid \<Rightarrow> 39 arch_cap.ASIDPoolCap pool 0 40 | arch_cap.PageTableCap ptr data \<Rightarrow> 41 arch_cap.PageTableCap ptr None 42 | arch_cap.PageDirectoryCap ptr data \<Rightarrow> 43 arch_cap.PageDirectoryCap ptr None 44 | _ \<Rightarrow> acap)" 45 46lemma 47 cap_master_arch_cap_eqDs1: 48 "cap_master_arch_cap cap = (arch_cap.PageCap dev ref rghts sz mapdata) 49 \<Longrightarrow> rghts = UNIV \<and> mapdata = None 50 \<and> (\<exists>rghts mapdata. cap = (arch_cap.PageCap dev ref rghts sz mapdata))" 51 "cap_master_arch_cap cap = arch_cap.ASIDControlCap 52 \<Longrightarrow> cap = arch_cap.ASIDControlCap" 53 "cap_master_arch_cap cap = (arch_cap.ASIDPoolCap pool asid) 54 \<Longrightarrow> asid = 0 \<and> (\<exists>asid. cap = (arch_cap.ASIDPoolCap pool asid))" 55 "cap_master_arch_cap cap = (arch_cap.PageTableCap ptr data) 56 \<Longrightarrow> data = None \<and> (\<exists>data. cap = (arch_cap.PageTableCap ptr data))" 57 "cap_master_arch_cap cap = (arch_cap.PageDirectoryCap ptr data2) 58 \<Longrightarrow> data2 = None \<and> (\<exists>data2. cap = (arch_cap.PageDirectoryCap ptr data2))" 59 by (clarsimp simp: cap_master_arch_cap_def 60 split: arch_cap.split_asm)+ 61 62lemma 63 cap_master_arch_inv: 64 "cap_master_arch_cap (cap_master_arch_cap ac) = cap_master_arch_cap ac" 65 by (cases ac; simp add: cap_master_arch_cap_def) 66 67definition 68 "is_ap_cap cap \<equiv> case cap of (ArchObjectCap (arch_cap.ASIDPoolCap ap asid)) \<Rightarrow> True | _ \<Rightarrow> False" 69 70lemmas is_ap_cap_simps [simp] = is_ap_cap_def [split_simps cap.split arch_cap.split] 71 72definition 73 "reachable_pg_cap cap \<equiv> \<lambda>s. 74 is_pg_cap cap \<and> 75 (\<exists>vref. vs_cap_ref cap = Some vref \<and> (vref \<unrhd> obj_ref_of cap) s)" 76 77definition 78 replaceable_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool" 79where 80 "replaceable_final_arch_cap s sl newcap \<equiv> \<lambda>cap. 81 (\<forall>vref. vs_cap_ref cap = Some vref 82 \<longrightarrow> (vs_cap_ref newcap = Some vref 83 \<and> obj_refs newcap = obj_refs cap) 84 \<or> (\<forall>oref \<in> obj_refs cap. \<not> (vref \<unrhd> oref) s)) 85 \<and> no_cap_to_obj_with_diff_ref newcap {sl} s 86 \<and> ((is_pt_cap newcap \<or> is_pd_cap newcap) \<longrightarrow> cap_asid newcap = None 87 \<longrightarrow> (\<forall> r \<in> obj_refs newcap. 88 obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) 89 \<and> ((is_pt_cap newcap \<or> is_pd_cap newcap) 90 \<longrightarrow> ((is_pt_cap newcap \<and> is_pt_cap cap \<or> is_pd_cap newcap \<and> is_pd_cap cap) 91 \<longrightarrow> (cap_asid newcap = None \<longrightarrow> cap_asid cap = None) 92 \<longrightarrow> obj_refs cap \<noteq> obj_refs newcap) 93 \<longrightarrow> (\<forall>sl'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs newcap 94 \<and> (is_pd_cap newcap \<and> is_pd_cap cap' \<or> is_pt_cap newcap \<and> is_pt_cap cap') 95 \<and> (cap_asid newcap = None \<or> cap_asid cap' = None)) sl' s \<longrightarrow> sl' = sl)) 96 \<and> \<not>is_ap_cap newcap" 97 98definition 99 replaceable_non_final_arch_cap :: "'z::state_ext state \<Rightarrow> cslot_ptr \<Rightarrow> cap \<Rightarrow> cap \<Rightarrow> bool" 100where 101 "replaceable_non_final_arch_cap s sl newcap \<equiv> \<lambda>cap. \<not> reachable_pg_cap cap s" 102 103declare 104 replaceable_final_arch_cap_def[simp] 105 replaceable_non_final_arch_cap_def[simp] 106 107lemma unique_table_refsD: 108 "\<lbrakk> unique_table_refs cps; cps p = Some cap; cps p' = Some cap'; 109 obj_refs cap = obj_refs cap'\<rbrakk> 110 \<Longrightarrow> table_cap_ref cap = table_cap_ref cap'" 111 unfolding unique_table_refs_def 112 by blast 113 114lemma table_cap_ref_vs_cap_ref_Some: 115 "table_cap_ref x = Some y \<Longrightarrow> vs_cap_ref x = Some y" 116 by (clarsimp simp: table_cap_ref_def vs_cap_ref_def 117 split: cap.splits arch_cap.splits) 118 119lemma set_cap_valid_vs_lookup: 120 "\<lbrace>\<lambda>s. valid_vs_lookup s 121 \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s 122 \<longrightarrow> vs_cap_ref cap' = Some vref 123 \<longrightarrow> (vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap') 124 \<or> (\<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s) 125 \<or> (\<forall>oref. oref \<in> obj_refs cap' \<longrightarrow> \<not> (vref \<unrhd> oref) s)) 126 \<and> unique_table_refs (caps_of_state s)\<rbrace> 127 set_cap cap ptr 128 \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>" 129 apply (simp add: valid_vs_lookup_def 130 del: split_paired_All split_paired_Ex) 131 apply (rule hoare_pre) 132 apply (wp hoare_vcg_all_lift hoare_convert_imp[OF set_cap.vs_lookup_pages] 133 hoare_vcg_disj_lift) 134 apply (elim conjE allEI, rule impI, drule(1) mp) 135 apply (simp only: simp_thms) 136 apply (elim exE conjE) 137 apply (case_tac "p' = ptr") 138 apply (clarsimp simp: cte_wp_at_caps_of_state) 139 apply (elim disjE impCE) 140 apply fastforce 141 apply clarsimp 142 apply (drule (1) not_final_another_caps) 143 apply (erule obj_ref_is_gen_obj_ref) 144 apply (simp, elim exEI, clarsimp simp: gen_obj_refs_eq) 145 apply (rule conjI, clarsimp) 146 apply (drule(3) unique_table_refsD) 147 apply (clarsimp simp: reachable_pg_cap_def is_pg_cap_def) 148 apply (case_tac cap, simp_all add: vs_cap_ref_simps)[1] 149 apply (rename_tac arch_cap) 150 apply (case_tac arch_cap, 151 simp_all add: vs_cap_ref_simps table_cap_ref_simps)[1] 152 apply (clarsimp dest!: table_cap_ref_vs_cap_ref_Some) 153 apply fastforce 154 apply (clarsimp dest!: table_cap_ref_vs_cap_ref_Some)+ 155 apply (auto simp: cte_wp_at_caps_of_state)[1] 156 done 157 158crunch arch[wp]: set_cap "\<lambda>s. P (arch_state s)" (simp: split_def) 159 160lemma set_cap_valid_table_caps: 161 "\<lbrace>\<lambda>s. valid_table_caps s 162 \<and> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap = None 163 \<longrightarrow> (\<forall>r \<in> obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s))\<rbrace> 164 set_cap cap ptr 165 \<lbrace>\<lambda>rv. valid_table_caps\<rbrace>" 166 apply (simp add: valid_table_caps_def) 167 apply (wp hoare_vcg_all_lift 168 hoare_vcg_disj_lift hoare_convert_imp[OF set_cap_caps_of_state] 169 hoare_use_eq[OF set_cap_arch set_cap_obj_at_impossible]) 170 apply (simp add: empty_table_caps_of) 171 done 172 173lemma set_cap_unique_table_caps: 174 "\<lbrace>\<lambda>s. unique_table_caps (caps_of_state s) 175 \<and> ((is_pt_cap cap \<or> is_pd_cap cap) 176 \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> 177 (is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap) 178 \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) 179 \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) 180 \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap 181 \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') 182 \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace> 183 set_cap cap ptr 184 \<lbrace>\<lambda>rv s. unique_table_caps (caps_of_state s)\<rbrace>" 185 apply wp 186 apply (simp only: unique_table_caps_def) 187 apply (elim conjE) 188 apply (erule impCE) 189 apply clarsimp 190 apply (erule impCE) 191 prefer 2 192 apply (simp del: imp_disjL) 193 apply (thin_tac "\<forall>a b. P a b" for P) 194 apply (auto simp: cte_wp_at_caps_of_state)[1] 195 apply (clarsimp simp del: imp_disjL del: allI) 196 apply (case_tac "cap_asid cap \<noteq> None") 197 apply (clarsimp del: allI) 198 apply (elim allEI | rule impI)+ 199 apply (auto simp: is_pt_cap_def is_pd_cap_def)[1] 200 apply (elim allEI) 201 apply (intro conjI impI) 202 apply (elim allEI) 203 apply (auto simp: is_pt_cap_def is_pd_cap_def)[1] 204 apply (elim allEI) 205 apply (auto simp: is_pt_cap_def is_pd_cap_def)[1] 206 done 207 208lemma set_cap_unique_table_refs: 209 "\<lbrace>\<lambda>s. unique_table_refs (caps_of_state s) 210 \<and> no_cap_to_obj_with_diff_ref cap {ptr} s\<rbrace> 211 set_cap cap ptr 212 \<lbrace>\<lambda>rv s. unique_table_refs (caps_of_state s)\<rbrace>" 213 apply wp 214 apply clarsimp 215 apply (simp add: unique_table_refs_def 216 split del: if_split del: split_paired_All) 217 apply (erule allEI, erule allEI) 218 apply (clarsimp split del: if_split) 219 apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def 220 cte_wp_at_caps_of_state 221 split: if_split_asm) 222 done 223 224lemma set_cap_valid_arch_caps: 225 "\<lbrace>\<lambda>s. valid_arch_caps s 226 \<and> (\<forall>vref cap'. cte_wp_at ((=) cap') ptr s 227 \<longrightarrow> vs_cap_ref cap' = Some vref 228 \<longrightarrow> (vs_cap_ref cap = Some vref \<and> obj_refs cap = obj_refs cap') 229 \<or> (\<not> is_final_cap' cap' s \<and> \<not> reachable_pg_cap cap' s) 230 \<or> (\<forall>oref \<in> obj_refs cap'. \<not> (vref \<unrhd> oref) s)) 231 \<and> no_cap_to_obj_with_diff_ref cap {ptr} s 232 \<and> ((is_pt_cap cap \<or> is_pd_cap cap) \<longrightarrow> cap_asid cap = None 233 \<longrightarrow> (\<forall>r \<in> obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s)) 234 \<and> ((is_pt_cap cap \<or> is_pd_cap cap) 235 \<longrightarrow> (\<forall>oldcap. caps_of_state s ptr = Some oldcap \<longrightarrow> 236 (is_pt_cap cap \<and> is_pt_cap oldcap \<or> is_pd_cap cap \<and> is_pd_cap oldcap) 237 \<longrightarrow> (cap_asid cap = None \<longrightarrow> cap_asid oldcap = None) 238 \<longrightarrow> obj_refs oldcap \<noteq> obj_refs cap) 239 \<longrightarrow> (\<forall>ptr'. cte_wp_at (\<lambda>cap'. obj_refs cap' = obj_refs cap 240 \<and> (is_pd_cap cap \<and> is_pd_cap cap' \<or> is_pt_cap cap \<and> is_pt_cap cap') 241 \<and> (cap_asid cap = None \<or> cap_asid cap' = None)) ptr' s \<longrightarrow> ptr' = ptr))\<rbrace> 242 set_cap cap ptr 243 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 244 apply (simp add: valid_arch_caps_def pred_conj_def) 245 apply (wp set_cap_valid_vs_lookup set_cap_valid_table_caps 246 set_cap_unique_table_caps set_cap_unique_table_refs) 247 by simp_all blast+ 248 249lemma valid_table_capsD: 250 "\<lbrakk> cte_wp_at ((=) cap) ptr s; valid_table_caps s; 251 is_pt_cap cap | is_pd_cap cap; cap_asid cap = None \<rbrakk> 252 \<Longrightarrow> \<forall>r \<in> obj_refs cap. obj_at (empty_table (set (second_level_tables (arch_state s)))) r s" 253 apply (clarsimp simp: cte_wp_at_caps_of_state valid_table_caps_def) 254 apply (cases ptr, fastforce) 255 done 256 257lemma unique_table_capsD: 258 "\<lbrakk> unique_table_caps cps; cps ptr = Some cap; cps ptr' = Some cap'; 259 obj_refs cap = obj_refs cap'; cap_asid cap = None \<or> cap_asid cap' = None; 260 (is_pd_cap cap \<and> is_pd_cap cap') \<or> (is_pt_cap cap \<and> is_pt_cap cap') \<rbrakk> 261 \<Longrightarrow> ptr = ptr'" 262 unfolding unique_table_caps_def 263 by blast 264 265lemma set_cap_cap_refs_in_kernel_window[wp]: 266 "\<lbrace>cap_refs_in_kernel_window 267 and (\<lambda>s. \<forall>ref \<in> cap_range cap. arm_kernel_vspace (arch_state s) ref 268 = ArmVSpaceKernelWindow)\<rbrace> 269 set_cap cap p 270 \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 271 apply (simp add: cap_refs_in_kernel_window_def valid_refs_def2 272 pred_conj_def) 273 apply (rule hoare_lift_Pf2[where f=arch_state]) 274 apply wp 275 apply (fastforce elim!: ranE split: if_split_asm) 276 apply wp 277 done 278 279lemma cap_refs_in_kernel_windowD: 280 "\<lbrakk> caps_of_state s ptr = Some cap; cap_refs_in_kernel_window s \<rbrakk> 281 \<Longrightarrow> \<forall>ref \<in> cap_range cap. 282 arm_kernel_vspace (arch_state s) ref = ArmVSpaceKernelWindow" 283 apply (clarsimp simp: cap_refs_in_kernel_window_def valid_refs_def 284 cte_wp_at_caps_of_state) 285 apply (cases ptr, fastforce) 286 done 287 288lemma valid_cap_imp_valid_vm_rights: 289 "valid_cap (cap.ArchObjectCap (PageCap dev mw rs sz m)) s \<Longrightarrow> 290 rs \<in> valid_vm_rights" 291 by (simp add: valid_cap_def valid_vm_rights_def) 292 293lemma acap_rights_update_idem [simp]: 294 "acap_rights_update R (acap_rights_update R' cap) = acap_rights_update R cap" 295 by (simp add: acap_rights_update_def split: arch_cap.splits) 296 297lemma cap_master_arch_cap_rights [simp]: 298 "cap_master_arch_cap (acap_rights_update R cap) = cap_master_arch_cap cap" 299 by (simp add: cap_master_arch_cap_def acap_rights_update_def 300 split: arch_cap.splits) 301 302lemma acap_rights_update_id [intro!, simp]: 303 "valid_arch_cap ac s \<Longrightarrow> acap_rights_update (acap_rights ac) ac = ac" 304 unfolding acap_rights_update_def acap_rights_def valid_arch_cap_def 305 by (cases ac; simp) 306 307lemma obj_ref_none_no_asid: 308 "{} = obj_refs new_cap \<longrightarrow> None = table_cap_ref new_cap" 309 "obj_refs new_cap = {} \<longrightarrow> table_cap_ref new_cap = None" 310 by (simp add: table_cap_ref_def split: cap.split arch_cap.split)+ 311 312lemma set_cap_hyp_refs_of [wp]: 313 "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> 314 set_cap cp p 315 \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" 316 apply (simp add: set_cap_def set_object_def split_def) 317 apply (wp get_object_wp | wpc)+ 318 apply (auto elim!: rsubst[where P=P] 319 simp: ARM.state_hyp_refs_of_def obj_at_def 320 intro!: ext 321 split: if_split_asm) 322 done 323 324lemma state_hyp_refs_of_revokable[simp]: 325 "state_hyp_refs_of (s \<lparr> is_original_cap := m \<rparr>) = state_hyp_refs_of s" 326 by (simp add: state_hyp_refs_of_def) 327 328end 329 330end 331