1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11(* Wellformedness of caps, kernel objects, states on the C level 12*) 13 14theory Wellformed_C 15imports 16 "CLib.CTranslationNICTA" 17 CLevityCatch 18 "CSpec.Substitute" 19begin 20 21context begin interpretation Arch . (*FIXME: arch_split*) 22 23abbreviation 24 cte_Ptr :: "word64 \<Rightarrow> cte_C ptr" where "cte_Ptr == Ptr" 25abbreviation 26 mdb_Ptr :: "word64 \<Rightarrow> mdb_node_C ptr" where "mdb_Ptr == Ptr" 27abbreviation 28 cap_Ptr :: "word64 \<Rightarrow> cap_C ptr" where "cap_Ptr == Ptr" 29abbreviation 30 tcb_Ptr :: "word64 \<Rightarrow> tcb_C ptr" where "tcb_Ptr == Ptr" 31abbreviation 32 atcb_Ptr :: "word64 \<Rightarrow> arch_tcb_C ptr" where "atcb_Ptr == Ptr" 33abbreviation 34 ep_Ptr :: "word64 \<Rightarrow> endpoint_C ptr" where "ep_Ptr == Ptr" 35abbreviation 36 ntfn_Ptr :: "word64 \<Rightarrow> notification_C ptr" where "ntfn_Ptr == Ptr" 37abbreviation 38 ap_Ptr :: "word64 \<Rightarrow> asid_pool_C ptr" where "ap_Ptr == Ptr" 39abbreviation 40 pte_Ptr :: "word64 \<Rightarrow> pte_C ptr" where "pte_Ptr == Ptr" 41abbreviation 42 pde_Ptr :: "word64 \<Rightarrow> pde_C ptr" where "pde_Ptr == Ptr" 43abbreviation 44 pdpte_Ptr :: "word64 \<Rightarrow> pdpte_C ptr" where "pdpte_Ptr == Ptr" 45abbreviation 46 pml4e_Ptr :: "word64 \<Rightarrow> pml4e_C ptr" where "pml4e_Ptr == Ptr" 47 48(* 1024 = number of entries in ioport table 49 = 2^16 (total number of ioports) / word_bits *) 50type_synonym ioport_table_C = "machine_word[1024]" 51 52type_synonym tcb_cnode_array = "cte_C[5]" 53type_synonym fpu_bytes_array = "word8[fpu_bytes]" 54type_synonym registers_array = "machine_word[23]" 55 56abbreviation "user_context_Ptr \<equiv> Ptr :: addr \<Rightarrow> user_context_C ptr" 57abbreviation "machine_word_Ptr \<equiv> Ptr :: addr \<Rightarrow> machine_word ptr" 58abbreviation "tcb_cnode_Ptr \<equiv> Ptr :: addr \<Rightarrow> tcb_cnode_array ptr" 59abbreviation "fpu_state_Ptr \<equiv> Ptr :: addr \<Rightarrow> user_fpu_state_C ptr" 60abbreviation "fpu_bytes_Ptr \<equiv> Ptr :: addr \<Rightarrow> fpu_bytes_array ptr" 61abbreviation "registers_Ptr \<equiv> Ptr :: addr \<Rightarrow> registers_array ptr" 62abbreviation "ioport_table_Ptr \<equiv> Ptr :: addr \<Rightarrow> ioport_table_C ptr" 63 64lemma halt_spec: 65 "Gamma \<turnstile> {} Call halt_'proc {}" 66 apply (rule hoare_complete) 67 apply (simp add: HoarePartialDef.valid_def) 68 done 69 70definition 71 isUntypedCap_C :: "cap_CL \<Rightarrow> bool" where 72 "isUntypedCap_C c \<equiv> 73 case c of 74 Cap_untyped_cap q \<Rightarrow> True 75 | _ \<Rightarrow> False" 76 77definition 78 isNullCap_C :: "cap_CL \<Rightarrow> bool" where 79 "isNullCap_C c \<equiv> 80 case c of 81 Cap_null_cap \<Rightarrow> True 82 | _ \<Rightarrow> False" 83 84definition 85 isEndpointCap_C :: "cap_CL \<Rightarrow> bool" where 86 "isEndpointCap_C v \<equiv> case v of 87 Cap_endpoint_cap ec \<Rightarrow> True 88 | _ \<Rightarrow> False" 89 90definition 91 isCNodeCap_C :: "cap_CL \<Rightarrow> bool" where 92 "isCNodeCap_C c \<equiv> case c of 93 Cap_cnode_cap a \<Rightarrow> True 94 | _ \<Rightarrow> False" 95 96 97definition 98 isThreadCap_C :: "cap_CL \<Rightarrow> bool" where 99 "isThreadCap_C c \<equiv> case c of 100 Cap_thread_cap a \<Rightarrow> True 101 | _ \<Rightarrow> False" 102 103definition 104 isIRQControlCap_C :: "cap_CL \<Rightarrow> bool" where 105 "isIRQControlCap_C c \<equiv> case c of 106 Cap_irq_control_cap \<Rightarrow> True 107 | _ \<Rightarrow> False" 108 109definition 110 isIRQHandlerCap_C :: "cap_CL \<Rightarrow> bool" where 111 "isIRQHandlerCap_C c \<equiv> case c of 112 Cap_irq_handler_cap a \<Rightarrow> True 113 | _ \<Rightarrow> False" 114 115definition 116 isNotificationCap_C :: "cap_CL \<Rightarrow> bool" where 117 "isNotificationCap_C v \<equiv> case v of 118 Cap_notification_cap aec \<Rightarrow> True 119 | _ \<Rightarrow> False" 120 121definition 122 ep_at_C' :: "word64 \<Rightarrow> heap_raw_state \<Rightarrow> bool" 123where 124 "ep_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: endpoint_C typ_heap)" \<comment> \<open>endpoint_lift is total\<close> 125 126definition 127 ntfn_at_C' :: "word64 \<Rightarrow> heap_raw_state \<Rightarrow> bool" 128 where \<comment> \<open>notification_lift is total\<close> 129 "ntfn_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: notification_C typ_heap)" 130 131definition 132 tcb_at_C' :: "word64 \<Rightarrow> heap_raw_state \<Rightarrow> bool" 133 where 134 "tcb_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: tcb_C typ_heap)" 135 136definition 137 cte_at_C' :: "word64 \<Rightarrow> heap_raw_state \<Rightarrow> bool" 138 where 139 "cte_at_C' p h \<equiv> Ptr p \<in> dom (clift h :: cte_C typ_heap)" 140 141definition 142 ctcb_ptr_to_tcb_ptr :: "tcb_C ptr \<Rightarrow> word64" 143 where 144 "ctcb_ptr_to_tcb_ptr p \<equiv> ptr_val p - ctcb_offset" 145 146definition 147 tcb_ptr_to_ctcb_ptr :: "word64 \<Rightarrow> tcb_C ptr" 148 where 149 "tcb_ptr_to_ctcb_ptr p \<equiv> Ptr (p + ctcb_offset)" 150 151primrec 152 tcb_queue_relation :: "(tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> 153 (tcb_C ptr \<Rightarrow> tcb_C option) \<Rightarrow> word64 list \<Rightarrow> 154 tcb_C ptr \<Rightarrow> tcb_C ptr \<Rightarrow> bool" 155where 156 "tcb_queue_relation getNext getPrev hp [] qprev qhead = (qhead = NULL)" 157| "tcb_queue_relation getNext getPrev hp (x#xs) qprev qhead = 158 (qhead = tcb_ptr_to_ctcb_ptr x \<and> 159 (\<exists>tcb. (hp qhead = Some tcb \<and> getPrev tcb = qprev \<and> tcb_queue_relation getNext getPrev hp xs qhead (getNext tcb))))" 160 161abbreviation 162 "ep_queue_relation \<equiv> tcb_queue_relation tcbEPNext_C tcbEPPrev_C" 163 164abbreviation 165 "sched_queue_relation \<equiv> tcb_queue_relation tcbSchedNext_C tcbSchedPrev_C" 166 167 168definition 169wordSizeCase :: "'a \<Rightarrow> 'a \<Rightarrow> 'a" where 170"wordSizeCase a b \<equiv> (if bitSize (undefined::machine_word) = 32 171 then a 172 else if bitSize (undefined::machine_word) = 64 173 then b 174 else error [] 175 )" 176 177 178primrec 179 capBits_C :: "cap_CL \<Rightarrow> nat" 180where 181 "capBits_C Cap_null_cap = 0" 182| "capBits_C (Cap_untyped_cap uc) = unat (capBlockSize_CL uc)" 183| "capBits_C (Cap_endpoint_cap ec) = wordSizeCase 4 5" 184| "capBits_C (Cap_notification_cap aec) = wordSizeCase 4 5" 185| "capBits_C (Cap_cnode_cap cnc) = wordSizeCase 4 5" 186| "capBits_C (Cap_thread_cap tc) = 10" 187| "capBits_C (Cap_zombie_cap zc) = (wordSizeCase 4 5)" 188 189 190definition 191capUntypedPtr_C :: "cap_CL \<Rightarrow> word64" where 192 "capUntypedPtr_C cap \<equiv> case cap of 193 (Cap_untyped_cap uc) \<Rightarrow> (capBlockSize_CL uc) 194 | Cap_endpoint_cap ep \<Rightarrow> (capEPPtr_CL ep) 195 | Cap_notification_cap ntfn \<Rightarrow> (capNtfnPtr_CL ntfn) 196 | Cap_cnode_cap ccap \<Rightarrow> (capCNodePtr_CL ccap) 197 | Cap_reply_cap rc \<Rightarrow> (cap_reply_cap_CL.capTCBPtr_CL rc) 198 | Cap_thread_cap tc \<Rightarrow> (cap_thread_cap_CL.capTCBPtr_CL tc) 199 | Cap_frame_cap fc \<Rightarrow> (cap_frame_cap_CL.capFBasePtr_CL fc) 200 | Cap_page_table_cap ptc \<Rightarrow> (cap_page_table_cap_CL.capPTBasePtr_CL ptc) 201 | Cap_page_directory_cap pdc \<Rightarrow> (cap_page_directory_cap_CL.capPDBasePtr_CL pdc) 202 | Cap_pdpt_cap pdptc \<Rightarrow> (cap_pdpt_cap_CL.capPDPTBasePtr_CL pdptc) 203 | Cap_pml4_cap pml4c \<Rightarrow> (cap_pml4_cap_CL.capPML4BasePtr_CL pml4c) 204 | _ \<Rightarrow> error []" 205 206definition ZombieTCB_C_def: 207"ZombieTCB_C \<equiv> bit 6" (*wordRadix*) 208 209definition 210 isZombieTCB_C :: "word64 \<Rightarrow> bool" where 211 "isZombieTCB_C v \<equiv> v = ZombieTCB_C" 212 213definition 214vmrights_to_H :: "word64 \<Rightarrow> vmrights" where 215"vmrights_to_H c \<equiv> 216 if c = scast Kernel_C.VMReadWrite then VMReadWrite 217 else if c = scast Kernel_C.VMReadOnly then VMReadOnly 218 else VMKernelOnly" 219 220(* Force clarity over name collisions *) 221abbreviation 222 X64SmallPage :: "vmpage_size" where 223 "X64SmallPage == X64.X64SmallPage" 224abbreviation 225 X64LargePage :: "vmpage_size" where 226 "X64LargePage == X64.X64LargePage" 227abbreviation 228 X64HugePage :: "vmpage_size" where 229 "X64HugePage == X64.X64HugePage" 230 231definition 232 framesize_to_H :: "machine_word \<Rightarrow> vmpage_size" 233where 234 "framesize_to_H c \<equiv> 235 if c = scast Kernel_C.X86_SmallPage then X64SmallPage 236 else if c = scast Kernel_C.X86_LargePage then X64LargePage 237 else X64HugePage" 238 239definition 240 framesize_from_H :: "vmpage_size \<Rightarrow> machine_word" 241where 242 "framesize_from_H sz \<equiv> 243 case sz of 244 X64SmallPage \<Rightarrow> scast Kernel_C.X86_SmallPage 245 | X64LargePage \<Rightarrow> scast Kernel_C.X86_LargePage 246 | X64HugePage \<Rightarrow> scast Kernel_C.X64_HugePage" 247 248lemma framesize_from_to_H: 249 "framesize_to_H (framesize_from_H sz) = sz" 250 by (simp add: framesize_to_H_def framesize_from_H_def 251 Kernel_C.X86_SmallPage_def Kernel_C.X86_LargePage_def 252 Kernel_C.X64_HugePage_def 253 split: if_split vmpage_size.splits) 254 255lemma framesize_from_H_eq: 256 "(framesize_from_H sz = framesize_from_H sz') = (sz = sz')" 257 by (cases sz; cases sz'; 258 simp add: framesize_from_H_def X86_SmallPage_def X86_LargePage_def X64_HugePage_def) 259 260definition 261 maptype_to_H :: "machine_word \<Rightarrow> vmmap_type" 262where 263 "maptype_to_H c \<equiv> 264 if c = scast Kernel_C.X86_MappingNone then VMNoMap 265 else VMVSpaceMap" 266 267end 268 269record cte_CL = 270 cap_CL :: cap_CL 271 cteMDBNode_CL :: mdb_node_CL 272 273context begin interpretation Arch . (*FIXME: arch_split*) 274 275definition 276 cte_lift :: "cte_C \<rightharpoonup> cte_CL" 277 where 278 "cte_lift c \<equiv> case cap_lift (cte_C.cap_C c) of 279 None \<Rightarrow> None 280 | Some cap \<Rightarrow> Some \<lparr> cap_CL = cap, 281 cteMDBNode_CL = mdb_node_lift (cteMDBNode_C c) \<rparr>" 282 283lemma to_bool_false [simp]: "\<not> to_bool false" 284 by (simp add: to_bool_def false_def) 285 286(* this is slightly weird, but the bitfield generator 287 masks everything with the expected bit length. 288 So we do that here too. *) 289definition 290 to_bool_bf :: "'a::len word \<Rightarrow> bool" where 291 "to_bool_bf w \<equiv> (w && mask 1) = 1" 292 293lemma to_bool_bf_mask1 [simp]: 294 "to_bool_bf (mask (Suc 0))" 295 by (simp add: mask_def to_bool_bf_def) 296 297lemma to_bool_bf_0 [simp]: "\<not>to_bool_bf 0" 298 by (simp add: to_bool_bf_def) 299 300lemma to_bool_bf_1 [simp]: "to_bool_bf 1" 301 by (simp add: to_bool_bf_def mask_def) 302 303lemma to_bool_bf_false [simp]: 304 "\<not>to_bool_bf false" 305 by (simp add: false_def) 306 307lemma to_bool_bf_true [simp]: 308 "to_bool_bf true" 309 by (simp add: true_def) 310 311lemma to_bool_to_bool_bf: 312 "w = false \<or> w = true \<Longrightarrow> to_bool_bf w = to_bool w" 313 by (auto simp: false_def true_def to_bool_def to_bool_bf_def mask_def) 314 315lemma to_bool_bf_mask_1 [simp]: 316 "to_bool_bf (w && mask (Suc 0)) = to_bool_bf w" 317 by (simp add: to_bool_bf_def) 318 319lemma to_bool_bf_and [simp]: 320 "to_bool_bf (a && b) = (to_bool_bf a \<and> to_bool_bf (b::word64))" 321 apply (clarsimp simp: to_bool_bf_def) 322 apply (rule iffI) 323 apply (subst (asm) bang_eq) 324 apply (simp add: word_size) 325 apply (rule conjI) 326 apply (rule word_eqI) 327 apply (auto simp add: word_size)[1] 328 apply (rule word_eqI) 329 apply (auto simp add: word_size)[1] 330 apply clarsimp 331 apply (rule word_eqI) 332 apply (subst (asm) bang_eq)+ 333 apply (auto simp add: word_size)[1] 334 done 335 336lemma to_bool_bf_to_bool_mask: 337 "w && mask (Suc 0) = w \<Longrightarrow> to_bool_bf w = to_bool (w::word64)" 338 apply (auto simp add: to_bool_bf_def to_bool_def mask_eq_iff_w2p word_size) 339 apply (auto simp add: mask_def dest: word_less_cases) 340 done 341 342definition 343 mdb_node_to_H :: "mdb_node_CL \<Rightarrow> mdbnode" 344 where 345 "mdb_node_to_H n \<equiv> MDB (mdbNext_CL n) 346 (mdbPrev_CL n) 347 (to_bool (mdbRevocable_CL n)) 348 (to_bool (mdbFirstBadged_CL n))" 349 350 351definition 352cap_to_H :: "cap_CL \<Rightarrow> capability" 353where 354"cap_to_H c \<equiv> case c of 355 Cap_null_cap \<Rightarrow> NullCap 356 | Cap_zombie_cap zc \<Rightarrow> (if isZombieTCB_C(capZombieType_CL zc) 357 then 358 (Zombie ((capZombieID_CL zc) && ~~(mask(5))) 359 (ZombieTCB) 360 (unat ((capZombieID_CL zc) && mask(5)))) 361 else let radix = unat (capZombieType_CL zc) in 362 (Zombie ((capZombieID_CL zc) && ~~(mask (radix+1))) 363 (ZombieCNode radix) 364 (unat ((capZombieID_CL zc) && mask(radix+1))))) 365 | Cap_cnode_cap ccap \<Rightarrow> 366 CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) 367 (capCNodeGuard_CL ccap) 368 (unat (capCNodeGuardSize_CL ccap)) 369 | Cap_untyped_cap uc \<Rightarrow> UntypedCap (to_bool(capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) 370 | Cap_endpoint_cap ec \<Rightarrow> 371 EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool(capCanSend_CL ec)) (to_bool(capCanReceive_CL ec)) 372 (to_bool(capCanGrant_CL ec)) 373 | Cap_notification_cap ntfn \<Rightarrow> 374 NotificationCap (capNtfnPtr_CL ntfn)(capNtfnBadge_CL ntfn)(to_bool(capNtfnCanSend_CL ntfn)) 375 (to_bool(capNtfnCanReceive_CL ntfn)) 376 | Cap_reply_cap rc \<Rightarrow> ReplyCap (ctcb_ptr_to_tcb_ptr (Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) 377 | Cap_thread_cap tc \<Rightarrow> ThreadCap(ctcb_ptr_to_tcb_ptr (Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) 378 | Cap_irq_handler_cap ihc \<Rightarrow> IRQHandlerCap (ucast(capIRQ_CL ihc)) 379 | Cap_irq_control_cap \<Rightarrow> IRQControlCap 380 | Cap_asid_control_cap \<Rightarrow> ArchObjectCap ASIDControlCap 381 | Cap_asid_pool_cap apc \<Rightarrow> ArchObjectCap (ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) 382 | Cap_frame_cap fc \<Rightarrow> ArchObjectCap (PageCap (capFBasePtr_CL fc) 383 (vmrights_to_H(capFVMRights_CL fc)) 384 (maptype_to_H(capFMapType_CL fc)) (framesize_to_H(capFSize_CL fc)) 385 (to_bool(capFIsDevice_CL fc)) 386 (if capFMappedASID_CL fc = 0 387 then None else 388 Some(capFMappedASID_CL fc, capFMappedAddress_CL fc))) 389 | Cap_page_table_cap ptc \<Rightarrow> ArchObjectCap (PageTableCap (cap_page_table_cap_CL.capPTBasePtr_CL ptc) 390 (if to_bool (cap_page_table_cap_CL.capPTIsMapped_CL ptc) 391 then Some( ((cap_page_table_cap_CL.capPTMappedASID_CL ptc)),(cap_page_table_cap_CL.capPTMappedAddress_CL ptc)) 392 else None)) 393 | Cap_page_directory_cap pdf \<Rightarrow> ArchObjectCap (PageDirectoryCap (cap_page_directory_cap_CL.capPDBasePtr_CL pdf) 394 (if to_bool (cap_page_directory_cap_CL.capPDIsMapped_CL pdf) 395 then Some (cap_page_directory_cap_CL.capPDMappedASID_CL pdf, cap_page_directory_cap_CL.capPDMappedAddress_CL pdf) 396 else None)) 397 | Cap_pdpt_cap pdf \<Rightarrow> ArchObjectCap (PDPointerTableCap (cap_pdpt_cap_CL.capPDPTBasePtr_CL pdf) 398 (if to_bool (cap_pdpt_cap_CL.capPDPTIsMapped_CL pdf) 399 then Some (cap_pdpt_cap_CL.capPDPTMappedASID_CL pdf, cap_pdpt_cap_CL.capPDPTMappedAddress_CL pdf) 400 else None)) 401 | Cap_pml4_cap pdf \<Rightarrow> ArchObjectCap (PML4Cap (cap_pml4_cap_CL.capPML4BasePtr_CL pdf) 402 (if to_bool (cap_pml4_cap_CL.capPML4IsMapped_CL pdf) 403 then Some (cap_pml4_cap_CL.capPML4MappedASID_CL pdf) 404 else None)) 405 | Cap_domain_cap \<Rightarrow> DomainCap 406 | Cap_io_port_control_cap \<Rightarrow> ArchObjectCap IOPortControlCap 407 | Cap_io_port_cap ioc \<Rightarrow> ArchObjectCap (IOPortCap (ucast(capIOPortFirstPort_CL ioc)) (ucast(capIOPortLastPort_CL ioc)))" 408 409lemmas cap_to_H_simps = cap_to_H_def[split_simps cap_CL.split] 410 411definition 412 cte_to_H :: "cte_CL \<Rightarrow> cte" 413 where 414 "cte_to_H cte \<equiv> CTE (cap_to_H (cap_CL cte)) (mdb_node_to_H (cteMDBNode_CL cte))" 415 416 417 418definition 419cl_valid_cap :: "cap_CL \<Rightarrow> bool" 420where 421"cl_valid_cap c \<equiv> 422 case c of 423 Cap_irq_handler_cap fc \<Rightarrow> ((capIRQ_CL fc) && mask 8 = capIRQ_CL fc) 424 | Cap_frame_cap fc \<Rightarrow> capFSize_CL fc < 3 \<and> capFMapType_CL fc < 2 \<and> capFVMRights_CL fc < 4 \<and> capFVMRights_CL fc \<noteq> 0 425 | Cap_pml4_cap pc \<Rightarrow> to_bool (capPML4IsMapped_CL pc) = (capPML4MappedASID_CL pc \<noteq> ucast asidInvalid) 426 | x \<Rightarrow> True" 427 428definition 429c_valid_cap :: "cap_C \<Rightarrow> bool" 430where 431"c_valid_cap c \<equiv> case_option True cl_valid_cap (cap_lift c)" 432 433 434definition 435cl_valid_cte :: "cte_CL \<Rightarrow> bool" 436where 437"cl_valid_cte c \<equiv> cl_valid_cap (cap_CL c)" 438 439 440definition 441c_valid_cte :: "cte_C \<Rightarrow> bool" 442where 443"c_valid_cte c \<equiv> c_valid_cap (cte_C.cap_C c)" 444 445(* all uninteresting cases can be deduced from the cap tag *) 446lemma c_valid_cap_simps [simp]: 447 "cap_get_tag c = scast cap_thread_cap \<Longrightarrow> c_valid_cap c" 448 "cap_get_tag c = scast cap_notification_cap \<Longrightarrow> c_valid_cap c" 449 "cap_get_tag c = scast cap_endpoint_cap \<Longrightarrow> c_valid_cap c" 450 "cap_get_tag c = scast cap_cnode_cap \<Longrightarrow> c_valid_cap c" 451 "cap_get_tag c = scast cap_page_directory_cap \<Longrightarrow> c_valid_cap c" 452 "cap_get_tag c = scast cap_asid_control_cap \<Longrightarrow> c_valid_cap c" 453 "cap_get_tag c = scast cap_irq_control_cap \<Longrightarrow> c_valid_cap c" 454 "cap_get_tag c = scast cap_page_table_cap \<Longrightarrow> c_valid_cap c" 455 "cap_get_tag c = scast cap_asid_pool_cap \<Longrightarrow> c_valid_cap c" 456 "cap_get_tag c = scast cap_untyped_cap \<Longrightarrow> c_valid_cap c" 457 "cap_get_tag c = scast cap_zombie_cap \<Longrightarrow> c_valid_cap c" 458 "cap_get_tag c = scast cap_reply_cap \<Longrightarrow> c_valid_cap c" 459 "cap_get_tag c = scast cap_null_cap \<Longrightarrow> c_valid_cap c" 460 "cap_get_tag c = scast cap_pdpt_cap \<Longrightarrow> c_valid_cap c" 461 "cap_get_tag c = scast cap_io_port_cap \<Longrightarrow> c_valid_cap c" 462 unfolding c_valid_cap_def cap_lift_def cap_tag_defs 463 by (simp add: cl_valid_cap_def)+ 464 465lemma ptr_val_tcb_ptr_mask2: 466 "is_aligned thread tcbBlockSizeBits 467 \<Longrightarrow> ptr_val (tcb_ptr_to_ctcb_ptr thread) && (~~ mask tcbBlockSizeBits) 468 = thread" 469 apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def projectKOs) 470 apply (simp add: is_aligned_add_helper ctcb_offset_defs objBits_simps') 471 done 472 473lemma maxDom_to_H: 474 "ucast maxDom = maxDomain" 475 by (simp add: maxDomain_def maxDom_def numDomains_def) 476 477lemma maxPrio_to_H: 478 "ucast seL4_MaxPrio = maxPriority" 479 by (simp add: maxPriority_def seL4_MaxPrio_def numPriorities_def) 480 481(* Input abbreviations for API object types *) 482(* disambiguates names *) 483 484abbreviation(input) 485 NotificationObject :: sword32 486where 487 "NotificationObject == seL4_NotificationObject" 488 489abbreviation(input) 490 CapTableObject :: sword32 491where 492 "CapTableObject == seL4_CapTableObject" 493 494abbreviation(input) 495 EndpointObject :: sword32 496where 497 "EndpointObject == seL4_EndpointObject" 498 499abbreviation(input) 500 LargePageObject :: sword32 501where 502 "LargePageObject == seL4_X86_LargePageObject" 503 504abbreviation(input) 505 PageDirectoryObject :: sword32 506where 507 "PageDirectoryObject == seL4_X86_PageDirectoryObject" 508 509abbreviation(input) 510 PageTableObject :: sword32 511where 512 "PageTableObject == seL4_X86_PageTableObject" 513 514abbreviation(input) 515 HugePageObject :: sword32 516where 517 "HugePageObject == seL4_X64_HugePageObject" 518 519abbreviation(input) 520 SmallPageObject :: sword32 521where 522 "SmallPageObject == seL4_X86_4K" 523 524abbreviation(input) 525 PDPTObject :: sword32 526where 527 "PDPTObject == seL4_X86_PDPTObject" 528 529abbreviation(input) 530 PML4Object :: sword32 531where 532 "PML4Object == seL4_X64_PML4Object" 533 534abbreviation(input) 535 TCBObject :: sword32 536where 537 "TCBObject == seL4_TCBObject" 538 539abbreviation(input) 540 UntypedObject :: sword32 541where 542 "UntypedObject == seL4_UntypedObject" 543 544abbreviation(input) 545 maxPrio :: sword32 546where 547 "maxPrio == seL4_MaxPrio" 548 549abbreviation(input) 550 minPrio :: sword32 551where 552 "minPrio == seL4_MinPrio" 553 554abbreviation(input) 555 nAPIObjects :: sword32 556where 557 "nAPIObjects == seL4_NonArchObjectTypeCount" 558 559abbreviation(input) 560 nObjects :: sword32 561where 562 "nObjects == seL4_ObjectTypeCount" 563 564abbreviation(input) 565 prioInvalid :: sword32 566where 567 "prioInvalid == seL4_InvalidPrio" 568 569end 570 571end 572