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 Invariants_H 12imports 13 LevityCatch 14 "AInvs.Deterministic_AI" 15 "AInvs.AInvs" 16 "Lib.AddUpdSimps" 17begin 18 19context Arch begin 20lemmas [crunch_def] = 21 deriveCap_def finaliseCap_def 22 hasCancelSendRights_def sameRegionAs_def isPhysicalCap_def 23 sameObjectAs_def updateCapData_def maskCapRights_def 24 createObject_def capUntypedPtr_def capUntypedSize_def 25 performInvocation_def decodeInvocation_def 26 27context begin global_naming global 28requalify_facts 29 Retype_H.deriveCap_def Retype_H.finaliseCap_def 30 Retype_H.hasCancelSendRights_def Retype_H.sameRegionAs_def Retype_H.isPhysicalCap_def 31 Retype_H.sameObjectAs_def Retype_H.updateCapData_def Retype_H.maskCapRights_def 32 Retype_H.createObject_def Retype_H.capUntypedPtr_def Retype_H.capUntypedSize_def 33 Retype_H.performInvocation_def Retype_H.decodeInvocation_def 34end 35 36end 37 38context begin interpretation Arch . (*FIXME: arch_split*) 39\<comment> \<open>---------------------------------------------------------------------------\<close> 40section "Invariants on Executable Spec" 41 42definition 43 "ps_clear p n s \<equiv> ({p .. p + (1 << n) - 1} - {p}) \<inter> dom (ksPSpace s) = {}" 44 45definition 46 "pspace_no_overlap' ptr bits \<equiv> 47 \<lambda>s. \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> 48 ({x .. x + (2 ^ objBitsKO ko) - 1}) \<inter> {ptr .. (ptr &&~~ mask bits) + (2 ^ bits - 1)} = {}" 49 50definition 51 "ko_wp_at' P p s \<equiv> 52 \<exists>ko. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) \<and> P ko \<and> 53 ps_clear p (objBitsKO ko) s" 54 55 56 57definition 58 obj_at' :: "('a::pspace_storable \<Rightarrow> bool) \<Rightarrow> word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 59where obj_at'_real_def: 60 "obj_at' P p s \<equiv> 61 ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> P obj) p s" 62 63definition 64 typ_at' :: "kernel_object_type \<Rightarrow> word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 65where 66 "typ_at' T \<equiv> ko_wp_at' (\<lambda>ko. koTypeOf ko = T)" 67 68abbreviation 69 "ep_at' \<equiv> obj_at' ((\<lambda>x. True) :: endpoint \<Rightarrow> bool)" 70abbreviation 71 "ntfn_at' \<equiv> obj_at' ((\<lambda>x. True) :: Structures_H.notification \<Rightarrow> bool)" 72abbreviation 73 "tcb_at' \<equiv> obj_at' ((\<lambda>x. True) :: tcb \<Rightarrow> bool)" 74abbreviation 75 "real_cte_at' \<equiv> obj_at' ((\<lambda>x. True) :: cte \<Rightarrow> bool)" 76 77abbreviation 78 "ko_at' v \<equiv> obj_at' (\<lambda>k. k = v)" 79 80abbreviation 81 "pde_at' \<equiv> typ_at' (ArchT PDET)" 82abbreviation 83 "pte_at' \<equiv> typ_at' (ArchT PTET)" 84end 85 86record itcb' = 87 itcbState :: thread_state 88 itcbFaultHandler :: cptr 89 itcbIPCBuffer :: vptr 90 itcbBoundNotification :: "word32 option" 91 itcbPriority :: priority 92 itcbFault :: "fault option" 93 itcbTimeSlice :: nat 94 itcbMCP :: priority 95 96definition "tcb_to_itcb' tcb \<equiv> \<lparr> itcbState = tcbState tcb, 97 itcbFaultHandler = tcbFaultHandler tcb, 98 itcbIPCBuffer = tcbIPCBuffer tcb, 99 itcbBoundNotification = tcbBoundNotification tcb, 100 itcbPriority = tcbPriority tcb, 101 itcbFault = tcbFault tcb, 102 itcbTimeSlice = tcbTimeSlice tcb, 103 itcbMCP = tcbMCP tcb\<rparr>" 104 105lemma [simp]: "itcbState (tcb_to_itcb' tcb) = tcbState tcb" 106 by (auto simp: tcb_to_itcb'_def) 107 108lemma [simp]: "itcbFaultHandler (tcb_to_itcb' tcb) = tcbFaultHandler tcb" 109 by (auto simp: tcb_to_itcb'_def) 110 111lemma [simp]: "itcbIPCBuffer (tcb_to_itcb' tcb) = tcbIPCBuffer tcb" 112 by (auto simp: tcb_to_itcb'_def) 113 114lemma [simp]: "itcbBoundNotification (tcb_to_itcb' tcb) = tcbBoundNotification tcb" 115 by (auto simp: tcb_to_itcb'_def) 116 117lemma [simp]: "itcbPriority (tcb_to_itcb' tcb) = tcbPriority tcb" 118 by (auto simp: tcb_to_itcb'_def) 119 120lemma [simp]: "itcbFault (tcb_to_itcb' tcb) = tcbFault tcb" 121 by (auto simp: tcb_to_itcb'_def) 122 123lemma [simp]: "itcbTimeSlice (tcb_to_itcb' tcb) = tcbTimeSlice tcb" 124 by (auto simp: tcb_to_itcb'_def) 125 126lemma [simp]: "itcbMCP (tcb_to_itcb' tcb) = tcbMCP tcb" 127 by (auto simp: tcb_to_itcb'_def) 128 129definition 130 pred_tcb_at' :: "(itcb' \<Rightarrow> 'a) \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 131where 132 "pred_tcb_at' proj test \<equiv> obj_at' (\<lambda>ko. test (proj (tcb_to_itcb' ko)))" 133 134abbreviation "st_tcb_at' \<equiv> pred_tcb_at' itcbState" 135abbreviation "bound_tcb_at' \<equiv> pred_tcb_at' itcbBoundNotification" 136abbreviation "mcpriority_tcb_at' \<equiv> pred_tcb_at' itcbMCP" 137 138lemma st_tcb_at'_def: 139 "st_tcb_at' test \<equiv> obj_at' (test \<circ> tcbState)" 140 by (simp add: pred_tcb_at'_def o_def) 141 142 143text {* cte with property at *} 144definition 145 "cte_wp_at' P p s \<equiv> \<exists>cte::cte. fst (getObject p s) = {(cte,s)} \<and> P cte" 146 147abbreviation 148 "cte_at' \<equiv> cte_wp_at' \<top>" 149 150definition 151 tcb_cte_cases :: "word32 \<rightharpoonup> ((tcb \<Rightarrow> cte) \<times> ((cte \<Rightarrow> cte) \<Rightarrow> tcb \<Rightarrow> tcb))" 152where 153 "tcb_cte_cases \<equiv> [ 0 \<mapsto> (tcbCTable, tcbCTable_update), 154 16 \<mapsto> (tcbVTable, tcbVTable_update), 155 32 \<mapsto> (tcbReply, tcbReply_update), 156 48 \<mapsto> (tcbCaller, tcbCaller_update), 157 64 \<mapsto> (tcbIPCBufferFrame, tcbIPCBufferFrame_update) ]" 158 159definition 160 max_ipc_words :: word32 161where 162 "max_ipc_words \<equiv> capTransferDataSize + msgMaxLength + msgMaxExtraCaps + 2" 163 164definition 165 tcb_st_refs_of' :: "Structures_H.thread_state \<Rightarrow> (word32 \<times> reftype) set" 166where 167 "tcb_st_refs_of' z \<equiv> case z of (Running) => {} 168 | (Inactive) => {} 169 | (Restart) => {} 170 | (BlockedOnReceive x) => {(x, TCBBlockedRecv)} 171 | (BlockedOnSend x a b c) => {(x, TCBBlockedSend)} 172 | (BlockedOnNotification x) => {(x, TCBSignal)} 173 | (BlockedOnReply) => {} 174 | (IdleThreadState) => {}" 175 176definition 177 ep_q_refs_of' :: "Structures_H.endpoint \<Rightarrow> (word32 \<times> reftype) set" 178where 179 "ep_q_refs_of' x \<equiv> case x of 180 IdleEP => {} 181 | (RecvEP q) => set q \<times> {EPRecv} 182 | (SendEP q) => set q \<times> {EPSend}" 183 184definition 185 ntfn_q_refs_of' :: "Structures_H.ntfn \<Rightarrow> (word32 \<times> reftype) set" 186where 187 "ntfn_q_refs_of' x \<equiv> case x of IdleNtfn => {} 188 | (WaitingNtfn q) => set q \<times> {NTFNSignal} 189 | (ActiveNtfn b) => {}" 190 191definition 192 ntfn_bound_refs' :: "word32 option \<Rightarrow> (word32 \<times> reftype) set" 193where 194 "ntfn_bound_refs' t \<equiv> set_option t \<times> {NTFNBound}" 195 196definition 197 tcb_bound_refs' :: "word32 option \<Rightarrow> (word32 \<times> reftype) set" 198where 199 "tcb_bound_refs' a \<equiv> set_option a \<times> {TCBBound}" 200 201definition 202 refs_of' :: "Structures_H.kernel_object \<Rightarrow> (word32 \<times> reftype) set" 203where 204 "refs_of' x \<equiv> case x of 205 (KOTCB tcb) => tcb_st_refs_of' (tcbState tcb) \<union> tcb_bound_refs' (tcbBoundNotification tcb) 206 | (KOCTE cte) => {} 207 | (KOEndpoint ep) => ep_q_refs_of' ep 208 | (KONotification ntfn) => ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn) 209 | (KOUserData) => {} 210 | (KOUserDataDevice) => {} 211 | (KOKernelData) => {} 212 | (KOArch ako) => {}" 213 214definition 215 state_refs_of' :: "kernel_state \<Rightarrow> word32 \<Rightarrow> (word32 \<times> reftype) set" 216where 217 "state_refs_of' s \<equiv> (\<lambda>x. case (ksPSpace s x) 218 of None \<Rightarrow> {} 219 | Some ko \<Rightarrow> 220 (if is_aligned x (objBitsKO ko) \<and> ps_clear x (objBitsKO ko) s 221 then refs_of' ko 222 else {}))" 223 224 225primrec 226 live' :: "Structures_H.kernel_object \<Rightarrow> bool" 227where 228 "live' (KOTCB tcb) = 229 (bound (tcbBoundNotification tcb) \<or> 230 (tcbState tcb \<noteq> Inactive \<and> tcbState tcb \<noteq> IdleThreadState) \<or> tcbQueued tcb)" 231| "live' (KOCTE cte) = False" 232| "live' (KOEndpoint ep) = (ep \<noteq> IdleEP)" 233| "live' (KONotification ntfn) = (bound (ntfnBoundTCB ntfn) \<or> (\<exists>ts. ntfnObj ntfn = WaitingNtfn ts))" 234| "live' (KOUserData) = False" 235| "live' (KOUserDataDevice) = False" 236| "live' (KOKernelData) = False" 237| "live' (KOArch ako) = False" 238 239primrec 240 zobj_refs' :: "capability \<Rightarrow> word32 set" 241where 242 "zobj_refs' NullCap = {}" 243| "zobj_refs' DomainCap = {}" 244| "zobj_refs' (UntypedCap d r n f) = {}" 245| "zobj_refs' (EndpointCap r badge x y z) = {r}" 246| "zobj_refs' (NotificationCap r badge x y) = {r}" 247| "zobj_refs' (CNodeCap r b g gsz) = {}" 248| "zobj_refs' (ThreadCap r) = {r}" 249| "zobj_refs' (Zombie r b n) = {}" 250| "zobj_refs' (ArchObjectCap ac) = {}" 251| "zobj_refs' (IRQControlCap) = {}" 252| "zobj_refs' (IRQHandlerCap irq) = {}" 253| "zobj_refs' (ReplyCap tcb m) = {}" 254 255definition 256 ex_nonz_cap_to' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 257where 258 "ex_nonz_cap_to' ref \<equiv> 259 (\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. ref \<in> zobj_refs' (cteCap c)) cref s)" 260 261definition 262 if_live_then_nonz_cap' :: "kernel_state \<Rightarrow> bool" 263where 264 "if_live_then_nonz_cap' s \<equiv> 265 \<forall>ptr. ko_wp_at' live' ptr s \<longrightarrow> ex_nonz_cap_to' ptr s" 266 267 268primrec 269 cte_refs' :: "capability \<Rightarrow> word32 \<Rightarrow> word32 set" 270where 271 "cte_refs' (UntypedCap d p n f) x = {}" 272| "cte_refs' (NullCap) x = {}" 273| "cte_refs' (DomainCap) x = {}" 274| "cte_refs' (EndpointCap ref badge s r g) x = {}" 275| "cte_refs' (NotificationCap ref badge s r) x = {}" 276| "cte_refs' (CNodeCap ref bits g gs) x = 277 (\<lambda>x. ref + (x * 2 ^ cteSizeBits)) ` {0 .. 2 ^ bits - 1}" 278| "cte_refs' (ThreadCap ref) x = 279 (\<lambda>x. ref + x) ` (dom tcb_cte_cases)" 280| "cte_refs' (Zombie r b n) x = 281 (\<lambda>x. r + (x * 2 ^ cteSizeBits)) ` {0 ..< of_nat n}" 282| "cte_refs' (ArchObjectCap cap) x = {}" 283| "cte_refs' (IRQControlCap) x = {}" 284| "cte_refs' (IRQHandlerCap irq) x = {x + (ucast irq) * 16}" 285| "cte_refs' (ReplyCap tcb m) x = {}" 286 287 288abbreviation 289 "irq_node' s \<equiv> intStateIRQNode (ksInterruptState s)" 290 291definition 292 ex_cte_cap_wp_to' :: "(capability \<Rightarrow> bool) \<Rightarrow> word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 293where 294 "ex_cte_cap_wp_to' P ptr \<equiv> \<lambda>s. \<exists>cref. 295 cte_wp_at' (\<lambda>c. P (cteCap c) 296 \<and> ptr \<in> cte_refs' (cteCap c) (irq_node' s)) cref s" 297 298abbreviation 299 "ex_cte_cap_to' \<equiv> ex_cte_cap_wp_to' \<top>" 300 301definition 302 if_unsafe_then_cap' :: "kernel_state \<Rightarrow> bool" 303where 304 "if_unsafe_then_cap' s \<equiv> \<forall>cref. cte_wp_at' (\<lambda>c. cteCap c \<noteq> NullCap) cref s \<longrightarrow> ex_cte_cap_to' cref s" 305 306section "Valid caps and objects (Haskell)" 307 308 309context begin interpretation Arch . (*FIXME: arch_split*) 310primrec 311 acapBits :: "arch_capability \<Rightarrow> nat" 312where 313 "acapBits (ASIDPoolCap x y) = asidLowBits + 2" 314| "acapBits ASIDControlCap = asidHighBits + 2" 315| "acapBits (PageCap d x y sz z) = pageBitsForSize sz" 316| "acapBits (PageTableCap x y) = 10" 317| "acapBits (PageDirectoryCap x y) = 14" 318end 319 320 321primrec 322 zBits :: "zombie_type \<Rightarrow> nat" 323where 324 "zBits (ZombieCNode n) = objBits (undefined::cte) + n" 325| "zBits (ZombieTCB) = tcbBlockSizeBits" 326 327primrec 328 capBits :: "capability \<Rightarrow> nat" 329where 330 "capBits NullCap = 0" 331| "capBits DomainCap = 0" 332| "capBits (UntypedCap d r b f) = b" 333| "capBits (EndpointCap r b x y z) = objBits (undefined::endpoint)" 334| "capBits (NotificationCap r b x y) = objBits (undefined::Structures_H.notification)" 335| "capBits (CNodeCap r b g gs) = objBits (undefined::cte) + b" 336| "capBits (ThreadCap r) = objBits (undefined::tcb)" 337| "capBits (Zombie r z n) = zBits z" 338| "capBits (IRQControlCap) = 0" 339| "capBits (IRQHandlerCap irq) = 0" 340| "capBits (ReplyCap tcb m) = objBits (undefined :: tcb)" 341| "capBits (ArchObjectCap x) = acapBits x" 342 343lemmas objBits_defs = 344 tcbBlockSizeBits_def epSizeBits_def ntfnSizeBits_def cteSizeBits_def 345 346definition 347 "capAligned c \<equiv> 348 is_aligned (capUntypedPtr c) (capBits c) \<and> capBits c < word_bits" 349 350definition 351 "obj_range' (p::word32) ko \<equiv> {p .. p + 2 ^ objBitsKO ko - 1}" 352 353primrec (nonexhaustive) 354 usableUntypedRange :: "capability \<Rightarrow> word32 set" 355where 356 "usableUntypedRange (UntypedCap d p n f) = 357 (if f < 2^n then {p+of_nat f .. p + 2 ^ n - 1} else {})" 358 359definition 360 "valid_untyped' d ptr bits idx s \<equiv> 361 \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {ptr .. ptr + 2 ^ bits - 1} \<subset> obj_range' ptr' ko 362 \<or> obj_range' ptr' ko \<inter> usableUntypedRange(UntypedCap d ptr bits idx) \<noteq> {}) ptr' s" 363 364 365 366context begin interpretation Arch . (*FIXME: arch_split*) 367 368definition 369 page_table_at' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 370where 371 "page_table_at' x \<equiv> \<lambda>s. is_aligned x ptBits 372 \<and> (\<forall>y < 2 ^ 8. typ_at' (ArchT PTET) (x + (y << 2)) s)" 373 374definition 375 page_directory_at' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 376where 377 "page_directory_at' x \<equiv> \<lambda>s. is_aligned x pdBits 378 \<and> (\<forall>y < 2 ^ 12. typ_at' (ArchT PDET) (x + (y << 2)) s)" 379 380abbreviation 381 "asid_pool_at' \<equiv> typ_at' (ArchT ASIDPoolT)" 382 383(* FIXME: duplicated with vmsz_aligned *) 384definition 385 "vmsz_aligned' ref sz \<equiv> is_aligned ref (pageBitsForSize sz)" 386 387primrec 388 zombieCTEs :: "zombie_type \<Rightarrow> nat" 389where 390 "zombieCTEs ZombieTCB = 5" 391| "zombieCTEs (ZombieCNode n) = (2 ^ n)" 392 393definition 394 valid_cap' :: "capability \<Rightarrow> kernel_state \<Rightarrow> bool" 395where valid_cap'_def: 396 "valid_cap' c s \<equiv> capAligned c \<and> 397 (case c of 398 Structures_H.NullCap \<Rightarrow> True 399 | Structures_H.DomainCap \<Rightarrow> True 400 | Structures_H.UntypedCap d r n f \<Rightarrow> 401 valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits 402 \<and> f \<le> 2^n \<and> is_aligned (of_nat f :: word32) minUntypedSizeBits 403 | Structures_H.EndpointCap r badge x y z \<Rightarrow> ep_at' r s 404 | Structures_H.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s 405 | Structures_H.CNodeCap r bits guard guard_sz \<Rightarrow> 406 bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> 407 guard && mask guard_sz = guard \<and> 408 (\<forall>addr. real_cte_at' (r + 2^cteSizeBits * (addr && mask bits)) s) 409 | Structures_H.ThreadCap r \<Rightarrow> tcb_at' r s 410 | Structures_H.ReplyCap r m \<Rightarrow> tcb_at' r s 411 | Structures_H.IRQControlCap \<Rightarrow> True 412 | Structures_H.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ 413 | Structures_H.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits 414 \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 415 \<and> (\<forall>addr. real_cte_at' (r + 2^cteSizeBits * (addr && mask n)) s)) 416 | Structures_H.ArchObjectCap ac \<Rightarrow> (case ac of 417 ASIDPoolCap pool asid \<Rightarrow> 418 typ_at' (ArchT ASIDPoolT) pool s \<and> is_aligned asid asid_low_bits \<and> asid \<le> 2^asid_bits - 1 419 | ASIDControlCap \<Rightarrow> True 420 | PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> 421 (\<forall>p < 2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) 422 (ref + p * 2 ^ pageBits) s) \<and> 423 (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 424 0 < asid \<and> asid \<le> 2 ^ asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < kernelBase) 425 | PageTableCap ref mapdata \<Rightarrow> 426 page_table_at' ref s \<and> 427 (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 428 0 < asid \<and> asid \<le> 2^asid_bits - 1 \<and> ref < kernelBase) 429 | PageDirectoryCap ref mapdata \<Rightarrow> 430 page_directory_at' ref s \<and> 431 case_option True (\<lambda>asid. 0 < asid \<and> asid \<le> 2^asid_bits - 1) mapdata))" 432 433abbreviation (input) 434 valid_cap'_syn :: "kernel_state \<Rightarrow> capability \<Rightarrow> bool" ("_ \<turnstile>' _" [60, 60] 61) 435where 436 "s \<turnstile>' c \<equiv> valid_cap' c s" 437 438definition 439 valid_cte' :: "cte \<Rightarrow> kernel_state \<Rightarrow> bool" 440where 441 "valid_cte' cte s \<equiv> s \<turnstile>' (cteCap cte)" 442 443definition 444 valid_tcb_state' :: "Structures_H.thread_state \<Rightarrow> kernel_state \<Rightarrow> bool" 445where 446 "valid_tcb_state' ts s \<equiv> case ts of 447 Structures_H.BlockedOnReceive ref \<Rightarrow> ep_at' ref s 448 | Structures_H.BlockedOnSend ref b d c \<Rightarrow> ep_at' ref s 449 | Structures_H.BlockedOnNotification ref \<Rightarrow> ntfn_at' ref s 450 | _ \<Rightarrow> True" 451 452definition 453 valid_ipc_buffer_ptr' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 454where 455 "valid_ipc_buffer_ptr' a s \<equiv> is_aligned a msg_align_bits \<and> typ_at' UserDataT (a && ~~ mask pageBits) s" 456 457definition 458 valid_bound_ntfn' :: "word32 option \<Rightarrow> kernel_state \<Rightarrow> bool" 459where 460 "valid_bound_ntfn' ntfn_opt s \<equiv> case ntfn_opt of 461 None \<Rightarrow> True 462 | Some a \<Rightarrow> ntfn_at' a s" 463 464definition 465 is_device_page_cap' :: "capability \<Rightarrow> bool" 466where 467 "is_device_page_cap' cap \<equiv> case cap of 468 capability.ArchObjectCap (arch_capability.PageCap dev _ _ _ _) \<Rightarrow> dev 469 | _ \<Rightarrow> False" 470 471definition 472 valid_tcb' :: "Structures_H.tcb \<Rightarrow> kernel_state \<Rightarrow> bool" 473where 474 "valid_tcb' t s \<equiv> (\<forall>(getF, setF) \<in> ran tcb_cte_cases. s \<turnstile>' cteCap (getF t)) 475 \<and> valid_tcb_state' (tcbState t) s 476 \<and> is_aligned (tcbIPCBuffer t) msg_align_bits 477 \<and> valid_bound_ntfn' (tcbBoundNotification t) s 478 \<and> tcbDomain t \<le> maxDomain 479 \<and> tcbPriority t \<le> maxPriority 480 \<and> tcbMCP t \<le> maxPriority" 481 482definition 483 valid_ep' :: "Structures_H.endpoint \<Rightarrow> kernel_state \<Rightarrow> bool" 484where 485 "valid_ep' ep s \<equiv> case ep of 486 Structures_H.IdleEP \<Rightarrow> True 487 | Structures_H.SendEP ts \<Rightarrow> (ts \<noteq> [] \<and> (\<forall>t \<in> set ts. tcb_at' t s) \<and> distinct ts) 488 | Structures_H.RecvEP ts \<Rightarrow> (ts \<noteq> [] \<and> (\<forall>t \<in> set ts. tcb_at' t s) \<and> distinct ts)" 489 490 491definition 492 valid_bound_tcb' :: "word32 option \<Rightarrow> kernel_state \<Rightarrow> bool" 493where 494 "valid_bound_tcb' tcb_opt s \<equiv> case tcb_opt of 495 None \<Rightarrow> True 496 | Some t \<Rightarrow> tcb_at' t s" 497 498definition 499 valid_ntfn' :: "Structures_H.notification \<Rightarrow> kernel_state \<Rightarrow> bool" 500where 501 "valid_ntfn' ntfn s \<equiv> (case ntfnObj ntfn of 502 Structures_H.IdleNtfn \<Rightarrow> True 503 | Structures_H.WaitingNtfn ts \<Rightarrow> 504 (ts \<noteq> [] \<and> (\<forall>t \<in> set ts. tcb_at' t s) \<and> distinct ts 505 \<and> (case ntfnBoundTCB ntfn of Some tcb \<Rightarrow> ts = [tcb] | _ \<Rightarrow> True)) 506 | Structures_H.ActiveNtfn b \<Rightarrow> True) 507 \<and> valid_bound_tcb' (ntfnBoundTCB ntfn) s" 508 509definition 510 valid_mapping' :: "word32 \<Rightarrow> vmpage_size \<Rightarrow> kernel_state \<Rightarrow> bool" 511where 512 "valid_mapping' x sz s \<equiv> is_aligned x (pageBitsForSize sz) 513 \<and> ptrFromPAddr x \<noteq> 0" 514 515primrec 516 valid_pte' :: "ARM_H.pte \<Rightarrow> kernel_state \<Rightarrow> bool" 517where 518 "valid_pte' (InvalidPTE) = \<top>" 519| "valid_pte' (LargePagePTE ptr _ _ _ _) = (valid_mapping' ptr ARMLargePage)" 520| "valid_pte' (SmallPagePTE ptr _ _ _ _) = (valid_mapping' ptr ARMSmallPage)" 521 522primrec 523 valid_pde' :: "ARM_H.pde \<Rightarrow> kernel_state \<Rightarrow> bool" 524where 525 "valid_pde' (InvalidPDE) = \<top>" 526| "valid_pde' (SectionPDE ptr _ _ _ _ _ _) = (valid_mapping' ptr ARMSection)" 527| "valid_pde' (SuperSectionPDE ptr _ _ _ _ _) = (valid_mapping' ptr ARMSuperSection)" 528| "valid_pde' (PageTablePDE ptr _ _) = (\<lambda>_. is_aligned ptr ptBits)" 529 530primrec 531 valid_asid_pool' :: "asidpool \<Rightarrow> kernel_state \<Rightarrow> bool" 532where 533 "valid_asid_pool' (ASIDPool pool) 534 = (\<lambda>s. dom pool \<subseteq> {0 .. 2^asid_low_bits - 1} 535 \<and> 0 \<notin> ran pool \<and> (\<forall>x \<in> ran pool. is_aligned x pdBits))" 536 537primrec 538 valid_arch_obj' :: "arch_kernel_object \<Rightarrow> kernel_state \<Rightarrow> bool" 539where 540 "valid_arch_obj' (KOASIDPool pool) = valid_asid_pool' pool" 541| "valid_arch_obj' (KOPDE pde) = valid_pde' pde" 542| "valid_arch_obj' (KOPTE pte) = valid_pte' pte" 543 544definition 545 valid_obj' :: "Structures_H.kernel_object \<Rightarrow> kernel_state \<Rightarrow> bool" 546where 547 "valid_obj' ko s \<equiv> case ko of 548 KOEndpoint endpoint \<Rightarrow> valid_ep' endpoint s 549 | KONotification notification \<Rightarrow> valid_ntfn' notification s 550 | KOKernelData \<Rightarrow> False 551 | KOUserData \<Rightarrow> True 552 | KOUserDataDevice \<Rightarrow> True 553 | KOTCB tcb \<Rightarrow> valid_tcb' tcb s 554 | KOCTE cte \<Rightarrow> valid_cte' cte s 555 | KOArch arch_kernel_object \<Rightarrow> valid_arch_obj' arch_kernel_object s" 556 557definition 558 pspace_aligned' :: "kernel_state \<Rightarrow> bool" 559where 560 "pspace_aligned' s \<equiv> 561 \<forall>x \<in> dom (ksPSpace s). is_aligned x (objBitsKO (the (ksPSpace s x)))" 562 563definition 564 pspace_distinct' :: "kernel_state \<Rightarrow> bool" 565where 566 "pspace_distinct' s \<equiv> 567 \<forall>x \<in> dom (ksPSpace s). ps_clear x (objBitsKO (the (ksPSpace s x))) s" 568 569definition 570 valid_objs' :: "kernel_state \<Rightarrow> bool" 571where 572 "valid_objs' s \<equiv> \<forall>obj \<in> ran (ksPSpace s). valid_obj' obj s" 573 574type_synonym cte_heap = "word32 \<Rightarrow> cte option" 575 576definition 577 map_to_ctes :: "(word32 \<rightharpoonup> kernel_object) \<Rightarrow> cte_heap" 578where 579 "map_to_ctes m \<equiv> \<lambda>x. 580 let cte_bits = objBitsKO (KOCTE undefined); 581 tcb_bits = objBitsKO (KOTCB undefined); 582 y = (x && (~~ mask tcb_bits)) 583 in 584 if \<exists>cte. m x = Some (KOCTE cte) \<and> is_aligned x cte_bits 585 \<and> {x + 1 .. x + (1 << cte_bits) - 1} \<inter> dom m = {} 586 then case m x of Some (KOCTE cte) \<Rightarrow> Some cte 587 else if \<exists>tcb. m y = Some (KOTCB tcb) 588 \<and> {y + 1 .. y + (1 << tcb_bits) - 1} \<inter> dom m = {} 589 then case m y of Some (KOTCB tcb) \<Rightarrow> 590 option_map (\<lambda>(getF, setF). getF tcb) (tcb_cte_cases (x - y)) 591 else None" 592 593abbreviation 594 "ctes_of s \<equiv> map_to_ctes (ksPSpace s)" 595 596definition 597 mdb_next :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 option" 598where 599 "mdb_next s c \<equiv> option_map (mdbNext o cteMDBNode) (s c)" 600 601definition 602 mdb_next_rel :: "cte_heap \<Rightarrow> (word32 \<times> word32) set" 603where 604 "mdb_next_rel m \<equiv> {(x, y). mdb_next m x = Some y}" 605 606abbreviation 607 mdb_next_direct :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool" ("_ \<turnstile> _ \<leadsto> _" [60,0,60] 61) 608where 609 "m \<turnstile> a \<leadsto> b \<equiv> (a, b) \<in> mdb_next_rel m" 610 611abbreviation 612 mdb_next_trans :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool" ("_ \<turnstile> _ \<leadsto>\<^sup>+ _" [60,0,60] 61) 613where 614 "m \<turnstile> a \<leadsto>\<^sup>+ b \<equiv> (a,b) \<in> (mdb_next_rel m)\<^sup>+" 615 616abbreviation 617 mdb_next_rtrans :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool" ("_ \<turnstile> _ \<leadsto>\<^sup>* _" [60,0,60] 61) 618where 619 "m \<turnstile> a \<leadsto>\<^sup>* b \<equiv> (a,b) \<in> (mdb_next_rel m)\<^sup>*" 620 621definition 622 "valid_badges m \<equiv> 623 \<forall>p p' cap node cap' node'. 624 m p = Some (CTE cap node) \<longrightarrow> 625 m p' = Some (CTE cap' node') \<longrightarrow> 626 (m \<turnstile> p \<leadsto> p') \<longrightarrow> 627 (sameRegionAs cap cap') \<longrightarrow> 628 (isEndpointCap cap \<longrightarrow> 629 capEPBadge cap \<noteq> capEPBadge cap' \<longrightarrow> 630 capEPBadge cap' \<noteq> 0 \<longrightarrow> 631 mdbFirstBadged node') 632 \<and> 633 (isNotificationCap cap \<longrightarrow> 634 capNtfnBadge cap \<noteq> capNtfnBadge cap' \<longrightarrow> 635 capNtfnBadge cap' \<noteq> 0 \<longrightarrow> 636 mdbFirstBadged node')" 637 638fun (sequential) 639 untypedRange :: "capability \<Rightarrow> word32 set" 640where 641 "untypedRange (UntypedCap d p n f) = {p .. p + 2 ^ n - 1}" 642| "untypedRange c = {}" 643 644primrec 645 acapClass :: "arch_capability \<Rightarrow> capclass" 646where 647 "acapClass (ASIDPoolCap x y) = PhysicalClass" 648| "acapClass ASIDControlCap = ASIDMasterClass" 649| "acapClass (PageCap d x y sz z) = PhysicalClass" 650| "acapClass (PageTableCap x y) = PhysicalClass" 651| "acapClass (PageDirectoryCap x y) = PhysicalClass" 652 653primrec 654 capClass :: "capability \<Rightarrow> capclass" 655where 656 "capClass (NullCap) = NullClass" 657| "capClass (DomainCap) = DomainClass" 658| "capClass (UntypedCap d p n f) = PhysicalClass" 659| "capClass (EndpointCap ref badge s r g) = PhysicalClass" 660| "capClass (NotificationCap ref badge s r) = PhysicalClass" 661| "capClass (CNodeCap ref bits g gs) = PhysicalClass" 662| "capClass (ThreadCap ref) = PhysicalClass" 663| "capClass (Zombie r b n) = PhysicalClass" 664| "capClass (IRQControlCap) = IRQClass" 665| "capClass (IRQHandlerCap irq) = IRQClass" 666| "capClass (ReplyCap tcb m) = ReplyClass tcb" 667| "capClass (ArchObjectCap cap) = acapClass cap" 668 669definition 670 "capRange cap \<equiv> 671 if capClass cap \<noteq> PhysicalClass then {} 672 else {capUntypedPtr cap .. capUntypedPtr cap + 2 ^ capBits cap - 1}" 673 674definition 675 "caps_contained' m \<equiv> 676 \<forall>p p' c n c' n'. 677 m p = Some (CTE c n) \<longrightarrow> 678 m p' = Some (CTE c' n') \<longrightarrow> 679 \<not>isUntypedCap c' \<longrightarrow> 680 capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> 681 capRange c' \<subseteq> untypedRange c" 682 683definition 684 valid_dlist :: "cte_heap \<Rightarrow> bool" 685where 686 "valid_dlist m \<equiv> 687 \<forall>p cte. m p = Some cte \<longrightarrow> 688 (let prev = mdbPrev (cteMDBNode cte); 689 next = mdbNext (cteMDBNode cte) 690 in (prev \<noteq> 0 \<longrightarrow> (\<exists>cte'. m prev = Some cte' \<and> mdbNext (cteMDBNode cte') = p)) \<and> 691 (next \<noteq> 0 \<longrightarrow> (\<exists>cte'. m next = Some cte' \<and> mdbPrev (cteMDBNode cte') = p)))" 692 693definition 694 "no_0 m \<equiv> m 0 = None" 695definition 696 "no_loops m \<equiv> \<forall>c. \<not> m \<turnstile> c \<leadsto>\<^sup>+ c" 697definition 698 "mdb_chain_0 m \<equiv> \<forall>x \<in> dom m. m \<turnstile> x \<leadsto>\<^sup>+ 0" 699 700definition 701 "class_links m \<equiv> \<forall>p p' cte cte'. 702 m p = Some cte \<longrightarrow> 703 m p' = Some cte' \<longrightarrow> 704 m \<turnstile> p \<leadsto> p' \<longrightarrow> 705 capClass (cteCap cte) = capClass (cteCap cte')" 706 707definition 708 "is_chunk m cap p p' \<equiv> 709 \<forall>p''. m \<turnstile> p \<leadsto>\<^sup>+ p'' \<longrightarrow> m \<turnstile> p'' \<leadsto>\<^sup>* p' \<longrightarrow> 710 (\<exists>cap'' n''. m p'' = Some (CTE cap'' n'') \<and> sameRegionAs cap cap'')" 711 712definition 713 "mdb_chunked m \<equiv> \<forall>p p' cap cap' n n'. 714 m p = Some (CTE cap n) \<longrightarrow> 715 m p' = Some (CTE cap' n') \<longrightarrow> 716 sameRegionAs cap cap' \<longrightarrow> 717 p \<noteq> p' \<longrightarrow> 718 (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> 719 (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> 720 (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)" 721 722definition 723 parentOf :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool" ("_ \<turnstile> _ parentOf _") 724where 725 "s \<turnstile> c' parentOf c \<equiv> 726 \<exists>cte' cte. s c = Some cte \<and> s c' = Some cte' \<and> isMDBParentOf cte' cte" 727 728 729context 730notes [[inductive_internals =true]] 731begin 732 733inductive 734 subtree :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool" ("_ \<turnstile> _ \<rightarrow> _" [60,0,60] 61) 735 for s :: cte_heap and c :: word32 736where 737 direct_parent: 738 "\<lbrakk> s \<turnstile> c \<leadsto> c'; c' \<noteq> 0; s \<turnstile> c parentOf c'\<rbrakk> \<Longrightarrow> s \<turnstile> c \<rightarrow> c'" 739 | 740 trans_parent: 741 "\<lbrakk> s \<turnstile> c \<rightarrow> c'; s \<turnstile> c' \<leadsto> c''; c'' \<noteq> 0; s \<turnstile> c parentOf c'' \<rbrakk> \<Longrightarrow> s \<turnstile> c \<rightarrow> c''" 742 743end 744 745definition 746 "descendants_of' c s \<equiv> {c'. s \<turnstile> c \<rightarrow> c'}" 747 748definition 749 "untyped_mdb' m \<equiv> 750 \<forall>p p' c n c' n'. 751 m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> 752 m p' = Some (CTE c' n') \<longrightarrow> \<not> isUntypedCap c' \<longrightarrow> 753 capRange c' \<inter> untypedRange c \<noteq> {} \<longrightarrow> 754 p' \<in> descendants_of' p m" 755 756definition 757 "untyped_inc' m \<equiv> 758 \<forall>p p' c c' n n'. 759 m p = Some (CTE c n) \<longrightarrow> isUntypedCap c \<longrightarrow> 760 m p' = Some (CTE c' n') \<longrightarrow> isUntypedCap c' \<longrightarrow> 761 (untypedRange c \<subseteq> untypedRange c' \<or> 762 untypedRange c' \<subseteq> untypedRange c \<or> 763 untypedRange c \<inter> untypedRange c' = {}) \<and> 764 (untypedRange c \<subset> untypedRange c' \<longrightarrow> (p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' ={})) \<and> 765 (untypedRange c' \<subset> untypedRange c \<longrightarrow> (p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c ={})) \<and> 766 (untypedRange c = untypedRange c' \<longrightarrow> (p' \<in> descendants_of' p m \<and> usableUntypedRange c={} 767 \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p'))" 768 769definition 770 "valid_nullcaps m \<equiv> \<forall>p n. m p = Some (CTE NullCap n) \<longrightarrow> n = nullMDBNode" 771 772definition 773 "ut_revocable' m \<equiv> \<forall>p cap n. m p = Some (CTE cap n) \<longrightarrow> isUntypedCap cap \<longrightarrow> mdbRevocable n" 774 775definition 776 "irq_control m \<equiv> 777 \<forall>p n. m p = Some (CTE IRQControlCap n) \<longrightarrow> 778 mdbRevocable n \<and> 779 (\<forall>p' n'. m p' = Some (CTE IRQControlCap n') \<longrightarrow> p' = p)" 780 781definition 782 isArchPageCap :: "capability \<Rightarrow> bool" 783where 784 "isArchPageCap cap \<equiv> case cap of ArchObjectCap (PageCap d ref rghts sz data) \<Rightarrow> True | _ \<Rightarrow> False" 785 786definition 787 distinct_zombie_caps :: "(word32 \<Rightarrow> capability option) \<Rightarrow> bool" 788where 789 "distinct_zombie_caps caps \<equiv> \<forall>ptr ptr' cap cap'. caps ptr = Some cap 790 \<and> caps ptr' = Some cap' \<and> ptr \<noteq> ptr' \<and> isZombie cap 791 \<and> capClass cap' = PhysicalClass \<and> \<not> isUntypedCap cap' \<and> \<not> isArchPageCap cap' 792 \<and> capBits cap = capBits cap' \<longrightarrow> capUntypedPtr cap \<noteq> capUntypedPtr cap'" 793 794definition 795 distinct_zombies :: "cte_heap \<Rightarrow> bool" 796where 797 "distinct_zombies m \<equiv> distinct_zombie_caps (option_map cteCap \<circ> m)" 798 799definition 800 reply_masters_rvk_fb :: "cte_heap \<Rightarrow> bool" 801where 802 "reply_masters_rvk_fb ctes \<equiv> \<forall>cte \<in> ran ctes. 803 isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte) 804 \<longrightarrow> mdbRevocable (cteMDBNode cte) \<and> mdbFirstBadged (cteMDBNode cte)" 805 806definition 807 valid_mdb_ctes :: "cte_heap \<Rightarrow> bool" 808where 809 "valid_mdb_ctes \<equiv> \<lambda>m. valid_dlist m \<and> no_0 m \<and> mdb_chain_0 m \<and> 810 valid_badges m \<and> caps_contained' m \<and> 811 mdb_chunked m \<and> untyped_mdb' m \<and> 812 untyped_inc' m \<and> valid_nullcaps m \<and> 813 ut_revocable' m \<and> class_links m \<and> distinct_zombies m 814 \<and> irq_control m \<and> reply_masters_rvk_fb m" 815 816definition 817 valid_mdb' :: "kernel_state \<Rightarrow> bool" 818where 819 "valid_mdb' \<equiv> \<lambda>s. valid_mdb_ctes (ctes_of s)" 820 821definition 822 "no_0_obj' \<equiv> \<lambda>s. ksPSpace s 0 = None" 823 824definition 825 vs_ptr_align :: "Structures_H.kernel_object \<Rightarrow> nat" where 826 "vs_ptr_align obj \<equiv> 827 case obj of KOArch (KOPTE (pte.LargePagePTE _ _ _ _ _)) \<Rightarrow> 6 828 | KOArch (KOPDE (pde.SuperSectionPDE _ _ _ _ _ _)) \<Rightarrow> 6 829 | _ \<Rightarrow> 0" 830 831definition "vs_valid_duplicates' \<equiv> \<lambda>h. 832 \<forall>x y. case h x of None \<Rightarrow> True 833 | Some ko \<Rightarrow> is_aligned y 2 \<longrightarrow> 834 x && ~~ mask (vs_ptr_align ko) = y && ~~ mask (vs_ptr_align ko) \<longrightarrow> 835 h x = h y" 836 837definition 838 valid_pspace' :: "kernel_state \<Rightarrow> bool" 839where 840 "valid_pspace' \<equiv> valid_objs' and 841 pspace_aligned' and 842 pspace_distinct' and 843 no_0_obj' and 844 valid_mdb'" 845 846primrec 847 runnable' :: "Structures_H.thread_state \<Rightarrow> bool" 848where 849 "runnable' (Structures_H.Running) = True" 850| "runnable' (Structures_H.Inactive) = False" 851| "runnable' (Structures_H.Restart) = True" 852| "runnable' (Structures_H.IdleThreadState) = False" 853| "runnable' (Structures_H.BlockedOnReceive a) = False" 854| "runnable' (Structures_H.BlockedOnReply) = False" 855| "runnable' (Structures_H.BlockedOnSend a b c d) = False" 856| "runnable' (Structures_H.BlockedOnNotification x) = False" 857 858definition 859 inQ :: "domain \<Rightarrow> priority \<Rightarrow> tcb \<Rightarrow> bool" 860where 861 "inQ d p tcb \<equiv> tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d" 862 863definition 864 (* for given domain and priority, the scheduler bitmap indicates a thread is in the queue *) 865 (* second level of the bitmap is stored in reverse for better cache locality in common case *) 866 bitmapQ :: "domain \<Rightarrow> priority \<Rightarrow> kernel_state \<Rightarrow> bool" 867where 868 "bitmapQ d p s \<equiv> ksReadyQueuesL1Bitmap s d !! prioToL1Index p 869 \<and> ksReadyQueuesL2Bitmap s (d, invertL1Index (prioToL1Index p)) 870 !! unat (p && mask wordRadix)" 871 872definition 873 valid_queues_no_bitmap :: "kernel_state \<Rightarrow> bool" 874where 875 "valid_queues_no_bitmap \<equiv> \<lambda>s. 876 (\<forall>d p. (\<forall>t \<in> set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) 877 \<and> distinct (ksReadyQueues s (d, p)) 878 \<and> (d > maxDomain \<or> p > maxPriority \<longrightarrow> ksReadyQueues s (d,p) = []))" 879 880definition 881 (* A priority is used as a two-part key into the bitmap structure. If an L2 bitmap entry 882 is set without an L1 entry, updating the L1 entry (shared by many priorities) may make 883 unexpected threads schedulable *) 884 bitmapQ_no_L2_orphans :: "kernel_state \<Rightarrow> bool" 885where 886 "bitmapQ_no_L2_orphans \<equiv> \<lambda>s. 887 \<forall>d i j. ksReadyQueuesL2Bitmap s (d, invertL1Index i) !! j \<and> i < l2BitmapSize 888 \<longrightarrow> (ksReadyQueuesL1Bitmap s d !! i)" 889 890definition 891 (* If the scheduler finds a set bit in L1 of the bitmap, it must find some bit set in L2 892 when it looks there. This lets it omit a check. 893 L2 entries have wordBits bits each. That means the L1 word only indexes 894 a small number of L2 entries, despite being stored in a wordBits word. 895 We allow only bits corresponding to L2 indices to be set. 896 *) 897 bitmapQ_no_L1_orphans :: "kernel_state \<Rightarrow> bool" 898where 899 "bitmapQ_no_L1_orphans \<equiv> \<lambda>s. 900 \<forall>d i. ksReadyQueuesL1Bitmap s d !! i \<longrightarrow> ksReadyQueuesL2Bitmap s (d, invertL1Index i) \<noteq> 0 \<and> 901 i < l2BitmapSize" 902 903definition 904 valid_bitmapQ :: "kernel_state \<Rightarrow> bool" 905where 906 "valid_bitmapQ \<equiv> \<lambda>s. (\<forall>d p. bitmapQ d p s \<longleftrightarrow> ksReadyQueues s (d,p) \<noteq> [])" 907 908definition 909 valid_queues :: "kernel_state \<Rightarrow> bool" 910where 911 "valid_queues \<equiv> \<lambda>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> 912 bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s" 913 914definition 915 (* when a thread gets added to / removed from a queue, but before bitmap updated *) 916 valid_bitmapQ_except :: "domain \<Rightarrow> priority \<Rightarrow> kernel_state \<Rightarrow> bool" 917where 918 "valid_bitmapQ_except d' p' \<equiv> \<lambda>s. 919 (\<forall>d p. (d \<noteq> d' \<or> p \<noteq> p') \<longrightarrow> (bitmapQ d p s \<longleftrightarrow> ksReadyQueues s (d,p) \<noteq> []))" 920 921lemmas bitmapQ_defs = valid_bitmapQ_def valid_bitmapQ_except_def bitmapQ_def 922 bitmapQ_no_L2_orphans_def bitmapQ_no_L1_orphans_def 923 924definition 925 valid_queues' :: "kernel_state \<Rightarrow> bool" 926where 927 "valid_queues' \<equiv> \<lambda>s. \<forall>d p t. obj_at' (inQ d p) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))" 928 929definition tcb_in_cur_domain' :: "32 word \<Rightarrow> kernel_state \<Rightarrow> bool" where 930 "tcb_in_cur_domain' t \<equiv> \<lambda>s. obj_at' (\<lambda>tcb. ksCurDomain s = tcbDomain tcb) t s" 931 932definition 933 ct_idle_or_in_cur_domain' :: "kernel_state \<Rightarrow> bool" where 934 "ct_idle_or_in_cur_domain' \<equiv> \<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> 935 ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s" 936 937definition 938 "ct_in_state' test \<equiv> \<lambda>s. st_tcb_at' test (ksCurThread s) s" 939 940definition 941 "ct_not_inQ \<equiv> \<lambda>s. ksSchedulerAction s = ResumeCurrentThread 942 \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s" 943 944abbreviation 945 "idle' \<equiv> \<lambda>st. st = Structures_H.IdleThreadState" 946 947abbreviation 948 "activatable' st \<equiv> runnable' st \<or> idle' st" 949 950primrec 951 sch_act_wf :: "scheduler_action \<Rightarrow> kernel_state \<Rightarrow> bool" 952where 953 "sch_act_wf ResumeCurrentThread = ct_in_state' activatable'" 954| "sch_act_wf ChooseNewThread = \<top>" 955| "sch_act_wf (SwitchToThread t) = (\<lambda>s. st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s)" 956 957definition 958 sch_act_simple :: "kernel_state \<Rightarrow> bool" 959where 960 "sch_act_simple \<equiv> \<lambda>s. (ksSchedulerAction s = ResumeCurrentThread) \<or> 961 (ksSchedulerAction s = ChooseNewThread)" 962 963definition 964 sch_act_sane :: "kernel_state \<Rightarrow> bool" 965where 966 "sch_act_sane \<equiv> 967 \<lambda>s. \<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<noteq> ksCurThread s" 968 969abbreviation 970 "sch_act_not t \<equiv> \<lambda>s. ksSchedulerAction s \<noteq> SwitchToThread t" 971 972abbreviation "idle_tcb_at' \<equiv> pred_tcb_at' (\<lambda>t. (itcbState t, itcbBoundNotification t))" 973 974definition 975 valid_idle' :: "kernel_state \<Rightarrow> bool" 976where 977 "valid_idle' \<equiv> \<lambda>s. idle_tcb_at' (\<lambda>p. idle' (fst p) \<and> snd p = None) (ksIdleThread s) s" 978 979definition 980 valid_irq_node' :: "word32 \<Rightarrow> kernel_state \<Rightarrow> bool" 981where 982 "valid_irq_node' x \<equiv> 983 \<lambda>s. is_aligned x 12 \<and> (\<forall>irq :: irq. real_cte_at' (x + 16 * (ucast irq)) s)" 984 985definition 986 valid_refs' :: "word32 set \<Rightarrow> cte_heap \<Rightarrow> bool" 987where 988 "valid_refs' R \<equiv> \<lambda>m. \<forall>c \<in> ran m. R \<inter> capRange (cteCap c) = {}" 989 990definition 991 page_directory_refs' :: "word32 \<Rightarrow> word32 set" 992where 993 "page_directory_refs' x \<equiv> (\<lambda>y. x + (y << 2)) ` {y. y < 2 ^ 12}" 994 995definition 996 page_table_refs' :: "word32 \<Rightarrow> word32 set" 997where 998 "page_table_refs' x \<equiv> (\<lambda>y. x + (y << 2)) ` {y. y < 2 ^ 8}" 999 1000definition 1001 global_refs' :: "kernel_state \<Rightarrow> obj_ref set" 1002where 1003 "global_refs' \<equiv> \<lambda>s. 1004 {ksIdleThread s} \<union> 1005 page_directory_refs' (armKSGlobalPD (ksArchState s)) \<union> 1006 (\<Union>pt \<in> set (armKSGlobalPTs (ksArchState s)). page_table_refs' pt) \<union> 1007 range (\<lambda>irq :: irq. irq_node' s + 16 * ucast irq)" 1008 1009definition 1010 valid_cap_sizes' :: "nat \<Rightarrow> cte_heap \<Rightarrow> bool" 1011where 1012 "valid_cap_sizes' n hp = (\<forall>cte \<in> ran hp. 2 ^ capBits (cteCap cte) \<le> n)" 1013 1014definition 1015 valid_global_refs' :: "kernel_state \<Rightarrow> bool" 1016where 1017 "valid_global_refs' \<equiv> \<lambda>s. valid_refs' kernel_data_refs (ctes_of s) 1018 \<and> global_refs' s \<subseteq> kernel_data_refs 1019 \<and> valid_cap_sizes' (gsMaxObjectSize s) (ctes_of s)" 1020 1021definition 1022 pspace_domain_valid :: "kernel_state \<Rightarrow> bool" 1023where 1024 "pspace_domain_valid = (\<lambda>s. \<forall>x ko. ksPSpace s x = Some ko \<longrightarrow> 1025 ({x .. x + (2 ^ objBitsKO ko) - 1}) \<inter> kernel_data_refs = {})" 1026 1027definition 1028 valid_asid_table' :: "(asid \<rightharpoonup> word32) \<Rightarrow> kernel_state \<Rightarrow> bool" 1029where 1030 "valid_asid_table' table \<equiv> \<lambda>s. dom table \<subseteq> {0 .. 2^asid_high_bits - 1} 1031 \<and> 0 \<notin> ran table" 1032 1033definition 1034 valid_global_pts' :: "word32 list \<Rightarrow> kernel_state \<Rightarrow> bool" 1035where 1036 "valid_global_pts' pts \<equiv> \<lambda>s. \<forall>p \<in> set pts. page_table_at' p s" 1037 1038definition 1039 valid_asid_map' :: "(word32 \<rightharpoonup> word8 \<times> word32) \<Rightarrow> bool" 1040where 1041 "valid_asid_map' m \<equiv> inj_on (option_map snd o m) (dom m) 1042 \<and> dom m \<subseteq> ({0 .. mask asid_bits} - {0})" 1043 1044definition 1045 valid_arch_state' :: "kernel_state \<Rightarrow> bool" 1046where 1047 "valid_arch_state' \<equiv> \<lambda>s. 1048 valid_asid_table' (armKSASIDTable (ksArchState s)) s \<and> 1049 page_directory_at' (armKSGlobalPD (ksArchState s)) s \<and> 1050 valid_global_pts' (armKSGlobalPTs (ksArchState s)) s \<and> 1051 is_inv (armKSHWASIDTable (ksArchState s)) 1052 (option_map fst o armKSASIDMap (ksArchState s)) \<and> 1053 valid_asid_map' (armKSASIDMap (ksArchState s))" 1054 1055definition 1056 irq_issued' :: "irq \<Rightarrow> kernel_state \<Rightarrow> bool" 1057where 1058 "irq_issued' irq \<equiv> \<lambda>s. intStateIRQTable (ksInterruptState s) irq = IRQSignal" 1059 1060definition 1061 cteCaps_of :: "kernel_state \<Rightarrow> word32 \<Rightarrow> capability option" 1062where 1063 "cteCaps_of s \<equiv> option_map cteCap \<circ> ctes_of s" 1064 1065definition 1066 valid_irq_handlers' :: "kernel_state \<Rightarrow> bool" 1067where 1068 "valid_irq_handlers' \<equiv> \<lambda>s. \<forall>cap \<in> ran (cteCaps_of s). \<forall>irq. 1069 cap = IRQHandlerCap irq \<longrightarrow> irq_issued' irq s" 1070 1071definition 1072 "irqs_masked' \<equiv> \<lambda>s. \<forall>irq > maxIRQ. intStateIRQTable (ksInterruptState s) irq = IRQInactive" 1073 1074definition 1075 pd_asid_slot :: word32 1076where 1077 "pd_asid_slot \<equiv> 0xff0" 1078 1079 (* ideally, all mappings above kernel_base are global and kernel-only, and 1080 of them one particular mapping is clear. at the moment all we can easily say 1081 is that the mapping is clear. *) 1082definition 1083 valid_pde_mapping_offset' :: "word32 \<Rightarrow> bool" 1084where 1085 "valid_pde_mapping_offset' offset \<equiv> offset \<noteq> pd_asid_slot * 4" 1086 1087definition 1088 valid_pde_mapping' :: "word32 \<Rightarrow> pde \<Rightarrow> bool" 1089where 1090 "valid_pde_mapping' offset pde \<equiv> pde = InvalidPDE \<or> valid_pde_mapping_offset' offset" 1091 1092definition 1093 valid_pde_mappings' :: "kernel_state \<Rightarrow> bool" 1094where 1095 "valid_pde_mappings' \<equiv> \<lambda>s. 1096 \<forall>x pde. ko_at' pde x s 1097 \<longrightarrow> valid_pde_mapping' (x && mask pdBits) pde" 1098 1099definition 1100 "valid_irq_masks' table masked \<equiv> \<forall>irq. table irq = IRQInactive \<longrightarrow> masked irq" 1101 1102abbreviation 1103 "valid_irq_states' s \<equiv> 1104 valid_irq_masks' (intStateIRQTable (ksInterruptState s)) (irq_masks (ksMachineState s))" 1105 1106defs pointerInUserData_def: 1107 "pointerInUserData p \<equiv> \<lambda>s. (typ_at' UserDataT (p && ~~ mask pageBits) s)" 1108 1109(* pointerInDeviceData is not defined in spec but is necessary for valid_machine_state' *) 1110definition pointerInDeviceData :: "machine_word \<Rightarrow> kernel_state \<Rightarrow> bool" 1111where 1112 "pointerInDeviceData p \<equiv> \<lambda>s. (typ_at' UserDataDeviceT (p && ~~ mask pageBits) s)" 1113 1114definition 1115 "valid_machine_state' \<equiv> 1116 \<lambda>s. \<forall>p. pointerInUserData p s \<or> pointerInDeviceData p s \<or> underlying_memory (ksMachineState s) p = 0" 1117 1118definition 1119 "untyped_ranges_zero_inv cps urs \<equiv> 1120 urs = ran (untypedZeroRange \<circ>\<^sub>m cps)" 1121 1122abbreviation 1123 "untyped_ranges_zero' s \<equiv> untyped_ranges_zero_inv (cteCaps_of s) 1124 (gsUntypedZeroRanges s)" 1125 1126(* FIXME: this really should be a definition like the above. *) 1127(* The schedule is invariant. *) 1128abbreviation 1129 "valid_dom_schedule' \<equiv> 1130 \<lambda>s. ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) 1131 \<and> ksDomSchedule s = ksDomSchedule (newKernelState undefined) 1132 \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined))" 1133 1134definition 1135 valid_state' :: "kernel_state \<Rightarrow> bool" 1136where 1137 "valid_state' \<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s 1138 \<and> valid_queues s \<and> sym_refs (state_refs_of' s) 1139 \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s 1140 \<and> valid_idle' s 1141 \<and> valid_global_refs' s \<and> valid_arch_state' s 1142 \<and> valid_irq_node' (irq_node' s) s 1143 \<and> valid_irq_handlers' s 1144 \<and> valid_irq_states' s 1145 \<and> valid_machine_state' s 1146 \<and> irqs_masked' s 1147 \<and> valid_queues' s 1148 \<and> ct_not_inQ s 1149 \<and> ct_idle_or_in_cur_domain' s 1150 \<and> valid_pde_mappings' s 1151 \<and> pspace_domain_valid s 1152 \<and> ksCurDomain s \<le> maxDomain 1153 \<and> valid_dom_schedule' s 1154 \<and> untyped_ranges_zero' s" 1155 1156definition 1157 "cur_tcb' s \<equiv> tcb_at' (ksCurThread s) s" 1158 1159definition 1160 invs' :: "kernel_state \<Rightarrow> bool" where 1161 "invs' \<equiv> valid_state' and cur_tcb'" 1162 1163subsection "Derived concepts" 1164 1165abbreviation 1166 "awaiting_reply' ts \<equiv> ts = Structures_H.BlockedOnReply" 1167 1168 (* x-symbol doesn't have a reverse leadsto.. *) 1169definition 1170 mdb_prev :: "cte_heap \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> bool" ("_ \<turnstile> _ \<leftarrow> _" [60,0,60] 61) 1171where 1172 "m \<turnstile> c \<leftarrow> c' \<equiv> (\<exists>z. m c' = Some z \<and> c = mdbPrev (cteMDBNode z))" 1173 1174definition 1175 makeObjectT :: "kernel_object_type \<Rightarrow> kernel_object" 1176 where 1177 "makeObjectT tp \<equiv> case tp of 1178 EndpointT \<Rightarrow> injectKO (makeObject :: endpoint) 1179 | NotificationT \<Rightarrow> injectKO (makeObject :: Structures_H.notification) 1180 | CTET \<Rightarrow> injectKO (makeObject :: cte) 1181 | TCBT \<Rightarrow> injectKO (makeObject :: tcb) 1182 | UserDataT \<Rightarrow> injectKO (makeObject :: user_data) 1183 | UserDataDeviceT \<Rightarrow> injectKO (makeObject :: user_data_device) 1184 | KernelDataT \<Rightarrow> KOKernelData 1185 | ArchT atp \<Rightarrow> (case atp of 1186 PDET \<Rightarrow> injectKO (makeObject :: pde) 1187 | PTET \<Rightarrow> injectKO (makeObject :: pte) 1188 | ASIDPoolT \<Rightarrow> injectKO (makeObject :: asidpool))" 1189 1190definition 1191 objBitsT :: "kernel_object_type \<Rightarrow> nat" 1192 where 1193 "objBitsT tp \<equiv> objBitsKO (makeObjectT tp)" 1194 1195 1196abbreviation 1197 "active' st \<equiv> st = Structures_H.Running \<or> st = Structures_H.Restart" 1198 1199abbreviation 1200 "simple' st \<equiv> st = Structures_H.Inactive \<or> 1201 st = Structures_H.Running \<or> 1202 st = Structures_H.Restart \<or> 1203 idle' st \<or> awaiting_reply' st" 1204 1205abbreviation 1206 "ct_active' \<equiv> ct_in_state' active'" 1207 1208abbreviation 1209 "ct_running' \<equiv> ct_in_state' (\<lambda>st. st = Structures_H.Running)" 1210 1211abbreviation(input) 1212 "all_invs_but_sym_refs_ct_not_inQ' 1213 \<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s 1214 \<and> valid_queues s \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s 1215 \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s 1216 \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s 1217 \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s 1218 \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s 1219 \<and> pspace_domain_valid s 1220 \<and> ksCurDomain s \<le> maxDomain 1221 \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s" 1222 1223abbreviation(input) 1224 "all_invs_but_ct_not_inQ' 1225 \<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s 1226 \<and> valid_queues s \<and> sym_refs (state_refs_of' s) 1227 \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s 1228 \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s 1229 \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s 1230 \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s 1231 \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s 1232 \<and> pspace_domain_valid s 1233 \<and> ksCurDomain s \<le> maxDomain 1234 \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s" 1235 1236lemma all_invs_but_sym_refs_not_ct_inQ_check': 1237 "(all_invs_but_sym_refs_ct_not_inQ' and sym_refs \<circ> state_refs_of' and ct_not_inQ) = invs'" 1238 by (simp add: pred_conj_def conj_commute conj_left_commute invs'_def valid_state'_def) 1239 1240lemma all_invs_but_not_ct_inQ_check': 1241 "(all_invs_but_ct_not_inQ' and ct_not_inQ) = invs'" 1242 by (simp add: pred_conj_def conj_commute conj_left_commute invs'_def valid_state'_def) 1243 1244definition 1245 "all_invs_but_ct_idle_or_in_cur_domain' 1246 \<equiv> \<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s 1247 \<and> valid_queues s \<and> sym_refs (state_refs_of' s) 1248 \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s 1249 \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s 1250 \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s 1251 \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s 1252 \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_not_inQ s \<and> valid_pde_mappings' s 1253 \<and> pspace_domain_valid s 1254 \<and> ksCurDomain s \<le> maxDomain 1255 \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s" 1256 1257lemmas invs_no_cicd'_def = all_invs_but_ct_idle_or_in_cur_domain'_def 1258 1259lemma all_invs_but_ct_idle_or_in_cur_domain_check': 1260 "(all_invs_but_ct_idle_or_in_cur_domain' and ct_idle_or_in_cur_domain') = invs'" 1261 by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def pred_conj_def 1262 conj_left_commute conj_commute invs'_def valid_state'_def) 1263 1264abbreviation (input) 1265 "invs_no_cicd' \<equiv> all_invs_but_ct_idle_or_in_cur_domain'" 1266 1267lemma invs'_to_invs_no_cicd'_def: 1268 "invs' = (all_invs_but_ct_idle_or_in_cur_domain' and ct_idle_or_in_cur_domain')" 1269 by (fastforce simp: invs'_def all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def ) 1270end 1271 1272locale mdb_next = 1273 fixes m :: cte_heap 1274 1275 fixes greater_eq 1276 defines "greater_eq a b \<equiv> m \<turnstile> a \<leadsto>\<^sup>* b" 1277 1278 fixes greater 1279 defines "greater a b \<equiv> m \<turnstile> a \<leadsto>\<^sup>+ b" 1280 1281locale mdb_order = mdb_next + 1282 assumes no_0: "no_0 m" 1283 assumes chain: "mdb_chain_0 m" 1284 1285\<comment> \<open>---------------------------------------------------------------------------\<close> 1286section "Alternate split rules for preserving subgoal order" 1287context begin interpretation Arch . (*FIXME: arch_split*) 1288lemma capability_splits[split]: 1289 "P (case capability of capability.ThreadCap x \<Rightarrow> f1 x 1290 | capability.NullCap \<Rightarrow> f2 1291 | capability.NotificationCap x xa xb xc \<Rightarrow> f3 x xa xb xc 1292 | capability.IRQHandlerCap x \<Rightarrow> f4 x 1293 | capability.EndpointCap x xa xb xc xd \<Rightarrow> f5 x xa xb xc xd 1294 | capability.DomainCap \<Rightarrow> f6 1295 | capability.Zombie x xa xb \<Rightarrow> f7 x xa xb 1296 | capability.ArchObjectCap x \<Rightarrow> f8 x 1297 | capability.ReplyCap x xa \<Rightarrow> f9 x xa 1298 | capability.UntypedCap dev x xa xb \<Rightarrow> f10 dev x xa xb 1299 | capability.CNodeCap x xa xb xc \<Rightarrow> f11 x xa xb xc 1300 | capability.IRQControlCap \<Rightarrow> f12) = 1301 ((\<forall>x1. capability = capability.ThreadCap x1 \<longrightarrow> P (f1 x1)) \<and> 1302 (capability = capability.NullCap \<longrightarrow> P f2) \<and> 1303 (\<forall>x31 x32 x33 x34. 1304 capability = 1305 capability.NotificationCap x31 x32 x33 x34 \<longrightarrow> 1306 P (f3 x31 x32 x33 x34)) \<and> 1307 (\<forall>x4. capability = capability.IRQHandlerCap x4 \<longrightarrow> 1308 P (f4 x4)) \<and> 1309 (\<forall>x51 x52 x53 x54 x55. 1310 capability = 1311 capability.EndpointCap x51 x52 x53 x54 x55 \<longrightarrow> 1312 P (f5 x51 x52 x53 x54 x55)) \<and> 1313 (capability = capability.DomainCap \<longrightarrow> P f6) \<and> 1314 (\<forall>x71 x72 x73. 1315 capability = capability.Zombie x71 x72 x73 \<longrightarrow> 1316 P (f7 x71 x72 x73)) \<and> 1317 (\<forall>x8. capability = capability.ArchObjectCap x8 \<longrightarrow> 1318 P (f8 x8)) \<and> 1319 (\<forall>x91 x92. 1320 capability = capability.ReplyCap x91 x92 \<longrightarrow> 1321 P (f9 x91 x92)) \<and> 1322 (\<forall>dev x101 x102 x103. 1323 capability = capability.UntypedCap dev x101 x102 x103 \<longrightarrow> 1324 P (f10 dev x101 x102 x103)) \<and> 1325 (\<forall>x111 x112 x113 x114. 1326 capability = capability.CNodeCap x111 x112 x113 x114 \<longrightarrow> 1327 P (f11 x111 x112 x113 x114)) \<and> 1328 (capability = capability.IRQControlCap \<longrightarrow> P f12))" 1329 "P (case capability of capability.ThreadCap x \<Rightarrow> f1 x 1330 | capability.NullCap \<Rightarrow> f2 1331 | capability.NotificationCap x xa xb xc \<Rightarrow> f3 x xa xb xc 1332 | capability.IRQHandlerCap x \<Rightarrow> f4 x 1333 | capability.EndpointCap x xa xb xc xd \<Rightarrow> f5 x xa xb xc xd 1334 | capability.DomainCap \<Rightarrow> f6 1335 | capability.Zombie x xa xb \<Rightarrow> f7 x xa xb 1336 | capability.ArchObjectCap x \<Rightarrow> f8 x 1337 | capability.ReplyCap x xa \<Rightarrow> f9 x xa 1338 | capability.UntypedCap dev x xa xb \<Rightarrow> f10 dev x xa xb 1339 | capability.CNodeCap x xa xb xc \<Rightarrow> f11 x xa xb xc 1340 | capability.IRQControlCap \<Rightarrow> f12) = 1341 (\<not> ((\<exists>x1. capability = capability.ThreadCap x1 \<and> 1342 \<not> P (f1 x1)) \<or> 1343 capability = capability.NullCap \<and> \<not> P f2 \<or> 1344 (\<exists>x31 x32 x33 x34. 1345 capability = 1346 capability.NotificationCap x31 x32 x33 x34 \<and> 1347 \<not> P (f3 x31 x32 x33 x34)) \<or> 1348 (\<exists>x4. capability = capability.IRQHandlerCap x4 \<and> 1349 \<not> P (f4 x4)) \<or> 1350 (\<exists>x51 x52 x53 x54 x55. 1351 capability = 1352 capability.EndpointCap x51 x52 x53 x54 x55 \<and> 1353 \<not> P (f5 x51 x52 x53 x54 x55)) \<or> 1354 capability = capability.DomainCap \<and> \<not> P f6 \<or> 1355 (\<exists>x71 x72 x73. 1356 capability = capability.Zombie x71 x72 x73 \<and> 1357 \<not> P (f7 x71 x72 x73)) \<or> 1358 (\<exists>x8. capability = capability.ArchObjectCap x8 \<and> 1359 \<not> P (f8 x8)) \<or> 1360 (\<exists>x91 x92. 1361 capability = capability.ReplyCap x91 x92 \<and> 1362 \<not> P (f9 x91 x92)) \<or> 1363 (\<exists>x101 x102 x103 dev. 1364 capability = capability.UntypedCap dev x101 x102 x103 \<and> 1365 \<not> P (f10 dev x101 x102 x103)) \<or> 1366 (\<exists>x111 x112 x113 x114. 1367 capability = 1368 capability.CNodeCap x111 x112 x113 x114 \<and> 1369 \<not> P (f11 x111 x112 x113 x114)) \<or> 1370 capability = capability.IRQControlCap \<and> \<not> P f12))" 1371 by (case_tac capability; simp)+ 1372 1373lemma thread_state_splits[split]: 1374 " P (case thread_state of 1375 Structures_H.thread_state.BlockedOnReceive x \<Rightarrow> f1 x 1376 | Structures_H.thread_state.BlockedOnReply \<Rightarrow> f2 1377 | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> f3 x 1378 | Structures_H.thread_state.Running \<Rightarrow> f4 1379 | Structures_H.thread_state.Inactive \<Rightarrow> f5 1380 | Structures_H.thread_state.IdleThreadState \<Rightarrow> f6 1381 | Structures_H.thread_state.BlockedOnSend x xa xb xc \<Rightarrow> 1382 f7 x xa xb xc 1383 | Structures_H.thread_state.Restart \<Rightarrow> f8) = 1384 ((\<forall>x11. 1385 thread_state = 1386 Structures_H.thread_state.BlockedOnReceive x11 \<longrightarrow> 1387 P (f1 x11)) \<and> 1388 (awaiting_reply' thread_state \<longrightarrow> P f2) \<and> 1389 (\<forall>x3. thread_state = 1390 Structures_H.thread_state.BlockedOnNotification x3 \<longrightarrow> 1391 P (f3 x3)) \<and> 1392 (thread_state = Structures_H.thread_state.Running \<longrightarrow> 1393 P f4) \<and> 1394 (thread_state = Structures_H.thread_state.Inactive \<longrightarrow> 1395 P f5) \<and> 1396 (idle' thread_state \<longrightarrow> P f6) \<and> 1397 (\<forall>x71 x72 x73 x74. 1398 thread_state = 1399 Structures_H.thread_state.BlockedOnSend x71 x72 x73 1400 x74 \<longrightarrow> 1401 P (f7 x71 x72 x73 x74)) \<and> 1402 (thread_state = Structures_H.thread_state.Restart \<longrightarrow> P f8))" 1403 "P (case thread_state of 1404 Structures_H.thread_state.BlockedOnReceive x \<Rightarrow> f1 x 1405 | Structures_H.thread_state.BlockedOnReply \<Rightarrow> f2 1406 | Structures_H.thread_state.BlockedOnNotification x \<Rightarrow> f3 x 1407 | Structures_H.thread_state.Running \<Rightarrow> f4 1408 | Structures_H.thread_state.Inactive \<Rightarrow> f5 1409 | Structures_H.thread_state.IdleThreadState \<Rightarrow> f6 1410 | Structures_H.thread_state.BlockedOnSend x xa xb xc \<Rightarrow> 1411 f7 x xa xb xc 1412 | Structures_H.thread_state.Restart \<Rightarrow> f8) = 1413 (\<not> ((\<exists>x11. 1414 thread_state = 1415 Structures_H.thread_state.BlockedOnReceive x11 \<and> 1416 \<not> P (f1 x11)) \<or> 1417 awaiting_reply' thread_state \<and> \<not> P f2 \<or> 1418 (\<exists>x3. thread_state = 1419 Structures_H.thread_state.BlockedOnNotification 1420 x3 \<and> 1421 \<not> P (f3 x3)) \<or> 1422 thread_state = Structures_H.thread_state.Running \<and> 1423 \<not> P f4 \<or> 1424 thread_state = Structures_H.thread_state.Inactive \<and> 1425 \<not> P f5 \<or> 1426 idle' thread_state \<and> \<not> P f6 \<or> 1427 (\<exists>x71 x72 x73 x74. 1428 thread_state = 1429 Structures_H.thread_state.BlockedOnSend x71 x72 x73 1430 x74 \<and> 1431 \<not> P (f7 x71 x72 x73 x74)) \<or> 1432 thread_state = Structures_H.thread_state.Restart \<and> 1433 \<not> P f8))" 1434 by (case_tac thread_state; simp)+ 1435 1436lemma ntfn_splits[split]: 1437 " P (case ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> f1 1438 | Structures_H.ntfn.ActiveNtfn x \<Rightarrow> f2 x 1439 | Structures_H.ntfn.WaitingNtfn x \<Rightarrow> f3 x) = 1440 ((ntfn = Structures_H.ntfn.IdleNtfn \<longrightarrow> P f1) \<and> 1441 (\<forall>x2. ntfn = Structures_H.ntfn.ActiveNtfn x2 \<longrightarrow> 1442 P (f2 x2)) \<and> 1443 (\<forall>x3. ntfn = Structures_H.ntfn.WaitingNtfn x3 \<longrightarrow> 1444 P (f3 x3)))" 1445 "P (case ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> f1 1446 | Structures_H.ntfn.ActiveNtfn x \<Rightarrow> f2 x 1447 | Structures_H.ntfn.WaitingNtfn x \<Rightarrow> f3 x) = 1448 (\<not> (ntfn = Structures_H.ntfn.IdleNtfn \<and> \<not> P f1 \<or> 1449 (\<exists>x2. ntfn = Structures_H.ntfn.ActiveNtfn x2 \<and> 1450 \<not> P (f2 x2)) \<or> 1451 (\<exists>x3. ntfn = Structures_H.ntfn.WaitingNtfn x3 \<and> 1452 \<not> P (f3 x3))))" 1453 by (case_tac ntfn; simp)+ 1454\<comment> \<open>---------------------------------------------------------------------------\<close> 1455 1456section "Lemmas" 1457 1458schematic_goal wordBits_def': "wordBits = numeral ?n" (* arch-specific consequence *) 1459 by (simp add: wordBits_def word_size) 1460 1461lemma valid_bound_ntfn'_None[simp]: 1462 "valid_bound_ntfn' None = \<top>" 1463 by (auto simp: valid_bound_ntfn'_def) 1464 1465lemma valid_bound_ntfn'_Some[simp]: 1466 "valid_bound_ntfn' (Some x) = ntfn_at' x" 1467 by (auto simp: valid_bound_ntfn'_def) 1468 1469lemma valid_bound_tcb'_None[simp]: 1470 "valid_bound_tcb' None = \<top>" 1471 by (auto simp: valid_bound_tcb'_def) 1472 1473lemma valid_bound_tcb'_Some[simp]: 1474 "valid_bound_tcb' (Some x) = tcb_at' x" 1475 by (auto simp: valid_bound_tcb'_def) 1476 1477lemmas untypedBits_defs = minUntypedSizeBits_def maxUntypedSizeBits_def 1478lemmas objBits_simps = objBits_def objBitsKO_def word_size_def 1479lemmas objBits_simps' = objBits_simps objBits_defs 1480lemmas wordRadix_def' = wordRadix_def[simplified] 1481 1482lemma valid_duplicates'_D: 1483 "\<lbrakk>vs_valid_duplicates' m; m (p::word32) = Some ko;is_aligned p' 2; 1484 p && ~~ mask (vs_ptr_align ko) = p' && ~~ mask (vs_ptr_align ko)\<rbrakk> 1485 \<Longrightarrow> m p' = Some ko " 1486 apply (clarsimp simp:vs_valid_duplicates'_def) 1487 apply (drule_tac x = p in spec) 1488 apply auto 1489 done 1490 1491lemma ps_clear_def2: 1492 "p \<le> p + 1 \<Longrightarrow> ps_clear p n s = ({p + 1 .. p + (1 << n) - 1} \<inter> dom (ksPSpace s) = {})" 1493 apply (simp add: ps_clear_def) 1494 apply safe 1495 apply (drule_tac a=x in equals0D) 1496 apply clarsimp 1497 apply (drule mp, simp) 1498 apply (erule disjE) 1499 apply simp 1500 apply clarsimp 1501 apply (drule_tac a=x in equals0D) 1502 apply clarsimp 1503 apply (case_tac "p + 1 \<le> x") 1504 apply clarsimp 1505 apply (simp add: linorder_not_le) 1506 apply (drule plus_one_helper, simp) 1507 done 1508 1509lemma projectKO_stateI: 1510 "fst (projectKO e s) = {(obj, s)} \<Longrightarrow> fst (projectKO e s') = {(obj, s')}" 1511 unfolding projectKO_def 1512 by (auto simp: fail_def return_def valid_def split: option.splits) 1513 1514lemma singleton_in_magnitude_check: 1515 "(x, s) \<in> fst (magnitudeCheck a b c s') \<Longrightarrow> \<forall>s'. fst (magnitudeCheck a b c s') = {(x, s')}" 1516 by (simp add: magnitudeCheck_def when_def in_monad return_def 1517 split: if_split_asm option.split_asm) 1518 1519lemma wordSizeCase_simp [simp]: "wordSizeCase a b = a" 1520 by (simp add: wordSizeCase_def wordBits_def word_size) 1521 1522lemma projectKO_eq: 1523 "(fst (projectKO ko c) = {(obj, c)}) = (projectKO_opt ko = Some obj)" 1524 by (simp add: projectKO_def fail_def return_def split: option.splits) 1525 1526lemma lookupBefore_None: 1527 "(lookupBefore x m = None) = (\<forall>y \<le> x. m y = None)" 1528 by (simp add: lookupBefore_def Let_def dom_def, fastforce) 1529 1530lemma lookupBefore_exact: 1531 "m x = Some y \<Longrightarrow> lookupBefore x m = Some (x, y)" 1532 apply (simp add: lookupBefore_def Let_def cong: conj_cong) 1533 apply (rule context_conjI) 1534 apply (rule exI[where x=x]) 1535 apply (simp add: domI) 1536 apply (rule order_antisym) 1537 apply simp 1538 apply (rule Max_ge) 1539 apply simp 1540 apply simp 1541 apply (simp add: domI) 1542 done 1543 1544lemma obj_at'_def': 1545 "obj_at' P p s = (\<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) 1546 \<and> fst (projectKO ko s) = {(obj,s)} \<and> P obj 1547 \<and> ps_clear p (objBitsKO ko) s)" 1548 apply (simp add: obj_at'_real_def ko_wp_at'_def projectKO_eq 1549 True_notin_set_replicate_conv objBits_def) 1550 apply fastforce 1551 done 1552 1553lemma obj_at'_def: 1554 "obj_at' P p s \<equiv> \<exists>ko obj. ksPSpace s p = Some ko \<and> is_aligned p (objBitsKO ko) 1555 \<and> fst (projectKO ko s) = {(obj,s)} \<and> P obj 1556 \<and> ps_clear p (objBitsKO ko) s" 1557 by (simp add: obj_at'_def') 1558 1559lemma obj_atE' [elim?]: 1560 assumes objat: "obj_at' P ptr s" 1561 and rl: "\<And>ko obj. 1562 \<lbrakk> ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); 1563 fst (projectKO ko s) = {(obj,s)}; P obj; 1564 ps_clear ptr (objBitsKO ko) s \<rbrakk> \<Longrightarrow> R" 1565 shows "R" 1566 using objat unfolding obj_at'_def by (auto intro!: rl) 1567 1568lemma obj_atI' [intro?]: 1569 "\<lbrakk> ksPSpace s ptr = Some ko; is_aligned ptr (objBitsKO ko); 1570 fst (projectKO ko s) = {(obj, s)}; P obj; 1571 ps_clear ptr (objBitsKO ko) s \<rbrakk> 1572 \<Longrightarrow> obj_at' P ptr s" 1573 unfolding obj_at'_def by (auto) 1574 1575 1576lemma cte_at'_def: 1577 "cte_at' p s \<equiv> \<exists>cte::cte. fst (getObject p s) = {(cte,s)}" 1578 by (simp add: cte_wp_at'_def) 1579 1580 1581lemma tcb_cte_cases_simps[simp]: 1582 "tcb_cte_cases 0 = Some (tcbCTable, tcbCTable_update)" 1583 "tcb_cte_cases 16 = Some (tcbVTable, tcbVTable_update)" 1584 "tcb_cte_cases 32 = Some (tcbReply, tcbReply_update)" 1585 "tcb_cte_cases 48 = Some (tcbCaller, tcbCaller_update)" 1586 "tcb_cte_cases 64 = Some (tcbIPCBufferFrame, tcbIPCBufferFrame_update)" 1587 by (simp add: tcb_cte_cases_def)+ 1588 1589lemma refs_of'_simps[simp]: 1590 "refs_of' (KOTCB tcb) = tcb_st_refs_of' (tcbState tcb) \<union> tcb_bound_refs' (tcbBoundNotification tcb)" 1591 "refs_of' (KOCTE cte) = {}" 1592 "refs_of' (KOEndpoint ep) = ep_q_refs_of' ep" 1593 "refs_of' (KONotification ntfn) = ntfn_q_refs_of' (ntfnObj ntfn) \<union> ntfn_bound_refs' (ntfnBoundTCB ntfn)" 1594 "refs_of' (KOUserData) = {}" 1595 "refs_of' (KOUserDataDevice) = {}" 1596 "refs_of' (KOKernelData) = {}" 1597 "refs_of' (KOArch ako) = {}" 1598 by (auto simp: refs_of'_def) 1599 1600lemma tcb_st_refs_of'_simps[simp]: 1601 "tcb_st_refs_of' (Running) = {}" 1602 "tcb_st_refs_of' (Inactive) = {}" 1603 "tcb_st_refs_of' (Restart) = {}" 1604 "\<And>x. tcb_st_refs_of' (BlockedOnReceive x) = {(x, TCBBlockedRecv)}" 1605 "\<And>x c. tcb_st_refs_of' (BlockedOnSend x a b c) = {(x, TCBBlockedSend)}" 1606 "\<And>x. tcb_st_refs_of' (BlockedOnNotification x) = {(x, TCBSignal)}" 1607 "tcb_st_refs_of' (BlockedOnReply) = {}" 1608 "tcb_st_refs_of' (IdleThreadState) = {}" 1609 by (auto simp: tcb_st_refs_of'_def) 1610 1611lemma ep_q_refs_of'_simps[simp]: 1612 "ep_q_refs_of' IdleEP = {}" 1613 "ep_q_refs_of' (RecvEP q) = set q \<times> {EPRecv}" 1614 "ep_q_refs_of' (SendEP q) = set q \<times> {EPSend}" 1615 by (auto simp: ep_q_refs_of'_def) 1616 1617lemma ntfn_q_refs_of'_simps[simp]: 1618 "ntfn_q_refs_of' IdleNtfn = {}" 1619 "ntfn_q_refs_of' (WaitingNtfn q) = set q \<times> {NTFNSignal}" 1620 "ntfn_q_refs_of' (ActiveNtfn b) = {}" 1621 by (auto simp: ntfn_q_refs_of'_def) 1622 1623lemma ntfn_bound_refs'_simps[simp]: 1624 "ntfn_bound_refs' (Some t) = {(t, NTFNBound)}" 1625 "ntfn_bound_refs' None = {}" 1626 by (auto simp: ntfn_bound_refs'_def) 1627 1628lemma tcb_bound_refs'_simps[simp]: 1629 "tcb_bound_refs' (Some a) = {(a, TCBBound)}" 1630 "tcb_bound_refs' None = {}" 1631 by (auto simp: tcb_bound_refs'_def) 1632 1633lemma refs_of_rev': 1634 "(x, TCBBlockedRecv) \<in> refs_of' ko = 1635 (\<exists>tcb. ko = KOTCB tcb \<and> tcbState tcb = BlockedOnReceive x)" 1636 "(x, TCBBlockedSend) \<in> refs_of' ko = 1637 (\<exists>tcb. ko = KOTCB tcb \<and> (\<exists>a b c. tcbState tcb = BlockedOnSend x a b c))" 1638 "(x, TCBSignal) \<in> refs_of' ko = 1639 (\<exists>tcb. ko = KOTCB tcb \<and> tcbState tcb = BlockedOnNotification x)" 1640 "(x, EPRecv) \<in> refs_of' ko = 1641 (\<exists>ep. ko = KOEndpoint ep \<and> (\<exists>q. ep = RecvEP q \<and> x \<in> set q))" 1642 "(x, EPSend) \<in> refs_of' ko = 1643 (\<exists>ep. ko = KOEndpoint ep \<and> (\<exists>q. ep = SendEP q \<and> x \<in> set q))" 1644 "(x, NTFNSignal) \<in> refs_of' ko = 1645 (\<exists>ntfn. ko = KONotification ntfn \<and> (\<exists>q. ntfnObj ntfn = WaitingNtfn q \<and> x \<in> set q))" 1646 "(x, TCBBound) \<in> refs_of' ko = 1647 (\<exists>tcb. ko = KOTCB tcb \<and> (tcbBoundNotification tcb = Some x))" 1648 "(x, NTFNBound) \<in> refs_of' ko = 1649 (\<exists>ntfn. ko = KONotification ntfn \<and> (ntfnBoundTCB ntfn = Some x))" 1650 by (auto simp: refs_of'_def 1651 tcb_st_refs_of'_def 1652 ep_q_refs_of'_def 1653 ntfn_q_refs_of'_def 1654 ntfn_bound_refs'_def 1655 tcb_bound_refs'_def 1656 split: Structures_H.kernel_object.splits 1657 Structures_H.thread_state.splits 1658 Structures_H.endpoint.splits 1659 Structures_H.notification.splits 1660 Structures_H.ntfn.splits)+ 1661 1662lemma ko_wp_at'_weakenE: 1663 "\<lbrakk> ko_wp_at' P p s; \<And>ko. P ko \<Longrightarrow> Q ko \<rbrakk> \<Longrightarrow> ko_wp_at' Q p s" 1664 by (clarsimp simp: ko_wp_at'_def) 1665 1666lemma projectKO_opt_tcbD: 1667 "projectKO_opt ko = Some (tcb :: tcb) \<Longrightarrow> ko = KOTCB tcb" 1668 by (cases ko, simp_all add: projectKO_opt_tcb) 1669 1670lemma st_tcb_at_refs_of_rev': 1671 "ko_wp_at' (\<lambda>ko. (x, TCBBlockedRecv) \<in> refs_of' ko) t s 1672 = st_tcb_at' (\<lambda>ts. ts = BlockedOnReceive x ) t s" 1673 "ko_wp_at' (\<lambda>ko. (x, TCBBlockedSend) \<in> refs_of' ko) t s 1674 = st_tcb_at' (\<lambda>ts. \<exists>a b c. ts = BlockedOnSend x a b c) t s" 1675 "ko_wp_at' (\<lambda>ko. (x, TCBSignal) \<in> refs_of' ko) t s 1676 = st_tcb_at' (\<lambda>ts. ts = BlockedOnNotification x) t s" 1677 by (fastforce simp: refs_of_rev' pred_tcb_at'_def obj_at'_real_def 1678 projectKO_opt_tcb[where e="KOTCB y" for y] 1679 elim!: ko_wp_at'_weakenE 1680 dest!: projectKO_opt_tcbD)+ 1681 1682lemma state_refs_of'_elemD: 1683 "\<lbrakk> ref \<in> state_refs_of' s x \<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>obj. ref \<in> refs_of' obj) x s" 1684 by (clarsimp simp add: state_refs_of'_def ko_wp_at'_def 1685 split: option.splits if_split_asm) 1686 1687lemma state_refs_of'_eqD: 1688 "\<lbrakk> state_refs_of' s x = S; S \<noteq> {} \<rbrakk> \<Longrightarrow> ko_wp_at' (\<lambda>obj. refs_of' obj = S) x s" 1689 by (clarsimp simp add: state_refs_of'_def ko_wp_at'_def 1690 split: option.splits if_split_asm) 1691 1692lemma obj_at_state_refs_ofD': 1693 "obj_at' P p s \<Longrightarrow> \<exists>obj. P obj \<and> state_refs_of' s p = refs_of' (injectKO obj)" 1694 apply (clarsimp simp: obj_at'_real_def project_inject ko_wp_at'_def conj_commute) 1695 apply (rule exI, erule conjI) 1696 apply (clarsimp simp: state_refs_of'_def) 1697 done 1698 1699lemma ko_at_state_refs_ofD': 1700 "ko_at' ko p s \<Longrightarrow> state_refs_of' s p = refs_of' (injectKO ko)" 1701 by (clarsimp dest!: obj_at_state_refs_ofD') 1702 1703definition 1704 tcb_ntfn_is_bound' :: "word32 option \<Rightarrow> tcb \<Rightarrow> bool" 1705where 1706 "tcb_ntfn_is_bound' ntfn tcb \<equiv> tcbBoundNotification tcb = ntfn" 1707 1708lemma st_tcb_at_state_refs_ofD': 1709 "st_tcb_at' P t s \<Longrightarrow> \<exists>ts ntfnptr. P ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s 1710 \<and> state_refs_of' s t = (tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr)" 1711 by (auto simp: pred_tcb_at'_def tcb_ntfn_is_bound'_def obj_at'_def projectKO_eq 1712 project_inject state_refs_of'_def) 1713 1714lemma bound_tcb_at_state_refs_ofD': 1715 "bound_tcb_at' P t s \<Longrightarrow> \<exists>ts ntfnptr. P ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s 1716 \<and> state_refs_of' s t = (tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr)" 1717 by (auto simp: pred_tcb_at'_def obj_at'_def tcb_ntfn_is_bound'_def projectKO_eq 1718 project_inject state_refs_of'_def) 1719 1720lemma sym_refs_obj_atD': 1721 "\<lbrakk> obj_at' P p s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow> 1722 \<exists>obj. P obj \<and> state_refs_of' s p = refs_of' (injectKO obj) 1723 \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO obj). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)" 1724 apply (drule obj_at_state_refs_ofD') 1725 apply (erule exEI, clarsimp) 1726 apply (drule sym, simp) 1727 apply (drule(1) sym_refsD) 1728 apply (erule state_refs_of'_elemD) 1729 done 1730 1731lemma sym_refs_ko_atD': 1732 "\<lbrakk> ko_at' ko p s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow> 1733 state_refs_of' s p = refs_of' (injectKO ko) \<and> 1734 (\<forall>(x, tp)\<in>refs_of' (injectKO ko). ko_wp_at' (\<lambda>ko. (p, symreftype tp) \<in> refs_of' ko) x s)" 1735 by (drule(1) sym_refs_obj_atD', simp) 1736 1737lemma sym_refs_st_tcb_atD': 1738 "\<lbrakk> st_tcb_at' P t s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow> 1739 \<exists>ts ntfnptr. P ts \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s 1740 \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr 1741 \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (t, symreftype tp) \<in> refs_of' ko) x s)" 1742 apply (drule st_tcb_at_state_refs_ofD') 1743 apply (erule exE)+ 1744 apply (rule_tac x=ts in exI) 1745 apply (rule_tac x=ntfnptr in exI) 1746 apply clarsimp 1747 apply (frule obj_at_state_refs_ofD') 1748 apply (drule (1)sym_refs_obj_atD') 1749 apply auto 1750 done 1751 1752lemma sym_refs_bound_tcb_atD': 1753 "\<lbrakk> bound_tcb_at' P t s; sym_refs (state_refs_of' s) \<rbrakk> \<Longrightarrow> 1754 \<exists>ts ntfnptr. P ntfnptr \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s 1755 \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr 1756 \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (t, symreftype tp) \<in> refs_of' ko) x s)" 1757 apply (drule bound_tcb_at_state_refs_ofD') 1758 apply (erule exE)+ 1759 apply (rule_tac x=ts in exI) 1760 apply (rule_tac x=ntfnptr in exI) 1761 apply clarsimp 1762 apply (frule obj_at_state_refs_ofD') 1763 apply (drule (1)sym_refs_obj_atD') 1764 apply auto 1765 done 1766 1767lemma ex_nonz_cap_toE': 1768 "\<lbrakk> ex_nonz_cap_to' p s; \<And>cref. cte_wp_at' (\<lambda>c. p \<in> zobj_refs' (cteCap c)) cref s \<Longrightarrow> Q \<rbrakk> 1769 \<Longrightarrow> Q" 1770 by (fastforce simp: ex_nonz_cap_to'_def) 1771 1772lemma refs_of_live': 1773 "refs_of' ko \<noteq> {} \<Longrightarrow> live' ko" 1774 apply (cases ko, simp_all) 1775 apply clarsimp 1776 apply (rename_tac notification) 1777 apply (case_tac "ntfnObj notification"; simp) 1778 apply fastforce+ 1779 done 1780 1781lemma if_live_then_nonz_capE': 1782 "\<lbrakk> if_live_then_nonz_cap' s; ko_wp_at' live' p s \<rbrakk> 1783 \<Longrightarrow> ex_nonz_cap_to' p s" 1784 by (fastforce simp: if_live_then_nonz_cap'_def) 1785 1786lemma if_live_then_nonz_capD': 1787 assumes x: "if_live_then_nonz_cap' s" "ko_wp_at' P p s" 1788 assumes y: "\<And>obj. \<lbrakk> P obj; ksPSpace s p = Some obj; is_aligned p (objBitsKO obj) \<rbrakk> \<Longrightarrow> live' obj" 1789 shows "ex_nonz_cap_to' p s" using x 1790 by (clarsimp elim!: if_live_then_nonz_capE' y 1791 simp: ko_wp_at'_def) 1792 1793lemma if_live_state_refsE: 1794 "\<lbrakk> if_live_then_nonz_cap' s; 1795 state_refs_of' s p \<noteq> {} \<rbrakk> \<Longrightarrow> ex_nonz_cap_to' p s" 1796 by (clarsimp simp: state_refs_of'_def ko_wp_at'_def 1797 split: option.splits if_split_asm 1798 elim!: refs_of_live' if_live_then_nonz_capE') 1799 1800lemmas ex_cte_cap_to'_def = ex_cte_cap_wp_to'_def 1801 1802lemma if_unsafe_then_capD': 1803 "\<lbrakk> cte_wp_at' P p s; if_unsafe_then_cap' s; \<And>cte. P cte \<Longrightarrow> cteCap cte \<noteq> NullCap \<rbrakk> 1804 \<Longrightarrow> ex_cte_cap_to' p s" 1805 unfolding if_unsafe_then_cap'_def 1806 apply (erule allE, erule mp) 1807 apply (clarsimp simp: cte_wp_at'_def) 1808 done 1809 1810lemmas valid_cap_simps' = 1811 valid_cap'_def[split_simps capability.split arch_capability.split] 1812 1813lemma max_ipc_words: 1814 "max_ipc_words = 0x80" 1815 unfolding max_ipc_words_def 1816 by (simp add: msgMaxLength_def msgLengthBits_def msgMaxExtraCaps_def msgExtraCapBits_def capTransferDataSize_def) 1817 1818lemma valid_objsI' [intro]: 1819 "(\<And>obj x. ksPSpace s x = Some obj \<Longrightarrow> valid_obj' obj s) \<Longrightarrow> valid_objs' s" 1820 unfolding valid_objs'_def by (auto elim: ranE) 1821 1822lemma valid_objsE' [elim]: 1823 "\<lbrakk> valid_objs' s; ksPSpace s x = Some obj; valid_obj' obj s \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 1824 unfolding valid_objs'_def by auto 1825 1826lemma pspace_distinctD': 1827 "\<lbrakk> ksPSpace s x = Some v; pspace_distinct' s \<rbrakk> \<Longrightarrow> ps_clear x (objBitsKO v) s" 1828 apply (simp add: pspace_distinct'_def) 1829 apply (drule bspec, erule domI) 1830 apply simp 1831 done 1832 1833lemma pspace_alignedD': 1834 "\<lbrakk> ksPSpace s x = Some v; pspace_aligned' s \<rbrakk> \<Longrightarrow> is_aligned x (objBitsKO v)" 1835 apply (simp add: pspace_aligned'_def) 1836 apply (drule bspec, erule domI) 1837 apply simp 1838 done 1839 1840lemma next_unfold: 1841 "mdb_next s c = 1842 (case s c of Some cte \<Rightarrow> Some (mdbNext (cteMDBNode cte)) | None \<Rightarrow> None)" 1843 by (simp add: mdb_next_def split: option.split) 1844 1845lemma 1846 is_physical_cases: 1847 "(capClass cap = PhysicalClass) = 1848 (case cap of NullCap \<Rightarrow> False 1849 | DomainCap \<Rightarrow> False 1850 | IRQControlCap \<Rightarrow> False 1851 | IRQHandlerCap irq \<Rightarrow> False 1852 | ReplyCap r m \<Rightarrow> False 1853 | ArchObjectCap ASIDControlCap \<Rightarrow> False 1854 | _ \<Rightarrow> True)" 1855 by (simp split: capability.splits arch_capability.splits zombie_type.splits) 1856 1857lemma sch_act_sane_not: 1858 "sch_act_sane s = sch_act_not (ksCurThread s) s" 1859 by (auto simp: sch_act_sane_def) 1860 1861lemma objBits_cte_conv: 1862 "objBits (cte :: cte) = cteSizeBits" 1863 by (simp add: objBits_def objBitsKO_def wordSizeCase_def word_size) 1864 1865lemma valid_pde_mapping'_simps[simp]: 1866 "valid_pde_mapping' offset (InvalidPDE) = True" 1867 "valid_pde_mapping' offset (SectionPDE ptr a b c d e w) 1868 = valid_pde_mapping_offset' offset" 1869 "valid_pde_mapping' offset (SuperSectionPDE ptr a' b' c' d' w) 1870 = valid_pde_mapping_offset' offset" 1871 "valid_pde_mapping' offset (PageTablePDE ptr x z'') 1872 = valid_pde_mapping_offset' offset" 1873 by (clarsimp simp: valid_pde_mapping'_def)+ 1874 1875lemmas valid_irq_states'_def = valid_irq_masks'_def 1876 1877lemma valid_pspaceI' [intro]: 1878 "\<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; valid_mdb' s; no_0_obj' s\<rbrakk> 1879 \<Longrightarrow> valid_pspace' s" unfolding valid_pspace'_def by simp 1880 1881lemma valid_pspaceE' [elim]: 1882 "\<lbrakk>valid_pspace' s; 1883 \<lbrakk> valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; 1884 valid_mdb' s\<rbrakk> \<Longrightarrow> R \<rbrakk> \<Longrightarrow> R" 1885 unfolding valid_pspace'_def by simp 1886 1887lemma idle'_no_refs: 1888 "valid_idle' s \<Longrightarrow> state_refs_of' s (ksIdleThread s) = {}" 1889 by (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def tcb_ntfn_is_bound'_def 1890 projectKO_eq project_inject state_refs_of'_def) 1891 1892lemma idle'_not_queued': 1893 "\<lbrakk>valid_idle' s; sym_refs (state_refs_of' s); 1894 state_refs_of' s ptr = insert t queue \<times> {rt}\<rbrakk>\<Longrightarrow> 1895 ksIdleThread s \<notin> queue" 1896 by (frule idle'_no_refs, fastforce simp: valid_idle'_def sym_refs_def) 1897 1898lemma idle'_not_queued: 1899 "\<lbrakk>valid_idle' s; sym_refs (state_refs_of' s); 1900 state_refs_of' s ptr = queue \<times> {rt}\<rbrakk> \<Longrightarrow> 1901 ksIdleThread s \<notin> queue" 1902 by (frule idle'_no_refs, fastforce simp: valid_idle'_def sym_refs_def) 1903 1904 1905lemma obj_at_conj': 1906 "\<lbrakk> obj_at' P p s; obj_at' Q p s \<rbrakk> \<Longrightarrow> obj_at' (\<lambda>k. P k \<and> Q k) p s" 1907 by (auto simp: obj_at'_def) 1908 1909lemma pred_tcb_at_conj': 1910 "\<lbrakk> pred_tcb_at' proj P t s; pred_tcb_at' proj Q t s \<rbrakk> \<Longrightarrow> pred_tcb_at' proj (\<lambda>a. P a \<and> Q a) t s" 1911 apply (simp add: pred_tcb_at'_def) 1912 apply (erule (1) obj_at_conj') 1913 done 1914 1915lemma obj_at_False' [simp]: 1916 "obj_at' (\<lambda>k. False) t s = False" 1917 by (simp add: obj_at'_def) 1918 1919lemma pred_tcb_at_False' [simp]: 1920 "pred_tcb_at' proj (\<lambda>st. False) t s = False" 1921 by (simp add: pred_tcb_at'_def obj_at'_def) 1922 1923lemma obj_at'_pspaceI: 1924 "obj_at' t ref s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> obj_at' t ref s'" 1925 by (auto intro!: projectKO_stateI simp: obj_at'_def ps_clear_def) 1926 1927lemma cte_wp_at'_pspaceI: 1928 "\<lbrakk>cte_wp_at' P p s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> cte_wp_at' P p s'" 1929 apply (clarsimp simp add: cte_wp_at'_def getObject_def) 1930 apply (drule equalityD2) 1931 apply (clarsimp simp: in_monad loadObject_cte gets_def 1932 get_def bind_def return_def split_def) 1933 apply (case_tac b) 1934 apply (simp_all add: in_monad typeError_def) 1935 prefer 2 1936 apply (simp add: in_monad return_def alignError_def assert_opt_def 1937 alignCheck_def magnitudeCheck_def when_def bind_def 1938 split: if_split_asm option.splits) 1939 apply (clarsimp simp: in_monad return_def alignError_def fail_def assert_opt_def 1940 alignCheck_def bind_def when_def 1941 objBits_cte_conv tcbCTableSlot_def tcbVTableSlot_def 1942 tcbReplySlot_def cteSizeBits_def 1943 split: if_split_asm 1944 dest!: singleton_in_magnitude_check) 1945 done 1946 1947lemma valid_untyped'_pspaceI: 1948 "\<lbrakk>ksPSpace s = ksPSpace s'; valid_untyped' d p n idx s\<rbrakk> 1949 \<Longrightarrow> valid_untyped' d p n idx s'" 1950 by (simp add: valid_untyped'_def ko_wp_at'_def ps_clear_def) 1951 1952lemma typ_at'_pspaceI: 1953 "typ_at' T p s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> typ_at' T p s'" 1954 by (simp add: typ_at'_def ko_wp_at'_def ps_clear_def) 1955 1956lemma valid_cap'_pspaceI: 1957 "s \<turnstile>' cap \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> s' \<turnstile>' cap" 1958 unfolding valid_cap'_def 1959 by (cases cap) 1960 (force intro: obj_at'_pspaceI[rotated] 1961 cte_wp_at'_pspaceI valid_untyped'_pspaceI 1962 typ_at'_pspaceI[rotated] 1963 simp: page_table_at'_def page_directory_at'_def 1964 split: arch_capability.split zombie_type.split option.splits)+ 1965 1966lemma valid_arch_obj'_pspaceI: 1967 "valid_arch_obj' obj s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_arch_obj' obj s'" 1968 apply (cases obj; simp) 1969 apply (rename_tac asidpool) 1970 apply (case_tac asidpool, 1971 auto simp: page_directory_at'_def intro: typ_at'_pspaceI[rotated])[1] 1972 apply (rename_tac pte) 1973 apply (case_tac pte; simp add: valid_mapping'_def) 1974 apply (rename_tac pde) 1975 apply (case_tac pde; 1976 auto simp: page_table_at'_def valid_mapping'_def 1977 intro: typ_at'_pspaceI[rotated]) 1978 done 1979 1980lemma valid_obj'_pspaceI: 1981 "valid_obj' obj s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_obj' obj s'" 1982 unfolding valid_obj'_def 1983 by (cases obj) 1984 (auto simp: valid_ep'_def valid_ntfn'_def valid_tcb'_def valid_cte'_def 1985 valid_tcb_state'_def valid_arch_obj'_pspaceI valid_bound_tcb'_def 1986 valid_bound_ntfn'_def 1987 split: Structures_H.endpoint.splits Structures_H.notification.splits 1988 Structures_H.thread_state.splits ntfn.splits option.splits 1989 intro: obj_at'_pspaceI valid_cap'_pspaceI) 1990 1991lemma valid_objs'_pspaceI: 1992 "\<lbrakk>valid_objs' s; ksPSpace s = ksPSpace s'\<rbrakk> \<Longrightarrow> valid_objs' s'" 1993 by (auto simp: valid_objs'_def intro: valid_obj'_pspaceI) 1994 1995lemma pred_tcb_at'_pspaceI: 1996 "pred_tcb_at' proj P t s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> pred_tcb_at' proj P t s'" 1997 unfolding pred_tcb_at'_def by (fast intro: obj_at'_pspaceI) 1998 1999lemma valid_mdb'_pspaceI: 2000 "valid_mdb' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_mdb' s'" 2001 unfolding valid_mdb'_def by simp 2002 2003lemma state_refs_of'_pspaceI: 2004 "P (state_refs_of' s) \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> P (state_refs_of' s')" 2005 unfolding state_refs_of'_def ps_clear_def by simp 2006 2007lemma if_live_then_nonz_cap'_pspaceI: 2008 "if_live_then_nonz_cap' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> if_live_then_nonz_cap' s'" 2009 unfolding if_live_then_nonz_cap'_def ex_nonz_cap_to'_def 2010 apply (simp add: ko_wp_at'_def ps_clear_def) 2011 apply (erule allEI) 2012 apply (fastforce intro: cte_wp_at'_pspaceI) 2013 done 2014 2015lemma no_0_obj_pspaceI: 2016 "no_0_obj' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> no_0_obj' s'" 2017 by (simp add: no_0_obj'_def) 2018 2019lemma valid_pspace': 2020 "valid_pspace' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> valid_pspace' s'" 2021 by (auto simp add: valid_pspace'_def valid_objs'_def pspace_aligned'_def 2022 pspace_distinct'_def ps_clear_def no_0_obj'_def ko_wp_at'_def 2023 typ_at'_def 2024 intro: valid_obj'_pspaceI valid_mdb'_pspaceI) 2025 2026lemma ex_cte_cap_to_pspaceI'[elim]: 2027 "ex_cte_cap_to' p s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> 2028 intStateIRQNode (ksInterruptState s) = intStateIRQNode (ksInterruptState s') 2029 \<Longrightarrow> ex_cte_cap_to' p s'" 2030 by (fastforce simp: ex_cte_cap_to'_def elim: cte_wp_at'_pspaceI) 2031 2032lemma ifunsafe_valid_pspaceI'[elim]: 2033 "if_unsafe_then_cap' s \<Longrightarrow> ksPSpace s = ksPSpace s' \<Longrightarrow> 2034 intStateIRQNode (ksInterruptState s) = intStateIRQNode (ksInterruptState s') 2035 \<Longrightarrow> if_unsafe_then_cap' s'" 2036 by (fastforce simp: if_unsafe_then_cap'_def intro: cte_wp_at'_pspaceI) 2037 2038lemma valid_idle'_pspace_itI[elim]: 2039 "\<lbrakk> valid_idle' s; ksPSpace s = ksPSpace s'; ksIdleThread s = ksIdleThread s' \<rbrakk> 2040 \<Longrightarrow> valid_idle' s'" 2041 apply (clarsimp simp: valid_idle'_def ex_nonz_cap_to'_def) 2042 apply (erule pred_tcb_at'_pspaceI, assumption) 2043 done 2044 2045lemma obj_at'_weaken: 2046 assumes x: "obj_at' P t s" 2047 assumes y: "\<And>obj. P obj \<Longrightarrow> P' obj" 2048 shows "obj_at' P' t s" 2049 by (insert x, clarsimp simp: obj_at'_def y) 2050 2051lemma cte_wp_at_weakenE': 2052 "\<lbrakk>cte_wp_at' P t s; \<And>c. P c \<Longrightarrow> P' c\<rbrakk> \<Longrightarrow> cte_wp_at' P' t s" 2053 by (fastforce simp: cte_wp_at'_def) 2054 2055lemma obj_at'_weakenE: 2056 "\<lbrakk> obj_at' P p s; \<And>k. P k \<Longrightarrow> P' k \<rbrakk> \<Longrightarrow> obj_at' P' p s" 2057 by (clarsimp simp: obj_at'_def) 2058 2059lemma pred_tcb'_weakenE: 2060 "\<lbrakk> pred_tcb_at' proj P t s; \<And>st. P st \<Longrightarrow> P' st \<rbrakk> \<Longrightarrow> pred_tcb_at' proj P' t s" 2061 apply (simp add: pred_tcb_at'_def) 2062 apply (erule obj_at'_weakenE) 2063 apply clarsimp 2064 done 2065 2066lemma lookupBefore_fst_snd: 2067 "lookupBefore x s = Some v \<Longrightarrow> snd v = the (s (fst v))" 2068 by (clarsimp simp add: lookupBefore_def Let_def split: if_split_asm) 2069 2070lemma lookupBefore_exact2: 2071 "\<lbrakk> lookupBefore x s = Some v; fst v = x \<rbrakk> \<Longrightarrow> s x = Some (snd v)" 2072 apply (cases v) 2073 apply (clarsimp simp add: lookupBefore_def Let_def split: if_split_asm) 2074 apply (drule subst[where P="\<lambda>x. x \<in> y" for y, OF _ Max_in]) 2075 apply simp 2076 apply fastforce 2077 apply clarsimp 2078 done 2079 2080lemma lookupBefore_char: 2081 "(lookupBefore x s = Some (y, v)) = (y \<le> x \<and> s y = Some v \<and> (\<forall>z. z \<le> x \<and> y < z \<longrightarrow> s z = None))" 2082 apply (simp add: lookupBefore_def Let_def cong: conj_cong) 2083 apply (rule conjI) 2084 apply (clarsimp simp: dom_def) 2085 apply clarsimp 2086 apply (rule iffI) 2087 apply (erule conjE) 2088 apply (frule subst[where P="\<lambda>x. x \<in> y'" for y', OF _ Max_in]) 2089 apply simp 2090 apply fastforce 2091 apply clarsimp 2092 apply (rule ccontr, clarsimp) 2093 apply (subst(asm) Max_less_iff) 2094 apply simp 2095 apply fastforce 2096 apply (drule_tac x=z in bspec) 2097 apply fastforce 2098 apply simp 2099 apply clarsimp 2100 apply (rule order_antisym) 2101 apply (subst Max_le_iff) 2102 apply simp 2103 apply fastforce 2104 apply fastforce 2105 apply (rule Max_ge) 2106 apply simp 2107 apply fastforce 2108 done 2109 2110lemma lookupAround2_char1: 2111 "(fst (lookupAround2 x s) = Some (y, v)) = 2112 (y \<le> x \<and> s y = Some v \<and> (\<forall>z. y < z \<and> z \<le> x \<longrightarrow> s z = None))" 2113 apply (simp add: lookupAround2_def Let_def split_def lookupAround_def 2114 split del: if_split 2115 split: option.split) 2116 apply (intro conjI impI iffI) 2117 apply (clarsimp split: if_split_asm) 2118 apply (rule Max_prop) 2119 apply (simp add: order_less_imp_le) 2120 apply fastforce 2121 apply (clarsimp split: if_split_asm) 2122 apply (rule Max_prop) 2123 apply clarsimp 2124 apply fastforce 2125 apply (clarsimp split: if_split_asm) 2126 apply (subst(asm) Max_less_iff) 2127 apply simp 2128 apply fastforce 2129 apply (fastforce intro: order_neq_le_trans) 2130 apply (clarsimp cong: conj_cong) 2131 apply (rule conjI) 2132 apply fastforce 2133 apply (rule order_antisym) 2134 apply (subst Max_le_iff) 2135 apply simp 2136 apply fastforce 2137 apply clarsimp 2138 apply (rule ccontr) 2139 apply (fastforce simp add: linorder_not_le) 2140 apply (rule Max_ge) 2141 apply simp 2142 apply fastforce 2143 apply (intro allI impI iffI) 2144 apply clarsimp 2145 apply simp 2146 apply clarsimp 2147 apply (drule spec[where x=x]) 2148 apply simp 2149 done 2150 2151lemma lookupAround2_None1: 2152 "(fst (lookupAround2 x s) = None) = (\<forall>y \<le> x. s y = None)" 2153 apply (simp add: lookupAround2_def Let_def split_def lookupAround_def 2154 split del: if_split 2155 split: option.split) 2156 apply safe 2157 apply (fastforce split: if_split_asm) 2158 apply (clarsimp simp: order_less_imp_le) 2159 apply fastforce 2160 done 2161 2162lemma lookupAround2_None2: 2163 "(snd (lookupAround2 x s) = None) = (\<forall>y. x < y \<longrightarrow> s y = None)" 2164 apply (simp add: lookupAround2_def Let_def split_def del: maybe_def 2165 split: option.splits) 2166 apply (simp add: o_def map_option_is_None [where f=fst, unfolded map_option_case]) 2167 apply (simp add: lookupAround_def Let_def) 2168 apply fastforce 2169 done 2170 2171lemma lookupAround2_char2: 2172 "(snd (lookupAround2 x s) = Some y) = (x < y \<and> s y \<noteq> None \<and> (\<forall>z. x < z \<and> z < y \<longrightarrow> s z = None))" 2173 apply (simp add: lookupAround2_def Let_def split_def o_def 2174 del: maybe_def 2175 split: option.splits) 2176 apply (simp add: o_def map_option_is_None [where f=fst, unfolded map_option_case]) 2177 apply (simp add: lookupAround_def Let_def) 2178 apply (rule conjI) 2179 apply fastforce 2180 apply clarsimp 2181 apply (rule iffI) 2182 apply (frule subst[where P="\<lambda>x. x \<in> y2" for y2, OF _ Min_in]) 2183 apply simp 2184 apply fastforce 2185 apply clarsimp 2186 apply (subst(asm) Min_gr_iff, simp, fastforce, simp(no_asm_use), fastforce) 2187 apply clarsimp 2188 apply (rule order_antisym) 2189 apply (fastforce intro: Min_le) 2190 apply (subst Min_ge_iff) 2191 apply simp 2192 apply fastforce 2193 apply clarsimp 2194 apply (rule ccontr, simp add: linorder_not_le) 2195 done 2196 2197lemma ps_clearI: 2198 "\<lbrakk> is_aligned p n; (1 :: word32) < 2 ^ n; 2199 \<And>x. \<lbrakk> x > p; x \<le> p + 2 ^ n - 1 \<rbrakk> \<Longrightarrow> ksPSpace s x = None \<rbrakk> 2200 \<Longrightarrow> ps_clear p n s" 2201 apply (subgoal_tac "p \<le> p + 1") 2202 apply (simp add: ps_clear_def2) 2203 apply (rule ccontr, erule nonemptyE, clarsimp) 2204 apply (drule minus_one_helper[where x="z + 1" for z]) 2205 apply clarsimp 2206 apply simp 2207 apply (erule is_aligned_get_word_bits) 2208 apply (erule(1) is_aligned_no_wrap') 2209 apply simp 2210 done 2211 2212lemma ps_clear_lookupAround2: 2213 "\<lbrakk> ps_clear p' n s; ksPSpace s p' = Some x; 2214 p' \<le> p; p \<le> p' + 2 ^ n - 1; 2215 \<lbrakk> fst (lookupAround2 p (ksPSpace s)) = Some (p', x); 2216 case_option True (\<lambda>x. x - p' >= 2 ^ n) (snd (lookupAround2 p (ksPSpace s))) 2217 \<rbrakk> \<Longrightarrow> P (lookupAround2 p (ksPSpace s)) \<rbrakk> \<Longrightarrow> P (lookupAround2 p (ksPSpace s))" 2218 apply (drule meta_mp) 2219 apply (cases "fst (lookupAround2 p (ksPSpace s))") 2220 apply (simp add: lookupAround2_None1) 2221 apply clarsimp 2222 apply (clarsimp simp: lookupAround2_char1) 2223 apply (frule spec[where x=p']) 2224 apply (simp add: linorder_not_less ps_clear_def) 2225 apply (drule_tac f="\<lambda>S. a \<in> S" in arg_cong) 2226 apply (simp add: domI) 2227 apply (frule(1) order_trans, simp) 2228 apply (erule meta_mp) 2229 apply (clarsimp split: option.split) 2230 apply (clarsimp simp: lookupAround2_char2 ps_clear_def) 2231 apply (drule_tac a=x2 in equals0D) 2232 apply (simp add: domI) 2233 apply (subst(asm) order_less_imp_le[OF order_le_less_trans[where y=p]], 2234 assumption, assumption) 2235 apply simp 2236 apply (erule impCE, simp_all) 2237 apply (simp add: linorder_not_le) 2238 apply (subst(asm) add_diff_eq[symmetric], 2239 subst(asm) add.commute, 2240 drule word_l_diffs(2), 2241 fastforce simp only: field_simps) 2242 apply (rule ccontr, simp add: linorder_not_le) 2243 apply (drule minus_one_helper3, fastforce) 2244 done 2245 2246lemma in_magnitude_check: 2247 "\<lbrakk> is_aligned x n; (1 :: word32) < 2 ^ n; ksPSpace s x = Some y \<rbrakk> \<Longrightarrow> 2248 ((v, s') \<in> fst (magnitudeCheck x (snd (lookupAround2 x (ksPSpace s))) n s)) 2249 = (s' = s \<and> ps_clear x n s)" 2250 apply (rule iffI) 2251 apply (clarsimp simp: magnitudeCheck_def in_monad lookupAround2_None2 2252 lookupAround2_char2 2253 split: option.split_asm) 2254 apply (erule(1) ps_clearI) 2255 apply simp 2256 apply (erule(1) ps_clearI) 2257 apply (simp add: linorder_not_less) 2258 apply (drule minus_one_helper[where x="2 ^ n"]) 2259 apply (clarsimp simp: power_overflow) 2260 apply (drule word_l_diffs) 2261 apply simp 2262 apply (simp add: field_simps) 2263 apply clarsimp 2264 apply (erule is_aligned_get_word_bits) 2265 apply (erule(1) ps_clear_lookupAround2) 2266 apply simp 2267 apply (simp add: is_aligned_no_overflow) 2268 apply (clarsimp simp add: magnitudeCheck_def in_monad 2269 split: option.split_asm) 2270 apply simp 2271 apply (simp add: power_overflow) 2272 done 2273 2274lemma in_magnitude_check3: 2275 "\<lbrakk> \<forall>z. x < z \<and> z \<le> y \<longrightarrow> ksPSpace s z = None; is_aligned x n; 2276 (1 :: word32) < 2 ^ n; ksPSpace s x = Some v; x \<le> y; y - x < 2 ^ n \<rbrakk> \<Longrightarrow> 2277 fst (magnitudeCheck x (snd (lookupAround2 y (ksPSpace s))) n s) 2278 = (if ps_clear x n s then {((), s)} else {})" 2279 apply (rule set_eqI, rule iffI) 2280 apply (clarsimp simp: magnitudeCheck_def lookupAround2_char2 2281 lookupAround2_None2 in_monad 2282 split: option.split_asm) 2283 apply (drule(1) range_convergence1) 2284 apply (erule(1) ps_clearI) 2285 apply simp 2286 apply (erule is_aligned_get_word_bits) 2287 apply (drule(1) range_convergence2) 2288 apply (erule(1) ps_clearI) 2289 apply (simp add: linorder_not_less) 2290 apply (drule minus_one_helper[where x="2 ^ n" for n], simp) 2291 apply (drule word_l_diffs, simp) 2292 apply (simp add: field_simps) 2293 apply (simp add: power_overflow) 2294 apply (clarsimp split: if_split_asm) 2295 apply (erule(1) ps_clear_lookupAround2) 2296 apply simp 2297 apply (drule minus_one_helper3[where x="y - x"]) 2298 apply (drule word_plus_mono_right[where x=x and y="y - x"]) 2299 apply (erule is_aligned_get_word_bits) 2300 apply (simp add: field_simps is_aligned_no_overflow) 2301 apply simp 2302 apply (simp add: field_simps) 2303 apply (simp add: magnitudeCheck_def return_def 2304 iffD2[OF linorder_not_less] when_def 2305 split: option.split_asm) 2306 done 2307 2308lemma in_alignCheck[simp]: 2309 "((v, s') \<in> fst (alignCheck x n s)) = (s' = s \<and> is_aligned x n)" 2310 by (simp add: alignCheck_def in_monad is_aligned_mask[symmetric] 2311 alignError_def conj_comms 2312 cong: conj_cong) 2313 2314lemma tcb_space_clear: 2315 "\<lbrakk> tcb_cte_cases (y - x) = Some (getF, setF); 2316 is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; 2317 ksPSpace s x = Some (KOTCB tcb); ksPSpace s y = Some v; 2318 \<lbrakk> x = y; getF = tcbCTable; setF = tcbCTable_update \<rbrakk> \<Longrightarrow> P 2319 \<rbrakk> \<Longrightarrow> P" 2320 apply (cases "x = y") 2321 apply simp 2322 apply (clarsimp simp: ps_clear_def) 2323 apply (drule_tac a=y in equals0D) 2324 apply (simp add: domI) 2325 apply (subgoal_tac "\<exists>z. y = x + z \<and> z < 2 ^ tcbBlockSizeBits") 2326 apply (elim exE conjE) 2327 apply (frule(1) is_aligned_no_wrap'[rotated, rotated]) 2328 apply (simp add: word_bits_conv objBits_defs) 2329 apply (erule notE, subst field_simps, rule word_plus_mono_right) 2330 apply (drule minus_one_helper3,simp,erule is_aligned_no_wrap') 2331 apply (simp add: word_bits_conv) 2332 apply (simp add: objBits_defs) 2333 apply (rule_tac x="y - x" in exI) 2334 apply (simp add: tcb_cte_cases_def split: if_split_asm) 2335 done 2336 2337lemma tcb_ctes_clear: 2338 "\<lbrakk> tcb_cte_cases (y - x) = Some (getF, setF); 2339 is_aligned x tcbBlockSizeBits; ps_clear x tcbBlockSizeBits s; 2340 ksPSpace s x = Some (KOTCB tcb) \<rbrakk> 2341 \<Longrightarrow> \<not> ksPSpace s y = Some (KOCTE cte)" 2342 apply clarsimp 2343 apply (erule(4) tcb_space_clear) 2344 apply simp 2345 done 2346 2347lemma cte_wp_at_cases': 2348 shows "cte_wp_at' P p s = 2349 ((\<exists>cte. ksPSpace s p = Some (KOCTE cte) \<and> is_aligned p cte_level_bits 2350 \<and> P cte \<and> ps_clear p cteSizeBits s) \<or> 2351 (\<exists>n tcb getF setF. ksPSpace s (p - n) = Some (KOTCB tcb) \<and> is_aligned (p - n) tcbBlockSizeBits 2352 \<and> tcb_cte_cases n = Some (getF, setF) \<and> P (getF tcb) \<and> ps_clear (p - n) tcbBlockSizeBits s))" 2353 (is "?LHS = ?RHS") 2354 apply (rule iffI) 2355 apply (clarsimp simp: cte_wp_at'_def split_def 2356 getObject_def bind_def simpler_gets_def 2357 assert_opt_def return_def fail_def 2358 split: option.splits 2359 del: disjCI) 2360 apply (clarsimp simp: loadObject_cte typeError_def alignError_def 2361 fail_def return_def objBits_simps' 2362 is_aligned_mask[symmetric] alignCheck_def 2363 tcbVTableSlot_def field_simps tcbCTableSlot_def 2364 tcbReplySlot_def tcbCallerSlot_def 2365 tcbIPCBufferSlot_def 2366 lookupAround2_char1 2367 cte_level_bits_def Ball_def 2368 unless_def when_def bind_def 2369 split: kernel_object.splits if_split_asm option.splits 2370 del: disjCI) 2371 apply (subst(asm) in_magnitude_check3, simp+, 2372 simp split: if_split_asm, (rule disjI2)?, intro exI, rule conjI, 2373 erule rsubst[where P="\<lambda>x. ksPSpace s x = v" for s v], 2374 fastforce simp add: field_simps, simp)+ 2375 apply (subst(asm) in_magnitude_check3, simp+) 2376 apply (simp split: if_split_asm) 2377 apply (simp add: cte_wp_at'_def getObject_def split_def 2378 bind_def simpler_gets_def return_def 2379 assert_opt_def fail_def objBits_simps' 2380 split: option.splits) 2381 apply (elim disjE conjE exE) 2382 apply (erule(1) ps_clear_lookupAround2) 2383 apply simp 2384 apply (simp add: field_simps) 2385 apply (erule is_aligned_no_wrap') 2386 apply (simp add: cte_level_bits_def word_bits_conv) 2387 apply (simp add: cte_level_bits_def) 2388 apply (simp add: loadObject_cte unless_def alignCheck_def 2389 is_aligned_mask[symmetric] objBits_simps' 2390 cte_level_bits_def magnitudeCheck_def 2391 return_def fail_def) 2392 apply (clarsimp simp: bind_def return_def when_def fail_def 2393 split: option.splits) 2394 apply simp 2395 apply (erule(1) ps_clear_lookupAround2) 2396 prefer 3 2397 apply (simp add: loadObject_cte unless_def alignCheck_def 2398 is_aligned_mask[symmetric] objBits_simps' 2399 cte_level_bits_def magnitudeCheck_def 2400 return_def fail_def tcbCTableSlot_def tcbVTableSlot_def 2401 tcbIPCBufferSlot_def tcbReplySlot_def tcbCallerSlot_def 2402 split: option.split_asm) 2403 apply (clarsimp simp: bind_def tcb_cte_cases_def split: if_split_asm) 2404 apply (clarsimp simp: bind_def tcb_cte_cases_def iffD2[OF linorder_not_less] 2405 when_False return_def 2406 split: if_split_asm) 2407 apply (subgoal_tac "p - n \<le> (p - n) + n", simp) 2408 apply (erule is_aligned_no_wrap') 2409 apply (simp add: word_bits_conv) 2410 apply (simp add: tcb_cte_cases_def split: if_split_asm) 2411 apply (subgoal_tac "(p - n) + n \<le> (p - n) + 511") 2412 apply (simp add: field_simps) 2413 apply (rule word_plus_mono_right) 2414 apply (simp add: tcb_cte_cases_def split: if_split_asm) 2415 apply (erule is_aligned_no_wrap') 2416 apply simp 2417 done 2418 2419lemma tcb_at_cte_at': 2420 "tcb_at' t s \<Longrightarrow> cte_at' t s" 2421 apply (clarsimp simp add: cte_wp_at_cases' obj_at'_def projectKO_def 2422 del: disjCI) 2423 apply (case_tac ko) 2424 apply (simp_all add: projectKO_opt_tcb fail_def) 2425 apply (rule exI[where x=0]) 2426 apply (clarsimp simp add: return_def objBits_simps) 2427 done 2428 2429lemma cte_wp_atE' [consumes 1, case_names CTE TCB]: 2430 assumes cte: "cte_wp_at' P ptr s" 2431 and r1: "\<And>cte. 2432 \<lbrakk> ksPSpace s ptr = Some (KOCTE cte); ps_clear ptr cte_level_bits s; 2433 is_aligned ptr cte_level_bits; P cte \<rbrakk> \<Longrightarrow> R" 2434 and r2: "\<And> tcb ptr' getF setF. 2435 \<lbrakk> ksPSpace s ptr' = Some (KOTCB tcb); ps_clear ptr' tcbBlockSizeBits s; is_aligned ptr' tcbBlockSizeBits; 2436 tcb_cte_cases (ptr - ptr') = Some (getF, setF); P (getF tcb) \<rbrakk> \<Longrightarrow> R" 2437 shows "R" 2438 by (rule disjE [OF iffD1 [OF cte_wp_at_cases' cte]]) 2439 (auto intro: r1 r2 simp: cte_level_bits_def objBits_defs) 2440 2441lemma cte_wp_at_cteI': 2442 assumes "ksPSpace s ptr = Some (KOCTE cte)" 2443 assumes "is_aligned ptr cte_level_bits" 2444 assumes "ps_clear ptr cte_level_bits s" 2445 assumes "P cte" 2446 shows "cte_wp_at' P ptr s" 2447 using assms by (simp add: cte_wp_at_cases' cte_level_bits_def objBits_defs) 2448 2449lemma cte_wp_at_tcbI': 2450 assumes "ksPSpace s ptr' = Some (KOTCB tcb)" 2451 assumes "is_aligned ptr' tcbBlockSizeBits" 2452 assumes "ps_clear ptr' tcbBlockSizeBits s" 2453 and "tcb_cte_cases (ptr - ptr') = Some (getF, setF)" 2454 and "P (getF tcb)" 2455 shows "cte_wp_at' P ptr s" 2456 using assms 2457 apply (simp add: cte_wp_at_cases') 2458 apply (rule disjI2, rule exI[where x="ptr - ptr'"]) 2459 apply simp 2460 done 2461 2462lemma obj_at_ko_at': 2463 "obj_at' P p s \<Longrightarrow> \<exists>ko. ko_at' ko p s \<and> P ko" 2464 by (auto simp add: obj_at'_def) 2465 2466lemma obj_at_aligned': 2467 fixes P :: "('a :: pspace_storable) \<Rightarrow> bool" 2468 assumes oat: "obj_at' P p s" 2469 and oab: "\<And>(v :: 'a) (v' :: 'a). objBits v = objBits v'" 2470 shows "is_aligned p (objBits (obj :: 'a))" 2471 using oat 2472 apply (clarsimp simp add: obj_at'_def) 2473 apply (clarsimp simp add: projectKO_def fail_def return_def 2474 project_inject objBits_def[symmetric] 2475 split: option.splits) 2476 apply (erule subst[OF oab]) 2477 done 2478 2479(* locateSlot *) 2480lemma locateSlot_conv: 2481 "locateSlotBasic A B = return (A + 2 ^ cte_level_bits * B)" 2482 "locateSlotTCB = locateSlotBasic" 2483 "locateSlotCNode A bits B = (do 2484 x \<leftarrow> stateAssert (\<lambda>s. case (gsCNodes s A) of None \<Rightarrow> False | Some n \<Rightarrow> n = bits \<and> B < 2 ^ n) []; 2485 locateSlotBasic A B od)" 2486 "locateSlotCap c B = (do 2487 x \<leftarrow> stateAssert (\<lambda>s. ((isCNodeCap c \<or> (isZombie c \<and> capZombieType c \<noteq> ZombieTCB)) 2488 \<and> (case gsCNodes s (capUntypedPtr c) of None \<Rightarrow> False 2489 | Some n \<Rightarrow> (isCNodeCap c \<and> n = capCNodeBits c 2490 \<or> isZombie c \<and> n = zombieCTEBits (capZombieType c)) \<and> B < 2 ^ n)) 2491 \<or> isThreadCap c \<or> (isZombie c \<and> capZombieType c = ZombieTCB)) []; 2492 locateSlotBasic (capUntypedPtr c) B od)" 2493 apply (simp_all add: locateSlotCap_def locateSlotTCB_def fun_eq_iff) 2494 apply (simp add: locateSlotBasic_def objBits_simps cte_level_bits_def objBits_defs) 2495 apply (simp add: locateSlotCNode_def stateAssert_def) 2496 apply (cases c, simp_all add: locateSlotCNode_def isZombie_def isThreadCap_def 2497 isCNodeCap_def capUntypedPtr_def stateAssert_def 2498 bind_assoc exec_get locateSlotTCB_def 2499 objBits_simps' 2500 split: zombie_type.split) 2501 done 2502 2503lemma typ_at_tcb': 2504 "typ_at' TCBT = tcb_at'" 2505 apply (rule ext)+ 2506 apply (simp add: obj_at'_real_def typ_at'_def) 2507 apply (simp add: ko_wp_at'_def) 2508 apply (rule iffI) 2509 apply clarsimp 2510 apply (case_tac ko) 2511 apply (auto simp: projectKO_opt_tcb)[9] 2512 apply (case_tac ko) 2513 apply (auto simp: projectKO_opt_tcb) 2514 done 2515 2516lemma typ_at_ep: 2517 "typ_at' EndpointT = ep_at'" 2518 apply (rule ext)+ 2519 apply (simp add: obj_at'_real_def typ_at'_def) 2520 apply (simp add: ko_wp_at'_def) 2521 apply (rule iffI) 2522 apply clarsimp 2523 apply (case_tac ko) 2524 apply (auto simp: projectKO_opt_ep)[9] 2525 apply (case_tac ko) 2526 apply (auto simp: projectKO_opt_ep) 2527 done 2528 2529lemma typ_at_ntfn: 2530 "typ_at' NotificationT = ntfn_at'" 2531 apply (rule ext)+ 2532 apply (simp add: obj_at'_real_def typ_at'_def) 2533 apply (simp add: ko_wp_at'_def) 2534 apply (rule iffI) 2535 apply clarsimp 2536 apply (case_tac ko) 2537 apply (auto simp: projectKO_opt_ntfn)[8] 2538 apply clarsimp 2539 apply (case_tac ko) 2540 apply (auto simp: projectKO_opt_ntfn) 2541 done 2542 2543lemma typ_at_cte: 2544 "typ_at' CTET = real_cte_at'" 2545 apply (rule ext)+ 2546 apply (simp add: obj_at'_real_def typ_at'_def) 2547 apply (simp add: ko_wp_at'_def) 2548 apply (rule iffI) 2549 apply clarsimp 2550 apply (case_tac ko) 2551 apply (auto simp: projectKO_opt_cte)[8] 2552 apply clarsimp 2553 apply (case_tac ko) 2554 apply (auto simp: projectKO_opt_cte) 2555 done 2556 2557lemma cte_at_typ': 2558 "cte_at' c = (\<lambda>s. typ_at' CTET c s \<or> (\<exists>n. typ_at' TCBT (c - n) s \<and> n \<in> dom tcb_cte_cases))" 2559proof - 2560 have P: "\<And>ko. (koTypeOf ko = CTET) = (\<exists>cte. ko = KOCTE cte)" 2561 "\<And>ko. (koTypeOf ko = TCBT) = (\<exists>tcb. ko = KOTCB tcb)" 2562 by (case_tac ko, simp_all)+ 2563 have Q: "\<And>P f. (\<exists>x. (\<exists>y. x = f y) \<and> P x) = (\<exists>y. P (f y))" 2564 by fastforce 2565 show ?thesis 2566 by (fastforce simp: cte_wp_at_cases' obj_at'_real_def typ_at'_def 2567 ko_wp_at'_def objBits_simps' P Q conj_comms cte_level_bits_def) 2568qed 2569 2570lemma typ_at_lift_tcb': 2571 "\<lbrace>typ_at' TCBT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' TCBT p\<rbrace> \<Longrightarrow> \<lbrace>tcb_at' p\<rbrace> f \<lbrace>\<lambda>_. tcb_at' p\<rbrace>" 2572 by (simp add: typ_at_tcb') 2573 2574lemma typ_at_lift_ep': 2575 "\<lbrace>typ_at' EndpointT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' EndpointT p\<rbrace> \<Longrightarrow> \<lbrace>ep_at' p\<rbrace> f \<lbrace>\<lambda>_. ep_at' p\<rbrace>" 2576 by (simp add: typ_at_ep) 2577 2578lemma typ_at_lift_ntfn': 2579 "\<lbrace>typ_at' NotificationT p\<rbrace> f \<lbrace>\<lambda>_. typ_at' NotificationT p\<rbrace> \<Longrightarrow> \<lbrace>ntfn_at' p\<rbrace> f \<lbrace>\<lambda>_. ntfn_at' p\<rbrace>" 2580 by (simp add: typ_at_ntfn) 2581 2582lemma typ_at_lift_cte': 2583 "\<lbrace>typ_at' CTET p\<rbrace> f \<lbrace>\<lambda>_. typ_at' CTET p\<rbrace> \<Longrightarrow> \<lbrace>real_cte_at' p\<rbrace> f \<lbrace>\<lambda>_. real_cte_at' p\<rbrace>" 2584 by (simp add: typ_at_cte) 2585 2586lemma typ_at_lift_cte_at': 2587 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 2588 shows "\<lbrace>cte_at' c\<rbrace> f \<lbrace>\<lambda>rv. cte_at' c\<rbrace>" 2589 apply (simp only: cte_at_typ') 2590 apply (wp hoare_vcg_disj_lift hoare_vcg_ex_lift x) 2591 done 2592 2593lemma typ_at_lift_page_directory_at': 2594 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 2595 shows "\<lbrace>page_directory_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_directory_at' p\<rbrace>" 2596 unfolding page_directory_at'_def All_less_Ball 2597 by (wp hoare_vcg_const_Ball_lift x) 2598 2599lemma typ_at_lift_page_table_at': 2600 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 2601 shows "\<lbrace>page_table_at' p\<rbrace> f \<lbrace>\<lambda>rv. page_table_at' p\<rbrace>" 2602 unfolding page_table_at'_def All_less_Ball 2603 by (wp hoare_vcg_const_Ball_lift x) 2604 2605lemma ko_wp_typ_at': 2606 "ko_wp_at' P p s \<Longrightarrow> \<exists>T. typ_at' T p s" 2607 by (clarsimp simp: typ_at'_def ko_wp_at'_def) 2608 2609lemma koType_obj_range': 2610 "koTypeOf k = koTypeOf k' \<Longrightarrow> obj_range' p k = obj_range' p k'" 2611 apply (rule ccontr) 2612 apply (simp add: obj_range'_def objBitsKO_def archObjSize_def 2613 split: kernel_object.splits arch_kernel_object.splits) 2614 done 2615 2616lemma typ_at_lift_valid_untyped': 2617 assumes P: "\<And>T p. \<lbrace>\<lambda>s. \<not>typ_at' T p s\<rbrace> f \<lbrace>\<lambda>rv s. \<not>typ_at' T p s\<rbrace>" 2618 shows "\<lbrace>\<lambda>s. valid_untyped' d p n idx s\<rbrace> f \<lbrace>\<lambda>rv s. valid_untyped' d p n idx s\<rbrace>" 2619 apply (clarsimp simp: valid_untyped'_def split del:if_split) 2620 apply (rule hoare_vcg_all_lift) 2621 apply (clarsimp simp: valid_def split del:if_split) 2622 apply (frule ko_wp_typ_at') 2623 apply clarsimp 2624 apply (cut_tac T=T and p=ptr' in P) 2625 apply (simp add: valid_def) 2626 apply (erule_tac x=s in allE) 2627 apply (erule impE) 2628 prefer 2 2629 apply (drule (1) bspec) 2630 apply simp 2631 apply (clarsimp simp: typ_at'_def ko_wp_at'_def simp del:atLeastAtMost_iff) 2632 apply (elim disjE) 2633 apply (clarsimp simp:psubset_eq simp del:atLeastAtMost_iff) 2634 apply (drule_tac p=ptr' in koType_obj_range') 2635 apply (erule impE) 2636 apply simp 2637 apply simp 2638 apply (drule_tac p = ptr' in koType_obj_range') 2639 apply (clarsimp split:if_splits) 2640 done 2641 2642lemma typ_at_lift_asid_at': 2643 "(\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>_. typ_at' T p\<rbrace>) \<Longrightarrow> \<lbrace>asid_pool_at' p\<rbrace> f \<lbrace>\<lambda>_. asid_pool_at' p\<rbrace>" 2644 by assumption 2645 2646lemma typ_at_lift_valid_cap': 2647 assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" 2648 shows "\<lbrace>\<lambda>s. valid_cap' cap s\<rbrace> f \<lbrace>\<lambda>rv s. valid_cap' cap s\<rbrace>" 2649 including no_pre 2650 apply (simp add: valid_cap'_def) 2651 apply wp 2652 apply (case_tac cap; 2653 simp add: valid_cap'_def P [where P=id, simplified] typ_at_lift_tcb' 2654 hoare_vcg_prop typ_at_lift_ep' 2655 typ_at_lift_ntfn' typ_at_lift_cte_at' 2656 hoare_vcg_conj_lift [OF typ_at_lift_cte_at']) 2657 apply (rename_tac zombie_type nat) 2658 apply (case_tac zombie_type; simp) 2659 apply (wp typ_at_lift_tcb' P hoare_vcg_all_lift typ_at_lift_cte')+ 2660 apply (rename_tac arch_capability) 2661 apply (case_tac arch_capability, 2662 simp_all add: P [where P=id, simplified] page_table_at'_def 2663 hoare_vcg_prop page_directory_at'_def All_less_Ball 2664 split del: if_splits) 2665 apply (wp hoare_vcg_const_Ball_lift P typ_at_lift_valid_untyped' 2666 hoare_vcg_all_lift typ_at_lift_cte')+ 2667 done 2668 2669 2670lemma typ_at_lift_valid_irq_node': 2671 assumes P: "\<And>P T p. \<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at' T p s)\<rbrace>" 2672 shows "\<lbrace>valid_irq_node' p\<rbrace> f \<lbrace>\<lambda>_. valid_irq_node' p\<rbrace>" 2673 apply (simp add: valid_irq_node'_def) 2674 apply (wp hoare_vcg_all_lift P typ_at_lift_cte') 2675 done 2676 2677lemma valid_pde_lift': 2678 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 2679 shows "\<lbrace>\<lambda>s. valid_pde' pde s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pde' pde s\<rbrace>" 2680 by (cases pde) (simp add: valid_mapping'_def|wp x typ_at_lift_page_table_at')+ 2681 2682lemma valid_pte_lift': 2683 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 2684 shows "\<lbrace>\<lambda>s. valid_pte' pte s\<rbrace> f \<lbrace>\<lambda>rv s. valid_pte' pte s\<rbrace>" 2685 by (cases pte) (simp add: valid_mapping'_def|wp x typ_at_lift_page_directory_at')+ 2686 2687lemma valid_asid_pool_lift': 2688 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 2689 shows "\<lbrace>\<lambda>s. valid_asid_pool' ap s\<rbrace> f \<lbrace>\<lambda>rv s. valid_asid_pool' ap s\<rbrace>" 2690 by (cases ap) (simp|wp x typ_at_lift_page_directory_at' hoare_vcg_const_Ball_lift)+ 2691 2692lemma valid_bound_tcb_lift: 2693 "(\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>_. typ_at' T p\<rbrace>) \<Longrightarrow> 2694 \<lbrace>valid_bound_tcb' tcb\<rbrace> f \<lbrace>\<lambda>_. valid_bound_tcb' tcb\<rbrace>" 2695 by (auto simp: valid_bound_tcb'_def valid_def typ_at_tcb'[symmetric] split: option.splits) 2696 2697lemmas typ_at_lifts = typ_at_lift_tcb' typ_at_lift_ep' 2698 typ_at_lift_ntfn' typ_at_lift_cte' 2699 typ_at_lift_cte_at' 2700 typ_at_lift_page_table_at' 2701 typ_at_lift_page_directory_at' 2702 typ_at_lift_asid_at' 2703 typ_at_lift_valid_untyped' 2704 typ_at_lift_valid_cap' 2705 valid_pde_lift' 2706 valid_pte_lift' 2707 valid_asid_pool_lift' 2708 valid_bound_tcb_lift 2709 2710lemma mdb_next_unfold: 2711 "s \<turnstile> c \<leadsto> c' = (\<exists>z. s c = Some z \<and> c' = mdbNext (cteMDBNode z))" 2712 by (auto simp add: mdb_next_rel_def mdb_next_def) 2713 2714lemma valid_dlist_prevD: 2715 "\<lbrakk> valid_dlist m; c \<noteq> 0; c' \<noteq> 0 \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c'" 2716 by (fastforce simp add: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) 2717 2718 2719lemma no_0_simps [simp]: 2720 assumes "no_0 m" 2721 shows "((m 0 = Some cte) = False) \<and> ((Some cte = m 0) = False)" 2722 using assms by (simp add: no_0_def) 2723 2724lemma valid_dlist_def2: 2725 "no_0 m \<Longrightarrow> valid_dlist m = (\<forall>c c'. c \<noteq> 0 \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c' = m \<turnstile> c \<leftarrow> c')" 2726 apply (rule iffI) 2727 apply (simp add: valid_dlist_prevD) 2728 apply (clarsimp simp: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) 2729 apply (subgoal_tac "p\<noteq>0") 2730 prefer 2 2731 apply clarsimp 2732 apply (rule conjI) 2733 apply clarsimp 2734 apply (erule_tac x="mdbPrev (cteMDBNode cte)" in allE) 2735 apply simp 2736 apply (erule_tac x=p in allE) 2737 apply clarsimp 2738 apply clarsimp 2739 apply (erule_tac x=p in allE) 2740 apply simp 2741 apply (erule_tac x="mdbNext (cteMDBNode cte)" in allE) 2742 apply clarsimp 2743 done 2744 2745lemma valid_dlist_def3: 2746 "valid_dlist m = ((\<forall>c c'. m \<turnstile> c \<leadsto> c' \<longrightarrow> c' \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leftarrow> c') \<and> 2747 (\<forall>c c'. m \<turnstile> c \<leftarrow> c' \<longrightarrow> c \<noteq> 0 \<longrightarrow> m \<turnstile> c \<leadsto> c'))" 2748 apply (rule iffI) 2749 apply (simp add: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) 2750 apply fastforce 2751 apply (clarsimp simp add: valid_dlist_def Let_def mdb_next_unfold mdb_prev_def) 2752 apply fastforce 2753 done 2754 2755lemma vdlist_prevD: 2756 "\<lbrakk> m \<turnstile> c \<leftarrow> c'; m c = Some cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'" 2757 by (fastforce simp: valid_dlist_def3) 2758 2759lemma vdlist_nextD: 2760 "\<lbrakk> m \<turnstile> c \<leadsto> c'; m c' = Some cte; valid_dlist m; no_0 m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'" 2761 by (fastforce simp: valid_dlist_def3) 2762 2763lemma vdlist_prevD0: 2764 "\<lbrakk> m \<turnstile> c \<leftarrow> c'; c \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leadsto> c'" 2765 by (fastforce simp: valid_dlist_def3) 2766 2767lemma vdlist_nextD0: 2768 "\<lbrakk> m \<turnstile> c \<leadsto> c'; c' \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> m \<turnstile> c \<leftarrow> c'" 2769 by (fastforce simp: valid_dlist_def3) 2770 2771lemma vdlist_prev_src_unique: 2772 "\<lbrakk> m \<turnstile> p \<leftarrow> x; m \<turnstile> p \<leftarrow> y; p \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> x = y" 2773 by (drule (2) vdlist_prevD0)+ (clarsimp simp: mdb_next_unfold) 2774 2775lemma vdlist_next_src_unique: 2776 "\<lbrakk> m \<turnstile> x \<leadsto> p; m \<turnstile> y \<leadsto> p; p \<noteq> 0; valid_dlist m \<rbrakk> \<Longrightarrow> x = y" 2777 by (drule (2) vdlist_nextD0)+ (clarsimp simp: mdb_prev_def) 2778 2779lemma cte_at_cte_wp_atD: 2780 "cte_at' p s \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) p s" 2781 by (clarsimp simp add: cte_wp_at'_def) 2782 2783lemma cte_at_cte_wp_atE: 2784 "\<lbrakk> cte_at' p s; \<And>cte. cte_wp_at' ((=) cte) p s \<Longrightarrow> P \<rbrakk> \<Longrightarrow> P" 2785 by (blast dest: cte_at_cte_wp_atD) 2786 2787lemma valid_pspace_no_0 [elim]: 2788 "valid_pspace' s \<Longrightarrow> no_0 (ctes_of s)" 2789 by (auto simp: valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) 2790 2791lemma valid_pspace_dlist [elim]: 2792 "valid_pspace' s \<Longrightarrow> valid_dlist (ctes_of s)" 2793 by (auto simp: valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) 2794 2795lemma cte_wp_at_conj': 2796 "\<lbrakk> cte_wp_at' P p s; cte_wp_at' Q p s \<rbrakk> \<Longrightarrow> cte_wp_at' (P and Q) p s" 2797 by (fastforce simp add: cte_wp_at'_def) 2798 2799lemma next_rtrancl_tranclE [consumes 1, case_names eq trancl]: 2800 assumes major: "m \<turnstile> x \<leadsto>\<^sup>* y" 2801 and r1: "x = y \<Longrightarrow> P" 2802 and r2: "\<lbrakk> x \<noteq> y; m \<turnstile> x \<leadsto>\<^sup>+ y \<rbrakk> \<Longrightarrow> P" 2803 shows "P" 2804 using major 2805 by (auto dest: rtranclD intro: r1 r2) 2806 2807lemmas trancl_induct' [induct set] = trancl_induct [consumes 1, case_names base step] 2808 2809lemma next_single_value: 2810 "\<lbrakk> m \<turnstile> x \<leadsto> y; m \<turnstile> x \<leadsto> z \<rbrakk> \<Longrightarrow> y = z" 2811 unfolding mdb_next_rel_def by simp 2812 2813lemma loop_split: 2814 assumes loop: "m \<turnstile> c \<leadsto>\<^sup>+ c" 2815 and split: "m \<turnstile> c \<leadsto>\<^sup>+ c'" 2816 shows "m \<turnstile> c' \<leadsto>\<^sup>+ c" 2817 using split loop 2818proof induct 2819 case base 2820 thus ?case 2821 by (auto dest: next_single_value elim: tranclE2) 2822next 2823 case (step y z) 2824 hence "m \<turnstile> y \<leadsto>\<^sup>+ c" by simp 2825 hence "m \<turnstile> z \<leadsto>\<^sup>* c" using step.hyps 2826 by (auto dest: next_single_value elim: tranclE2 intro: trancl_into_rtrancl) 2827 2828 thus ?case using step.prems 2829 by (cases rule: next_rtrancl_tranclE, simp_all) 2830qed 2831 2832lemma no_0_lhs: 2833 "\<lbrakk> m \<turnstile> c \<leadsto> y; no_0 m \<rbrakk> \<Longrightarrow> c \<noteq> 0" 2834 unfolding no_0_def 2835 by (erule contrapos_pn, simp add: mdb_next_unfold) 2836 2837lemma no_0_lhs_trancl: 2838 "\<lbrakk> m \<turnstile> c \<leadsto>\<^sup>+ y; no_0 m \<rbrakk> \<Longrightarrow> c \<noteq> 0" 2839 by (erule tranclE2, (rule no_0_lhs, simp_all)+) 2840 2841lemma mdb_chain_0_no_loops: 2842 assumes asm: "mdb_chain_0 m" 2843 and no0: "no_0 m" 2844 shows "no_loops m" 2845proof - 2846 { 2847 fix c 2848 assume mc: "m \<turnstile> c \<leadsto>\<^sup>+ c" 2849 2850 with asm have "m \<turnstile> c \<leadsto>\<^sup>+ 0" 2851 unfolding mdb_chain_0_def 2852 apply - 2853 apply (erule bspec, erule tranclE2) 2854 apply (auto intro: domI simp: mdb_next_unfold) 2855 done 2856 2857 with mc have "m \<turnstile> 0 \<leadsto>\<^sup>+ c" by (rule loop_split) 2858 hence False using no0 2859 by (clarsimp dest!: no_0_lhs_trancl) 2860 } 2861 thus "no_loops m" unfolding no_loops_def by auto 2862qed 2863 2864lemma valid_mdb_ctesE [elim]: 2865 "\<lbrakk>valid_mdb_ctes m; 2866 \<lbrakk> valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; 2867 caps_contained' m; mdb_chunked m; untyped_mdb' m; 2868 untyped_inc' m; valid_nullcaps m; ut_revocable' m; 2869 class_links m; distinct_zombies m; irq_control m; 2870 reply_masters_rvk_fb m \<rbrakk> 2871 \<Longrightarrow> P\<rbrakk> \<Longrightarrow> P" 2872 unfolding valid_mdb_ctes_def by auto 2873 2874lemma valid_mdb_ctesI [intro]: 2875 "\<lbrakk>valid_dlist m; no_0 m; mdb_chain_0 m; valid_badges m; 2876 caps_contained' m; mdb_chunked m; untyped_mdb' m; 2877 untyped_inc' m; valid_nullcaps m; ut_revocable' m; 2878 class_links m; distinct_zombies m; irq_control m; 2879 reply_masters_rvk_fb m \<rbrakk> 2880 \<Longrightarrow> valid_mdb_ctes m" 2881 unfolding valid_mdb_ctes_def by auto 2882 2883lemma mdb_next_fold: 2884 "(m \<turnstile> p \<leadsto> c) = (mdb_next m p = Some c)" 2885 unfolding mdb_next_rel_def 2886 by simp 2887end 2888locale PSpace_update_eq = 2889 fixes f :: "kernel_state \<Rightarrow> kernel_state" 2890 assumes pspace: "ksPSpace (f s) = ksPSpace s" 2891begin 2892 2893lemma state_refs_of'_eq[iff]: 2894 "state_refs_of' (f s) = state_refs_of' s" 2895 by (rule state_refs_of'_pspaceI [OF _ pspace], rule refl) 2896 2897lemma valid_space_update [iff]: 2898 "valid_pspace' (f s) = valid_pspace' s" 2899 by (fastforce simp: valid_pspace' pspace) 2900 2901lemma obj_at_update [iff]: 2902 "obj_at' P p (f s) = obj_at' P p s" 2903 by (fastforce intro: obj_at'_pspaceI simp: pspace) 2904 2905lemma ko_wp_at_update [iff]: 2906 "ko_wp_at' P p (f s) = ko_wp_at' P p s" 2907 by (simp add: pspace ko_wp_at'_def ps_clear_def) 2908 2909lemma cte_wp_at_update [iff]: 2910 "cte_wp_at' P p (f s) = cte_wp_at' P p s" 2911 by (fastforce intro: cte_wp_at'_pspaceI simp: pspace) 2912 2913lemma ex_nonz_cap_to_eq'[iff]: 2914 "ex_nonz_cap_to' p (f s) = ex_nonz_cap_to' p s" 2915 by (simp add: ex_nonz_cap_to'_def) 2916 2917lemma iflive_update [iff]: 2918 "if_live_then_nonz_cap' (f s) = if_live_then_nonz_cap' s" 2919 by (simp add: if_live_then_nonz_cap'_def ex_nonz_cap_to'_def) 2920 2921lemma valid_objs_update [iff]: 2922 "valid_objs' (f s) = valid_objs' s" 2923 apply (simp add: valid_objs'_def pspace) 2924 apply (fastforce intro: valid_obj'_pspaceI simp: pspace) 2925 done 2926 2927lemma pspace_aligned_update [iff]: 2928 "pspace_aligned' (f s) = pspace_aligned' s" 2929 by (simp add: pspace pspace_aligned'_def) 2930 2931lemma pspace_distinct_update [iff]: 2932 "pspace_distinct' (f s) = pspace_distinct' s" 2933 by (simp add: pspace pspace_distinct'_def ps_clear_def) 2934 2935lemma pred_tcb_at_update [iff]: 2936 "pred_tcb_at' proj P p (f s) = pred_tcb_at' proj P p s" 2937 by (simp add: pred_tcb_at'_def) 2938 2939lemma valid_cap_update [iff]: 2940 "(f s) \<turnstile>' c = s \<turnstile>' c" 2941 by (auto intro: valid_cap'_pspaceI simp: pspace) 2942 2943lemma typ_at_update' [iff]: 2944 "typ_at' T p (f s) = typ_at' T p s" 2945 by (simp add: typ_at'_def) 2946 2947lemma valid_asid_table_update' [iff]: 2948 "valid_asid_table' t (f s) = valid_asid_table' t s" 2949 by (simp add: valid_asid_table'_def) 2950 2951lemma page_table_at_update' [iff]: 2952 "page_table_at' p (f s) = page_table_at' p s" 2953 by (simp add: page_table_at'_def) 2954 2955lemma page_directory_at_update' [iff]: 2956 "page_directory_at' p (f s) = page_directory_at' p s" 2957 by (simp add: page_directory_at'_def) 2958 2959lemma valid_global_pts_update' [iff]: 2960 "valid_global_pts' pts (f s) = valid_global_pts' pts s" 2961 by (simp add: valid_global_pts'_def) 2962 2963lemma no_0_obj'_update [iff]: 2964 "no_0_obj' (f s) = no_0_obj' s" 2965 by (simp add: no_0_obj'_def pspace) 2966 2967lemma valid_pde_mappings'_update [iff]: 2968 "valid_pde_mappings' (f s) = valid_pde_mappings' s" 2969 by (simp add: valid_pde_mappings'_def) 2970 2971lemma pointerInUserData_update[iff]: 2972 "pointerInUserData p (f s) = pointerInUserData p s" 2973 by (simp add: pointerInUserData_def) 2974 2975lemma pointerInDeviceData_update[iff]: 2976 "pointerInDeviceData p (f s) = pointerInDeviceData p s" 2977 by (simp add: pointerInDeviceData_def) 2978 2979lemma pspace_domain_valid_update [iff]: 2980 "pspace_domain_valid (f s) = pspace_domain_valid s" 2981 by (simp add: pspace_domain_valid_def pspace) 2982 2983end 2984 2985locale Arch_Idle_update_eq = 2986 fixes f :: "kernel_state \<Rightarrow> kernel_state" 2987 assumes arch: "ksArchState (f s) = ksArchState s" 2988 assumes idle: "ksIdleThread (f s) = ksIdleThread s" 2989 assumes int_nd: "intStateIRQNode (ksInterruptState (f s)) 2990 = intStateIRQNode (ksInterruptState s)" 2991 assumes maxObj: "gsMaxObjectSize (f s) = gsMaxObjectSize s" 2992begin 2993 2994lemma global_refs_update' [iff]: 2995 "global_refs' (f s) = global_refs' s" 2996 by (simp add: global_refs'_def arch idle int_nd) 2997 2998end 2999 3000locale P_Arch_Idle_update_eq = PSpace_update_eq + Arch_Idle_update_eq 3001begin 3002 3003lemma valid_global_refs_update' [iff]: 3004 "valid_global_refs' (f s) = valid_global_refs' s" 3005 by (simp add: valid_global_refs'_def pspace arch idle maxObj) 3006 3007lemma valid_arch_state_update' [iff]: 3008 "valid_arch_state' (f s) = valid_arch_state' s" 3009 by (simp add: valid_arch_state'_def arch) 3010 3011lemma valid_idle_update' [iff]: 3012 "valid_idle' (f s) = valid_idle' s" 3013 by (auto simp: pspace idle) 3014 3015lemma ifunsafe_update [iff]: 3016 "if_unsafe_then_cap' (f s) = if_unsafe_then_cap' s" 3017 by (simp add: if_unsafe_then_cap'_def ex_cte_cap_to'_def int_nd) 3018 3019end 3020 3021locale Int_update_eq = 3022 fixes f :: "kernel_state \<Rightarrow> kernel_state" 3023 assumes int: "ksInterruptState (f s) = ksInterruptState s" 3024begin 3025 3026lemma irqs_masked_update [iff]: 3027 "irqs_masked' (f s) = irqs_masked' s" 3028 by (simp add: irqs_masked'_def int) 3029 3030lemma irq_issued_update'[iff]: 3031 "irq_issued' irq (f s) = irq_issued' irq s" 3032 by (simp add: irq_issued'_def int) 3033 3034end 3035 3036locale P_Cur_update_eq = PSpace_update_eq + 3037 assumes curt: "ksCurThread (f s) = ksCurThread s" 3038 assumes curd: "ksCurDomain (f s) = ksCurDomain s" 3039begin 3040 3041lemma sch_act_wf[iff]: 3042 "sch_act_wf ks (f s) = sch_act_wf ks s" 3043apply (cases ks) 3044apply (simp_all add: ct_in_state'_def st_tcb_at'_def tcb_in_cur_domain'_def curt curd) 3045done 3046 3047end 3048 3049locale P_Int_update_eq = PSpace_update_eq + Int_update_eq 3050begin 3051 3052lemma valid_irq_handlers_update'[iff]: 3053 "valid_irq_handlers' (f s) = valid_irq_handlers' s" 3054 by (simp add: valid_irq_handlers'_def cteCaps_of_def pspace) 3055 3056end 3057 3058locale P_Int_Cur_update_eq = 3059 P_Int_update_eq + P_Cur_update_eq 3060 3061locale P_Arch_Idle_Int_update_eq = 3062 P_Arch_Idle_update_eq + P_Int_update_eq 3063 3064locale P_Arch_Idle_Int_Cur_update_eq = 3065 P_Arch_Idle_Int_update_eq + P_Cur_update_eq 3066 3067interpretation sa_update: 3068 P_Arch_Idle_Int_Cur_update_eq "ksSchedulerAction_update f" 3069 by unfold_locales auto 3070 3071interpretation ready_queue_update: 3072 P_Arch_Idle_Int_Cur_update_eq "ksReadyQueues_update f" 3073 by unfold_locales auto 3074 3075interpretation ready_queue_bitmap1_update: 3076 P_Arch_Idle_Int_Cur_update_eq "ksReadyQueuesL1Bitmap_update f" 3077 by unfold_locales auto 3078 3079interpretation ready_queue_bitmap2_update: 3080 P_Arch_Idle_Int_Cur_update_eq "ksReadyQueuesL2Bitmap_update f" 3081 by unfold_locales auto 3082 3083interpretation cur_thread_update': 3084 P_Arch_Idle_Int_update_eq "ksCurThread_update f" 3085 by unfold_locales auto 3086 3087interpretation machine_state_update': 3088 P_Arch_Idle_Int_Cur_update_eq "ksMachineState_update f" 3089 by unfold_locales auto 3090 3091interpretation interrupt_state_update': 3092 P_Cur_update_eq "ksInterruptState_update f" 3093 by unfold_locales auto 3094 3095interpretation idle_update': 3096 P_Int_Cur_update_eq "ksIdleThread_update f" 3097 by unfold_locales auto 3098 3099interpretation arch_state_update': 3100 P_Int_Cur_update_eq "ksArchState_update f" 3101 by unfold_locales auto 3102 3103interpretation wu_update': 3104 P_Arch_Idle_Int_Cur_update_eq "ksWorkUnitsCompleted_update f" 3105 by unfold_locales auto 3106 3107interpretation gsCNodes_update: P_Arch_Idle_update_eq "gsCNodes_update f" 3108 by unfold_locales simp_all 3109 3110interpretation gsUserPages_update: P_Arch_Idle_update_eq "gsUserPages_update f" 3111 by unfold_locales simp_all 3112lemma ko_wp_at_aligned: 3113 "ko_wp_at' ((=) ko) p s \<Longrightarrow> is_aligned p (objBitsKO ko)" 3114 by (simp add: ko_wp_at'_def) 3115 3116interpretation ksCurDomain: 3117 P_Arch_Idle_Int_update_eq "ksCurDomain_update f" 3118 by unfold_locales auto 3119 3120interpretation ksDomScheduleIdx: 3121 P_Arch_Idle_Int_Cur_update_eq "ksDomScheduleIdx_update f" 3122 by unfold_locales auto 3123 3124interpretation ksDomSchedule: 3125 P_Arch_Idle_Int_Cur_update_eq "ksDomSchedule_update f" 3126 by unfold_locales auto 3127 3128interpretation ksDomainTime: 3129 P_Arch_Idle_Int_Cur_update_eq "ksDomainTime_update f" 3130 by unfold_locales auto 3131 3132interpretation gsUntypedZeroRanges: 3133 P_Arch_Idle_Int_Cur_update_eq "gsUntypedZeroRanges_update f" 3134 by unfold_locales auto 3135 3136lemma ko_wp_at_norm: 3137 "ko_wp_at' P p s \<Longrightarrow> \<exists>ko. P ko \<and> ko_wp_at' ((=) ko) p s" 3138 by (auto simp add: ko_wp_at'_def) 3139 3140lemma valid_mdb'_queues [iff]: 3141 "valid_mdb' (ksReadyQueues_update f s) = valid_mdb' s" 3142 by (simp add: valid_mdb'_def) 3143 3144lemma valid_mdb_machine_state [iff]: 3145 "valid_mdb' (ksMachineState_update f s) = valid_mdb' s" 3146 by (simp add: valid_mdb'_def) 3147 3148lemma cte_wp_at_norm': 3149 "cte_wp_at' P p s \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) p s \<and> P cte" 3150 by (simp add: cte_wp_at'_def) 3151 3152lemma pred_tcb_at'_disj: 3153 "(pred_tcb_at' proj P t s \<or> pred_tcb_at' proj Q t s) = pred_tcb_at' proj (\<lambda>a. P a \<or> Q a) t s" 3154 by (fastforce simp add: pred_tcb_at'_def obj_at'_def) 3155 3156lemma pred_tcb_at' [elim!]: 3157 "pred_tcb_at' proj P t s \<Longrightarrow> tcb_at' t s" 3158 by (auto simp add: pred_tcb_at'_def obj_at'_def) 3159 3160lemma valid_pspace_mdb' [elim!]: 3161 "valid_pspace' s \<Longrightarrow> valid_mdb' s" 3162 by (simp add: valid_pspace'_def) 3163 3164lemmas hoare_use_eq_irq_node' = hoare_use_eq[where f=irq_node'] 3165 3166lemma ex_cte_cap_to'_pres: 3167 "\<lbrakk> \<And>P p. \<lbrace>cte_wp_at' P p\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; 3168 \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> \<rbrakk> 3169 \<Longrightarrow> \<lbrace>ex_cte_cap_wp_to' P p\<rbrace> f \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace>" 3170 apply (simp add: ex_cte_cap_wp_to'_def) 3171 apply (rule hoare_pre) 3172 apply (erule hoare_use_eq_irq_node') 3173 apply (rule hoare_vcg_ex_lift) 3174 apply assumption 3175 apply simp 3176 done 3177context begin interpretation Arch . (*FIXME: arch_split*) 3178lemma page_directory_pde_atI': 3179 "\<lbrakk> page_directory_at' p s; x < 2 ^ pageBits \<rbrakk> \<Longrightarrow> pde_at' (p + (x << 2)) s" 3180 by (simp add: page_directory_at'_def pageBits_def) 3181 3182lemma page_table_pte_atI': 3183 "\<lbrakk> page_table_at' p s; x < 2^(ptBits - 2) \<rbrakk> \<Longrightarrow> pte_at' (p + (x << 2)) s" 3184 by (simp add: page_table_at'_def pageBits_def ptBits_def pteBits_def) 3185 3186lemma valid_global_refsD': 3187 "\<lbrakk> ctes_of s p = Some cte; valid_global_refs' s \<rbrakk> \<Longrightarrow> 3188 kernel_data_refs \<inter> capRange (cteCap cte) = {} \<and> global_refs' s \<subseteq> kernel_data_refs" 3189 by (clarsimp simp: valid_global_refs'_def valid_refs'_def ran_def) blast 3190 3191lemma no_0_prev: 3192 "no_0 m \<Longrightarrow> \<not> m \<turnstile> p \<leftarrow> 0" 3193 by (simp add: mdb_prev_def) 3194 3195lemma ut_revocableD': 3196 "\<lbrakk>m p = Some (CTE cap n); isUntypedCap cap; ut_revocable' m \<rbrakk> \<Longrightarrow> mdbRevocable n" 3197 unfolding ut_revocable'_def by blast 3198 3199lemma nullcapsD': 3200 "\<lbrakk>m p = Some (CTE NullCap n); valid_nullcaps m \<rbrakk> \<Longrightarrow> n = nullMDBNode" 3201 unfolding valid_nullcaps_def by blast 3202 3203lemma untyped_mdbD': 3204 "\<lbrakk>m p = Some (CTE c n); isUntypedCap c; 3205 m p' = Some (CTE c' n'); \<not>isUntypedCap c'; 3206 capRange c' \<inter> untypedRange c \<noteq> {}; untyped_mdb' m \<rbrakk> \<Longrightarrow> 3207 p' \<in> descendants_of' p m" 3208 unfolding untyped_mdb'_def by blast 3209 3210lemma untyped_incD': 3211 "\<lbrakk> m p = Some (CTE c n); isUntypedCap c; 3212 m p' = Some (CTE c' n'); isUntypedCap c'; untyped_inc' m \<rbrakk> \<Longrightarrow> 3213 (untypedRange c \<subseteq> untypedRange c' \<or> untypedRange c' \<subseteq> untypedRange c \<or> untypedRange c \<inter> untypedRange c' = {}) \<and> 3214 (untypedRange c \<subset> untypedRange c' \<longrightarrow> (p \<in> descendants_of' p' m \<and> untypedRange c \<inter> usableUntypedRange c' = {})) \<and> 3215 (untypedRange c' \<subset> untypedRange c \<longrightarrow> (p' \<in> descendants_of' p m \<and> untypedRange c' \<inter> usableUntypedRange c = {})) \<and> 3216 (untypedRange c = untypedRange c' \<longrightarrow> (p' \<in> descendants_of' p m \<and> usableUntypedRange c = {} 3217 \<or> p \<in> descendants_of' p' m \<and> usableUntypedRange c' = {} \<or> p = p'))" 3218 unfolding untyped_inc'_def 3219 apply (drule_tac x = p in spec) 3220 apply (drule_tac x = p' in spec) 3221 apply (elim allE impE) 3222 apply simp+ 3223 done 3224 3225lemma caps_containedD': 3226 "\<lbrakk> m p = Some (CTE c n); m p' = Some (CTE c' n'); 3227 \<not> isUntypedCap c'; capRange c' \<inter> untypedRange c \<noteq> {}; 3228 caps_contained' m\<rbrakk> 3229 \<Longrightarrow> capRange c' \<subseteq> untypedRange c" 3230 unfolding caps_contained'_def by blast 3231 3232lemma class_linksD: 3233 "\<lbrakk> m p = Some cte; m p' = Some cte'; m \<turnstile> p \<leadsto> p'; class_links m \<rbrakk> \<Longrightarrow> 3234 capClass (cteCap cte) = capClass (cteCap cte')" 3235 using class_links_def by blast 3236 3237lemma mdb_chunkedD: 3238 "\<lbrakk> m p = Some (CTE cap n); m p' = Some (CTE cap' n'); 3239 sameRegionAs cap cap'; p \<noteq> p'; mdb_chunked m \<rbrakk> 3240 \<Longrightarrow> (m \<turnstile> p \<leadsto>\<^sup>+ p' \<or> m \<turnstile> p' \<leadsto>\<^sup>+ p) \<and> 3241 (m \<turnstile> p \<leadsto>\<^sup>+ p' \<longrightarrow> is_chunk m cap p p') \<and> 3242 (m \<turnstile> p' \<leadsto>\<^sup>+ p \<longrightarrow> is_chunk m cap' p' p)" 3243 using mdb_chunked_def by blast 3244 3245lemma irq_controlD: 3246 "\<lbrakk> m p = Some (CTE IRQControlCap n); m p' = Some (CTE IRQControlCap n'); 3247 irq_control m \<rbrakk> \<Longrightarrow> p' = p" 3248 unfolding irq_control_def by blast 3249 3250lemma irq_revocable: 3251 "\<lbrakk> m p = Some (CTE IRQControlCap n); irq_control m \<rbrakk> \<Longrightarrow> mdbRevocable n" 3252 unfolding irq_control_def by blast 3253 3254lemma sch_act_wf_arch [simp]: 3255 "sch_act_wf sa (ksArchState_update f s) = sch_act_wf sa s" 3256 by (cases sa) (simp_all add: ct_in_state'_def tcb_in_cur_domain'_def) 3257 3258lemma valid_queues_arch [simp]: 3259 "valid_queues (ksArchState_update f s) = valid_queues s" 3260 by (simp add: valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 3261 3262lemma if_unsafe_then_cap_arch' [simp]: 3263 "if_unsafe_then_cap' (ksArchState_update f s) = if_unsafe_then_cap' s" 3264 by (simp add: if_unsafe_then_cap'_def ex_cte_cap_to'_def) 3265 3266lemma valid_idle_arch' [simp]: 3267 "valid_idle' (ksArchState_update f s) = valid_idle' s" 3268 by (simp add: valid_idle'_def) 3269 3270lemma valid_irq_node_arch' [simp]: 3271 "valid_irq_node' w (ksArchState_update f s) = valid_irq_node' w s" 3272 by (simp add: valid_irq_node'_def) 3273 3274lemma sch_act_wf_machine_state [simp]: 3275 "sch_act_wf sa (ksMachineState_update f s) = sch_act_wf sa s" 3276 by (cases sa) (simp_all add: ct_in_state'_def tcb_in_cur_domain'_def) 3277 3278lemma valid_queues_machine_state [simp]: 3279 "valid_queues (ksMachineState_update f s) = valid_queues s" 3280 by (simp add: valid_queues_def valid_queues_no_bitmap_def bitmapQ_defs) 3281 3282lemma valid_queues_arch' [simp]: 3283 "valid_queues' (ksArchState_update f s) = valid_queues' s" 3284 by (simp add: valid_queues'_def) 3285 3286lemma valid_queues_machine_state' [simp]: 3287 "valid_queues' (ksMachineState_update f s) = valid_queues' s" 3288 by (simp add: valid_queues'_def) 3289 3290lemma valid_irq_node'_machine_state [simp]: 3291 "valid_irq_node' x (ksMachineState_update f s) = valid_irq_node' x s" 3292 by (simp add: valid_irq_node'_def) 3293 3294(* these should be reasonable safe for automation because of the 0 pattern *) 3295lemma no_0_ko_wp' [elim!]: 3296 "\<lbrakk> ko_wp_at' Q 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" 3297 by (simp add: ko_wp_at'_def no_0_obj'_def) 3298 3299lemma no_0_obj_at' [elim!]: 3300 "\<lbrakk> obj_at' Q 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" 3301 by (simp add: obj_at'_def no_0_obj'_def) 3302 3303lemma no_0_typ_at' [elim!]: 3304 "\<lbrakk> typ_at' T 0 s; no_0_obj' s \<rbrakk> \<Longrightarrow> P" 3305 by (clarsimp simp: typ_at'_def) 3306 3307lemma no_0_ko_wp'_eq [simp]: 3308 "no_0_obj' s \<Longrightarrow> ko_wp_at' P 0 s = False" 3309 by (simp add: ko_wp_at'_def no_0_obj'_def) 3310 3311lemma no_0_obj_at'_eq [simp]: 3312 "no_0_obj' s \<Longrightarrow> obj_at' P 0 s = False" 3313 by (simp add: obj_at'_def no_0_obj'_def) 3314 3315lemma no_0_typ_at'_eq [simp]: 3316 "no_0_obj' s \<Longrightarrow> typ_at' P 0 s = False" 3317 by (simp add: typ_at'_def) 3318 3319lemma valid_pspace_valid_objs'[elim!]: 3320 "valid_pspace' s \<Longrightarrow> valid_objs' s" 3321 by (simp add: valid_pspace'_def) 3322 3323declare badgeBits_def [simp] 3324 3325lemma ex_cte_cap_to'_pres_asm: 3326 "\<lbrakk> \<And>P p. \<lbrace>cte_wp_at' P p and Q\<rbrace> f \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>; 3327 \<And>P. \<lbrace>\<lambda>s. P (irq_node' s)\<rbrace> f \<lbrace>\<lambda>rv s. P (irq_node' s)\<rbrace> \<rbrakk> 3328 \<Longrightarrow> \<lbrace>ex_cte_cap_wp_to' P p and Q\<rbrace> f \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P p\<rbrace>" 3329 apply (simp add: ex_cte_cap_to'_def pred_conj_def) 3330 apply (rule hoare_pre, erule hoare_use_eq_irq_node') 3331 apply (rule hoare_vcg_ex_lift, assumption) 3332 apply simp 3333 done 3334 3335lemma simple_sane_strg: 3336 "sch_act_simple s \<longrightarrow> sch_act_sane s" 3337 by (simp add: sch_act_sane_def sch_act_simple_def) 3338 3339lemma sch_act_wf_cases: 3340 "sch_act_wf action = (case action of 3341 ResumeCurrentThread \<Rightarrow> ct_in_state' activatable' 3342 | ChooseNewThread \<Rightarrow> \<top> 3343 | SwitchToThread t \<Rightarrow> \<lambda>s. st_tcb_at' runnable' t s \<and> tcb_in_cur_domain' t s)" 3344by (cases action) auto 3345end 3346 3347lemma (in PSpace_update_eq) cteCaps_of_update[iff]: "cteCaps_of (f s) = cteCaps_of s" 3348 by (simp add: cteCaps_of_def pspace) 3349 3350lemma vms_sch_act_update'[iff]: 3351 "valid_machine_state' (ksSchedulerAction_update f s) = 3352 valid_machine_state' s" 3353 by (simp add: valid_machine_state'_def ) 3354context begin interpretation Arch . (*FIXME: arch_split*) 3355lemma objBitsT_simps: 3356 "objBitsT EndpointT = epSizeBits" 3357 "objBitsT NotificationT = ntfnSizeBits" 3358 "objBitsT CTET = cteSizeBits" 3359 "objBitsT TCBT = tcbBlockSizeBits" 3360 "objBitsT UserDataT = pageBits" 3361 "objBitsT UserDataDeviceT = pageBits" 3362 "objBitsT KernelDataT = pageBits" 3363 "objBitsT (ArchT PDET) = 2" 3364 "objBitsT (ArchT PTET) = 2" 3365 "objBitsT (ArchT ASIDPoolT) = pageBits" 3366 unfolding objBitsT_def makeObjectT_def 3367 by (simp_all add: makeObject_simps objBits_simps archObjSize_def pteBits_def pdeBits_def) 3368 3369lemma objBitsT_koTypeOf : 3370 "(objBitsT (koTypeOf ko)) = objBitsKO ko" 3371 apply (cases ko; simp add: objBits_simps objBitsT_simps) 3372 apply (rename_tac arch_kernel_object) 3373 apply (case_tac arch_kernel_object; simp add: archObjSize_def objBitsT_simps 3374 pteBits_def pdeBits_def) 3375 done 3376 3377lemma sane_update [intro!]: 3378 "sch_act_sane (s\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>)" 3379 by (simp add: sch_act_sane_def) 3380 3381lemma typ_at_aligned': 3382 "\<lbrakk> typ_at' tp p s \<rbrakk> \<Longrightarrow> is_aligned p (objBitsT tp)" 3383 by (clarsimp simp add: typ_at'_def ko_wp_at'_def objBitsT_koTypeOf) 3384 3385lemma valid_queues_obj_at'D: 3386 "\<lbrakk> t \<in> set (ksReadyQueues s (d, p)); valid_queues s \<rbrakk> 3387 \<Longrightarrow> obj_at' (inQ d p) t s" 3388 apply (unfold valid_queues_def valid_queues_no_bitmap_def) 3389 apply (elim conjE) 3390 apply (drule_tac x=d in spec) 3391 apply (drule_tac x=p in spec) 3392 apply (clarsimp) 3393 apply (drule(1) bspec) 3394 apply (erule obj_at'_weakenE) 3395 apply (clarsimp) 3396 done 3397 3398lemma obj_at'_and: 3399 "obj_at' (P and P') t s = (obj_at' P t s \<and> obj_at' P' t s)" 3400 by (rule iffI, (clarsimp simp: obj_at'_def)+) 3401 3402lemma obj_at'_activatable_st_tcb_at': 3403 "obj_at' (activatable' \<circ> tcbState) t = st_tcb_at' activatable' t" 3404 by (rule ext, clarsimp simp: st_tcb_at'_def) 3405 3406lemma st_tcb_at'_runnable_is_activatable: 3407 "st_tcb_at' runnable' t s \<Longrightarrow> st_tcb_at' activatable' t s" 3408 by (simp add: st_tcb_at'_def) 3409 (fastforce elim: obj_at'_weakenE) 3410 3411lemma tcb_at'_has_tcbPriority: 3412 "tcb_at' t s \<Longrightarrow> \<exists>p. obj_at' (\<lambda>tcb. tcbPriority tcb = p) t s" 3413 by (clarsimp simp add: obj_at'_def) 3414 3415lemma pred_tcb_at'_Not: 3416 "pred_tcb_at' f (Not o P) t s = (tcb_at' t s \<and> \<not> pred_tcb_at' f P t s)" 3417 by (auto simp: pred_tcb_at'_def obj_at'_def) 3418 3419lemma obj_at'_conj_distrib: 3420 "obj_at' (\<lambda>ko. P ko \<and> Q ko) p s \<Longrightarrow> obj_at' P p s \<and> obj_at' Q p s" 3421 by (auto simp: obj_at'_def) 3422 3423lemma not_obj_at'_strengthen: 3424 "obj_at' (Not \<circ> P) p s \<Longrightarrow> \<not> obj_at' P p s" 3425 by (clarsimp simp: obj_at'_def) 3426 3427lemma not_pred_tcb_at'_strengthen: 3428 "pred_tcb_at' f (Not \<circ> P) p s \<Longrightarrow> \<not> pred_tcb_at' f P p s" 3429 by (clarsimp simp: pred_tcb_at'_def obj_at'_def) 3430 3431lemma obj_at'_ko_at'_prop: 3432 "ko_at' ko t s \<Longrightarrow> obj_at' P t s = P ko" 3433 by (drule obj_at_ko_at', clarsimp simp: obj_at'_def) 3434 3435lemma idle_tcb_at'_split: 3436 "idle_tcb_at' (\<lambda>p. P (fst p) \<and> Q (snd p)) t s \<Longrightarrow> st_tcb_at' P t s \<and> bound_tcb_at' Q t s" 3437 by (clarsimp simp: pred_tcb_at'_def dest!: obj_at'_conj_distrib) 3438 3439lemma valid_queues_no_bitmap_def': 3440 "valid_queues_no_bitmap = 3441 (\<lambda>s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). 3442 obj_at' (inQ d p) t s \<and> st_tcb_at' runnable' t s) \<and> 3443 distinct (ksReadyQueues s (d, p)) \<and> (d > maxDomain \<or> p > maxPriority \<longrightarrow> ksReadyQueues s (d,p) = []))" 3444 apply (rule ext, rule iffI) 3445 apply (clarsimp simp: valid_queues_def valid_queues_no_bitmap_def obj_at'_and pred_tcb_at'_def o_def 3446 elim!: obj_at'_weakenE)+ 3447 done 3448 3449lemma valid_queues_running: 3450 assumes Q: "t \<in> set(ksReadyQueues s (d, p))" "valid_queues s" 3451 shows "st_tcb_at' runnable' t s" 3452 using assms by (clarsimp simp add: valid_queues_def valid_queues_no_bitmap_def') 3453 3454lemma valid_refs'_cteCaps: 3455 "valid_refs' S (ctes_of s) = (\<forall>c \<in> ran (cteCaps_of s). S \<inter> capRange c = {})" 3456 by (fastforce simp: valid_refs'_def cteCaps_of_def elim!: ranE) 3457 3458lemma valid_cap_sizes_cteCaps: 3459 "valid_cap_sizes' n (ctes_of s) = (\<forall>c \<in> ran (cteCaps_of s). 2 ^ capBits c \<le> n)" 3460 apply (simp add: valid_cap_sizes'_def cteCaps_of_def) 3461 apply (fastforce elim!: ranE) 3462 done 3463 3464lemma cte_at_valid_cap_sizes_0: 3465 "valid_cap_sizes' n ctes \<Longrightarrow> ctes p = Some cte \<Longrightarrow> 0 < n" 3466 apply (clarsimp simp: valid_cap_sizes'_def) 3467 apply (drule bspec, erule ranI) 3468 apply (rule Suc_le_lessD, erule order_trans[rotated]) 3469 apply simp 3470 done 3471 3472lemma invs_valid_stateI' [elim!]: 3473 "invs' s \<Longrightarrow> valid_state' s" 3474 by (simp add: invs'_def) 3475 3476lemma tcb_at_invs' [elim!]: 3477 "invs' s \<Longrightarrow> tcb_at' (ksCurThread s) s" 3478 by (simp add: invs'_def cur_tcb'_def) 3479 3480lemma invs_valid_objs' [elim!]: 3481 "invs' s \<Longrightarrow> valid_objs' s" 3482 by (simp add: invs'_def valid_state'_def valid_pspace'_def) 3483 3484lemma invs_pspace_aligned' [elim!]: 3485 "invs' s \<Longrightarrow> pspace_aligned' s" 3486 by (simp add: invs'_def valid_state'_def valid_pspace'_def) 3487 3488lemma invs_pspace_distinct' [elim!]: 3489 "invs' s \<Longrightarrow> pspace_distinct' s" 3490 by (simp add: invs'_def valid_state'_def valid_pspace'_def) 3491 3492lemma invs_valid_pspace' [elim!]: 3493 "invs' s \<Longrightarrow> valid_pspace' s" 3494 by (simp add: invs'_def valid_state'_def) 3495 3496lemma invs_arch_state' [elim!]: 3497 "invs' s \<Longrightarrow> valid_arch_state' s" 3498 by (simp add: invs'_def valid_state'_def) 3499 3500lemma invs_cur' [elim!]: 3501 "invs' s \<Longrightarrow> cur_tcb' s" 3502 by (simp add: invs'_def) 3503 3504lemma invs_mdb' [elim!]: 3505 "invs' s \<Longrightarrow> valid_mdb' s" 3506 by (simp add: invs'_def valid_state'_def valid_pspace'_def) 3507 3508lemma valid_mdb_no_loops [elim!]: 3509 "valid_mdb_ctes m \<Longrightarrow> no_loops m" 3510 by (auto intro: mdb_chain_0_no_loops) 3511 3512lemma invs_no_loops [elim!]: 3513 "invs' s \<Longrightarrow> no_loops (ctes_of s)" 3514 apply (rule valid_mdb_no_loops) 3515 apply (simp add: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def) 3516 done 3517 3518lemma invs_iflive'[elim!]: 3519 "invs' s \<Longrightarrow> if_live_then_nonz_cap' s" 3520 by (simp add: invs'_def valid_state'_def) 3521 3522lemma invs_unsafe_then_cap' [elim!]: 3523 "invs' s \<Longrightarrow> if_unsafe_then_cap' s" 3524 by (simp add: invs'_def valid_state'_def) 3525 3526lemma invs_sym' [elim!]: 3527 "invs' s \<Longrightarrow> sym_refs (state_refs_of' s)" 3528 by (simp add: invs'_def valid_state'_def) 3529 3530lemma invs_sch_act_wf' [elim!]: 3531 "invs' s \<Longrightarrow> sch_act_wf (ksSchedulerAction s) s" 3532 by (simp add: invs'_def valid_state'_def) 3533 3534lemma invs_queues [elim!]: 3535 "invs' s \<Longrightarrow> valid_queues s" 3536 by (simp add: invs'_def valid_state'_def) 3537 3538lemma invs_valid_idle'[elim!]: 3539 "invs' s \<Longrightarrow> valid_idle' s" 3540 by (fastforce simp: invs'_def valid_state'_def) 3541 3542lemma invs_valid_global'[elim!]: 3543 "invs' s \<Longrightarrow> valid_global_refs' s" 3544 by (fastforce simp: invs'_def valid_state'_def) 3545 3546lemma invs_invs_no_cicd': 3547 "invs' s \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s" 3548 by (simp add: invs'_to_invs_no_cicd'_def) 3549 3550lemma valid_queues_valid_bitmapQ: 3551 "valid_queues s \<Longrightarrow> valid_bitmapQ s" 3552 by (simp add: valid_queues_def) 3553 3554lemma valid_queues_valid_queues_no_bitmap: 3555 "valid_queues s \<Longrightarrow> valid_queues_no_bitmap s" 3556 by (simp add: valid_queues_def) 3557 3558lemma valid_queues_bitmapQ_no_L1_orphans: 3559 "valid_queues s \<Longrightarrow> bitmapQ_no_L1_orphans s" 3560 by (simp add: valid_queues_def) 3561 3562lemma invs'_bitmapQ_no_L1_orphans: 3563 "invs' s \<Longrightarrow> bitmapQ_no_L1_orphans s" 3564 by (drule invs_queues, simp add: valid_queues_def) 3565 3566lemma invs_ksCurDomain_maxDomain' [elim!]: 3567 "invs' s \<Longrightarrow> ksCurDomain s \<le> maxDomain" 3568 by (simp add: invs'_def valid_state'_def) 3569 3570lemma ksCurThread_active_not_idle': 3571 "\<lbrakk> ct_active' s ; valid_idle' s \<rbrakk> \<Longrightarrow> ksCurThread s \<noteq> ksIdleThread s" 3572 apply clarsimp 3573 apply (clarsimp simp: ct_in_state'_def valid_idle'_def) 3574 apply (drule idle_tcb_at'_split) 3575 apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) 3576 done 3577 3578lemma simple_st_tcb_at_state_refs_ofD': 3579 "st_tcb_at' simple' t s \<Longrightarrow> bound_tcb_at' (\<lambda>x. tcb_bound_refs' x = state_refs_of' s t) t s" 3580 by (fastforce simp: pred_tcb_at'_def obj_at'_def state_refs_of'_def 3581 projectKO_eq project_inject) 3582 3583lemma cur_tcb_arch' [iff]: 3584 "cur_tcb' (ksArchState_update f s) = cur_tcb' s" 3585 by (simp add: cur_tcb'_def) 3586 3587lemma cur_tcb'_machine_state [simp]: 3588 "cur_tcb' (ksMachineState_update f s) = cur_tcb' s" 3589 by (simp add: cur_tcb'_def) 3590 3591lemma invs_no_0_obj'[elim!]: 3592 "invs' s \<Longrightarrow> no_0_obj' s" 3593 by (simp add: invs'_def valid_state'_def valid_pspace'_def) 3594 3595lemma invs'_ksSchedulerAction: 3596 "\<lbrakk> invs' s; sch_act_wf sa s; sa \<noteq> ResumeCurrentThread \<rbrakk> \<Longrightarrow> 3597 invs' (s \<lparr>ksSchedulerAction := sa\<rparr>)" 3598 by (clarsimp simp add: invs'_def valid_state'_def valid_queues_def valid_queues_no_bitmap_def 3599 bitmapQ_defs valid_irq_node'_def valid_queues'_def cur_tcb'_def 3600 ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def ct_not_inQ_def) 3601 3602lemma invs'_gsCNodes_update[simp]: 3603 "invs' (gsCNodes_update f s') = invs' s'" 3604 apply (clarsimp simp: invs'_def valid_state'_def valid_queues_def valid_queues_no_bitmap_def 3605 bitmapQ_defs 3606 valid_queues'_def valid_irq_node'_def valid_irq_handlers'_def 3607 irq_issued'_def irqs_masked'_def valid_machine_state'_def 3608 cur_tcb'_def) 3609 apply (cases "ksSchedulerAction s'") 3610 apply (simp_all add: ct_in_state'_def tcb_in_cur_domain'_def ct_idle_or_in_cur_domain'_def ct_not_inQ_def) 3611 done 3612 3613lemma invs'_gsUserPages_update[simp]: 3614 "invs' (gsUserPages_update f s') = invs' s'" 3615 apply (clarsimp simp: invs'_def valid_state'_def valid_queues_def valid_queues_no_bitmap_def 3616 bitmapQ_defs 3617 valid_queues'_def valid_irq_node'_def valid_irq_handlers'_def 3618 irq_issued'_def irqs_masked'_def valid_machine_state'_def 3619 cur_tcb'_def) 3620 apply (cases "ksSchedulerAction s'") 3621 apply (simp_all add: ct_in_state'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def ct_not_inQ_def) 3622 done 3623 3624lemma invs_queues_tcb_in_cur_domain': 3625 "\<lbrakk> ksReadyQueues s (d, p) = x # xs; invs' s; d = ksCurDomain s\<rbrakk> 3626 \<Longrightarrow> tcb_in_cur_domain' x s" 3627apply (subgoal_tac "x \<in> set (ksReadyQueues s (d, p))") 3628 apply (drule (1) valid_queues_obj_at'D[OF _ invs_queues]) 3629 apply (auto simp: inQ_def tcb_in_cur_domain'_def elim: obj_at'_weakenE) 3630done 3631 3632lemma invs_no_cicd_queues_tcb_in_cur_domain': 3633 "\<lbrakk> ksReadyQueues s (d, p) = x # xs; all_invs_but_ct_idle_or_in_cur_domain' s; d = ksCurDomain s\<rbrakk> 3634 \<Longrightarrow> tcb_in_cur_domain' x s" 3635apply (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def tcb_in_cur_domain'_def) 3636apply (elim conjE) 3637apply (subgoal_tac "x \<in> set (ksReadyQueues s (d, p))") 3638 apply (drule (1) valid_queues_obj_at'D) 3639 apply (auto simp: inQ_def elim: obj_at'_weakenE) 3640done 3641 3642lemma pred_tcb'_neq_contra: 3643 "\<lbrakk> pred_tcb_at' proj P p s; pred_tcb_at' proj Q p s; \<And>st. P st \<noteq> Q st \<rbrakk> \<Longrightarrow> False" 3644 by (clarsimp simp: pred_tcb_at'_def obj_at'_def) 3645 3646lemma invs'_ksDomSchedule: 3647 "invs' s \<Longrightarrow> KernelStateData_H.ksDomSchedule s = KernelStateData_H.ksDomSchedule (newKernelState undefined)" 3648unfolding invs'_def valid_state'_def by clarsimp 3649 3650lemma invs'_ksDomScheduleIdx: 3651 "invs' s \<Longrightarrow> KernelStateData_H.ksDomScheduleIdx s < length (KernelStateData_H.ksDomSchedule (newKernelState undefined))" 3652unfolding invs'_def valid_state'_def by clarsimp 3653 3654lemma valid_bitmap_valid_bitmapQ_exceptE: 3655 "\<lbrakk> valid_bitmapQ_except d p s ; (bitmapQ d p s \<longleftrightarrow> ksReadyQueues s (d,p) \<noteq> []) ; 3656 bitmapQ_no_L2_orphans s \<rbrakk> 3657 \<Longrightarrow> valid_bitmapQ s" 3658 unfolding valid_bitmapQ_def valid_bitmapQ_except_def 3659 by force 3660 3661lemma valid_bitmap_valid_bitmapQ_exceptI[intro]: 3662 "valid_bitmapQ s \<Longrightarrow> valid_bitmapQ_except d p s" 3663 unfolding valid_bitmapQ_except_def valid_bitmapQ_def 3664 by simp 3665 3666lemma mask_wordRadix_less_wordBits: 3667 assumes sz: "wordRadix \<le> size w" 3668 shows "unat ((w::'a::len word) && mask wordRadix) < wordBits" 3669proof - 3670 note pow_num = semiring_numeral_class.power_numeral 3671 3672 { assume "wordRadix = size w" 3673 hence ?thesis 3674 by (fastforce intro!: unat_lt2p[THEN order_less_le_trans] 3675 simp: wordRadix_def wordBits_def' word_size) 3676 } moreover { 3677 assume "wordRadix < size w" 3678 hence ?thesis unfolding wordRadix_def wordBits_def' mask_def 3679 apply simp 3680 apply (subst unat_less_helper, simp_all) 3681 apply (rule word_and_le1[THEN order_le_less_trans]) 3682 apply (simp add: word_size bintrunc_mod2p) 3683 apply (subst int_mod_eq', simp_all) 3684 apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp) 3685 apply (simp del: pow_num) 3686 apply (subst int_mod_eq', simp_all) 3687 apply (rule order_le_less_trans[where y="2^wordRadix", simplified wordRadix_def], simp) 3688 apply (simp del: pow_num) 3689 done 3690 } 3691 ultimately show ?thesis using sz by fastforce 3692qed 3693 3694lemma priority_mask_wordRadix_size: 3695 "unat ((w::priority) && mask wordRadix) < wordBits" 3696 by (rule mask_wordRadix_less_wordBits, simp add: wordRadix_def word_size) 3697 3698end 3699(* The normalise_obj_at' tactic was designed to simplify situations similar to: 3700 ko_at' ko p s \<Longrightarrow> 3701 obj_at' (complicated_P (obj_at' (complicated_Q (obj_at' ...)) p s)) p s 3702 3703 It seems to also offer assistance in cases where there is lots of st_tcb_at', ko_at', obj_at' 3704 confusion. If your goal looks like that kind of mess, try it out. It can help to not unfold 3705 obj_at'_def which speeds up proofs. 3706 *) 3707context begin 3708 3709private definition 3710 "ko_at'_defn v \<equiv> ko_at' v" 3711 3712private lemma ko_at_defn_rewr: 3713 "ko_at'_defn ko p s \<Longrightarrow> (obj_at' P p s = P ko)" 3714 unfolding ko_at'_defn_def 3715 by (auto simp: obj_at'_def) 3716 3717private lemma ko_at_defn_uniqueD: 3718 "ko_at'_defn ko p s \<Longrightarrow> ko_at'_defn ko' p s \<Longrightarrow> ko' = ko" 3719 unfolding ko_at'_defn_def 3720 by (auto simp: obj_at'_def) 3721 3722private lemma ko_at_defn_pred_tcb_at': 3723 "ko_at'_defn ko p s \<Longrightarrow> (pred_tcb_at' proj P p s = P (proj (tcb_to_itcb' ko)))" 3724 by (auto simp: pred_tcb_at'_def ko_at_defn_rewr) 3725 3726private lemma ko_at_defn_ko_wp_at': 3727 "ko_at'_defn ko p s \<Longrightarrow> (ko_wp_at' P p s = P (injectKO ko))" 3728 by (clarsimp simp: ko_at'_defn_def obj_at'_real_def 3729 ko_wp_at'_def project_inject) 3730 3731method normalise_obj_at' = 3732 (clarsimp?, elim obj_at_ko_at'[folded ko_at'_defn_def, elim_format], 3733 clarsimp simp: ko_at_defn_rewr ko_at_defn_pred_tcb_at' ko_at_defn_ko_wp_at', 3734 ((drule(1) ko_at_defn_uniqueD)+)?, 3735 clarsimp simp: ko_at'_defn_def) 3736 3737end 3738 3739add_upd_simps "invs' (gsUntypedZeroRanges_update f s) 3740 \<and> valid_queues (gsUntypedZeroRanges_update f s)" 3741 (obj_at'_real_def) 3742declare upd_simps[simp] 3743end 3744