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