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 SR_lemmas_C 12imports 13 StateRelation_C 14 "Refine.Invariants_H" 15begin 16 17(* FIXME: move to Word_Lib *) 18lemma sign_extend_0[simp]: 19 "sign_extend a 0 = 0" 20 by (simp add: sign_extend_def) 21 22context begin interpretation Arch . (*FIXME: arch_split*) 23 24(* FIXME: move to ainvs? *) 25lemma sign_extend_canonical_address: 26 "(x = sign_extend 47 x) = canonical_address x" 27 by (fastforce simp: sign_extended_iff_sign_extend canonical_address_sign_extended) 28 29section "ctes" 30 31subsection "capabilities" 32 33lemma cteMDBNode_cte_to_H [simp]: 34 "cteMDBNode (cte_to_H cte) = mdb_node_to_H (cteMDBNode_CL cte)" 35 unfolding cte_to_H_def 36 by simp 37 38lemma cteMDBNode_CL_lift [simp]: 39 "cte_lift cte' = Some ctel \<Longrightarrow> 40 mdb_node_lift (cteMDBNode_C cte') = cteMDBNode_CL ctel" 41 unfolding cte_lift_def 42 by (fastforce split: option.splits) 43 44lemma cteCap_cte_to_H [simp]: 45 "cteCap (cte_to_H cte) = cap_to_H (cap_CL cte)" 46 unfolding cte_to_H_def 47 by simp 48 49lemma cap_CL_lift [simp]: 50 "cte_lift cte' = Some ctel \<Longrightarrow> cap_lift (cte_C.cap_C cte') = Some (cap_CL ctel)" 51 unfolding cte_lift_def 52 by (fastforce split: option.splits) 53 54lemma cteCap_update_cte_to_H [simp]: 55 "\<lbrakk> cte_lift cte' = Some z; cap_lift cap' = Some capl\<rbrakk> 56 \<Longrightarrow> map_option cte_to_H (cte_lift (cte_C.cap_C_update (\<lambda>_. cap') cte')) = 57 Some (cteCap_update (\<lambda>_. cap_to_H capl) (cte_to_H z))" 58 unfolding cte_lift_def 59 by (clarsimp simp: cte_to_H_def split: option.splits) 60 61lemma cteMDBNode_C_update_lift [simp]: 62 "cte_lift cte' = Some ctel \<Longrightarrow> 63 (cte_lift (cteMDBNode_C_update (\<lambda>_. m) cte') = Some x) 64 = (cteMDBNode_CL_update (\<lambda>_. mdb_node_lift m) ctel = x)" 65 unfolding cte_lift_def 66 by (fastforce split: option.splits) 67 68lemma ccap_relationE: 69 "\<lbrakk>ccap_relation c v; \<And>vl. \<lbrakk> cap_lift v = Some vl; c = cap_to_H vl; c_valid_cap v\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 70 unfolding ccap_relation_def map_option_case 71 apply clarsimp 72 apply (drule sym) 73 apply (clarsimp split: option.splits) 74 done 75 76 77definition 78 "pageSize cap \<equiv> case cap of ArchObjectCap (PageCap f R ty sz dev m) \<Rightarrow> sz" 79 80definition 81 "isArchCap_tag (n :: machine_word) \<equiv> n mod 2 = 1" 82 83lemma isArchCap_tag_def2: 84 "isArchCap_tag n \<equiv> n && 1 = 1" 85 by (simp add: isArchCap_tag_def word_mod_2p_is_mask[where n=1, simplified] mask_def) 86 87lemma cap_get_tag_isCap0: 88 assumes cr: "ccap_relation cap cap'" 89 shows "(cap_get_tag cap' = scast cap_thread_cap) = isThreadCap cap 90 \<and> (cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap) 91 \<and> (cap_get_tag cap' = scast cap_notification_cap) = isNotificationCap cap 92 \<and> (cap_get_tag cap' = scast cap_endpoint_cap) = isEndpointCap cap 93 \<and> (cap_get_tag cap' = scast cap_irq_handler_cap) = isIRQHandlerCap cap 94 \<and> (cap_get_tag cap' = scast cap_irq_control_cap) = isIRQControlCap cap 95 \<and> (cap_get_tag cap' = scast cap_zombie_cap) = isZombie cap 96 \<and> (cap_get_tag cap' = scast cap_reply_cap) = isReplyCap cap 97 \<and> (cap_get_tag cap' = scast cap_untyped_cap) = isUntypedCap cap 98 \<and> (cap_get_tag cap' = scast cap_cnode_cap) = isCNodeCap cap 99 \<and> isArchCap_tag (cap_get_tag cap') = isArchCap \<top> cap 100 \<and> (cap_get_tag cap' = scast cap_frame_cap) = (isArchPageCap cap) 101 \<and> (cap_get_tag cap' = scast cap_domain_cap) = isDomainCap cap 102 \<and> (cap_get_tag cap' = scast cap_io_port_cap) = isArchIOPortCap cap 103 \<and> (cap_get_tag cap' = scast cap_io_port_control_cap) = isIOPortControlCap' cap" 104 using cr 105 apply - 106 apply (erule ccap_relationE) 107 apply (simp add: cap_to_H_def cap_lift_def Let_def isArchCap_tag_def2 isArchCap_def) 108 by (clarsimp simp: isCap_simps cap_tag_defs word_le_nat_alt pageSize_def Let_def 109 split: if_split_asm) \<comment> \<open>takes a while\<close> 110 111 112 113lemma cap_get_tag_isCap: 114 assumes cr: "ccap_relation cap cap'" 115 shows "(cap_get_tag cap' = scast cap_thread_cap) = (isThreadCap cap)" 116 and "(cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)" 117 and "(cap_get_tag cap' = scast cap_notification_cap) = (isNotificationCap cap)" 118 and "(cap_get_tag cap' = scast cap_endpoint_cap) = (isEndpointCap cap)" 119 and "(cap_get_tag cap' = scast cap_irq_handler_cap) = (isIRQHandlerCap cap)" 120 and "(cap_get_tag cap' = scast cap_irq_control_cap) = (isIRQControlCap cap)" 121 and "(cap_get_tag cap' = scast cap_zombie_cap) = (isZombie cap)" 122 and "(cap_get_tag cap' = scast cap_reply_cap) = isReplyCap cap" 123 and "(cap_get_tag cap' = scast cap_untyped_cap) = (isUntypedCap cap)" 124 and "(cap_get_tag cap' = scast cap_cnode_cap) = (isCNodeCap cap)" 125 and "isArchCap_tag (cap_get_tag cap') = isArchCap \<top> cap" 126 and "(cap_get_tag cap' = scast cap_frame_cap) = (isArchPageCap cap)" 127 and "(cap_get_tag cap' = scast cap_domain_cap) = isDomainCap cap" 128 and "(cap_get_tag cap' = scast cap_io_port_cap) = (isArchIOPortCap cap)" 129 and "(cap_get_tag cap' = scast cap_io_port_control_cap) = (isIOPortControlCap' cap)" 130 using cap_get_tag_isCap0 [OF cr] by auto 131 132lemma cap_get_tag_NullCap: 133 assumes cr: "ccap_relation cap cap'" 134 shows "(cap_get_tag cap' = scast cap_null_cap) = (cap = NullCap)" 135 using cr 136 apply - 137 apply (rule iffI) 138 apply (clarsimp simp add: cap_lifts cap_get_tag_isCap cap_to_H_def) 139 apply (simp add: cap_get_tag_isCap isCap_simps) 140 done 141 142lemma cap_get_tag_ThreadCap: 143 assumes cr: "ccap_relation cap cap'" 144 shows "(cap_get_tag cap' = scast cap_thread_cap) = 145 (cap = ThreadCap (ctcb_ptr_to_tcb_ptr (Ptr (cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap')))))" 146 using cr 147 apply - 148 apply (rule iffI) 149 apply (erule ccap_relationE) 150 apply (clarsimp simp add: cap_lifts cap_to_H_def) 151 apply (simp add: cap_get_tag_isCap isCap_simps) 152 done 153 154lemma cap_get_tag_NotificationCap: 155 assumes cr: "ccap_relation cap cap'" 156 shows "(cap_get_tag cap' = scast cap_notification_cap) = 157 (cap = NotificationCap 158 (capNtfnPtr_CL (cap_notification_cap_lift cap')) 159 (capNtfnBadge_CL (cap_notification_cap_lift cap')) 160 (to_bool (capNtfnCanSend_CL (cap_notification_cap_lift cap'))) 161 (to_bool (capNtfnCanReceive_CL (cap_notification_cap_lift cap'))))" 162 using cr 163 apply - 164 apply (rule iffI) 165 apply (erule ccap_relationE) 166 apply (clarsimp simp add: cap_lifts cap_to_H_def) 167 apply (simp add: cap_get_tag_isCap isCap_simps) 168 done 169 170lemma cap_get_tag_EndpointCap: 171 assumes cr: "ccap_relation cap cap'" 172 shows "(cap_get_tag cap' = scast cap_endpoint_cap) = 173 (cap = EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift cap')) 174 (capEPBadge_CL (cap_endpoint_cap_lift cap')) 175 (to_bool (capCanSend_CL (cap_endpoint_cap_lift cap'))) 176 (to_bool (capCanReceive_CL (cap_endpoint_cap_lift cap'))) 177 (to_bool (capCanGrant_CL (cap_endpoint_cap_lift cap'))))" 178 using cr 179 apply - 180 apply (rule iffI) 181 apply (erule ccap_relationE) 182 apply (clarsimp simp add: cap_lifts cap_to_H_def) 183 apply (simp add: cap_get_tag_isCap isCap_simps) 184 done 185 186lemma cap_get_tag_CNodeCap: 187 assumes cr: "ccap_relation cap cap'" 188 shows "(cap_get_tag cap' = scast cap_cnode_cap) = 189 (cap = capability.CNodeCap (capCNodePtr_CL (cap_cnode_cap_lift cap')) 190 (unat (capCNodeRadix_CL (cap_cnode_cap_lift cap'))) 191 (capCNodeGuard_CL (cap_cnode_cap_lift cap')) 192 (unat (capCNodeGuardSize_CL (cap_cnode_cap_lift cap'))))" 193 using cr 194 apply - 195 apply (rule iffI) 196 apply (erule ccap_relationE) 197 apply (clarsimp simp add: cap_lifts cap_to_H_def Let_def) 198 apply (simp add: cap_get_tag_isCap isCap_simps Let_def) 199 done 200 201lemma cap_get_tag_IRQHandlerCap: 202 assumes cr: "ccap_relation cap cap'" 203 shows "(cap_get_tag cap' = scast cap_irq_handler_cap) = 204 (cap = capability.IRQHandlerCap (ucast (capIRQ_CL (cap_irq_handler_cap_lift cap'))))" 205 using cr 206 apply - 207 apply (rule iffI) 208 apply (erule ccap_relationE) 209 apply (clarsimp simp add: cap_lifts cap_to_H_def) 210 apply (simp add: cap_get_tag_isCap isCap_simps) 211 done 212 213lemma cap_get_tag_IRQControlCap: 214 assumes cr: "ccap_relation cap cap'" 215 shows "(cap_get_tag cap' = scast cap_irq_control_cap) = 216 (cap = capability.IRQControlCap)" 217 using cr 218 apply - 219 apply (rule iffI) 220 apply (clarsimp simp add: cap_lifts cap_get_tag_isCap isCap_simps cap_to_H_def) 221 apply (simp add: cap_get_tag_isCap isCap_simps) 222 done 223 224lemma cap_get_tag_ZombieCap: 225 assumes cr: "ccap_relation cap cap'" 226 shows "(cap_get_tag cap' = scast cap_zombie_cap) = 227 (cap = 228 (if isZombieTCB_C (capZombieType_CL (cap_zombie_cap_lift cap')) 229 then capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask 5) ZombieTCB 230 (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask 5)) 231 else let radix = unat (capZombieType_CL (cap_zombie_cap_lift cap')) 232 in capability.Zombie (capZombieID_CL (cap_zombie_cap_lift cap') && ~~ mask (radix + 1)) 233 (ZombieCNode radix) 234 (unat (capZombieID_CL (cap_zombie_cap_lift cap') && mask (radix + 1)))))" 235 using cr 236 apply - 237 apply (rule iffI) 238 apply (erule ccap_relationE) 239 apply (clarsimp simp add: cap_lifts cap_to_H_def) 240 apply (simp add: cap_get_tag_isCap isCap_simps Let_def 241 split: if_split_asm) 242 done 243 244 245 246lemma cap_get_tag_ReplyCap: 247 assumes cr: "ccap_relation cap cap'" 248 shows "(cap_get_tag cap' = scast cap_reply_cap) = 249 (cap = 250 ReplyCap (ctcb_ptr_to_tcb_ptr (Ptr (cap_reply_cap_CL.capTCBPtr_CL (cap_reply_cap_lift cap')))) 251 (to_bool (capReplyMaster_CL (cap_reply_cap_lift cap'))))" 252 using cr 253 apply - 254 apply (rule iffI) 255 apply (erule ccap_relationE) 256 apply (clarsimp simp add: cap_lifts cap_to_H_def) 257 apply (simp add: cap_get_tag_isCap isCap_simps) 258 done 259 260lemma cap_get_tag_UntypedCap: 261 assumes cr: "ccap_relation cap cap'" 262 shows "(cap_get_tag cap' = scast cap_untyped_cap) = 263 (cap = UntypedCap (to_bool (capIsDevice_CL (cap_untyped_cap_lift cap'))) 264 (capPtr_CL (cap_untyped_cap_lift cap')) 265 (unat (capBlockSize_CL (cap_untyped_cap_lift cap'))) 266 (unat (capFreeIndex_CL (cap_untyped_cap_lift cap') << 4)))" 267 using cr 268 apply - 269 apply (rule iffI) 270 apply (erule ccap_relationE) 271 apply (clarsimp simp add: cap_lifts cap_to_H_def) 272 apply (simp add: cap_get_tag_isCap isCap_simps) 273 done 274 275lemma cap_get_tag_DomainCap: 276 assumes cr: "ccap_relation cap cap'" 277 shows "(cap_get_tag cap' = scast cap_domain_cap) = (cap = DomainCap)" 278 using cr 279 apply - 280 apply (rule iffI) 281 apply (clarsimp simp add: cap_lifts cap_get_tag_isCap cap_to_H_def) 282 apply (simp add: cap_get_tag_isCap isCap_simps) 283 done 284 285lemmas cap_get_tag_to_H_iffs = 286 cap_get_tag_NullCap 287 cap_get_tag_ThreadCap 288 cap_get_tag_NotificationCap 289 cap_get_tag_EndpointCap 290 cap_get_tag_CNodeCap 291 cap_get_tag_IRQHandlerCap 292 cap_get_tag_IRQControlCap 293 cap_get_tag_ZombieCap 294 cap_get_tag_UntypedCap 295 cap_get_tag_DomainCap 296 297lemmas cap_get_tag_to_H = cap_get_tag_to_H_iffs [THEN iffD1] 298 299subsection "mdb" 300 301lemma cmdbnode_relation_mdb_node_to_H [simp]: 302 "cte_lift cte' = Some y 303 \<Longrightarrow> cmdbnode_relation (mdb_node_to_H (cteMDBNode_CL y)) (cteMDBNode_C cte')" 304 unfolding cmdbnode_relation_def mdb_node_to_H_def mdb_node_lift_def cte_lift_def 305 by (fastforce split: option.splits) 306 307(* MOVE --- here down doesn't really belong here, maybe in a haskell specific file?*) 308lemma tcb_cte_cases_in_range1: 309 assumes tc:"tcb_cte_cases (y - x) = Some v" 310 and al: "is_aligned x tcbBlockSizeBits" 311 shows "x \<le> y" 312proof - 313 note objBits_defs [simp] 314 315 from tc obtain q where yq: "y = x + q" and qv: "q < 2 ^ 9" 316 unfolding tcb_cte_cases_def 317 by (simp add: diff_eq_eq split: if_split_asm) 318 319 have "x \<le> x + 2 ^ tcbBlockSizeBits - 1" using al 320 by (rule is_aligned_no_overflow) 321 322 hence "x \<le> x + q" using qv 323 apply simp 324 apply unat_arith 325 apply simp 326 done 327 328 thus ?thesis using yq by simp 329qed 330 331lemma tcb_cte_cases_in_range2: 332 assumes tc: "tcb_cte_cases (y - x) = Some v" 333 and al: "is_aligned x tcbBlockSizeBits" 334 shows "y \<le> x + 2 ^ tcbBlockSizeBits - 1" 335proof - 336 note objBits_defs [simp] 337 338 from tc obtain q where yq: "y = x + q" and qv: "q \<le> 2 ^ tcbBlockSizeBits - 1" 339 unfolding tcb_cte_cases_def 340 by (simp add: diff_eq_eq split: if_split_asm) 341 342 have "x + q \<le> x + (2 ^ tcbBlockSizeBits - 1)" using qv 343 apply (rule word_plus_mono_right) 344 apply (rule is_aligned_no_overflow' [OF al]) 345 done 346 347 thus ?thesis using yq by (simp add: field_simps) 348qed 349 350lemmas tcbSlots = 351 tcbCTableSlot_def tcbVTableSlot_def 352 tcbReplySlot_def tcbCallerSlot_def tcbIPCBufferSlot_def 353 354lemma updateObject_cte_tcb: 355 assumes tc: "tcb_cte_cases (ptr - ptr') = Some (accF, updF)" 356 shows "updateObject ctea (KOTCB tcb) ptr ptr' next = 357 (do alignCheck ptr' (objBits tcb); 358 magnitudeCheck ptr' next (objBits tcb); 359 return (KOTCB (updF (\<lambda>_. ctea) tcb)) 360 od)" 361 using tc unfolding tcb_cte_cases_def 362 apply - 363 apply (clarsimp simp add: updateObject_cte Let_def 364 tcb_cte_cases_def objBits_simps' tcbSlots shiftl_t2n 365 split: if_split_asm cong: if_cong) 366 done 367 368definition 369 tcb_no_ctes_proj :: "tcb \<Rightarrow> Structures_H.thread_state \<times> machine_word \<times> machine_word \<times> arch_tcb \<times> bool \<times> word8 \<times> word8 \<times> word8 \<times> nat \<times> fault option \<times> machine_word option" 370 where 371 "tcb_no_ctes_proj t \<equiv> (tcbState t, tcbFaultHandler t, tcbIPCBuffer t, tcbArch t, tcbQueued t, 372 tcbMCP t, tcbPriority t, tcbDomain t, tcbTimeSlice t, tcbFault t, tcbBoundNotification t)" 373 374lemma tcb_cte_cases_proj_eq [simp]: 375 "tcb_cte_cases p = Some (getF, setF) \<Longrightarrow> 376 tcb_no_ctes_proj tcb = tcb_no_ctes_proj (setF f tcb)" 377 unfolding tcb_no_ctes_proj_def tcb_cte_cases_def 378 by (auto split: if_split_asm) 379 380(* NOTE: 5 = cte_level_bits *) 381lemma map_to_ctes_upd_cte': 382 "\<lbrakk> ksPSpace s p = Some (KOCTE cte'); is_aligned p cte_level_bits; ps_clear p cte_level_bits s \<rbrakk> 383 \<Longrightarrow> map_to_ctes (ksPSpace s(p |-> KOCTE cte)) = (map_to_ctes (ksPSpace s))(p |-> cte)" 384 apply (erule (1) map_to_ctes_upd_cte) 385 apply (simp add: field_simps ps_clear_def3 cte_level_bits_def mask_def) 386 done 387 388lemma map_to_ctes_upd_tcb': 389 "[| ksPSpace s p = Some (KOTCB tcb'); is_aligned p tcbBlockSizeBits; 390 ps_clear p tcbBlockSizeBits s |] 391==> map_to_ctes (ksPSpace s(p |-> KOTCB tcb)) = 392 (%x. if EX getF setF. 393 tcb_cte_cases (x - p) = Some (getF, setF) & 394 getF tcb ~= getF tcb' 395 then case tcb_cte_cases (x - p) of 396 Some (getF, setF) => Some (getF tcb) 397 else ctes_of s x)" 398 apply (erule (1) map_to_ctes_upd_tcb) 399 apply (simp add: field_simps ps_clear_def3 mask_def objBits_defs) 400 done 401 402 403lemma tcb_cte_cases_inv [simp]: 404 "tcb_cte_cases p = Some (getF, setF) \<Longrightarrow> getF (setF (\<lambda>_. v) tcb) = v" 405 unfolding tcb_cte_cases_def 406 by (simp split: if_split_asm) 407 408declare insert_dom [simp] 409 410lemma in_alignCheck': 411 "(z \<in> fst (alignCheck x n s)) = (snd z = s \<and> is_aligned x n)" 412 by (cases z, simp) 413 414lemma fst_alignCheck_empty [simp]: 415 "(fst (alignCheck x n s) = {}) = (\<not> is_aligned x n)" 416 apply (subst all_not_in_conv [symmetric]) 417 apply (clarsimp simp: in_alignCheck') 418 done 419 420lemma fst_setCTE0: 421 notes option.case_cong_weak [cong] 422 assumes ct: "cte_at' dest s" 423 shows "\<exists>(v, s') \<in> fst (setCTE dest cte s). 424 (s' = s \<lparr> ksPSpace := ksPSpace s' \<rparr>) 425 \<and> (dom (ksPSpace s) = dom (ksPSpace s')) 426 \<and> (\<forall>x \<in> dom (ksPSpace s). 427 case (the (ksPSpace s x)) of 428 KOCTE _ \<Rightarrow> (\<exists>cte. ksPSpace s' x = Some (KOCTE cte)) 429 | KOTCB t \<Rightarrow> (\<exists>t'. ksPSpace s' x = Some (KOTCB t') \<and> tcb_no_ctes_proj t = tcb_no_ctes_proj t') 430 | _ \<Rightarrow> ksPSpace s' x = ksPSpace s x)" 431 using ct 432 apply - 433 apply (clarsimp simp: setCTE_def setObject_def 434 bind_def return_def assert_opt_def gets_def split_beta get_def 435 modify_def put_def) 436 apply (erule cte_wp_atE') 437 apply (rule ps_clear_lookupAround2, assumption+) 438 apply simp 439 apply (erule is_aligned_no_overflow) 440 apply (simp (no_asm_simp) del: fun_upd_apply cong: option.case_cong) 441 apply (simp add: return_def updateObject_cte 442 bind_def assert_opt_def gets_def split_beta get_def 443 modify_def put_def unless_def when_def 444 objBits_simps 445 cong: bex_cong) 446 apply (rule bexI [where x = "((), s)"]) 447 apply (frule_tac s' = s in in_magnitude_check [where v = "()"]) 448 apply (simp add: cte_level_bits_def) 449 apply assumption 450 apply (simp add: objBits_defs cte_level_bits_def) 451 apply (erule bexI [rotated]) 452 apply (simp cong: if_cong) 453 apply rule 454 apply (simp split: kernel_object.splits) 455 apply (fastforce simp: tcb_no_ctes_proj_def) 456 apply (simp add: cte_level_bits_def objBits_defs) 457 (* clag *) 458 apply (rule ps_clear_lookupAround2, assumption+) 459 apply (erule (1) tcb_cte_cases_in_range1) 460 apply (erule (1) tcb_cte_cases_in_range2) 461 apply (simp add: return_def del: fun_upd_apply cong: bex_cong option.case_cong) 462 apply (subst updateObject_cte_tcb) 463 apply assumption 464 apply (simp add: bind_def return_def assert_opt_def gets_def split_beta get_def when_def 465 modify_def put_def unless_def when_def in_alignCheck') 466 apply (simp add: objBits_simps) 467 apply (simp add: magnitudeCheck_def return_def split: option.splits 468 cong: bex_cong if_cong) 469 apply (simp split: kernel_object.splits) 470 apply (fastforce simp: tcb_no_ctes_proj_def) 471 apply (simp add: magnitudeCheck_def when_def return_def fail_def 472 linorder_not_less 473 split: option.splits 474 cong: bex_cong if_cong) 475 apply rule 476 apply (simp split: kernel_object.splits) 477 apply (fastforce simp: tcb_no_ctes_proj_def) 478 done 479 480 481(* duplicates *) 482lemma pspace_alignedD' [intro?]: 483 assumes lu: "ksPSpace s x = Some v" 484 and al: "pspace_aligned' s" 485 shows "is_aligned x (objBitsKO v)" 486 using al lu unfolding pspace_aligned'_def 487 apply - 488 apply (drule (1) bspec [OF _ domI]) 489 apply simp 490 done 491 492declare pspace_distinctD' [intro?] 493 494lemma ctes_of_ksI [intro?]: 495 fixes s :: "kernel_state" 496 assumes ks: "ksPSpace s x = Some (KOCTE cte)" 497 and pa: "pspace_aligned' s" (* yuck *) 498 and pd: "pspace_distinct' s" 499 shows "ctes_of s x = Some cte" 500proof (rule ctes_of_eq_cte_wp_at') 501 from ks show "cte_wp_at' ((=) cte) x s" 502 proof (rule cte_wp_at_cteI' [OF _ _ _ refl]) 503 from ks pa have "is_aligned x (objBitsKO (KOCTE cte))" .. 504 thus "is_aligned x cte_level_bits" 505 unfolding cte_level_bits_def by (simp add: objBits_simps') 506 507 from ks pd have "ps_clear x (objBitsKO (KOCTE cte)) s" .. 508 thus "ps_clear x cte_level_bits s" 509 unfolding cte_level_bits_def by (simp add: objBits_simps') 510 qed 511qed 512 513 514lemma fst_setCTE: 515 assumes ct: "cte_at' dest s" 516 and rl: "\<And>s'. \<lbrakk> ((), s') \<in> fst (setCTE dest cte s); 517 (s' = s \<lparr> ksPSpace := ksPSpace s' \<rparr>); 518 (ctes_of s' = ctes_of s(dest \<mapsto> cte)); 519 (map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s')); 520 (map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s')); 521 (map_to_pml4es (ksPSpace s) = map_to_pml4es (ksPSpace s')); 522 (map_to_pdptes (ksPSpace s) = map_to_pdptes (ksPSpace s')); 523 (map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s')); 524 (map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s')); 525 (map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s')); 526 (map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s')); 527 (map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s')); 528 (map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) 529 = map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')); 530 \<forall>T p. typ_at' T p s = typ_at' T p s'\<rbrakk> \<Longrightarrow> P" 531 shows "P" 532proof - 533 (* Unpack the existential and bind x, theorems in this. Yuck *) 534 from fst_setCTE0 [where cte = cte, OF ct] guess s' by clarsimp 535 note thms = this 536 537 from thms have ceq: "ctes_of s' = ctes_of s(dest \<mapsto> cte)" 538 apply - 539 apply (erule use_valid [OF _ setCTE_ctes_of_wp]) 540 apply simp 541 done 542 543 show ?thesis 544 proof (rule rl) 545 show "map_to_eps (ksPSpace s) = map_to_eps (ksPSpace s')" 546 proof (rule map_comp_eqI) 547 fix x 548 assume xin: "x \<in> dom (ksPSpace s')" 549 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 550 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 551 ultimately have "(projectKO_opt ko' :: endpoint option) = projectKO_opt ko" using xin thms(4) ceq 552 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_ep) 553 thus "(projectKO_opt (the (ksPSpace s' x)) :: endpoint option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 554 by simp 555 qed fact 556 557 (* clag \<dots> *) 558 show "map_to_ntfns (ksPSpace s) = map_to_ntfns (ksPSpace s')" 559 proof (rule map_comp_eqI) 560 fix x 561 assume xin: "x \<in> dom (ksPSpace s')" 562 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 563 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 564 ultimately have "(projectKO_opt ko' :: Structures_H.notification option) = projectKO_opt ko" using xin thms(4) ceq 565 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_ntfn) 566 thus "(projectKO_opt (the (ksPSpace s' x)) :: Structures_H.notification option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 567 by simp 568 qed fact 569 570 show "map_to_pml4es (ksPSpace s) = map_to_pml4es (ksPSpace s')" 571 proof (rule map_comp_eqI) 572 fix x 573 assume xin: "x \<in> dom (ksPSpace s')" 574 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 575 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 576 ultimately have "(projectKO_opt ko' :: pml4e option) = projectKO_opt ko" using xin thms(4) ceq 577 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pml4e) 578 thus "(projectKO_opt (the (ksPSpace s' x)) :: pml4e option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 579 by simp 580 qed fact 581 582 show "map_to_pdptes (ksPSpace s) = map_to_pdptes (ksPSpace s')" 583 proof (rule map_comp_eqI) 584 fix x 585 assume xin: "x \<in> dom (ksPSpace s')" 586 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 587 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 588 ultimately have "(projectKO_opt ko' :: pdpte option) = projectKO_opt ko" using xin thms(4) ceq 589 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pdpte) 590 thus "(projectKO_opt (the (ksPSpace s' x)) :: pdpte option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 591 by simp 592 qed fact 593 594 show "map_to_pdes (ksPSpace s) = map_to_pdes (ksPSpace s')" 595 proof (rule map_comp_eqI) 596 fix x 597 assume xin: "x \<in> dom (ksPSpace s')" 598 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 599 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 600 ultimately have "(projectKO_opt ko' :: pde option) = projectKO_opt ko" using xin thms(4) ceq 601 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pde) 602 thus "(projectKO_opt (the (ksPSpace s' x)) :: pde option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 603 by simp 604 qed fact 605 606 show "map_to_ptes (ksPSpace s) = map_to_ptes (ksPSpace s')" 607 proof (rule map_comp_eqI) 608 fix x 609 assume xin: "x \<in> dom (ksPSpace s')" 610 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 611 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 612 ultimately have "(projectKO_opt ko' :: pte option) = projectKO_opt ko" using xin thms(4) ceq 613 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_pte) 614 thus "(projectKO_opt (the (ksPSpace s' x)) :: pte option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 615 by simp 616 qed fact 617 618 show "map_to_asidpools (ksPSpace s) = map_to_asidpools (ksPSpace s')" 619 proof (rule map_comp_eqI) 620 fix x 621 assume xin: "x \<in> dom (ksPSpace s')" 622 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 623 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 624 ultimately have "(projectKO_opt ko' :: asidpool option) = projectKO_opt ko" using xin thms(4) ceq 625 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_asidpool) 626 thus "(projectKO_opt (the (ksPSpace s' x)) :: asidpool option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 627 by simp 628 qed fact 629 630 show "map_to_user_data (ksPSpace s) = map_to_user_data (ksPSpace s')" 631 proof (rule map_comp_eqI) 632 fix x 633 assume xin: "x \<in> dom (ksPSpace s')" 634 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 635 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 636 ultimately have "(projectKO_opt ko' :: user_data option) = projectKO_opt ko" using xin thms(4) ceq 637 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_user_data) 638 thus "(projectKO_opt (the (ksPSpace s' x)) :: user_data option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 639 by simp 640 qed fact 641 642 show "map_to_user_data_device (ksPSpace s) = map_to_user_data_device (ksPSpace s')" 643 proof (rule map_comp_eqI) 644 fix x 645 assume xin: "x \<in> dom (ksPSpace s')" 646 then obtain ko where ko: "ksPSpace s x = Some ko" by (clarsimp simp: thms(3)[symmetric]) 647 moreover from xin obtain ko' where ko': "ksPSpace s' x = Some ko'" by clarsimp 648 ultimately have "(projectKO_opt ko' :: user_data_device option) = projectKO_opt ko" using xin thms(4) ceq 649 by - (drule (1) bspec, cases ko, auto simp: projectKO_opt_user_data_device) 650 thus "(projectKO_opt (the (ksPSpace s' x)) :: user_data_device option) = projectKO_opt (the (ksPSpace s x))" using ko ko' 651 by simp 652 qed fact 653 654 655 note sta = setCTE_typ_at'[where P="\<lambda>x. x = y" for y] 656 show typ_at: "\<forall>T p. typ_at' T p s = typ_at' T p s'" 657 using use_valid[OF _ sta, OF thms(1), OF refl] 658 by auto 659 660 show "map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = 661 map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')" 662 proof (rule ext) 663 fix x 664 665 have dm: "dom (map_to_tcbs (ksPSpace s)) = dom (map_to_tcbs (ksPSpace s'))" 666 using thms(3) thms(4) 667 apply - 668 apply (rule set_eqI) 669 apply rule 670 apply (frule map_comp_subset_domD) 671 apply simp 672 apply (drule (1) bspec) 673 apply (clarsimp simp: projectKOs dom_map_comp) 674 apply (frule map_comp_subset_domD) 675 apply (drule (1) bspec) 676 apply (auto simp: dom_map_comp projectKOs split: kernel_object.splits) 677 apply fastforce 678 done 679 680 { 681 assume "x \<in> dom (map_to_tcbs (ksPSpace s))" 682 hence "map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s) x) 683 = map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s') x)" 684 using thms(3) thms(4) 685 apply - 686 apply (frule map_comp_subset_domD) 687 apply simp 688 apply (drule (1) bspec) 689 apply (clarsimp simp: dom_map_comp projectKOs projectKO_opt_tcb) 690 apply (case_tac y) 691 apply simp_all 692 apply clarsimp 693 done 694 } moreover 695 { 696 assume "x \<notin> dom (map_to_tcbs (ksPSpace s))" 697 hence "map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s) x) 698 = map_option tcb_no_ctes_proj (map_to_tcbs (ksPSpace s') x)" 699 apply - 700 apply (frule subst [OF dm]) 701 apply (simp add: dom_def) 702 done 703 } ultimately show "(map_option tcb_no_ctes_proj \<circ> (map_to_tcbs (ksPSpace s))) x 704 = (map_option tcb_no_ctes_proj \<circ> (map_to_tcbs (ksPSpace s'))) x" 705 by auto 706 qed 707 qed fact+ 708qed 709 710lemma ctes_of_cte_at: 711 "ctes_of s p = Some x \<Longrightarrow> cte_at' p s" 712 by (simp add: cte_wp_at_ctes_of) 713 714lemma cor_map_relI: 715 assumes dm: "dom am = dom am'" 716 and rl: "\<And>x y y' z. \<lbrakk> am x = Some y; am' x = Some y'; 717 rel y z \<rbrakk> \<Longrightarrow> rel y' z" 718 shows "cmap_relation am cm sz rel \<Longrightarrow> cmap_relation am' cm sz rel" 719 unfolding cmap_relation_def 720 apply - 721 apply clarsimp 722 apply rule 723 apply (simp add: dm) 724 apply rule 725 apply (frule_tac P = "\<lambda>s. x \<in> s" in ssubst [OF dm]) 726 apply (drule (1) bspec) 727 apply (erule domD [where m = am, THEN exE]) 728 apply (rule rl, assumption+) 729 apply (clarsimp simp add: dom_def) 730 apply simp 731 done 732 733lemma setCTE_tcb_case: 734 assumes om: "map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s) = 735 map_option tcb_no_ctes_proj \<circ> map_to_tcbs (ksPSpace s')" 736 and rel: "cmap_relation (map_to_tcbs (ksPSpace s)) (clift (t_hrs_' (globals x))) tcb_ptr_to_ctcb_ptr ctcb_relation" 737 shows "cmap_relation (map_to_tcbs (ksPSpace s')) (clift (t_hrs_' (globals x))) tcb_ptr_to_ctcb_ptr ctcb_relation" 738 using om 739proof (rule cor_map_relI [OF map_option_eq_dom_eq]) 740 fix x tcb tcb' z 741 assume y: "map_to_tcbs (ksPSpace s) x = Some tcb" 742 and y': "map_to_tcbs (ksPSpace s') x = Some tcb'" and rel: "ctcb_relation tcb z" 743 744 hence "tcb_no_ctes_proj tcb = tcb_no_ctes_proj tcb'" using om 745 apply - 746 apply (simp add: o_def) 747 apply (drule fun_cong [where x = x]) 748 apply simp 749 done 750 751 thus "ctcb_relation tcb' z" using rel 752 unfolding tcb_no_ctes_proj_def ctcb_relation_def cfault_rel_def 753 by auto 754qed fact+ 755 756lemma lifth_update: 757 "clift (t_hrs_' s) ptr = clift (t_hrs_' s') ptr 758 \<Longrightarrow> lifth ptr s = lifth ptr s'" 759 unfolding lifth_def 760 by simp 761 762lemma getCTE_exs_valid: 763 "cte_at' dest s \<Longrightarrow> \<lbrace>(=) s\<rbrace> getCTE dest \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>" 764 unfolding exs_valid_def getCTE_def cte_wp_at'_def 765 by clarsimp 766 767lemma cmap_domE1: 768 "\<lbrakk> f ` dom am = dom cm; am x = Some v; \<And>v'. cm (f x) = Some v' \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 769 apply (drule equalityD1) 770 apply (drule subsetD) 771 apply (erule imageI [OF domI]) 772 apply (clarsimp simp: dom_def) 773 done 774 775lemma cmap_domE2: 776 "\<lbrakk> f ` dom am = dom cm; cm x = Some v'; \<And>x' v. \<lbrakk> x = f x'; am x' = Some v \<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 777 apply (drule equalityD2) 778 apply (drule subsetD) 779 apply (erule domI) 780 apply (clarsimp simp: dom_def) 781 done 782 783lemma cmap_relationE1: 784 "\<lbrakk> cmap_relation am cm f rel; am x = Some y; 785 \<And>y'. \<lbrakk>am x = Some y; rel y y'; cm (f x) = Some y'\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 786 unfolding cmap_relation_def 787 apply clarsimp 788 apply (erule (1) cmap_domE1) 789 apply (drule (1) bspec [OF _ domI]) 790 apply clarsimp 791 done 792 793lemma cmap_relationE2: 794 "\<lbrakk> cmap_relation am cm f rel; cm x = Some y'; 795 \<And>x' y. \<lbrakk>x = f x'; rel y y'; am x' = Some y\<rbrakk> \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 796 unfolding cmap_relation_def 797 apply clarsimp 798 apply (erule (1) cmap_domE2) 799 apply (drule (1) bspec [OF _ domI]) 800 apply clarsimp 801 done 802 803lemma cmap_relationI: 804 assumes doms: "f ` dom am = dom cm" 805 and rel: "\<And>x v v'. \<lbrakk>am x = Some v; cm (f x) = Some v' \<rbrakk> \<Longrightarrow> rel v v'" 806 shows "cmap_relation am cm f rel" 807 unfolding cmap_relation_def using doms 808proof (rule conjI) 809 show "\<forall>x\<in>dom am. rel (the (am x)) (the (cm (f x)))" 810 proof 811 fix x 812 assume "x \<in> dom am" 813 then obtain v where "am x = Some v" .. 814 moreover with doms obtain v' where "cm (f x) = Some v'" by (rule cmap_domE1) 815 ultimately show "rel (the (am x)) (the (cm (f x)))" 816 by (simp add: rel) 817 qed 818qed 819 820lemma cmap_relation_relI: 821 assumes "cmap_relation am cm f rel" 822 and "am x = Some v" 823 and "cm (f x) = Some v'" 824 shows "rel v v'" 825 using assms 826 by (fastforce elim!: cmap_relationE1) 827 828lemma cspace_cte_relationE: 829 "\<lbrakk> cmap_relation am cm Ptr ccte_relation; am x = Some y; 830 \<And>z k'. \<lbrakk>cm (Ptr x) = Some k'; cte_lift k' = Some z; cte_to_H z = y; c_valid_cte k' \<rbrakk> \<Longrightarrow> P 831 \<rbrakk> \<Longrightarrow> P" 832 apply (erule (1) cmap_relationE1) 833 apply (clarsimp simp: ccte_relation_def map_option_Some_eq2) 834 done 835 836lemma cmdbnode_relationE: 837 "\<lbrakk>cmdbnode_relation m v; m = mdb_node_to_H (mdb_node_lift v) \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 838 unfolding cmdbnode_relation_def 839 apply (drule sym) 840 apply clarsimp 841 done 842 843(* Used when the rel changes as well *) 844lemma cmap_relation_upd_relI: 845 fixes am :: "machine_word \<rightharpoonup> 'a" and cm :: "'b typ_heap" 846 assumes cr: "cmap_relation am cm f rel" 847 and cof: "am dest = Some v" 848 and cl: "cm (f dest) = Some v'" 849 and cc: "rel' nv nv'" 850 and rel: "\<And>x ov ov'. \<lbrakk> x \<noteq> dest; am x = Some ov; cm (f x) = Some ov'; rel ov ov' \<rbrakk> \<Longrightarrow> rel' ov ov'" 851 and inj: "inj f" 852 shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel'" 853 using assms 854 apply - 855 apply (rule cmap_relationE1, assumption+) 856 apply clarsimp 857 apply (rule cmap_relationI) 858 apply (simp add: cmap_relation_def) 859 apply (case_tac "x = dest") 860 apply simp 861 apply (simp add: inj_eq split: if_split_asm) 862 apply (erule (2) rel) 863 apply (erule (2) cmap_relation_relI) 864 done 865 866lemma cmap_relation_updI: 867 fixes am :: "machine_word \<rightharpoonup> 'a" and cm :: "'b typ_heap" 868 assumes cr: "cmap_relation am cm f rel" 869 and cof: "am dest = Some v" 870 and cl: "cm (f dest) = Some v'" 871 and cc: "rel nv nv'" 872 and inj: "inj f" 873 shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel" 874 using cr cof cl cc 875 apply (rule cmap_relation_upd_relI) 876 apply simp 877 apply fact 878 done 879 880declare inj_Ptr[simp] 881 882(* Ugh *) 883lemma cpspace_cte_relation_upd_capI: 884 assumes cr: "cmap_relation (map_to_ctes am) (clift cm) Ptr ccte_relation" 885 and cof: "map_to_ctes am dest = Some cte" 886 and cl: "clift cm (Ptr dest) = Some cte'" 887 and cc: "ccap_relation capl cap" 888 shows "cmap_relation ((map_to_ctes am)(dest \<mapsto> (cteCap_update (\<lambda>_. capl) cte))) 889 ((clift cm)(Ptr dest \<mapsto> cte_C.cap_C_update (\<lambda>_. cap) cte')) Ptr ccte_relation" 890 using cr cof cl cc 891 apply - 892 apply (frule (2) cmap_relation_relI) 893 apply (erule (2) cmap_relation_updI) 894 apply (clarsimp elim!: ccap_relationE simp: map_comp_Some_iff ccte_relation_def) 895 apply (subst (asm) map_option_Some_eq2) 896 apply clarsimp 897 apply (simp add: c_valid_cte_def cl_valid_cte_def) 898 apply simp 899done 900 901lemma cte_to_H_mdb_node_update [simp]: 902 "cte_to_H (cteMDBNode_CL_update (\<lambda>_. m) cte) = 903 cteMDBNode_update (\<lambda>_. mdb_node_to_H m) (cte_to_H cte)" 904 unfolding cte_to_H_def 905 by simp 906 907lemma cspace_cte_relation_upd_mdbI: 908 assumes cr: "cmap_relation (map_to_ctes am) (clift cm) Ptr ccte_relation" 909 and cof: "map_to_ctes am dest = Some cte" 910 and cl: "clift cm (Ptr dest) = Some cte'" 911 and cc: "cmdbnode_relation mdbl m" 912 shows "cmap_relation ((map_to_ctes am)(dest \<mapsto> cteMDBNode_update (\<lambda>_. mdbl) cte)) 913 ((clift cm)(Ptr dest \<mapsto> cte_C.cteMDBNode_C_update (\<lambda>_. m) cte')) Ptr ccte_relation" 914 using cr cof cl cc 915 apply - 916 apply (frule (2) cmap_relation_relI) 917 apply (erule (2) cmap_relation_updI) 918 apply (clarsimp elim!: cmdbnode_relationE 919 simp: map_comp_Some_iff ccte_relation_def c_valid_cte_def cl_valid_cte_def map_option_Some_eq2) 920 apply simp 921done 922 923lemma mdb_node_to_H_mdbPrev_update[simp]: 924 "mdb_node_to_H (mdbPrev_CL_update (\<lambda>_. x) m) 925 = mdbPrev_update (\<lambda>_. x) (mdb_node_to_H m)" 926 unfolding mdb_node_to_H_def by simp 927 928lemma mdb_node_to_H_mdbNext_update[simp]: 929 "mdb_node_to_H (mdbNext_CL_update (\<lambda>_. x) m) 930 = mdbNext_update (\<lambda>_. x) (mdb_node_to_H m)" 931 unfolding mdb_node_to_H_def by simp 932 933lemma mdb_node_to_H_mdbRevocable_update[simp]: 934 "mdb_node_to_H (mdbRevocable_CL_update (\<lambda>_. x) m) 935 = mdbRevocable_update (\<lambda>_. to_bool x) (mdb_node_to_H m)" 936 unfolding mdb_node_to_H_def by simp 937 938lemma mdb_node_to_H_mdbFirstBadged_update[simp]: 939 "mdb_node_to_H (mdbFirstBadged_CL_update (\<lambda>_. x) m) 940 = mdbFirstBadged_update (\<lambda>_. to_bool x) (mdb_node_to_H m)" 941 unfolding mdb_node_to_H_def by simp 942 943declare to_bool_from_bool [simp] 944 945lemma mdbNext_to_H [simp]: 946 "mdbNext (mdb_node_to_H n) = mdbNext_CL n" 947 unfolding mdb_node_to_H_def 948 by simp 949 950lemma mdbPrev_to_H [simp]: 951 "mdbPrev (mdb_node_to_H n) = mdbPrev_CL n" 952 unfolding mdb_node_to_H_def 953 by simp 954 955lemmas ctes_of_not_0 [simp] = valid_mdbD3' [of s, rotated] for s 956 957(* For getting rid of the generated guards -- will probably break with c_guard*) 958lemma cte_bits_le_3 [simp]: "3 \<le> cte_level_bits" 959 by (simp add: objBits_defs cte_level_bits_def) 960 961lemma cte_bits_le_tcb_bits: "cte_level_bits \<le> tcbBlockSizeBits" 962 by (simp add: cte_level_bits_def objBits_defs) 963 964lemma ctes_of_aligned_bits: 965 assumes pa: "pspace_aligned' s" 966 and cof: "ctes_of s p = Some cte" 967 and bits: "bits \<le> cte_level_bits" 968 shows "is_aligned p bits" 969proof - 970 from cof have "cte_wp_at' ((=) cte) p s" 971 by (simp add: cte_wp_at_ctes_of) 972 thus ?thesis 973 apply - 974 apply (rule is_aligned_weaken[OF _ bits]) 975 apply (erule cte_wp_atE') 976 apply assumption 977 apply (simp add: tcb_cte_cases_def field_simps split: if_split_asm) 978 apply (fastforce elim: aligned_add_aligned[OF _ _ cte_bits_le_tcb_bits] 979 simp: is_aligned_def cte_level_bits_def)+ 980 apply (erule is_aligned_weaken[OF _ cte_bits_le_tcb_bits]) 981 done 982qed 983 984lemma mdbNext_not_zero_eq: 985 "cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr (*ja \<and> (is_aligned (mdbNext n) 3)*) 986 \<longrightarrow> (mdbNext n \<noteq> 0) = (s' \<in> {_. mdbNext_CL (mdb_node_lift n') \<noteq> 0})" 987 by (fastforce elim: cmdbnode_relationE) 988 989lemma mdbPrev_not_zero_eq: 990 "cmdbnode_relation n n' \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr (*ja\<and> (is_aligned (mdbPrev n) 3)*) 991 \<longrightarrow> (mdbPrev n \<noteq> 0) = (s' \<in> {_. mdbPrev_CL (mdb_node_lift n') \<noteq> 0})" 992 by (fastforce elim: cmdbnode_relationE) 993 994abbreviation 995 "nullCapPointers cte \<equiv> cteCap cte = NullCap \<and> mdbNext (cteMDBNode cte) = nullPointer \<and> mdbPrev (cteMDBNode cte) = nullPointer" 996 997lemma nullCapPointers_def: 998 "is_an_abbreviation" unfolding is_an_abbreviation_def by simp 999 1000lemma valid_mdb_ctes_of_next: 1001 "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbNext (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbNext (cteMDBNode cte)) s" 1002 unfolding valid_mdb'_def valid_mdb_ctes_def 1003 apply clarsimp 1004 apply (erule (2) valid_dlistE) 1005 apply (simp add: cte_wp_at_ctes_of) 1006 done 1007 1008lemma valid_mdb_ctes_of_prev: 1009 "\<lbrakk> valid_mdb' s; ctes_of s p = Some cte; mdbPrev (cteMDBNode cte) \<noteq> 0 \<rbrakk> \<Longrightarrow> cte_at' (mdbPrev (cteMDBNode cte)) s" 1010 unfolding valid_mdb'_def valid_mdb_ctes_def 1011 apply clarsimp 1012 apply (erule (2) valid_dlistE) 1013 apply (simp add: cte_wp_at_ctes_of) 1014 done 1015 1016end 1017 1018context kernel 1019begin 1020 1021lemma cmap_relation_tcb [intro]: 1022 "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_tcb_relation (ksPSpace s) (t_hrs_' (globals s'))" 1023 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1024 by (simp add: Let_def) 1025 1026lemma cmap_relation_ep [intro]: 1027 "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_ep_relation (ksPSpace s) (t_hrs_' (globals s'))" 1028 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1029 by (simp add: Let_def) 1030 1031lemma cmap_relation_ntfn [intro]: 1032 "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_ntfn_relation (ksPSpace s) (t_hrs_' (globals s'))" 1033 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1034 by (simp add: Let_def) 1035 1036lemma cmap_relation_cte [intro]: 1037 "(s, s') \<in> rf_sr \<Longrightarrow> cpspace_cte_relation (ksPSpace s) (t_hrs_' (globals s'))" 1038 unfolding rf_sr_def state_relation_def cstate_relation_def cpspace_relation_def 1039 by (simp add: Let_def) 1040 1041lemma rf_sr_cpspace_asidpool_relation: 1042 "(s, s') \<in> rf_sr 1043 \<Longrightarrow> cpspace_asidpool_relation (ksPSpace s) (t_hrs_' (globals s'))" 1044 by (clarsimp simp: rf_sr_def cstate_relation_def 1045 cpspace_relation_def Let_def) 1046 1047lemma rf_sr_cpte_relation: 1048 "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_ptes (ksPSpace s)) 1049 (cslift s') pte_Ptr cpte_relation" 1050 by (clarsimp simp: rf_sr_def cstate_relation_def 1051 Let_def cpspace_relation_def) 1052lemma rf_sr_cpde_relation: 1053 "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pdes (ksPSpace s)) 1054 (cslift s') pde_Ptr cpde_relation" 1055 by (clarsimp simp: rf_sr_def cstate_relation_def 1056 Let_def cpspace_relation_def) 1057 1058lemma rf_sr_cpdpte_relation: 1059 "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pdptes (ksPSpace s)) 1060 (cslift s') pdpte_Ptr cpdpte_relation" 1061 by (clarsimp simp: rf_sr_def cstate_relation_def 1062 Let_def cpspace_relation_def) 1063 1064lemma rf_sr_cpml4e_relation: 1065 "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation (map_to_pml4es (ksPSpace s)) 1066 (cslift s') pml4e_Ptr cpml4e_relation" 1067 by (clarsimp simp: rf_sr_def cstate_relation_def 1068 Let_def cpspace_relation_def) 1069 1070lemma rf_sr_cte_relation: 1071 "\<lbrakk> (s, s') \<in> rf_sr; ctes_of s src = Some cte; cslift s' (Ptr src) = Some cte' \<rbrakk> \<Longrightarrow> ccte_relation cte cte'" 1072 apply (drule cmap_relation_cte) 1073 apply (erule (2) cmap_relation_relI) 1074 done 1075 1076lemma ccte_relation_ccap_relation: 1077 "ccte_relation cte cte' \<Longrightarrow> ccap_relation (cteCap cte) (cte_C.cap_C cte')" 1078 unfolding ccte_relation_def ccap_relation_def c_valid_cte_def cl_valid_cte_def c_valid_cap_def cl_valid_cap_def 1079 by (clarsimp simp: map_option_Some_eq2 if_bool_eq_conj) 1080 1081lemma ccte_relation_cmdbnode_relation: 1082 "ccte_relation cte cte' \<Longrightarrow> cmdbnode_relation (cteMDBNode cte) (cte_C.cteMDBNode_C cte')" 1083 unfolding ccte_relation_def ccap_relation_def 1084 by (clarsimp simp: map_option_Some_eq2) 1085 1086lemma rf_sr_ctes_of_clift: 1087 assumes sr: "(s, s') \<in> rf_sr" 1088 and cof: "ctes_of s p = Some cte" 1089 shows "\<exists>cte'. cslift s' (Ptr p) = Some cte' \<and> cte_lift cte' \<noteq> None \<and> cte = cte_to_H (the (cte_lift cte')) 1090 \<and> c_valid_cte cte'" 1091proof - 1092 from sr have "cpspace_cte_relation (ksPSpace s) (t_hrs_' (globals s'))" .. 1093 thus ?thesis using cof 1094 apply (rule cspace_cte_relationE) 1095 apply clarsimp 1096 done 1097qed 1098 1099lemma c_valid_cte_eq: 1100 "c_valid_cte c = case_option True cl_valid_cte (cte_lift c)" 1101 apply (clarsimp simp: c_valid_cte_def cl_valid_cte_def c_valid_cap_def split: option.splits) 1102 apply (unfold cte_lift_def) 1103 apply simp 1104done 1105 1106lemma rf_sr_ctes_of_cliftE: 1107 assumes cof: "ctes_of s p = Some cte" 1108 assumes sr: "(s, s') \<in> rf_sr" 1109 and rl: "\<And>cte' ctel'. \<lbrakk>ctes_of s p = Some (cte_to_H ctel'); 1110 cslift s' (Ptr p) = Some cte'; 1111 cte_lift cte' = Some ctel'; 1112 cte = cte_to_H ctel' ; 1113 cl_valid_cte ctel'\<rbrakk> \<Longrightarrow> R" 1114 shows "R" 1115 using sr cof 1116 apply - 1117 apply (frule (1) rf_sr_ctes_of_clift) 1118 apply (elim conjE exE) 1119 apply (rule rl) 1120 apply simp 1121 apply assumption 1122 apply clarsimp 1123 apply clarsimp 1124 apply (clarsimp simp: c_valid_cte_eq) 1125 done 1126 1127lemma cstate_relation_only_t_hrs: 1128 "\<lbrakk> t_hrs_' s = t_hrs_' t; 1129 ksReadyQueues_' s = ksReadyQueues_' t; 1130 ksReadyQueuesL1Bitmap_' s = ksReadyQueuesL1Bitmap_' t; 1131 ksReadyQueuesL2Bitmap_' s = ksReadyQueuesL2Bitmap_' t; 1132 ksSchedulerAction_' s = ksSchedulerAction_' t; 1133 ksCurThread_' s = ksCurThread_' t; 1134 ksIdleThread_' s = ksIdleThread_' t; 1135 ksWorkUnitsCompleted_' s = ksWorkUnitsCompleted_' t; 1136 intStateIRQNode_' s = intStateIRQNode_' t; 1137 intStateIRQTable_' s = intStateIRQTable_' t; 1138 x86KSASIDTable_' s = x86KSASIDTable_' t; 1139 x64KSCurrentUserCR3_' s = x64KSCurrentUserCR3_' t; 1140 phantom_machine_state_' s = phantom_machine_state_' t; 1141 ghost'state_' s = ghost'state_' t; 1142 ksDomScheduleIdx_' s = ksDomScheduleIdx_' t; 1143 ksCurDomain_' s = ksCurDomain_' t; 1144 ksDomainTime_' s = ksDomainTime_' t; 1145 num_ioapics_' s = num_ioapics_' t; 1146 x86KSIRQState_' s = x86KSIRQState_' t 1147 \<rbrakk> 1148 \<Longrightarrow> cstate_relation a s = cstate_relation a t" 1149 unfolding cstate_relation_def 1150 by (clarsimp simp add: Let_def carch_state_relation_def cmachine_state_relation_def) 1151 1152lemma rf_sr_upd: 1153 assumes 1154 "(t_hrs_' (globals x)) = (t_hrs_' (globals y))" 1155 "(ksReadyQueues_' (globals x)) = (ksReadyQueues_' (globals y))" 1156 "(ksReadyQueuesL1Bitmap_' (globals x)) = (ksReadyQueuesL1Bitmap_' (globals y))" 1157 "(ksReadyQueuesL2Bitmap_' (globals x)) = (ksReadyQueuesL2Bitmap_' (globals y))" 1158 "(ksSchedulerAction_' (globals x)) = (ksSchedulerAction_' (globals y))" 1159 "(ksCurThread_' (globals x)) = (ksCurThread_' (globals y))" 1160 "(ksIdleThread_' (globals x)) = (ksIdleThread_' (globals y))" 1161 "(ksWorkUnitsCompleted_' (globals x)) = (ksWorkUnitsCompleted_' (globals y))" 1162 "intStateIRQNode_'(globals x) = intStateIRQNode_' (globals y)" 1163 "intStateIRQTable_'(globals x) = intStateIRQTable_' (globals y)" 1164 "x86KSASIDTable_' (globals x) = x86KSASIDTable_' (globals y)" 1165 "x64KSCurrentUserCR3_' (globals x) = x64KSCurrentUserCR3_' (globals y)" 1166 "phantom_machine_state_' (globals x) = phantom_machine_state_' (globals y)" 1167 "ghost'state_' (globals x) = ghost'state_' (globals y)" 1168 "ksDomScheduleIdx_' (globals x) = ksDomScheduleIdx_' (globals y)" 1169 "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)" 1170 "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)" 1171 "num_ioapics_' (globals x) = num_ioapics_' (globals y)" 1172 "x86KSIRQState_' (globals x) = x86KSIRQState_' (globals y)" 1173 shows "((a, x) \<in> rf_sr) = ((a, y) \<in> rf_sr)" 1174 unfolding rf_sr_def using assms 1175 by simp (rule cstate_relation_only_t_hrs, auto) 1176 1177lemma rf_sr_upd_safe[simp]: 1178 assumes rl: "(t_hrs_' (globals (g y))) = (t_hrs_' (globals y))" 1179 and rq: "(ksReadyQueues_' (globals (g y))) = (ksReadyQueues_' (globals y))" 1180 and rqL1: "(ksReadyQueuesL1Bitmap_' (globals (g y))) = (ksReadyQueuesL1Bitmap_' (globals y))" 1181 and rqL2: "(ksReadyQueuesL2Bitmap_' (globals (g y))) = (ksReadyQueuesL2Bitmap_' (globals y))" 1182 and sa: "(ksSchedulerAction_' (globals (g y))) = (ksSchedulerAction_' (globals y))" 1183 and ct: "(ksCurThread_' (globals (g y))) = (ksCurThread_' (globals y))" 1184 and it: "(ksIdleThread_' (globals (g y))) = (ksIdleThread_' (globals y))" 1185 and isn: "intStateIRQNode_'(globals (g y)) = intStateIRQNode_' (globals y)" 1186 and ist: "intStateIRQTable_'(globals (g y)) = intStateIRQTable_' (globals y)" 1187 and dsi: "ksDomScheduleIdx_' (globals (g y)) = ksDomScheduleIdx_' (globals y)" 1188 and cdom: "ksCurDomain_' (globals (g y)) = ksCurDomain_' (globals y)" 1189 and dt: "ksDomainTime_' (globals (g y)) = ksDomainTime_' (globals y)" 1190 and arch: 1191 "x86KSASIDTable_' (globals (g y)) = x86KSASIDTable_' (globals y)" 1192 "x64KSCurrentUserCR3_' (globals (g y)) = x64KSCurrentUserCR3_' (globals y)" 1193 "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)" 1194 "num_ioapics_' (globals (g y)) = num_ioapics_' (globals y)" 1195 "x86KSIRQState_' (globals (g y)) = x86KSIRQState_' (globals y)" 1196 and gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)" 1197 and wu: "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))" 1198 shows "((a, (g y)) \<in> rf_sr) = ((a, y) \<in> rf_sr)" 1199 using rl rq rqL1 rqL2 sa ct it isn ist arch wu gs dsi cdom dt by - (rule rf_sr_upd) 1200 1201(* More of a well-formed lemma, but \<dots> *) 1202lemma valid_mdb_cslift_next: 1203 assumes vmdb: "valid_mdb' s" 1204 and sr: "(s, s') \<in> rf_sr" 1205 and cof: "ctes_of s p = Some cte" 1206 and nz: "mdbNext (cteMDBNode cte) \<noteq> 0" 1207 shows "cslift s' (Ptr (mdbNext (cteMDBNode cte)) :: cte_C ptr) \<noteq> None" 1208proof - 1209 from vmdb cof nz obtain cten where 1210 "ctes_of s (mdbNext (cteMDBNode cte)) = Some cten" 1211 by (auto simp: cte_wp_at_ctes_of dest!: valid_mdb_ctes_of_next) 1212 1213 with sr show ?thesis 1214 apply - 1215 apply (drule (1) rf_sr_ctes_of_clift) 1216 apply clarsimp 1217 done 1218qed 1219 1220lemma valid_mdb_cslift_prev: 1221 assumes vmdb: "valid_mdb' s" 1222 and sr: "(s, s') \<in> rf_sr" 1223 and cof: "ctes_of s p = Some cte" 1224 and nz: "mdbPrev (cteMDBNode cte) \<noteq> 0" 1225 shows "cslift s' (Ptr (mdbPrev (cteMDBNode cte)) :: cte_C ptr) \<noteq> None" 1226proof - 1227 from vmdb cof nz obtain cten where 1228 "ctes_of s (mdbPrev (cteMDBNode cte)) = Some cten" 1229 by (auto simp: cte_wp_at_ctes_of dest!: valid_mdb_ctes_of_prev) 1230 1231 with sr show ?thesis 1232 apply - 1233 apply (drule (1) rf_sr_ctes_of_clift) 1234 apply clarsimp 1235 done 1236qed 1237 1238lemma rf_sr_cte_at_valid: 1239 "\<lbrakk> cte_wp_at' P (ptr_val p) s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (p :: cte_C ptr)" 1240 apply (clarsimp simp: cte_wp_at_ctes_of) 1241 apply (drule (1) rf_sr_ctes_of_clift) 1242 apply (clarsimp simp add: typ_heap_simps) 1243 done 1244 1245lemma rf_sr_cte_at_validD: 1246 "\<lbrakk> cte_wp_at' P p s; (s,s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c (Ptr p :: cte_C ptr)" 1247 by (simp add: rf_sr_cte_at_valid) 1248 1249(* MOVE *) 1250lemma ccap_relation_NullCap_iff: 1251 "(ccap_relation NullCap cap') = (cap_get_tag cap' = scast cap_null_cap)" 1252 unfolding ccap_relation_def 1253 by (clarsimp simp: map_option_Some_eq2 c_valid_cap_def cl_valid_cap_def 1254 cap_to_H_def cap_lift_def Let_def cap_tag_defs 1255 split: if_split) 1256 1257(* MOVE *) 1258lemma ko_at_valid_ntfn': 1259 "\<lbrakk> ko_at' ntfn p s; valid_objs' s \<rbrakk> \<Longrightarrow> valid_ntfn' ntfn s" 1260 apply (erule obj_atE') 1261 apply (erule (1) valid_objsE') 1262 apply (simp add: projectKOs valid_obj'_def) 1263 done 1264 1265(* MOVE *) 1266lemma ntfn_blocked_in_queueD: 1267 "\<lbrakk> st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnNotification ntfn)) thread \<sigma>; ko_at' ntfn' ntfn \<sigma>; invs' \<sigma> \<rbrakk> 1268 \<Longrightarrow> thread \<in> set (ntfnQueue (ntfnObj ntfn')) \<and> isWaitingNtfn (ntfnObj ntfn')" 1269 apply (drule sym_refs_st_tcb_atD') 1270 apply clarsimp 1271 apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs 1272 refs_of_rev'[where ko = "KONotification ntfn'", simplified]) 1273 apply (cases "ntfnObj ntfn'") 1274 apply (simp_all add: isWaitingNtfn_def) 1275 done 1276 1277(* MOVE *) 1278lemma valid_ntfn_isWaitingNtfnD: 1279 "\<lbrakk> valid_ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn) \<rbrakk> 1280 \<Longrightarrow> (ntfnQueue (ntfnObj ntfn)) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s) 1281 \<and> distinct (ntfnQueue (ntfnObj ntfn))" 1282 unfolding valid_ntfn'_def isWaitingNtfn_def 1283 by (clarsimp split: Structures_H.notification.splits ntfn.splits) 1284 1285lemma cmap_relation_ko_atD: 1286 fixes ko :: "'a :: pspace_storable" and mp :: "word32 \<rightharpoonup> 'a" 1287 assumes ps: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') f rel" 1288 and ko: "ko_at' ko ptr s" 1289 shows "\<exists>ko'. cslift s' (f ptr) = Some ko' \<and> rel ko ko'" 1290 using ps ko unfolding cmap_relation_def 1291 apply clarsimp 1292 apply (drule bspec [where x = "ptr"]) 1293 apply (clarsimp simp: obj_at'_def projectKOs) 1294 apply (clarsimp simp: obj_at'_def projectKOs) 1295 apply (drule equalityD1) 1296 apply (drule subsetD [where c = "f ptr"]) 1297 apply (rule imageI) 1298 apply clarsimp 1299 apply clarsimp 1300 done 1301 1302lemma cmap_relation_ko_atE: 1303 fixes ko :: "'a :: pspace_storable" and mp :: "word32 \<rightharpoonup> 'a" 1304 assumes ps: "cmap_relation (projectKO_opt \<circ>\<^sub>m (ksPSpace s)) (cslift s') f rel" 1305 and ko: "ko_at' ko ptr s" 1306 and rl: "\<And>ko'. \<lbrakk>cslift s' (f ptr) = Some ko'; rel ko ko'\<rbrakk> \<Longrightarrow> P" 1307 shows P 1308 using ps ko 1309 apply - 1310 apply (drule (1) cmap_relation_ko_atD) 1311 apply (clarsimp) 1312 apply (erule (1) rl) 1313 done 1314 1315lemma ntfn_to_ep_queue: 1316 assumes ko: "ko_at' ntfn' ntfn s" 1317 and waiting: "isWaitingNtfn (ntfnObj ntfn')" 1318 and rf: "(s, s') \<in> rf_sr" 1319 shows "ep_queue_relation' (cslift s') (ntfnQueue (ntfnObj ntfn')) 1320 (Ptr (ntfnQueue_head_CL 1321 (notification_lift (the (cslift s' (Ptr ntfn)))))) 1322 (Ptr (ntfnQueue_tail_CL 1323 (notification_lift (the (cslift s' (Ptr ntfn))))))" 1324proof - 1325 from rf have 1326 "cmap_relation (map_to_ntfns (ksPSpace s)) (cslift s') Ptr (cnotification_relation (cslift s'))" 1327 by (rule cmap_relation_ntfn) 1328 1329 thus ?thesis using ko waiting 1330 apply - 1331 apply (erule (1) cmap_relation_ko_atE) 1332 apply (clarsimp simp: cnotification_relation_def Let_def isWaitingNtfn_def 1333 split: Structures_H.notification.splits ntfn.splits) 1334 done 1335qed 1336 1337lemma map_to_tcbs_from_tcb_at: 1338 "tcb_at' thread s \<Longrightarrow> map_to_tcbs (ksPSpace s) thread \<noteq> None" 1339 unfolding obj_at'_def 1340 by (clarsimp simp: projectKOs) 1341 1342lemma tcb_at_h_t_valid: 1343 "\<lbrakk> tcb_at' thread s; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread" 1344 apply (drule cmap_relation_tcb) 1345 apply (drule map_to_tcbs_from_tcb_at) 1346 apply (clarsimp simp add: cmap_relation_def) 1347 apply (drule (1) bspec [OF _ domI]) 1348 apply (clarsimp simp add: dom_def tcb_ptr_to_ctcb_ptr_def image_def) 1349 apply (drule equalityD1) 1350 apply (drule subsetD) 1351 apply simp 1352 apply (rule exI [where x = thread]) 1353 apply simp 1354 apply (clarsimp simp: typ_heap_simps) 1355 done 1356 1357lemma st_tcb_at_h_t_valid: 1358 "\<lbrakk> st_tcb_at' P thread s; (s, s') \<in> rf_sr \<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread" 1359 apply (drule pred_tcb_at') 1360 apply (erule (1) tcb_at_h_t_valid) 1361 done 1362 1363(* MOVE *) 1364lemma exs_getObject: 1365 assumes x: "\<And>q n ko. loadObject p q n ko = 1366 (loadObject_default p q n ko :: ('a :: pspace_storable) kernel)" 1367 assumes P: "\<And>(v::'a::pspace_storable). (1 :: machine_word) < 2 ^ (objBits v)" 1368 and objat: "obj_at' (P :: ('a::pspace_storable \<Rightarrow> bool)) p s" 1369 shows "\<lbrace>(=) s\<rbrace> getObject p \<exists>\<lbrace>\<lambda>r :: ('a :: pspace_storable). (=) s\<rbrace>" 1370 using objat unfolding exs_valid_def obj_at'_def 1371 apply clarsimp 1372 apply (rule_tac x = "(the (projectKO_opt ko), s)" in bexI) 1373 apply (clarsimp simp: split_def) 1374 apply (simp add: projectKO_def fail_def split: option.splits) 1375 apply (clarsimp simp: loadObject_default_def getObject_def in_monad return_def lookupAround2_char1 1376 split_def x P lookupAround2_char1 projectKOs 1377 objBits_def[symmetric] in_magnitude_check project_inject) 1378 done 1379 1380 1381lemma setObject_eq: 1382 fixes ko :: "('a :: pspace_storable)" 1383 assumes x: "\<And>(val :: 'a) old ptr ptr' next. updateObject val old ptr ptr' next = 1384 (updateObject_default val old ptr ptr' next :: kernel_object kernel)" 1385 assumes P: "\<And>(v::'a::pspace_storable). (1 :: machine_word) < 2 ^ (objBits v)" 1386 and ob: "\<And>(v :: 'a) (v' :: 'a). objBits v = objBits v'" 1387 and objat: "obj_at' (P :: ('a::pspace_storable \<Rightarrow> bool)) p s" 1388 shows "((), s\<lparr> ksPSpace := (ksPSpace s)(p \<mapsto> injectKO ko)\<rparr>) \<in> fst (setObject p ko s)" 1389 using objat unfolding setObject_def obj_at'_def 1390 apply (clarsimp simp: updateObject_default_def in_monad return_def lookupAround2_char1 1391 split_def x P lookupAround2_char1 projectKOs 1392 objBits_def[symmetric] in_magnitude_check project_inject) 1393 apply (frule ssubst [OF ob, where P = "is_aligned p" and v1 = ko]) 1394 apply (simp add: P in_magnitude_check) 1395 apply (rule conjI) 1396 apply (rule_tac x = obj in exI) 1397 apply simp 1398 apply (erule ssubst [OF ob]) 1399 done 1400 1401lemma getObject_eq: 1402 fixes ko :: "'a :: pspace_storable" 1403 assumes x: "\<And>q n ko. loadObject p q n ko = 1404 (loadObject_default p q n ko :: 'a kernel)" 1405 assumes P: "\<And>(v::'a). (1 :: machine_word) < 2 ^ (objBits v)" 1406 and objat: "ko_at' ko p s" 1407 shows "(ko, s) \<in> fst (getObject p s)" 1408 using objat unfolding exs_valid_def obj_at'_def 1409 apply clarsimp 1410 apply (simp add: projectKO_def fail_def split: option.splits) 1411 apply (clarsimp simp: loadObject_default_def getObject_def in_monad return_def lookupAround2_char1 1412 split_def x P lookupAround2_char2 projectKOs 1413 objBits_def[symmetric] in_magnitude_check project_inject) 1414 done 1415 1416lemma threadSet_eq: 1417 "ko_at' tcb thread s \<Longrightarrow> 1418 ((), s\<lparr> ksPSpace := (ksPSpace s)(thread \<mapsto> injectKO (f tcb))\<rparr>) \<in> fst (threadSet f thread s)" 1419 unfolding threadSet_def 1420 apply (clarsimp simp add: in_monad) 1421 apply (rule exI) 1422 apply (rule exI) 1423 apply (rule conjI) 1424 apply (rule getObject_eq) 1425 apply simp 1426 apply (simp add: objBits_simps') 1427 apply assumption 1428 apply (drule setObject_eq [rotated -1]) 1429 apply simp 1430 apply (simp add: objBits_simps') 1431 apply (simp add: objBits_simps) 1432 apply simp 1433 done 1434 1435definition 1436 "tcb_null_ep_ptrs a \<equiv> a \<lparr> tcbEPNext_C := NULL, tcbEPPrev_C := NULL \<rparr>" 1437 1438definition 1439 "tcb_null_sched_ptrs a \<equiv> a \<lparr> tcbSchedNext_C := NULL, tcbSchedPrev_C := NULL \<rparr>" 1440 1441definition 1442 "tcb_null_queue_ptrs a \<equiv> a \<lparr> tcbSchedNext_C := NULL, tcbSchedPrev_C := NULL, tcbEPNext_C := NULL, tcbEPPrev_C := NULL\<rparr>" 1443 1444lemma null_sched_queue: 1445 "map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp' 1446 \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp'" 1447 apply (rule ext) 1448 apply (erule_tac x = x in map_option_comp_eqE) 1449 apply simp 1450 apply (clarsimp simp: tcb_null_queue_ptrs_def tcb_null_sched_ptrs_def) 1451 done 1452 1453lemma null_ep_queue: 1454 "map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp' 1455 \<Longrightarrow> map_option tcb_null_queue_ptrs \<circ> mp = map_option tcb_null_queue_ptrs \<circ> mp'" 1456 apply (rule ext) 1457 apply (erule_tac x = x in map_option_comp_eqE) 1458 apply simp 1459 apply (case_tac v, case_tac v') 1460 apply (clarsimp simp: tcb_null_queue_ptrs_def tcb_null_ep_ptrs_def) 1461 done 1462 1463lemma null_sched_epD: 1464 assumes om: "map_option tcb_null_sched_ptrs \<circ> mp = map_option tcb_null_sched_ptrs \<circ> mp'" 1465 shows "map_option tcbEPNext_C \<circ> mp = map_option tcbEPNext_C \<circ> mp' \<and> 1466 map_option tcbEPPrev_C \<circ> mp = map_option tcbEPPrev_C \<circ> mp'" 1467 using om 1468 apply - 1469 apply (rule conjI) 1470 apply (rule ext) 1471 apply (erule_tac x = x in map_option_comp_eqE ) 1472 apply simp 1473 apply (case_tac v, case_tac v') 1474 apply (clarsimp simp: tcb_null_sched_ptrs_def) 1475 apply (rule ext) 1476 apply (erule_tac x = x in map_option_comp_eqE ) 1477 apply simp 1478 apply (case_tac v, case_tac v') 1479 apply (clarsimp simp: tcb_null_sched_ptrs_def) 1480 done 1481 1482lemma null_ep_schedD: 1483 assumes om: "map_option tcb_null_ep_ptrs \<circ> mp = map_option tcb_null_ep_ptrs \<circ> mp'" 1484 shows "map_option tcbSchedNext_C \<circ> mp = map_option tcbSchedNext_C \<circ> mp' \<and> 1485 map_option tcbSchedPrev_C \<circ> mp = map_option tcbSchedPrev_C \<circ> mp'" 1486 using om 1487 apply - 1488 apply (rule conjI) 1489 apply (rule ext) 1490 apply (erule_tac x = x in map_option_comp_eqE ) 1491 apply simp 1492 apply (case_tac v, case_tac v') 1493 apply (clarsimp simp: tcb_null_ep_ptrs_def) 1494 apply (rule ext) 1495 apply (erule_tac x = x in map_option_comp_eqE ) 1496 apply simp 1497 apply (case_tac v, case_tac v') 1498 apply (clarsimp simp: tcb_null_ep_ptrs_def) 1499 done 1500 1501lemma cmap_relation_cong: 1502 assumes adom: "dom am = dom am'" 1503 and cdom: "dom cm = dom cm'" 1504 and rel: "\<And>p a a' b b'. 1505 \<lbrakk> am p = Some a; am' p = Some a'; cm (f p) = Some b; cm' (f p) = Some b' \<rbrakk> \<Longrightarrow> rel a b = rel' a' b'" 1506 shows "cmap_relation am cm f rel = cmap_relation am' cm' f rel'" 1507 unfolding cmap_relation_def 1508 apply (clarsimp simp: adom cdom) 1509 apply (rule iffI) 1510 apply simp 1511 apply (erule conjE) 1512 apply (drule equalityD1) 1513 apply (rule ballI) 1514 apply (drule (1) bspec) 1515 apply (erule iffD1 [OF rel, rotated -1]) 1516 apply (rule Some_the, erule ssubst [OF adom]) 1517 apply (erule Some_the) 1518 apply (rule Some_the [where f = cm]) 1519 apply (drule subsetD) 1520 apply (erule imageI) 1521 apply (simp add: cdom) 1522 apply (rule Some_the [where f = cm']) 1523 apply (erule subsetD) 1524 apply (erule imageI) 1525 \<comment> \<open>clag\<close> 1526 apply simp 1527 apply (erule conjE) 1528 apply (drule equalityD1) 1529 apply (rule ballI) 1530 apply (drule (1) bspec) 1531 apply (erule iffD2 [OF rel, rotated -1]) 1532 apply (rule Some_the, erule ssubst [OF adom]) 1533 apply (erule Some_the) 1534 apply (rule Some_the [where f = cm]) 1535 apply (drule subsetD) 1536 apply (erule imageI) 1537 apply (simp add: cdom) 1538 apply (rule Some_the [where f = cm']) 1539 apply (erule subsetD) 1540 apply (erule imageI) 1541 done 1542 1543lemma ctcb_relation_null_queue_ptrs: 1544 assumes rel: "cmap_relation mp mp' tcb_ptr_to_ctcb_ptr ctcb_relation" 1545 and same: "map_option tcb_null_queue_ptrs \<circ> mp'' = map_option tcb_null_queue_ptrs \<circ> mp'" 1546 shows "cmap_relation mp mp'' tcb_ptr_to_ctcb_ptr ctcb_relation" 1547 using rel 1548 apply (rule iffD1 [OF cmap_relation_cong, OF _ map_option_eq_dom_eq, rotated -1]) 1549 apply simp 1550 apply (rule same [symmetric]) 1551 apply (drule compD [OF same]) 1552 apply (case_tac b, case_tac b') 1553 apply (simp add: ctcb_relation_def tcb_null_queue_ptrs_def) 1554 done 1555 1556lemma map_to_ko_atI': 1557 "\<lbrakk>(projectKO_opt \<circ>\<^sub>m (ksPSpace s)) x = Some v; invs' s\<rbrakk> \<Longrightarrow> ko_at' v x s" 1558 apply (clarsimp simp: map_comp_Some_iff) 1559 apply (erule aligned_distinct_obj_atI') 1560 apply clarsimp 1561 apply clarsimp 1562 apply (simp add: project_inject) 1563 done 1564 1565(* FIXME x64: do we still need these? 1566(* Levity: added (20090419 09:44:27) *) 1567declare ntfnQueue_head_mask_4 [simp] 1568 1569lemma ntfnQueue_tail_mask_4 [simp]: 1570 "ntfnQueue_tail_CL (notification_lift ko') && ~~ mask 4 = ntfnQueue_tail_CL (notification_lift ko')" 1571 unfolding notification_lift_def 1572 apply (clarsimp simp: mask_def word_bw_assocs sign_extend_def) 1573 apply word_bitwise *) 1574 1575lemma map_to_ctes_upd_tcb_no_ctes: 1576 "\<lbrakk>ko_at' tcb thread s ; \<forall>x\<in>ran tcb_cte_cases. (\<lambda>(getF, setF). getF tcb' = getF tcb) x \<rbrakk> 1577 \<Longrightarrow> map_to_ctes (ksPSpace s(thread \<mapsto> KOTCB tcb')) = map_to_ctes (ksPSpace s)" 1578 apply (erule obj_atE') 1579 apply (simp add: projectKOs objBits_simps) 1580 apply (subst map_to_ctes_upd_tcb') 1581 apply assumption+ 1582 apply (rule ext) 1583 apply (clarsimp split: if_split) 1584 apply (drule (1) bspec [OF _ ranI]) 1585 apply simp 1586 done 1587 1588lemma update_ntfn_map_tos: 1589 fixes P :: "Structures_H.notification \<Rightarrow> bool" 1590 assumes at: "obj_at' P p s" 1591 shows "map_to_eps (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_eps (ksPSpace s)" 1592 and "map_to_tcbs (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_tcbs (ksPSpace s)" 1593 and "map_to_ctes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_ctes (ksPSpace s)" 1594 and "map_to_pml4es (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_pml4es (ksPSpace s)" 1595 and "map_to_pdptes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_pdptes (ksPSpace s)" 1596 and "map_to_pdes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_pdes (ksPSpace s)" 1597 and "map_to_ptes (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_ptes (ksPSpace s)" 1598 and "map_to_asidpools (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_asidpools (ksPSpace s)" 1599 and "map_to_user_data (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_user_data (ksPSpace s)" 1600 and "map_to_user_data_device (ksPSpace s(p \<mapsto> KONotification ko)) = map_to_user_data_device (ksPSpace s)" 1601 using at 1602 by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI 1603 simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+ 1604 1605lemma update_ep_map_tos: 1606 fixes P :: "endpoint \<Rightarrow> bool" 1607 assumes at: "obj_at' P p s" 1608 shows "map_to_ntfns (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ntfns (ksPSpace s)" 1609 and "map_to_tcbs (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_tcbs (ksPSpace s)" 1610 and "map_to_ctes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ctes (ksPSpace s)" 1611 and "map_to_pml4es (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_pml4es (ksPSpace s)" 1612 and "map_to_pdptes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_pdptes (ksPSpace s)" 1613 and "map_to_pdes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_pdes (ksPSpace s)" 1614 and "map_to_ptes (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_ptes (ksPSpace s)" 1615 and "map_to_asidpools (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_asidpools (ksPSpace s)" 1616 and "map_to_user_data (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_user_data (ksPSpace s)" 1617 and "map_to_user_data_device (ksPSpace s(p \<mapsto> KOEndpoint ko)) = map_to_user_data_device (ksPSpace s)" 1618 using at 1619 by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI 1620 simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+ 1621 1622lemma update_tcb_map_tos: 1623 fixes P :: "tcb \<Rightarrow> bool" 1624 assumes at: "obj_at' P p s" 1625 shows "map_to_eps (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_eps (ksPSpace s)" 1626 and "map_to_ntfns (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_ntfns (ksPSpace s)" 1627 and "map_to_pml4es (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pml4es (ksPSpace s)" 1628 and "map_to_pdptes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pdptes (ksPSpace s)" 1629 and "map_to_pdes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_pdes (ksPSpace s)" 1630 and "map_to_ptes (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_ptes (ksPSpace s)" 1631 and "map_to_asidpools (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_asidpools (ksPSpace s)" 1632 and "map_to_user_data (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_user_data (ksPSpace s)" 1633 and "map_to_user_data_device (ksPSpace s(p \<mapsto> KOTCB ko)) = map_to_user_data_device (ksPSpace s)" 1634 using at 1635 by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI 1636 simp: projectKOs projectKO_opts_defs split: kernel_object.splits if_split_asm)+ 1637 1638lemma update_asidpool_map_tos: 1639 fixes P :: "asidpool \<Rightarrow> bool" 1640 assumes at: "obj_at' P p s" 1641 shows "map_to_ntfns (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ntfns (ksPSpace s)" 1642 and "map_to_tcbs (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_tcbs (ksPSpace s)" 1643 and "map_to_ctes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ctes (ksPSpace s)" 1644 and "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ko))) = map_to_pml4es (ksPSpace s)" 1645 and "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ko))) = map_to_pdptes (ksPSpace s)" 1646 and "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_pdes (ksPSpace s)" 1647 and "map_to_ptes (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_ptes (ksPSpace s)" 1648 and "map_to_eps (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_eps (ksPSpace s)" 1649 and "map_to_user_data (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data (ksPSpace s)" 1650 and "map_to_user_data_device (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) = map_to_user_data_device (ksPSpace s)" 1651 1652 using at 1653 by (auto elim!: obj_atE' intro!: map_to_ctes_upd_other map_comp_eqI 1654 simp: projectKOs projectKO_opts_defs 1655 split: if_split if_split_asm Structures_H.kernel_object.split_asm 1656 arch_kernel_object.split_asm) 1657 1658lemma update_asidpool_map_to_asidpools: 1659 "map_to_asidpools (ksPSpace s(p \<mapsto> KOArch (KOASIDPool ap))) 1660 = (map_to_asidpools (ksPSpace s))(p \<mapsto> ap)" 1661 by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) 1662 1663lemma update_pte_map_to_ptes: 1664 "map_to_ptes (ksPSpace s(p \<mapsto> KOArch (KOPTE pte))) 1665 = (map_to_ptes (ksPSpace s))(p \<mapsto> pte)" 1666 by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) 1667 1668lemma update_pte_map_tos: 1669 fixes P :: "pte \<Rightarrow> bool" 1670 assumes at: "obj_at' P p s" 1671 shows "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_ntfns (ksPSpace s)" 1672 and "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_tcbs (ksPSpace s)" 1673 and "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_ctes (ksPSpace s)" 1674 and "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPTE ko))) = map_to_pml4es (ksPSpace s)" 1675 and "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPTE ko))) = map_to_pdptes (ksPSpace s)" 1676 and "map_to_pdes (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_pdes (ksPSpace s)" 1677 and "map_to_eps (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_eps (ksPSpace s)" 1678 and "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_asidpools (ksPSpace s)" 1679 and "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_user_data (ksPSpace s)" 1680 and "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPTE pte)))) = map_to_user_data_device (ksPSpace s)" 1681 using at 1682 by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other 1683 split: if_split_asm if_split 1684 simp: projectKOs, 1685 auto simp: projectKO_opts_defs) 1686 1687lemma update_pde_map_to_pdes: 1688 "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOPDE pde))) 1689 = (map_to_pdes (ksPSpace s))(p \<mapsto> pde)" 1690 by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) 1691 1692lemma update_pde_map_tos: 1693 fixes P :: "pde \<Rightarrow> bool" 1694 assumes at: "obj_at' P p s" 1695 shows "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ntfns (ksPSpace s)" 1696 and "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_tcbs (ksPSpace s)" 1697 and "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ctes (ksPSpace s)" 1698 and "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPDE ko))) = map_to_pml4es (ksPSpace s)" 1699 and "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPDE ko))) = map_to_pdptes (ksPSpace s)" 1700 and "map_to_ptes (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_ptes (ksPSpace s)" 1701 and "map_to_eps (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_eps (ksPSpace s)" 1702 and "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_asidpools (ksPSpace s)" 1703 and "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_user_data (ksPSpace s)" 1704 and "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPDE pde)))) = map_to_user_data_device (ksPSpace s)" 1705 using at 1706 by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other 1707 split: if_split_asm if_split 1708 simp: projectKOs, 1709 auto simp: projectKO_opts_defs) 1710 1711lemma update_pdpte_map_to_pdptes: 1712 "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPDPTE pdpte))) 1713 = (map_to_pdptes (ksPSpace s))(p \<mapsto> pdpte)" 1714 by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) 1715 1716lemma update_pdpte_map_tos: 1717 fixes P :: "pdpte \<Rightarrow> bool" 1718 assumes at: "obj_at' P p s" 1719 shows "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_ntfns (ksPSpace s)" 1720 and "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_tcbs (ksPSpace s)" 1721 and "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_ctes (ksPSpace s)" 1722 and "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPDPTE ko))) = map_to_pml4es (ksPSpace s)" 1723 and "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOPDPTE ko))) = map_to_pdes (ksPSpace s)" 1724 and "map_to_ptes (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_ptes (ksPSpace s)" 1725 and "map_to_eps (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_eps (ksPSpace s)" 1726 and "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_asidpools (ksPSpace s)" 1727 and "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_user_data (ksPSpace s)" 1728 and "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPDPTE pdpte)))) = map_to_user_data_device (ksPSpace s)" 1729 using at 1730 by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other 1731 split: if_split_asm if_split 1732 simp: projectKOs, 1733 auto simp: projectKO_opts_defs) 1734 1735lemma update_pml4e_map_to_pml4es: 1736 "map_to_pml4es (ksPSpace s(p \<mapsto> KOArch (KOPML4E pml4e))) 1737 = (map_to_pml4es (ksPSpace s))(p \<mapsto> pml4e)" 1738 by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) 1739 1740lemma update_pml4e_map_tos: 1741 fixes P :: "pml4e \<Rightarrow> bool" 1742 assumes at: "obj_at' P p s" 1743 shows "map_to_ntfns (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_ntfns (ksPSpace s)" 1744 and "map_to_tcbs (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_tcbs (ksPSpace s)" 1745 and "map_to_ctes (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_ctes (ksPSpace s)" 1746 and "map_to_pdptes (ksPSpace s(p \<mapsto> KOArch (KOPML4E ko))) = map_to_pdptes (ksPSpace s)" 1747 and "map_to_pdes (ksPSpace s(p \<mapsto> KOArch (KOPML4E ko))) = map_to_pdes (ksPSpace s)" 1748 and "map_to_ptes (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_ptes (ksPSpace s)" 1749 and "map_to_eps (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_eps (ksPSpace s)" 1750 and "map_to_asidpools (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_asidpools (ksPSpace s)" 1751 and "map_to_user_data (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_user_data (ksPSpace s)" 1752 and "map_to_user_data_device (ksPSpace s(p \<mapsto> (KOArch (KOPML4E pml4e)))) = map_to_user_data_device (ksPSpace s)" 1753 using at 1754 by (auto elim!: obj_atE' intro!: map_comp_eqI map_to_ctes_upd_other 1755 split: if_split_asm if_split 1756 simp: projectKOs, 1757 auto simp: projectKO_opts_defs) 1758 1759lemma heap_to_page_data_cong [cong]: 1760 "\<lbrakk> map_to_user_data ks = map_to_user_data ks'; bhp = bhp' \<rbrakk> 1761 \<Longrightarrow> heap_to_user_data ks bhp = heap_to_user_data ks' bhp'" 1762 unfolding heap_to_user_data_def by simp 1763 1764lemma heap_to_device_data_cong [cong]: 1765 "\<lbrakk> map_to_user_data_device ks = map_to_user_data_device ks'; bhp = bhp' \<rbrakk> 1766 \<Longrightarrow> heap_to_device_data ks bhp = heap_to_device_data ks' bhp'" 1767 unfolding heap_to_device_data_def by simp 1768 1769lemma map_leD: 1770 "\<lbrakk> map_le m m'; m x = Some y \<rbrakk> \<Longrightarrow> m' x = Some y" 1771 by (simp add: map_le_def dom_def) 1772 1773lemma region_is_bytes_disjoint: 1774 assumes cleared: "region_is_bytes' p n (hrs_htd hrs)" 1775 and not_byte: "typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8)" 1776 shows "hrs_htd hrs \<Turnstile>\<^sub>t (p' :: 'a ptr) 1777 \<Longrightarrow> {p ..+ n} \<inter> {ptr_val p' ..+ size_of TYPE('a)} = {}" 1778 apply (clarsimp simp: h_t_valid_def valid_footprint_def Let_def) 1779 apply (clarsimp simp: set_eq_iff dest!: intvlD[where p="ptr_val p'"]) 1780 apply (drule_tac x="of_nat k" in spec, clarsimp simp: size_of_def) 1781 apply (cut_tac m=k in typ_slice_t_self[where td="typ_uinfo_t TYPE('a)"]) 1782 apply (clarsimp simp: in_set_conv_nth) 1783 apply (drule_tac x=i in map_leD, simp) 1784 apply (simp add: cleared[unfolded region_is_bytes'_def] not_byte size_of_def) 1785 done 1786 1787lemma region_actually_is_bytes: 1788 "region_actually_is_bytes' ptr len htd 1789 \<Longrightarrow> region_is_bytes' ptr len htd" 1790 by (simp add: region_is_bytes'_def region_actually_is_bytes'_def 1791 split: if_split) 1792 1793lemma zero_ranges_are_zero_update[simp]: 1794 "h_t_valid (hrs_htd hrs) c_guard (ptr :: 'a ptr) 1795 \<Longrightarrow> typ_uinfo_t TYPE('a :: wf_type) \<noteq> typ_uinfo_t TYPE(word8) 1796 \<Longrightarrow> zero_ranges_are_zero rs (hrs_mem_update (heap_update ptr v) hrs) 1797 = zero_ranges_are_zero rs hrs" 1798 apply (clarsimp simp: zero_ranges_are_zero_def hrs_mem_update 1799 intro!: ball_cong[OF refl] conj_cong[OF refl]) 1800 apply (drule region_actually_is_bytes) 1801 apply (drule(2) region_is_bytes_disjoint) 1802 apply (simp add: heap_update_def heap_list_update_disjoint_same Int_commute) 1803 done 1804 1805lemma inj_tcb_ptr_to_ctcb_ptr [simp]: 1806 "inj tcb_ptr_to_ctcb_ptr" 1807 apply (rule injI) 1808 apply (simp add: tcb_ptr_to_ctcb_ptr_def) 1809 done 1810 1811lemmas tcb_ptr_to_ctcb_ptr_eq [simp] = inj_eq [OF inj_tcb_ptr_to_ctcb_ptr] 1812 1813lemma obj_at_cslift_tcb: 1814 fixes P :: "tcb \<Rightarrow> bool" 1815 shows "\<lbrakk>obj_at' P thread s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> 1816 \<exists>ko ko'. ko_at' ko thread s \<and> P ko \<and> 1817 cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some ko' \<and> 1818 ctcb_relation ko ko'" 1819 apply (frule obj_at_ko_at') 1820 apply clarsimp 1821 apply (frule cmap_relation_tcb) 1822 apply (drule (1) cmap_relation_ko_atD) 1823 apply fastforce 1824 done 1825 1826fun 1827 thread_state_to_tsType :: "thread_state \<Rightarrow> machine_word" 1828where 1829 "thread_state_to_tsType (Structures_H.Running) = scast ThreadState_Running" 1830 | "thread_state_to_tsType (Structures_H.Restart) = scast ThreadState_Restart" 1831 | "thread_state_to_tsType (Structures_H.Inactive) = scast ThreadState_Inactive" 1832 | "thread_state_to_tsType (Structures_H.IdleThreadState) = scast ThreadState_IdleThreadState" 1833 | "thread_state_to_tsType (Structures_H.BlockedOnReply) = scast ThreadState_BlockedOnReply" 1834 | "thread_state_to_tsType (Structures_H.BlockedOnReceive oref) = scast ThreadState_BlockedOnReceive" 1835 | "thread_state_to_tsType (Structures_H.BlockedOnSend oref badge cg isc) = scast ThreadState_BlockedOnSend" 1836 | "thread_state_to_tsType (Structures_H.BlockedOnNotification oref) = scast ThreadState_BlockedOnNotification" 1837 1838 1839lemma ctcb_relation_thread_state_to_tsType: 1840 "ctcb_relation tcb ctcb \<Longrightarrow> tsType_CL (thread_state_lift (tcbState_C ctcb)) = thread_state_to_tsType (tcbState tcb)" 1841 unfolding ctcb_relation_def cthread_state_relation_def 1842 by (cases "(tcbState tcb)", simp_all) 1843 1844 1845lemma tcb_ptr_to_tcb_ptr [simp]: 1846 "tcb_ptr_to_ctcb_ptr (ctcb_ptr_to_tcb_ptr x) = x" 1847 unfolding tcb_ptr_to_ctcb_ptr_def ctcb_ptr_to_tcb_ptr_def 1848 by simp 1849 1850lemma ctcb_ptr_to_ctcb_ptr [simp]: 1851 "ctcb_ptr_to_tcb_ptr (tcb_ptr_to_ctcb_ptr x) = x" 1852 unfolding ctcb_ptr_to_tcb_ptr_def tcb_ptr_to_ctcb_ptr_def 1853 by simp 1854 1855declare ucast_id [simp] 1856 1857definition 1858 cap_rights_from_word_canon :: "machine_word \<Rightarrow> seL4_CapRights_CL" 1859 where 1860 "cap_rights_from_word_canon wd \<equiv> 1861 \<lparr> capAllowGrant_CL = from_bool (wd !! 2), 1862 capAllowRead_CL = from_bool (wd !! 1), 1863 capAllowWrite_CL = from_bool (wd !! 0)\<rparr>" 1864 1865definition 1866 cap_rights_from_word :: "machine_word \<Rightarrow> seL4_CapRights_CL" 1867 where 1868 "cap_rights_from_word wd \<equiv> SOME cr. 1869 to_bool (capAllowGrant_CL cr) = wd !! 2 \<and> 1870 to_bool (capAllowRead_CL cr) = wd !! 1 \<and> 1871 to_bool (capAllowWrite_CL cr) = wd !! 0" 1872 1873lemma cap_rights_to_H_from_word [simp]: 1874 "cap_rights_to_H (cap_rights_from_word wd) = rightsFromWord wd" 1875 unfolding cap_rights_from_word_def rightsFromWord_def 1876 apply (rule someI2_ex) 1877 apply (rule exI [where x = "cap_rights_from_word_canon wd"]) 1878 apply (simp add: cap_rights_from_word_canon_def) 1879 apply (simp add: cap_rights_to_H_def) 1880 done 1881 1882lemma cmap_relation_updI2: 1883 fixes am :: "machine_word \<rightharpoonup> 'a" and cm :: "'b typ_heap" 1884 assumes cr: "cmap_relation am cm f rel" 1885 and cof: "am dest = None" 1886 and cc: "rel nv nv'" 1887 and inj: "inj f" 1888 shows "cmap_relation (am(dest \<mapsto> nv)) (cm(f dest \<mapsto> nv')) f rel" 1889 using cr cof cc inj 1890 by (clarsimp simp add: cmap_relation_def inj_eq split: if_split) 1891 1892definition 1893 user_word_at :: "machine_word \<Rightarrow> machine_word \<Rightarrow> kernel_state \<Rightarrow> bool" 1894where 1895 "user_word_at x p \<equiv> \<lambda>s. is_aligned p 3 1896 \<and> pointerInUserData p s 1897 \<and> x = word_rcat (map (underlying_memory (ksMachineState s)) 1898 [p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])" 1899 1900definition 1901 device_word_at :: "machine_word \<Rightarrow> machine_word \<Rightarrow> kernel_state \<Rightarrow> bool" 1902where 1903 "device_word_at x p \<equiv> \<lambda>s. is_aligned p 3 1904 \<and> pointerInDeviceData p s 1905 \<and> x = word_rcat (map (underlying_memory (ksMachineState s)) 1906 [p + 7, p + 6, p + 5, p + 4, p + 3, p + 2, p + 1, p])" 1907 1908lemma rf_sr_heap_user_data_relation: 1909 "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation 1910 (heap_to_user_data (ksPSpace s) (underlying_memory (ksMachineState s))) 1911 (cslift s') Ptr cuser_user_data_relation" 1912 by (clarsimp simp: user_word_at_def rf_sr_def 1913 cstate_relation_def Let_def 1914 cpspace_relation_def) 1915 1916lemma rf_sr_heap_device_data_relation: 1917 "(s, s') \<in> rf_sr \<Longrightarrow> cmap_relation 1918 (heap_to_device_data (ksPSpace s) (underlying_memory (ksMachineState s))) 1919 (cslift s') Ptr cuser_user_data_device_relation" 1920 by (clarsimp simp: user_word_at_def rf_sr_def 1921 cstate_relation_def Let_def 1922 cpspace_relation_def) 1923 1924lemma ko_at_projectKO_opt: 1925 "ko_at' ko p s \<Longrightarrow> (projectKO_opt \<circ>\<^sub>m ksPSpace s) p = Some ko" 1926 by (clarsimp elim!: obj_atE' simp: projectKOs) 1927 1928lemma word_shift_by_3: 1929 "x * 8 = (x::'a::len word) << 3" 1930 by (simp add: shiftl_t2n) 1931 1932(* FIXME x64: move *) 1933lemma mask_shiftr_times_simp: 1934 "\<lbrakk>x > n;is_aligned p n\<rbrakk> \<Longrightarrow> (p && mask x >> n) * (2^n) = (p && mask x)" 1935 apply (subst mult.commute) 1936 apply (simp add: shiftl_t2n[symmetric]) 1937 by (simp add: is_aligned_andI1 is_aligned_shiftr_shiftl) 1938 1939lemma user_word_at_cross_over: 1940 "\<lbrakk> user_word_at x p s; (s, s') \<in> rf_sr; p' = Ptr p \<rbrakk> 1941 \<Longrightarrow> c_guard p' \<and> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t p' 1942 \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x" 1943 apply (drule rf_sr_heap_user_data_relation) 1944 apply (erule cmap_relationE1) 1945 apply (clarsimp simp: heap_to_user_data_def Let_def 1946 user_word_at_def pointerInUserData_def 1947 typ_at_to_obj_at'[where 'a=user_data, simplified]) 1948 apply (drule obj_at_ko_at', clarsimp) 1949 apply (rule conjI, rule exI, erule ko_at_projectKO_opt) 1950 apply (rule refl) 1951 apply (thin_tac "heap_to_user_data a b c = d" for a b c d) 1952 apply (cut_tac x=p and w="~~ mask pageBits" in word_plus_and_or_coroll2) 1953 apply (rule conjI) 1954 apply (clarsimp simp: user_word_at_def pointerInUserData_def) 1955 apply (simp add: c_guard_def c_null_guard_def ptr_aligned_def) 1956 apply (drule lift_t_g) 1957 apply (clarsimp simp: ) 1958 apply (simp add: align_of_def size_of_def) 1959 apply (fold is_aligned_def[where n=3, simplified], simp) 1960 apply (erule contra_subsetD[rotated]) 1961 apply (rule order_trans[rotated]) 1962 apply (rule_tac x="p && mask pageBits" and y=8 in intvl_sub_offset) 1963 apply (cut_tac y=p and a="mask pageBits && (~~ mask 3)" in word_and_le1) 1964 apply (subst(asm) word_bw_assocs[symmetric], subst(asm) is_aligned_neg_mask_eq, 1965 erule is_aligned_andI1) 1966 apply (simp add: word_le_nat_alt mask_def pageBits_def) 1967 apply simp 1968 apply (clarsimp simp: cuser_user_data_relation_def user_word_at_def) 1969 apply (frule_tac f="[''words_C'']" in h_t_valid_field[OF h_t_valid_clift], 1970 simp+) 1971 apply (drule_tac n="uint (p && mask pageBits >> 3)" in h_t_valid_Array_element) 1972 apply simp 1973 apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and) 1974 apply (insert int_and_leR [where a="uint (p >> 3)" and b=511], clarsimp)[1] 1975 apply (simp add: field_lvalue_def 1976 field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse] 1977 word_shift_by_3 shiftr_shiftl1 is_aligned_andI1) 1978 apply (drule_tac x="ucast (p >> 3)" in spec) 1979 apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask) 1980 apply (fold shiftl_t2n[where n=3, simplified, simplified mult.commute mult.left_commute]) 1981 apply (simp add: aligned_shiftr_mask_shiftl pageBits_def) 1982 apply (rule trans[rotated], rule_tac hp="hrs_mem (t_hrs_' (globals s'))" 1983 and x="Ptr &(Ptr (p && ~~ mask 12) \<rightarrow> [''words_C''])" 1984 in access_in_array) 1985 apply (rule trans) 1986 apply (erule typ_heap_simps) 1987 apply simp+ 1988 apply (rule order_less_le_trans, rule unat_lt2p) 1989 apply simp 1990 apply (fastforce simp add: typ_info_word) 1991 apply simp 1992 apply (rule_tac f="h_val hp" for hp in arg_cong) 1993 apply simp 1994 apply (simp add: field_lvalue_def) 1995 apply (simp add: ucast_nat_def ucast_ucast_mask) 1996 apply (fold shiftl_t2n[where n=3, simplified, simplified mult.commute mult.left_commute]) 1997 apply (simp add: aligned_shiftr_mask_shiftl) 1998 done 1999 2000(* FIXME: Because the following lemma is correct, writing to device memory refines from c to abstract. 2001 But because we ignore what are written to decice memory, read does not refine from c to abstract. 2002lemma device_word_at_cross_over: 2003 "\<lbrakk> device_word_at x p s; (s, s') \<in> rf_sr; p' = Ptr p \<rbrakk> 2004 \<Longrightarrow> c_guard p' \<and> hrs_htd (t_hrs_' (globals s')) \<Turnstile>\<^sub>t p' 2005 \<and> h_val (hrs_mem (t_hrs_' (globals s'))) p' = x" 2006 apply (drule rf_sr_heap_device_data_relation) 2007 apply (erule cmap_relationE1) 2008 apply (clarsimp simp: heap_to_device_data_def Let_def 2009 device_word_at_def pointerInDeviceData_def 2010 typ_at_to_obj_at'[where 'a=user_data_device, simplified]) 2011 apply (drule obj_at_ko_at', clarsimp) 2012 apply (rule conjI, rule exI, erule ko_at_projectKO_opt) 2013 apply (rule refl) 2014 apply (thin_tac "heap_to_device_data a b c = d" for a b c d) 2015 apply (cut_tac x=p and w="~~ mask pageBits" in word_plus_and_or_coroll2) 2016 apply (rule conjI) 2017 apply (clarsimp simp: device_word_at_def pointerInDeviceData_def) 2018 apply (simp add: c_guard_def c_null_guard_def ptr_aligned_def) 2019 apply (drule lift_t_g) 2020 apply (clarsimp simp: ) 2021 apply (simp add: align_of_def size_of_def) 2022 apply (fold is_aligned_def[where n=2, simplified], simp) 2023 apply (erule contra_subsetD[rotated]) 2024 apply (rule order_trans[rotated]) 2025 apply (rule_tac x="p && mask pageBits" and y=4 in intvl_sub_offset) 2026 apply (cut_tac y=p and a="mask pageBits && (~~ mask 2)" in word_and_le1) 2027 apply (subst(asm) word_bw_assocs[symmetric], subst(asm) aligned_neg_mask, 2028 erule is_aligned_andI1) 2029 apply (simp add: word_le_nat_alt mask_def pageBits_def) 2030 apply simp 2031 apply (clarsimp simp: cuser_user_data_device_relation_def device_word_at_def) 2032 apply (frule_tac f="[''words_C'']" in h_t_valid_field[OF h_t_valid_clift], 2033 simp+) 2034 apply (drule_tac n="uint (p && mask pageBits >> 2)" in h_t_valid_Array_element) 2035 apply simp 2036 apply (simp add: shiftr_over_and_dist mask_def pageBits_def uint_and) 2037 apply (insert int_and_leR [where a="uint (p >> 2)" and b=1023], clarsimp)[1] 2038 apply (simp add: field_lvalue_def 2039 field_lookup_offset_eq[OF trans, OF _ arg_cong[where f=Some, symmetric], OF _ prod.collapse] 2040 word32_shift_by_2 shiftr_shiftl1 is_aligned_andI1) 2041 apply (drule_tac x="ucast (p >> 2)" in spec) 2042 apply (simp add: byte_to_word_heap_def Let_def ucast_ucast_mask) 2043 apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute]) 2044 apply (simp add: aligned_shiftr_mask_shiftl pageBits_def) 2045 apply (rule trans[rotated], rule_tac hp="hrs_mem (t_hrs_' (globals s'))" 2046 and x="Ptr &(Ptr (p && ~~ mask 12) \<rightarrow> [''words_C''])" 2047 in access_in_array) 2048 apply (rule trans) 2049 apply (erule typ_heap_simps) 2050 apply simp+ 2051 apply (rule order_less_le_trans, rule unat_lt2p) 2052 apply simp 2053 apply (fastforce simp add: typ_info_word) 2054 apply simp 2055 apply (rule_tac f="h_val hp" for hp in arg_cong) 2056 apply simp 2057 apply (simp add: field_lvalue_def) 2058 apply (simp add: ucast_nat_def ucast_ucast_mask) 2059 apply (fold shiftl_t2n[where n=2, simplified, simplified mult.commute mult.left_commute]) 2060 apply (simp add: aligned_shiftr_mask_shiftl) 2061 done 2062*) 2063 2064(* FIXME: move to GenericLib *) 2065lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def] 2066 2067lemma unat_mask_3_less_8: 2068 "unat (p && mask 3 :: word64) < 8" 2069 apply (rule unat_less_helper) 2070 apply (rule order_le_less_trans, rule word_and_le1) 2071 apply (simp add: mask_def) 2072 done 2073 2074lemma memory_cross_over: 2075 "\<lbrakk>(\<sigma>, s) \<in> rf_sr; pspace_aligned' \<sigma>; pspace_distinct' \<sigma>; 2076 pointerInUserData ptr \<sigma>\<rbrakk> 2077 \<Longrightarrow> fst (t_hrs_' (globals s)) ptr = underlying_memory (ksMachineState \<sigma>) ptr" 2078 apply (subgoal_tac " c_guard (Ptr (ptr && ~~ mask 3)::machine_word ptr) \<and> 2079 s \<Turnstile>\<^sub>c (Ptr (ptr && ~~ mask 3)::machine_word ptr) \<and> h_val (hrs_mem (t_hrs_' (globals s))) (Ptr (ptr && ~~ mask 3)) = x" for x) 2080 prefer 2 2081 apply (drule_tac p="ptr && ~~ mask 3" in user_word_at_cross_over[rotated]) 2082 apply simp 2083 apply (simp add: user_word_at_def Aligned.is_aligned_neg_mask 2084 pointerInUserData_def pageBits_def mask_lower_twice) 2085 apply assumption 2086 apply (clarsimp simp: h_val_def from_bytes_def typ_info_word) 2087 apply (drule_tac f="word_rsplit :: machine_word \<Rightarrow> word8 list" in arg_cong) 2088 apply (simp add: word_rsplit_rcat_size word_size) 2089 apply (drule_tac f="\<lambda>xs. xs ! unat (ptr && mask 3)" in arg_cong) 2090 apply (simp add: heap_list_nth unat_mask_3_less_8 2091 word_plus_and_or_coroll2 add.commute 2092 hrs_mem_def) 2093 apply (cut_tac p=ptr in unat_mask_3_less_8) 2094 apply (subgoal_tac "(ptr && ~~ mask 3) + (ptr && mask 3) = ptr") 2095 apply (subgoal_tac "!n x. n < 8 \<longrightarrow> (unat (x::machine_word) = n) = (x = of_nat n)") 2096 apply (auto simp add: eval_nat_numeral unat_eq_0 add.commute 2097 elim!: less_SucE)[1] 2098 apply (clarsimp simp add: unat64_eq_of_nat word_bits_def) 2099 apply (simp add: add.commute word_plus_and_or_coroll2) 2100 done 2101 2102lemma cap_get_tag_isCap_ArchObject0: 2103 assumes cr: "ccap_relation (capability.ArchObjectCap cap) cap'" 2104 shows "(cap_get_tag cap' = scast cap_asid_control_cap) = isASIDControlCap cap 2105 \<and> (cap_get_tag cap' = scast cap_asid_pool_cap) = isASIDPoolCap cap 2106 \<and> (cap_get_tag cap' = scast cap_page_table_cap) = isPageTableCap cap 2107 \<and> (cap_get_tag cap' = scast cap_page_directory_cap) = isPageDirectoryCap cap 2108 \<and> (cap_get_tag cap' = scast cap_pdpt_cap) = isPDPointerTableCap cap 2109 \<and> (cap_get_tag cap' = scast cap_pml4_cap) = isPML4Cap cap 2110 \<and> (cap_get_tag cap' = scast cap_io_port_cap) = isIOPortCap cap 2111 \<and> (cap_get_tag cap' = scast cap_frame_cap) = (isPageCap cap) 2112 \<and> (cap_get_tag cap' = scast cap_io_port_control_cap) = (isIOPortControlCap cap)" 2113 using cr 2114 apply - 2115 apply (erule ccap_relationE) 2116 apply (simp add: cap_to_H_def cap_lift_def Let_def isArchCap_def) 2117 by (clarsimp simp: isCap_simps cap_tag_defs word_le_nat_alt pageSize_def Let_def split: if_split_asm) \<comment> \<open>takes a while\<close> 2118 2119lemma cap_get_tag_isCap_ArchObject: 2120 assumes cr: "ccap_relation (capability.ArchObjectCap cap) cap'" 2121 shows "(cap_get_tag cap' = scast cap_asid_control_cap) = isASIDControlCap cap" 2122 and "(cap_get_tag cap' = scast cap_asid_pool_cap) = isASIDPoolCap cap" 2123 and "(cap_get_tag cap' = scast cap_page_table_cap) = isPageTableCap cap" 2124 and "(cap_get_tag cap' = scast cap_page_directory_cap) = isPageDirectoryCap cap" 2125 and "(cap_get_tag cap' = scast cap_pdpt_cap) = isPDPointerTableCap cap" 2126 and "(cap_get_tag cap' = scast cap_pml4_cap) = isPML4Cap cap" 2127 and "(cap_get_tag cap' = scast cap_frame_cap) = (isPageCap cap)" 2128 and "(cap_get_tag cap' = scast cap_io_port_cap) = isIOPortCap cap" 2129 and "(cap_get_tag cap' = scast cap_io_port_control_cap) = isIOPortControlCap cap" 2130 using cap_get_tag_isCap_ArchObject0 [OF cr] by auto 2131 2132lemma cap_get_tag_isCap_unfolded_H_cap: 2133 shows "ccap_relation (capability.ThreadCap v0) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_thread_cap)" 2134 and "ccap_relation (capability.NullCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_null_cap)" 2135 and "ccap_relation (capability.NotificationCap v4 v5 v6 v7) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_notification_cap) " 2136 and "ccap_relation (capability.EndpointCap v8 v9 v10 v11 v12) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_endpoint_cap)" 2137 and "ccap_relation (capability.IRQHandlerCap v13) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_handler_cap)" 2138 and "ccap_relation (capability.IRQControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_irq_control_cap)" 2139 and "ccap_relation (capability.Zombie v14 v15 v16) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_zombie_cap)" 2140 and "ccap_relation (capability.ReplyCap v17 v18) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_reply_cap)" 2141 and "ccap_relation (capability.UntypedCap v100 v19 v20 v20b) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_untyped_cap)" 2142 and "ccap_relation (capability.CNodeCap v21 v22 v23 v24) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_cnode_cap)" 2143 and "ccap_relation (capability.DomainCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_domain_cap)" 2144 2145 and "ccap_relation (capability.ArchObjectCap arch_capability.ASIDControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_asid_control_cap)" 2146 and "ccap_relation (capability.ArchObjectCap (arch_capability.ASIDPoolCap v28 v29)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_asid_pool_cap)" 2147 and "ccap_relation (capability.ArchObjectCap (arch_capability.PageTableCap v30 v31)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_table_cap)" 2148 and "ccap_relation (capability.ArchObjectCap (arch_capability.PageDirectoryCap v32 v33)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_page_directory_cap)" 2149 and "ccap_relation (capability.ArchObjectCap (arch_capability.PDPointerTableCap v34 v35)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_pdpt_cap)" 2150 and "ccap_relation (capability.ArchObjectCap (arch_capability.PML4Cap v36 v37)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_pml4_cap)" 2151 and "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap v101 v44 v45 v46 v47 v48)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_frame_cap)" 2152 and "ccap_relation (capability.ArchObjectCap (arch_capability.IOPortCap v60 v61)) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_io_port_cap)" 2153 and "ccap_relation (capability.ArchObjectCap arch_capability.IOPortControlCap) cap' \<Longrightarrow> (cap_get_tag cap' = scast cap_io_port_control_cap)" 2154 apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps) 2155 apply (frule cap_get_tag_isCap(2), simp) 2156 apply (simp add: cap_get_tag_isCap cap_get_tag_isCap_ArchObject isCap_simps pageSize_def)+ 2157 done 2158 2159lemma cap_get_tag_isCap_ArchObject2_worker: 2160 "\<lbrakk> \<And>cap''. ccap_relation (ArchObjectCap cap'') cap' \<Longrightarrow> (cap_get_tag cap' = n) = P cap''; 2161 ccap_relation cap cap'; isArchCap_tag n \<rbrakk> 2162 \<Longrightarrow> (cap_get_tag cap' = n) 2163 = (isArchObjectCap cap \<and> P (capCap cap))" 2164 apply (rule iffI) 2165 apply (clarsimp simp: cap_get_tag_isCap isCap_simps) 2166 apply (clarsimp simp: isCap_simps) 2167 done 2168 2169lemma cap_get_tag_isCap_ArchObject2: 2170 assumes cr: "ccap_relation cap cap'" 2171 shows "(cap_get_tag cap' = scast cap_asid_control_cap) 2172 = (isArchObjectCap cap \<and> isASIDControlCap (capCap cap))" 2173 and "(cap_get_tag cap' = scast cap_asid_pool_cap) 2174 = (isArchObjectCap cap \<and> isASIDPoolCap (capCap cap))" 2175 and "(cap_get_tag cap' = scast cap_page_table_cap) 2176 = (isArchObjectCap cap \<and> isPageTableCap (capCap cap))" 2177 and "(cap_get_tag cap' = scast cap_page_directory_cap) 2178 = (isArchObjectCap cap \<and> isPageDirectoryCap (capCap cap))" 2179 and "(cap_get_tag cap' = scast cap_pdpt_cap) 2180 = (isArchObjectCap cap \<and> isPDPointerTableCap (capCap cap))" 2181 and "(cap_get_tag cap' = scast cap_pml4_cap) 2182 = (isArchObjectCap cap \<and> isPML4Cap (capCap cap))" 2183 and "(cap_get_tag cap' = scast cap_frame_cap) 2184 = (isArchObjectCap cap \<and> isPageCap (capCap cap))" 2185 and "(cap_get_tag cap' = scast cap_io_port_cap) 2186 = (isArchObjectCap cap \<and> isIOPortCap (capCap cap))" 2187 and "(cap_get_tag cap' = scast cap_io_port_control_cap) 2188 = (isArchObjectCap cap \<and> isIOPortControlCap (capCap cap))" 2189 by (rule cap_get_tag_isCap_ArchObject2_worker [OF _ cr], 2190 simp add: cap_get_tag_isCap_ArchObject, 2191 simp add: isArchCap_tag_def2 cap_tag_defs)+ 2192 2193schematic_goal cap_io_port_cap_lift_def': 2194 "cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap 2195 \<Longrightarrow> cap_io_port_cap_lift cap = 2196 \<lparr> capIOPortFirstPort_CL = ?first, 2197 capIOPortLastPort_CL = ?last \<rparr>" 2198 by (simp add: cap_io_port_cap_lift_def cap_lift_def cap_tag_defs) 2199 2200schematic_goal cap_frame_cap_lift_def': 2201 "cap_get_tag cap = SCAST(32 signed \<rightarrow> 64) cap_frame_cap 2202 \<Longrightarrow> cap_frame_cap_lift cap = 2203 \<lparr> capFMappedASID_CL = ?mapped_asid, 2204 capFBasePtr_CL = ?base_ptr, 2205 capFSize_CL = ?frame_size, 2206 capFMapType_CL = ?map_type, 2207 capFMappedAddress_CL = ?mapped_address, 2208 capFVMRights_CL = ?vm_rights, 2209 capFIsDevice_CL = ?is_device \<rparr>" 2210 by (simp add: cap_frame_cap_lift_def cap_lift_def cap_tag_defs) 2211 2212lemmas ccap_rel_cap_get_tag_cases_generic = 2213 cap_get_tag_isCap_unfolded_H_cap(1-11) 2214 [OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']] 2215 2216lemmas ccap_rel_cap_get_tag_cases_arch = 2217 cap_get_tag_isCap_unfolded_H_cap(12-20) 2218 [OF back_subst[of "\<lambda>cap. ccap_relation (ArchObjectCap cap) cap'" for cap'], 2219 OF back_subst[of "\<lambda>cap. ccap_relation cap cap'" for cap']] 2220 2221lemmas ccap_rel_cap_get_tag_cases_arch' = 2222 ccap_rel_cap_get_tag_cases_arch[OF _ refl] 2223 2224lemmas cap_lift_defs = 2225 cap_untyped_cap_lift_def 2226 cap_endpoint_cap_lift_def 2227 cap_notification_cap_lift_def 2228 cap_reply_cap_lift_def 2229 cap_cnode_cap_lift_def 2230 cap_thread_cap_lift_def 2231 cap_irq_handler_cap_lift_def 2232 cap_zombie_cap_lift_def 2233 cap_frame_cap_lift_def 2234 cap_page_table_cap_lift_def 2235 cap_page_directory_cap_lift_def 2236 cap_pdpt_cap_lift_def 2237 cap_pml4_cap_lift_def 2238 cap_asid_pool_cap_lift_def 2239 cap_io_port_cap_lift_def 2240 2241lemma cap_lift_Some_CapD: 2242 "\<And>c'. cap_lift c = Some (Cap_untyped_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_untyped_cap" 2243 "\<And>c'. cap_lift c = Some (Cap_endpoint_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_endpoint_cap" 2244 "\<And>c'. cap_lift c = Some (Cap_notification_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_notification_cap" 2245 "\<And>c'. cap_lift c = Some (Cap_reply_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_reply_cap" 2246 "\<And>c'. cap_lift c = Some (Cap_cnode_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_cnode_cap" 2247 "\<And>c'. cap_lift c = Some (Cap_thread_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_thread_cap" 2248 "\<And>c'. cap_lift c = Some (Cap_irq_handler_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_irq_handler_cap" 2249 "\<And>c'. cap_lift c = Some (Cap_zombie_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_zombie_cap" 2250 "\<And>c'. cap_lift c = Some (Cap_frame_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_frame_cap" 2251 "\<And>c'. cap_lift c = Some (Cap_page_table_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_page_table_cap" 2252 "\<And>c'. cap_lift c = Some (Cap_page_directory_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_page_directory_cap" 2253 "\<And>c'. cap_lift c = Some (Cap_pdpt_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_pdpt_cap" 2254 "\<And>c'. cap_lift c = Some (Cap_pml4_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_pml4_cap" 2255 "\<And>c'. cap_lift c = Some (Cap_asid_pool_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_asid_pool_cap" 2256 "\<And>c'. cap_lift c = Some (Cap_io_port_cap c') \<Longrightarrow> cap_get_tag c = SCAST(32 signed \<rightarrow> 64) cap_io_port_cap" 2257 by (auto simp: cap_lifts cap_lift_defs) 2258 2259lemma rf_sr_x64KSSKIMPML4: 2260 "(s, s') \<in> rf_sr \<Longrightarrow> x64KSSKIMPML4 (ksArchState s) = symbol_table ''x64KSSKIMPML4''" 2261 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def carch_globals_def) 2262 2263lemma ghost_assertion_size_logic': 2264 "unat (sz :: machine_word) \<le> gsMaxObjectSize s 2265 \<Longrightarrow> cstate_relation s gs 2266 \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs) = 0 \<or> 2267 sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' gs)" 2268 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def ghost_size_rel_def 2269 linorder_not_le word_less_nat_alt) 2270 2271lemma ghost_assertion_size_logic: 2272 "unat (sz :: machine_word) \<le> gsMaxObjectSize s 2273 \<Longrightarrow> (s, \<sigma>) \<in> rf_sr 2274 \<Longrightarrow> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>)) = 0 \<or> 2275 sz \<le> gs_get_assn cap_get_capSizeBits_'proc (ghost'state_' (globals \<sigma>))" 2276 by (clarsimp simp: rf_sr_def ghost_assertion_size_logic') 2277 2278lemma gs_set_assn_Delete_cstate_relation: 2279 "cstate_relation s (ghost'state_'_update (gs_set_assn cteDeleteOne_'proc v) gs) 2280 = cstate_relation s gs" 2281 apply (cases "ghost'state_' gs") 2282 by (auto simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 2283 cmachine_state_relation_def ghost_assertion_data_set_def 2284 ghost_size_rel_def ghost_assertion_data_get_def 2285 cteDeleteOne_'proc_def cap_get_capSizeBits_'proc_def) 2286 2287lemma update_typ_at: 2288 assumes at: "obj_at' P p s" 2289 and tp: "\<forall>obj. P obj \<longrightarrow> koTypeOf (injectKOS obj) = koTypeOf ko" 2290 shows "typ_at' T p' (s \<lparr>ksPSpace := ksPSpace s(p \<mapsto> ko)\<rparr>) = typ_at' T p' s" 2291 using at 2292 by (auto elim!: obj_atE' simp: typ_at'_def ko_wp_at'_def 2293 dest!: tp[rule_format] 2294 simp: project_inject projectKO_eq split: kernel_object.splits if_split_asm, 2295 simp_all add: objBits_def objBitsT_koTypeOf[symmetric] ps_clear_upd 2296 del: objBitsT_koTypeOf) 2297 2298lemma ptr_val_tcb_ptr_mask: 2299 "obj_at' (P :: tcb \<Rightarrow> bool) thread s 2300 \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && (~~ mask tcbBlockSizeBits) 2301 = thread" 2302 apply (clarsimp simp: obj_at'_def tcb_ptr_to_ctcb_ptr_def projectKOs) 2303 apply (simp add: is_aligned_add_helper ctcb_offset_defs objBits_simps') 2304 done 2305 2306lemmas ptr_val_tcb_ptr_mask'[simp] 2307 = ptr_val_tcb_ptr_mask[unfolded mask_def tcbBlockSizeBits_def, simplified] 2308 2309lemma typ_uinfo_t_diff_from_typ_name: 2310 "typ_name (typ_info_t TYPE ('a :: c_type)) \<noteq> typ_name (typ_info_t TYPE('b :: c_type)) 2311 \<Longrightarrow> typ_uinfo_t (aty :: 'a itself) \<noteq> typ_uinfo_t (bty :: 'b itself)" 2312 by (clarsimp simp: typ_uinfo_t_def td_diff_from_typ_name) 2313 2314declare ptr_add_assertion'[simp] typ_uinfo_t_diff_from_typ_name[simp] 2315 2316lemma clift_array_assertion_imp: 2317 "clift hrs (p :: (('a :: wf_type)['b :: finite]) ptr) = Some v 2318 \<Longrightarrow> htd = hrs_htd hrs 2319 \<Longrightarrow> n \<noteq> 0 2320 \<Longrightarrow> \<exists>i. p' = ptr_add (ptr_coerce p) (int i) 2321 \<and> i + n \<le> CARD('b) 2322 \<Longrightarrow> array_assertion (p' :: 'a ptr) n htd" 2323 apply clarsimp 2324 apply (drule h_t_valid_clift) 2325 apply (drule array_ptr_valid_array_assertionD) 2326 apply (drule_tac j=i in array_assertion_shrink_leftD, simp) 2327 apply (erule array_assertion_shrink_right) 2328 apply simp 2329 done 2330 2331lemma page_map_l4_at_carray_map_relation: 2332 "\<lbrakk> page_map_l4_at' pml4 s; cpspace_pml4e_array_relation (ksPSpace s) hp \<rbrakk> 2333 \<Longrightarrow> clift hp (pml4_Ptr pml4) \<noteq> None" 2334 apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) 2335 apply (drule spec, erule iffD1) 2336 apply (clarsimp simp: page_map_l4_at'_def) 2337 apply (drule_tac x="p' && mask pml4Bits >> 3" in spec) 2338 apply (clarsimp simp: shiftr_shiftl1) 2339 apply (drule mp) 2340 apply (simp add: shiftr_over_and_dist mask_def bit_simps 2341 order_le_less_trans[OF word_and_le1]) 2342 apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def bit_simps 2343 is_aligned_andI1 add.commute word_plus_and_or_coroll2 and_not_mask[symmetric] 2344 dest!: obj_at_ko_at' ko_at_projectKO_opt) 2345 done 2346 2347lemma page_map_l4_at_rf_sr: 2348 "\<lbrakk> page_map_l4_at' pml4 s; (s, s') \<in> rf_sr \<rbrakk> 2349 \<Longrightarrow> cslift s' (pml4_Ptr pml4) \<noteq> None" 2350 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2351 cpspace_relation_def page_map_l4_at_carray_map_relation) 2352 2353lemma pd_pointer_table_at_carray_map_relation: 2354 "\<lbrakk> pd_pointer_table_at' pdpt s; cpspace_pdpte_array_relation (ksPSpace s) hp \<rbrakk> 2355 \<Longrightarrow> clift hp (pdpt_Ptr pdpt) \<noteq> None" 2356 apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) 2357 apply (drule spec, erule iffD1) 2358 apply (clarsimp simp: pd_pointer_table_at'_def) 2359 apply (drule_tac x="p' && mask pdptBits >> 3" in spec) 2360 apply (clarsimp simp: shiftr_shiftl1) 2361 apply (drule mp) 2362 apply (simp add: shiftr_over_and_dist mask_def bit_simps 2363 order_le_less_trans[OF word_and_le1]) 2364 apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def bit_simps 2365 is_aligned_andI1 add.commute word_plus_and_or_coroll2 and_not_mask[symmetric] 2366 dest!: obj_at_ko_at' ko_at_projectKO_opt) 2367 done 2368 2369lemma pd_pointer_table_at_rf_sr: 2370 "\<lbrakk> pd_pointer_table_at' pd s; (s, s') \<in> rf_sr \<rbrakk> 2371 \<Longrightarrow> cslift s' (Ptr pd :: (pdpte_C[512]) ptr) \<noteq> None" 2372 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2373 cpspace_relation_def pd_pointer_table_at_carray_map_relation) 2374 2375lemma page_directory_at_carray_map_relation: 2376 "\<lbrakk> page_directory_at' pd s; cpspace_pde_array_relation (ksPSpace s) hp \<rbrakk> 2377 \<Longrightarrow> clift hp (pd_Ptr pd) \<noteq> None" 2378 apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) 2379 apply (drule spec, erule iffD1) 2380 apply (clarsimp simp: page_directory_at'_def) 2381 apply (drule_tac x="p' && mask pdBits >> 3" in spec) 2382 apply (clarsimp simp: shiftr_shiftl1) 2383 apply (drule mp) 2384 apply (simp add: shiftr_over_and_dist mask_def bit_simps 2385 order_le_less_trans[OF word_and_le1]) 2386 apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def bit_simps 2387 is_aligned_andI1 add.commute word_plus_and_or_coroll2 and_not_mask[symmetric] 2388 dest!: obj_at_ko_at' ko_at_projectKO_opt) 2389 done 2390 2391lemma page_directory_at_rf_sr: 2392 "\<lbrakk> page_directory_at' pd s; (s, s') \<in> rf_sr \<rbrakk> 2393 \<Longrightarrow> cslift s' (Ptr pd :: (pde_C[512]) ptr) \<noteq> None" 2394 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2395 cpspace_relation_def page_directory_at_carray_map_relation) 2396 2397lemma page_table_at_carray_map_relation: 2398 "\<lbrakk> page_table_at' pt s; cpspace_pte_array_relation (ksPSpace s) hp \<rbrakk> 2399 \<Longrightarrow> clift hp (pt_Ptr pt) \<noteq> None" 2400 apply (clarsimp simp: carray_map_relation_def h_t_valid_clift_Some_iff) 2401 apply (drule spec, erule iffD1) 2402 apply (clarsimp simp: page_table_at'_def) 2403 apply (drule_tac x="p' && mask ptBits >> 3" in spec) 2404 apply (clarsimp simp: shiftr_shiftl1) 2405 apply (drule mp) 2406 apply (simp add: shiftr_over_and_dist bit_simps mask_def 2407 order_le_less_trans[OF word_and_le1]) 2408 apply (clarsimp simp: typ_at_to_obj_at_arches objBits_simps archObjSize_def 2409 bit_simps and_not_mask[symmetric] 2410 is_aligned_andI1 add.commute word_plus_and_or_coroll2 2411 dest!: obj_at_ko_at' ko_at_projectKO_opt) 2412 done 2413 2414lemma page_table_at_rf_sr: 2415 "\<lbrakk> page_table_at' pd s; (s, s') \<in> rf_sr \<rbrakk> 2416 \<Longrightarrow> cslift s' (Ptr pd :: (pte_C[512]) ptr) \<noteq> None" 2417 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2418 cpspace_relation_def page_table_at_carray_map_relation) 2419 2420lemma gsUntypedZeroRanges_rf_sr: 2421 "\<lbrakk> (start, end) \<in> gsUntypedZeroRanges s; (s, s') \<in> rf_sr \<rbrakk> 2422 \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'" 2423 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 2424 zero_ranges_are_zero_def) 2425 apply (drule(1) bspec) 2426 apply clarsimp 2427 done 2428 2429lemma ctes_of_untyped_zero_rf_sr: 2430 "\<lbrakk> ctes_of s p = Some cte; (s, s') \<in> rf_sr; 2431 untyped_ranges_zero' s; 2432 untypedZeroRange (cteCap cte) = Some (start, end) \<rbrakk> 2433 \<Longrightarrow> region_actually_is_zero_bytes start (unat ((end + 1) - start)) s'" 2434 apply (erule gsUntypedZeroRanges_rf_sr[rotated]) 2435 apply (clarsimp simp: untyped_ranges_zero_inv_def) 2436 apply (rule_tac a=p in ranI) 2437 apply (simp add: map_comp_def cteCaps_of_def) 2438 done 2439 2440lemma heap_list_is_zero_mono: 2441 "heap_list_is_zero hmem p n \<Longrightarrow> n' \<le> n 2442 \<Longrightarrow> heap_list_is_zero hmem p n'" 2443 apply (induct n arbitrary: n' p) 2444 apply simp 2445 apply clarsimp 2446 apply (case_tac n', simp_all) 2447 done 2448 2449lemma heap_list_h_eq_better: 2450 "\<And>p. \<lbrakk> x \<in> {p..+q}; heap_list h q p = heap_list h' q p \<rbrakk> 2451 \<Longrightarrow> h x = h' x" 2452proof (induct q) 2453 case 0 thus ?case by simp 2454next 2455 case (Suc n) thus ?case by (force dest: intvl_neq_start) 2456qed 2457 2458lemma heap_list_is_zero_mono2: 2459 "heap_list_is_zero hmem p n 2460 \<Longrightarrow> {p' ..+ n'} \<le> {p ..+ n} 2461 \<Longrightarrow> heap_list_is_zero hmem p' n'" 2462 using heap_list_h_eq2[where h'="\<lambda>_. 0"] 2463 heap_list_h_eq_better[where h'="\<lambda>_. 0"] 2464 apply (simp(no_asm_use) add: heap_list_rpbs) 2465 apply blast 2466 done 2467 2468lemma invs_urz[elim!]: 2469 "invs' s \<Longrightarrow> untyped_ranges_zero' s" 2470 by (clarsimp simp: invs'_def valid_state'_def) 2471 2472lemma arch_fault_tag_not_fault_tag_simps [simp]: 2473 "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_CapFault) = False" 2474 "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_UserException) = False" 2475 "(arch_fault_to_fault_tag arch_fault = scast seL4_Fault_UnknownSyscall) = False" 2476 by (cases arch_fault ; simp add: seL4_Faults seL4_Arch_Faults)+ 2477 2478lemma capTCBPtr_eq: 2479 "\<lbrakk> ccap_relation cap cap'; isThreadCap cap \<rbrakk> 2480 \<Longrightarrow> cap_thread_cap_CL.capTCBPtr_CL (cap_thread_cap_lift cap') 2481 = ptr_val (tcb_ptr_to_ctcb_ptr (capTCBPtr cap))" 2482 apply (simp add: cap_get_tag_isCap[symmetric]) 2483 apply (drule(1) cap_get_tag_to_H) 2484 apply clarsimp 2485 done 2486 2487lemma rf_sr_sched_action_relation: 2488 "(s, s') \<in> rf_sr 2489 \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" 2490 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 2491 2492lemma canonical_address_tcb_ptr: 2493 "\<lbrakk>canonical_address t; is_aligned t tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2494 canonical_address (ptr_val (tcb_ptr_to_ctcb_ptr t))" 2495 apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def) 2496 apply (erule canonical_address_add) 2497 apply (clarsimp simp: objBits_simps' ctcb_offset_defs)+ 2498 done 2499 2500lemma canonical_address_ctcb_ptr: 2501 assumes "canonical_address (ctcb_ptr_to_tcb_ptr t)" "is_aligned (ctcb_ptr_to_tcb_ptr t) tcbBlockSizeBits" 2502 shows "canonical_address (ptr_val t)" 2503proof - 2504 from assms(2)[unfolded ctcb_ptr_to_tcb_ptr_def] 2505 have "canonical_address ((ptr_val t - ctcb_offset) + ctcb_offset)" 2506 apply (rule canonical_address_add; simp add: objBits_simps' ctcb_offset_defs) 2507 using assms(1) 2508 by (simp add: ctcb_ptr_to_tcb_ptr_def ctcb_offset_defs) 2509 thus ?thesis by simp 2510qed 2511 2512lemma tcb_and_not_mask_canonical: 2513 "\<lbrakk>pspace_canonical' s; tcb_at' t s; n < tcbBlockSizeBits\<rbrakk> \<Longrightarrow> 2514 tcb_Ptr (sign_extend 47 (ptr_val (tcb_ptr_to_ctcb_ptr t) && ~~ mask n)) = 2515 tcb_ptr_to_ctcb_ptr t" 2516 apply (frule (1) obj_at'_is_canonical) 2517 apply (drule canonical_address_tcb_ptr) 2518 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps' split: if_splits) 2519 apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend) 2520 apply (subgoal_tac "ptr_val (tcb_ptr_to_ctcb_ptr t) && ~~ mask n = ptr_val (tcb_ptr_to_ctcb_ptr t)") 2521 prefer 2 2522 apply (simp add: tcb_ptr_to_ctcb_ptr_def ctcb_offset_defs) 2523 apply (rule is_aligned_neg_mask_eq) 2524 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps') 2525 apply (rule is_aligned_add) 2526 apply (erule is_aligned_weaken, simp) 2527 apply (rule is_aligned_weaken[where x="tcbBlockSizeBits - 1"]) 2528 apply (simp add: is_aligned_def objBits_simps') 2529 apply (simp add: objBits_simps') 2530 apply simp 2531 done 2532 2533lemmas tcb_ptr_sign_extend_canonical = 2534 tcb_and_not_mask_canonical[where n=0, simplified mask_def objBits_simps', simplified] 2535 2536lemma fpu_null_state_typ_heap_preservation: 2537 assumes "fpu_null_state_relation s" 2538 assumes "(clift t :: user_fpu_state_C typ_heap) = clift s" 2539 shows "fpu_null_state_relation t" 2540 using assms by (simp add: fpu_null_state_relation_def) 2541 2542(* FIXME: move up to TypHeap? *) 2543lemma lift_t_Some_iff: 2544 "lift_t g hrs p = Some v \<longleftrightarrow> hrs_htd hrs, g \<Turnstile>\<^sub>t p \<and> h_val (hrs_mem hrs) p = v" 2545 unfolding hrs_htd_def hrs_mem_def by (cases hrs) (auto simp: lift_t_if) 2546 2547context 2548 fixes p :: "'a::mem_type ptr" 2549 fixes q :: "'b::c_type ptr" 2550 fixes d g\<^sub>p g\<^sub>q 2551 assumes val_p: "d,g\<^sub>p \<Turnstile>\<^sub>t p" 2552 assumes val_q: "d,g\<^sub>q \<Turnstile>\<^sub>t q" 2553 assumes disj: "typ_uinfo_t TYPE('a) \<bottom>\<^sub>t typ_uinfo_t TYPE('b)" 2554begin 2555 2556lemma h_val_heap_same_typ_disj: 2557 "h_val (heap_update p v h) q = h_val h q" 2558 using disj by (auto intro: h_val_heap_same[OF val_p val_q] 2559 simp: tag_disj_def sub_typ_proper_def field_of_t_def typ_tag_lt_def 2560 field_of_def typ_tag_le_def) 2561 2562lemma h_val_heap_same_hrs_mem_update_typ_disj: 2563 "h_val (hrs_mem (hrs_mem_update (heap_update p v) s)) q = h_val (hrs_mem s) q" 2564 by (simp add: hrs_mem_update h_val_heap_same_typ_disj) 2565 2566end 2567 2568lemma global_ioport_bitmap_relation_def2: 2569 "global_ioport_bitmap_relation (clift hrs) htable \<equiv> 2570 \<exists>ctable. hrs_htd hrs \<Turnstile>\<^sub>t (ioport_table_Ptr (symbol_table ''x86KSAllocatedIOPorts'')) 2571 \<and> h_val (hrs_mem hrs) (ioport_table_Ptr (symbol_table ''x86KSAllocatedIOPorts'')) = ctable 2572 \<and> cioport_bitmap_to_H ctable = htable 2573 \<and> ptr_span (ioport_table_Ptr (symbol_table ''x86KSAllocatedIOPorts'')) \<subseteq> kernel_data_refs" 2574 by (clarsimp simp: global_ioport_bitmap_relation_def lift_t_Some_iff) 2575 2576lemma fpu_null_state_relation_def2: 2577 "fpu_null_state_relation hrs \<equiv> 2578 hrs_htd hrs \<Turnstile>\<^sub>t fpu_state_Ptr (symbol_table ''x86KSnullFpuState'') 2579 \<and> h_val (hrs_mem hrs) (fpu_state_Ptr (symbol_table ''x86KSnullFpuState'')) 2580 = user_fpu_state_C (ARRAY i. FPUNullState (finite_index i)) 2581 \<and> ptr_span (fpu_state_Ptr (symbol_table ''x86KSnullFpuState'')) \<subseteq> kernel_data_refs" 2582 by (clarsimp simp: fpu_null_state_relation_def lift_t_Some_iff) 2583 2584lemma global_ioport_bitmap_heap_update_tag_disj': 2585 fixes p :: "'a::mem_type ptr" 2586 assumes valid: "hrs_htd h, g \<Turnstile>\<^sub>t p" 2587 assumes disj: "typ_uinfo_t TYPE(ioport_table_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)" 2588 shows "global_ioport_bitmap_relation (clift (hrs_mem_update (heap_update p v) h)) = global_ioport_bitmap_relation (clift h)" 2589 unfolding global_ioport_bitmap_relation_def 2590 using lift_t_heap_update_same[OF valid disj] 2591 by (clarsimp simp: global_ioport_bitmap_relation_def hrs_mem_update_def hrs_htd_def 2592 split: prod.splits) 2593 2594lemma fpu_null_state_heap_update_tag_disj': 2595 fixes p :: "'a::mem_type ptr" 2596 assumes valid: "hrs_htd h, g \<Turnstile>\<^sub>t p" 2597 assumes disj: "typ_uinfo_t TYPE(user_fpu_state_C) \<bottom>\<^sub>t typ_uinfo_t TYPE('a)" 2598 shows "fpu_null_state_relation (hrs_mem_update (heap_update p v) h) = fpu_null_state_relation h" 2599 unfolding fpu_null_state_relation_def 2600 using lift_t_heap_update_same[OF valid disj] 2601 by (clarsimp simp: fpu_null_state_relation_def hrs_mem_update_def hrs_htd_def 2602 split: prod.splits) 2603 2604lemmas h_t_valid_nested_fields = 2605 h_t_valid_field[OF h_t_valid_field[OF h_t_valid_field]] 2606 h_t_valid_field[OF h_t_valid_field] 2607 h_t_valid_field 2608 2609lemmas h_t_valid_fields_clift = 2610 h_t_valid_nested_fields[OF h_t_valid_clift] 2611 h_t_valid_clift 2612 2613lemmas global_ioport_bitmap_heap_update_tag_disj_simps = 2614 h_t_valid_fields_clift[THEN global_ioport_bitmap_heap_update_tag_disj'[OF _ tag_disj_via_td_name]] 2615 2616lemmas fpu_null_state_heap_update_tag_disj_simps = 2617 h_t_valid_fields_clift[THEN fpu_null_state_heap_update_tag_disj'[OF _ tag_disj_via_td_name]] 2618 2619end 2620end 2621