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 StateRelation_C 12imports Wellformed_C 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17definition 18 "lifth p s \<equiv> the (clift (t_hrs_' s) p)" 19 20definition 21 "array_relation r n a c \<equiv> \<forall>i \<le> n. r (a i) (index c (unat i))" 22 23(* used for bound ntfn/tcb *) 24definition 25 "option_to_ctcb_ptr x \<equiv> case x of None \<Rightarrow> NULL | Some t \<Rightarrow> tcb_ptr_to_ctcb_ptr t" 26 27 28definition 29 byte_to_word_heap :: "(word32 \<Rightarrow> word8) \<Rightarrow> (word32 \<Rightarrow> 10 word \<Rightarrow> word32)" 30 where 31 "byte_to_word_heap m base off \<equiv> let (ptr :: word32) = base + (ucast off * 4) in 32 word_rcat [m (ptr + 3), m (ptr + 2), m (ptr + 1), m ptr]" 33 34definition 35 heap_to_user_data :: "(word32 \<Rightarrow> kernel_object option) \<Rightarrow> (word32 \<Rightarrow> word8) \<Rightarrow> (word32 \<Rightarrow> (10 word \<Rightarrow> word32) option)" 36 where 37 "heap_to_user_data hp bhp \<equiv> \<lambda>p. let (uhp :: word32 \<Rightarrow> user_data option) = (projectKO_opt \<circ>\<^sub>m hp) in 38 option_map (\<lambda>_. byte_to_word_heap bhp p) (uhp p)" 39 40definition 41 heap_to_device_data :: "(word32 \<Rightarrow> kernel_object option) \<Rightarrow> (word32 \<Rightarrow> word8) \<Rightarrow> (word32 \<Rightarrow> (10 word \<Rightarrow> word32) option)" 42 where 43 "heap_to_device_data hp bhp \<equiv> \<lambda>p. let (uhp :: word32 \<Rightarrow> user_data_device option) = (projectKO_opt \<circ>\<^sub>m hp) in 44 option_map (\<lambda>_. byte_to_word_heap bhp p) (uhp p)" 45 46 47definition 48 cmap_relation :: "(word32 \<rightharpoonup> 'a) \<Rightarrow> 'b typ_heap \<Rightarrow> (word32 \<Rightarrow> 'b ptr) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> bool" 49 where 50 "cmap_relation as cs addr_fun rel \<equiv> 51 (addr_fun ` (dom as) = dom cs) \<and> 52 (\<forall>x \<in> dom as. rel (the (as x)) (the (cs (addr_fun x))))" 53 54definition 55 carray_map_relation :: "nat \<Rightarrow> (word32 \<rightharpoonup> ('a :: pre_storable)) 56 \<Rightarrow> ('b ptr \<Rightarrow> bool) \<Rightarrow> (word32 \<Rightarrow> 'b ptr) \<Rightarrow> bool" 57where 58 "carray_map_relation bits as cs addr_fun \<equiv> 59 (\<forall>p. (is_aligned p bits \<and> (\<forall>p'. p' && ~~ mask bits = p \<and> is_aligned p' (objBits (the (as p'))) 60 \<longrightarrow> p' \<in> dom as)) \<longleftrightarrow> cs (addr_fun p))" 61 62definition 63 cvariable_array_map_relation :: "(word32 \<rightharpoonup> 'a) \<Rightarrow> ('a \<Rightarrow> nat) 64 \<Rightarrow> (word32 \<Rightarrow> ('c :: c_type) ptr) \<Rightarrow> heap_typ_desc \<Rightarrow> bool" 65where 66 "cvariable_array_map_relation amap szs ptrfun htd 67 \<equiv> \<forall>p v. amap p = Some v \<longrightarrow> h_t_array_valid htd (ptrfun p) (szs v)" 68 69definition 70 asid_map_pd_to_hwasids :: "(asid \<rightharpoonup> hw_asid \<times> obj_ref) \<Rightarrow> (obj_ref \<Rightarrow> hw_asid set)" 71where 72 "asid_map_pd_to_hwasids mp \<equiv> \<lambda>pd. {hwasid. (hwasid, pd) \<in> ran mp}" 73 74definition 75 pd_pointer_to_asid_slot :: "obj_ref \<rightharpoonup> pde_C ptr" 76where 77 "pd_pointer_to_asid_slot pd \<equiv> if is_aligned pd pdBits then Some (Ptr (pd + 0x3FC0)) else None" 78 79definition 80 pde_stored_asid :: "pde_C \<rightharpoonup> hw_asid" 81where 82 "pde_stored_asid pde \<equiv> if pde_get_tag pde = scast pde_pde_invalid 83 \<and> to_bool (stored_asid_valid_CL (pde_pde_invalid_lift pde)) 84 then Some (ucast (stored_hw_asid_CL (pde_pde_invalid_lift pde))) 85 else None" 86 87end 88 89text {* 90 Conceptually, the constant armKSKernelVSpace_C resembles ghost state. 91 The constant specifies the use of certain address ranges, or ``windows''. 92 It is the very nature of these ranges is that they remain fixed 93 after initialization. 94 Hence, it is not necessary to carry this value around 95 as part of the actual state. 96 Rather, we simply fix it in a locale for the state relation. 97 98 Note that this locale does not build on @{text kernel} 99 but @{text substitute_pre}. 100 Hence, we can later base definitions for the ADT on it, 101 which can subsequently be instantiated for 102 @{text kernel_all_global_addresses} as well as @{text kernel_all_substitute}. 103*} 104locale state_rel = Arch + substitute_pre + (*FIXME: arch_split*) 105 fixes armKSKernelVSpace_C :: "machine_word \<Rightarrow> arm_vspace_region_use" 106 107locale kernel = kernel_all_substitute + state_rel 108 109context state_rel 110begin 111 112(* relates fixed adresses *) 113definition 114 "carch_globals s \<equiv> 115 (armUSGlobalPD s = symbol_table ''armUSGlobalPD'')" 116 117(* FIXME ARMHYP is this the right place? MOVE? *) 118definition 119 cur_vcpu_relation :: "(32 word \<times> bool) option \<Rightarrow> vcpu_C ptr \<Rightarrow> 32 word \<Rightarrow> bool" 120where 121 "cur_vcpu_relation akscurvcpu cvcpu cactive \<equiv> 122 case akscurvcpu 123 of Some acurvcpu \<Rightarrow> cvcpu = Ptr (fst acurvcpu) \<and> cvcpu \<noteq> NULL \<and> cactive = from_bool (snd acurvcpu) 124 | None \<Rightarrow> cvcpu = NULL \<and> cactive = 0" 125 126(* FIXME ARMHYP armUSGlobalPD points to page full of invalid PDEs, i.e. it's all zero *) 127(* FIXME ARMHYP TODO armKSGICVCPUNumListRegs \<le> GIC_VCPU_MAX_NUM_LR (64): missing invariant upstream? *) 128definition 129 carch_state_relation :: "Arch.kernel_state \<Rightarrow> globals \<Rightarrow> bool" 130where 131 "carch_state_relation astate cstate \<equiv> 132 armKSNextASID_' cstate = armKSNextASID astate \<and> 133 armKSKernelVSpace astate = armKSKernelVSpace_C \<and> 134 array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable astate) (armKSHWASIDTable_' cstate) \<and> 135 array_relation ((=) \<circ> option_to_ptr) (2^asid_high_bits - 1) (armKSASIDTable astate) (armKSASIDTable_' cstate) \<and> 136 (asid_map_pd_to_hwasids (armKSASIDMap astate)) 137 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m clift (t_hrs_' cstate) \<circ>\<^sub>m pd_pointer_to_asid_slot) \<and> 138 carch_globals astate \<and> 139 gic_vcpu_num_list_regs_' cstate = of_nat (armKSGICVCPUNumListRegs astate) \<and> 140 cur_vcpu_relation (armHSCurVCPU astate) (armHSCurVCPU_' cstate) (armHSVCPUActive_' cstate)" 141 142end 143 144context begin interpretation Arch . (*FIXME: arch_split*) 145 146definition 147 cmachine_state_relation :: "machine_state \<Rightarrow> globals \<Rightarrow> bool" 148where 149 "cmachine_state_relation s s' \<equiv> 150 irq_masks s = irq_masks (phantom_machine_state_' s') \<and> 151 irq_state s = irq_state (phantom_machine_state_' s') \<and> 152 device_state s = device_state (phantom_machine_state_' s') \<and> 153 exclusive_state s = exclusive_state (phantom_machine_state_' s') \<and> 154 machine_state_rest s = machine_state_rest (phantom_machine_state_' s')" 155 156 157definition 158 "globals_list_id_fudge = id" 159 160type_synonym ('a, 'b) ltyp_heap = "'a ptr \<rightharpoonup> 'b" 161 162abbreviation 163 map_to_tcbs :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> tcb" 164 where 165 "map_to_tcbs hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 166 167abbreviation 168 map_to_eps :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> endpoint" 169 where 170 "map_to_eps hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 171 172abbreviation 173 map_to_ntfns :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> notification" 174 where 175 "map_to_ntfns hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 176 177abbreviation 178 map_to_pdes :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> pde" 179 where 180 "map_to_pdes hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 181 182abbreviation 183 map_to_ptes :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> pte" 184 where 185 "map_to_ptes hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 186 187abbreviation 188 map_to_asidpools :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> asidpool" 189 where 190 "map_to_asidpools hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 191 192abbreviation 193 map_to_user_data :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> user_data" 194 where 195 "map_to_user_data hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 196 197abbreviation 198 map_to_vcpus :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> vcpu" 199 where 200 "map_to_vcpus hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 201 202abbreviation 203 map_to_user_data_device :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> word32 \<rightharpoonup> user_data_device" 204 where 205 "map_to_user_data_device hp \<equiv> projectKO_opt \<circ>\<^sub>m hp" 206 207 208definition 209 cmdbnode_relation :: "Structures_H.mdbnode \<Rightarrow> mdb_node_C \<Rightarrow> bool" 210where 211 "cmdbnode_relation amdb cmdb \<equiv> amdb = mdb_node_to_H (mdb_node_lift cmdb)" 212 213definition 214 ccte_relation :: "Structures_H.cte \<Rightarrow> cte_C \<Rightarrow> bool" 215where 216 "ccte_relation acte ccte \<equiv> Some acte = option_map cte_to_H (cte_lift ccte) 217 \<and> c_valid_cte ccte" 218 219lemma ccte_relation_c_valid_cte: "ccte_relation c c' \<Longrightarrow> c_valid_cte c'" 220 by (simp add: ccte_relation_def) 221 222 223definition 224 tcb_queue_relation' :: "(tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C \<Rightarrow> tcb_C ptr) \<Rightarrow> (tcb_C ptr \<Rightarrow> tcb_C option) \<Rightarrow> word32 list \<Rightarrow> tcb_C ptr \<Rightarrow> tcb_C ptr \<Rightarrow> bool" 225 where 226 "tcb_queue_relation' getNext getPrev hp queue qhead end \<equiv> 227 (end = (if queue = [] then NULL else (tcb_ptr_to_ctcb_ptr (last queue)))) 228 \<and> tcb_queue_relation getNext getPrev hp queue NULL qhead" 229 230fun 231 register_from_H :: "register \<Rightarrow> word32" 232 where 233 "register_from_H ARM_HYP.R0 = scast Kernel_C.R0" 234 | "register_from_H ARM_HYP.R1 = scast Kernel_C.R1" 235 | "register_from_H ARM_HYP.R2 = scast Kernel_C.R2" 236 | "register_from_H ARM_HYP.R3 = scast Kernel_C.R3" 237 | "register_from_H ARM_HYP.R4 = scast Kernel_C.R4" 238 | "register_from_H ARM_HYP.R5 = scast Kernel_C.R5" 239 | "register_from_H ARM_HYP.R6 = scast Kernel_C.R6" 240 | "register_from_H ARM_HYP.R7 = scast Kernel_C.R7" 241 | "register_from_H ARM_HYP.R8 = scast Kernel_C.R8" 242 | "register_from_H ARM_HYP.R9 = scast Kernel_C.R9" 243 | "register_from_H ARM_HYP.SL = scast Kernel_C.R10" 244 | "register_from_H ARM_HYP.FP = scast Kernel_C.R11" 245 | "register_from_H ARM_HYP.IP = scast Kernel_C.R12" 246 | "register_from_H ARM_HYP.SP = scast Kernel_C.SP" 247 | "register_from_H ARM_HYP.LR = scast Kernel_C.LR" 248 | "register_from_H ARM_HYP.LR_svc = scast Kernel_C.LR_svc" 249 | "register_from_H ARM_HYP.CPSR = scast Kernel_C.CPSR" 250 | "register_from_H ARM_HYP.TLS_BASE = scast Kernel_C.TLS_BASE" 251 | "register_from_H ARM_HYP.TPIDRURW = scast Kernel_C.TPIDRURW" 252 | "register_from_H ARM_HYP.FaultInstruction = scast Kernel_C.FaultInstruction" 253 254definition 255 ccontext_relation :: "(MachineTypes.register \<Rightarrow> word32) \<Rightarrow> user_context_C \<Rightarrow> bool" 256where 257 "ccontext_relation regs uc \<equiv> \<forall>r. regs r = index (registers_C uc) (unat (register_from_H r))" 258 259primrec 260 cthread_state_relation_lifted :: "Structures_H.thread_state \<Rightarrow> 261 (thread_state_CL \<times> seL4_Fault_CL option) \<Rightarrow> bool" 262where 263 "cthread_state_relation_lifted (Structures_H.Running) ts' 264 = (tsType_CL (fst ts') = scast ThreadState_Running)" 265| "cthread_state_relation_lifted (Structures_H.Restart) ts' 266 = (tsType_CL (fst ts') = scast ThreadState_Restart)" 267| "cthread_state_relation_lifted (Structures_H.Inactive) ts' 268 = (tsType_CL (fst ts') = scast ThreadState_Inactive)" 269| "cthread_state_relation_lifted (Structures_H.IdleThreadState) ts' 270 = (tsType_CL (fst ts') = scast ThreadState_IdleThreadState)" 271| "cthread_state_relation_lifted (Structures_H.BlockedOnReply) ts' 272 = (tsType_CL (fst ts') = scast ThreadState_BlockedOnReply)" 273| "cthread_state_relation_lifted (Structures_H.BlockedOnReceive oref) ts' 274 = (tsType_CL (fst ts') = scast ThreadState_BlockedOnReceive \<and> 275 oref = blockingObject_CL (fst ts'))" 276| "cthread_state_relation_lifted (Structures_H.BlockedOnSend oref badge cg isc) ts' 277 = (tsType_CL (fst ts') = scast ThreadState_BlockedOnSend 278 \<and> oref = blockingObject_CL (fst ts') 279 \<and> badge = blockingIPCBadge_CL (fst ts') 280 \<and> cg = to_bool (blockingIPCCanGrant_CL (fst ts')) 281 \<and> isc = to_bool (blockingIPCIsCall_CL (fst ts')))" 282| "cthread_state_relation_lifted (Structures_H.BlockedOnNotification oref) ts' 283 = (tsType_CL (fst ts') = scast ThreadState_BlockedOnNotification 284 \<and> oref = blockingObject_CL (fst ts'))" 285 286 287definition 288 cthread_state_relation :: "Structures_H.thread_state \<Rightarrow> 289 (thread_state_C \<times> seL4_Fault_C) \<Rightarrow> bool" 290where 291 "cthread_state_relation \<equiv> \<lambda>a (cs, cf). 292 cthread_state_relation_lifted a (thread_state_lift cs, seL4_Fault_lift cf)" 293 294definition "is_cap_fault cf \<equiv> 295 (case cf of (SeL4_Fault_CapFault _) \<Rightarrow> True 296 | _ \<Rightarrow> False)" 297 298lemma is_cap_fault_simp: "is_cap_fault cf = (\<exists> x. cf=SeL4_Fault_CapFault x)" 299 by (simp add: is_cap_fault_def split:seL4_Fault_CL.splits) 300 301 302definition 303 message_info_to_H :: "seL4_MessageInfo_C \<Rightarrow> Types_H.message_info" 304 where 305 "message_info_to_H mi \<equiv> Types_H.message_info.MI (length_CL (seL4_MessageInfo_lift mi)) 306 (extraCaps_CL (seL4_MessageInfo_lift mi)) 307 (capsUnwrapped_CL (seL4_MessageInfo_lift mi)) 308 (label_CL (seL4_MessageInfo_lift mi))" 309 310 311fun 312 lookup_fault_to_H :: "lookup_fault_CL \<Rightarrow> lookup_failure" 313 where 314 "lookup_fault_to_H Lookup_fault_invalid_root = InvalidRoot" 315 | "lookup_fault_to_H (Lookup_fault_guard_mismatch lf) = 316 (GuardMismatch (unat (bitsLeft_CL lf)) (guardFound_CL lf) (unat (bitsFound_CL lf)))" 317 | "lookup_fault_to_H (Lookup_fault_depth_mismatch lf) = 318 (DepthMismatch (unat (lookup_fault_depth_mismatch_CL.bitsLeft_CL lf)) 319 (unat (lookup_fault_depth_mismatch_CL.bitsFound_CL lf)))" 320 | "lookup_fault_to_H (Lookup_fault_missing_capability lf) = 321 (MissingCapability (unat (lookup_fault_missing_capability_CL.bitsLeft_CL lf)))" 322 323fun 324 fault_to_H :: "seL4_Fault_CL \<Rightarrow> lookup_fault_CL \<Rightarrow> fault option" 325where 326 "fault_to_H SeL4_Fault_NullFault lf = None" 327 | "fault_to_H (SeL4_Fault_CapFault cf) lf 328 = Some (CapFault (seL4_Fault_CapFault_CL.address_CL cf) (to_bool (inReceivePhase_CL cf)) (lookup_fault_to_H lf))" 329 | "fault_to_H (SeL4_Fault_VMFault vf) lf 330 = Some (ArchFault (VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]))" 331 | "fault_to_H (SeL4_Fault_UnknownSyscall us) lf 332 = Some (UnknownSyscallException (syscallNumber_CL us))" 333 | "fault_to_H (SeL4_Fault_UserException ue) lf 334 = Some (UserException (number_CL ue) (code_CL ue))" 335 | "fault_to_H (SeL4_Fault_VCPUFault vf) lf 336 = Some (ArchFault (VCPUFault (seL4_Fault_VCPUFault_CL.hsr_CL vf)))" 337 | "fault_to_H (SeL4_Fault_VGICMaintenance vf) lf 338 = Some (ArchFault (VGICMaintenance (if seL4_Fault_VGICMaintenance_CL.idxValid_CL vf = 1 339 then Some (seL4_Fault_VGICMaintenance_CL.idx_CL vf) 340 else None)))" 341 342definition 343 cfault_rel :: "Fault_H.fault option \<Rightarrow> seL4_Fault_CL option \<Rightarrow> lookup_fault_CL option \<Rightarrow> bool" 344where 345 "cfault_rel af cf lf \<equiv> \<exists>cf'. cf = Some cf' \<and> 346 (if (is_cap_fault cf') then (\<exists>lf'. lf = Some lf' \<and> fault_to_H cf' lf' = af) 347 else (fault_to_H cf' undefined = af))" 348 349definition 350 carch_tcb_relation :: "Structures_H.arch_tcb \<Rightarrow> arch_tcb_C \<Rightarrow> bool" 351where 352 "carch_tcb_relation aarch_tcb carch_tcb \<equiv> 353 ccontext_relation (atcbContextGet aarch_tcb) (tcbContext_C carch_tcb) 354 \<and> option_to_ptr (atcbVCPUPtr aarch_tcb) = tcbVCPU_C carch_tcb" 355 356definition 357 ctcb_relation :: "Structures_H.tcb \<Rightarrow> tcb_C \<Rightarrow> bool" 358where 359 "ctcb_relation atcb ctcb \<equiv> 360 tcbFaultHandler atcb = tcbFaultHandler_C ctcb 361 \<and> cthread_state_relation (tcbState atcb) (tcbState_C ctcb, tcbFault_C ctcb) 362 \<and> tcbIPCBuffer atcb = tcbIPCBuffer_C ctcb 363 \<and> carch_tcb_relation (tcbArch atcb) (tcbArch_C ctcb) 364 \<and> tcbQueued atcb = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ctcb))) 365 \<and> ucast (tcbDomain atcb) = tcbDomain_C ctcb 366 \<and> ucast (tcbPriority atcb) = tcbPriority_C ctcb 367 \<and> ucast (tcbMCP atcb) = tcbMCP_C ctcb 368 \<and> tcbTimeSlice atcb = unat (tcbTimeSlice_C ctcb) 369 \<and> cfault_rel (tcbFault atcb) (seL4_Fault_lift (tcbFault_C ctcb)) 370 (lookup_fault_lift (tcbLookupFailure_C ctcb)) 371 \<and> option_to_ptr (tcbBoundNotification atcb) = tcbBoundNotification_C ctcb" 372 373abbreviation 374 "ep_queue_relation' \<equiv> tcb_queue_relation' tcbEPNext_C tcbEPPrev_C" 375 376definition 377 cendpoint_relation :: "tcb_C typ_heap \<Rightarrow> Structures_H.endpoint \<Rightarrow> endpoint_C \<Rightarrow> bool" 378where 379 "cendpoint_relation h ntfn cep \<equiv> 380 let cstate = state_CL (endpoint_lift cep); 381 chead = (Ptr o epQueue_head_CL o endpoint_lift) cep; 382 cend = (Ptr o epQueue_tail_CL o endpoint_lift) cep in 383 case ntfn of 384 IdleEP \<Rightarrow> cstate = scast EPState_Idle \<and> ep_queue_relation' h [] chead cend 385 | SendEP q \<Rightarrow> cstate = scast EPState_Send \<and> ep_queue_relation' h q chead cend 386 | RecvEP q \<Rightarrow> cstate = scast EPState_Recv \<and> ep_queue_relation' h q chead cend" 387 388definition 389 cnotification_relation :: "tcb_C typ_heap \<Rightarrow> Structures_H.notification \<Rightarrow> 390 notification_C \<Rightarrow> bool" 391where 392 "cnotification_relation h antfn cntfn \<equiv> 393 let cntfn' = notification_lift cntfn; 394 cstate = notification_CL.state_CL cntfn'; 395 chead = (Ptr o ntfnQueue_head_CL) cntfn'; 396 cend = (Ptr o ntfnQueue_tail_CL) cntfn'; 397 cbound = ((Ptr o ntfnBoundTCB_CL) cntfn' :: tcb_C ptr) 398 in 399 (case ntfnObj antfn of 400 IdleNtfn \<Rightarrow> cstate = scast NtfnState_Idle \<and> ep_queue_relation' h [] chead cend 401 | WaitingNtfn q \<Rightarrow> cstate = scast NtfnState_Waiting \<and> ep_queue_relation' h q chead cend 402 | ActiveNtfn msgid \<Rightarrow> cstate = scast NtfnState_Active \<and> 403 msgid = ntfnMsgIdentifier_CL cntfn' \<and> 404 ep_queue_relation' h [] chead cend) 405 \<and> option_to_ctcb_ptr (ntfnBoundTCB antfn) = cbound" 406 407definition 408 "hap_from_vm_rights R \<equiv> case R of 409 VMNoAccess \<Rightarrow> 0 410 | VMKernelOnly \<Rightarrow> 0 411 | VMReadOnly \<Rightarrow> 1 412 | VMReadWrite \<Rightarrow> 3" 413 414definition 415 "memattr_from_cacheable c \<equiv> case c of 416 True \<Rightarrow> 0xf 417 | False \<Rightarrow> 0" 418 419definition 420 cpde_relation :: "pde \<Rightarrow> pde_C \<Rightarrow> bool" 421where 422 "cpde_relation pde cpde \<equiv> 423 (let cpde' = pde_lift cpde in 424 case pde of 425 InvalidPDE \<Rightarrow> 426 (\<exists>inv. cpde' = Some (Pde_pde_invalid inv)) (* seL4 uses invalid PDEs to stash other info *) 427 | PageTablePDE table \<Rightarrow> 428 cpde' = Some (Pde_pde_coarse 429 \<lparr> pde_pde_coarse_CL.address_CL = table \<rparr>) 430 | SectionPDE frame cacheable xn rights \<Rightarrow> 431 cpde' = Some (Pde_pde_section 432 \<lparr> pde_pde_section_CL.XN_CL = of_bool xn, 433 contiguous_hint_CL = 0, 434 pde_pde_section_CL.address_CL = frame, 435 AF_CL = 1, 436 SH_CL = 0, 437 HAP_CL = hap_from_vm_rights rights, 438 MemAttr_CL = memattr_from_cacheable cacheable \<rparr>) 439 | SuperSectionPDE frame cacheable xn rights \<Rightarrow> 440 cpde' = Some (Pde_pde_section 441 \<lparr> pde_pde_section_CL.XN_CL = of_bool xn, 442 contiguous_hint_CL = 1, 443 pde_pde_section_CL.address_CL = frame, 444 AF_CL = 1, 445 SH_CL = 0, 446 HAP_CL = hap_from_vm_rights rights, 447 MemAttr_CL = memattr_from_cacheable cacheable \<rparr>) 448 )" 449 450definition 451 cpte_relation :: "pte \<Rightarrow> pte_C \<Rightarrow> bool" 452where 453 "cpte_relation pte cpte \<equiv> 454 (let cpte' = pte_lift cpte in 455 case pte of 456 InvalidPTE \<Rightarrow> 457 (cpte' = Some (Pte_pte_invalid)) 458 | SmallPagePTE frame cacheable xn rights \<Rightarrow> 459 cpte' = Some (Pte_pte_small 460 \<lparr> pte_pte_small_CL.XN_CL = of_bool xn, 461 contiguous_hint_CL = 0, 462 pte_pte_small_CL.address_CL = frame, 463 AF_CL = 1, 464 SH_CL = 0, 465 HAP_CL = hap_from_vm_rights rights, 466 MemAttr_CL = memattr_from_cacheable cacheable \<rparr>) 467 | LargePagePTE frame cacheable xn rights \<Rightarrow> 468 cpte' = Some (Pte_pte_small 469 \<lparr> pte_pte_small_CL.XN_CL = of_bool xn, 470 contiguous_hint_CL = 1, 471 pte_pte_small_CL.address_CL = frame, 472 AF_CL = 1, 473 SH_CL = 0, 474 HAP_CL = hap_from_vm_rights rights, 475 MemAttr_CL = memattr_from_cacheable cacheable \<rparr>) 476 )" 477 478(* Invalid PTEs map to invalid PTEs (sanity check?) *) 479lemma pte_0: 480 "index (pte_C.words_C cpte) 0 = 0 \<and> index (pte_C.words_C cpte) 1 = 0 \<Longrightarrow> 481 pte_lift cpte = Some (Pte_pte_invalid)" 482 by (simp add: pte_lift_def pte_get_tag_def pte_pte_invalid_def) 483 484definition 485 casid_pool_relation :: "asidpool \<Rightarrow> asid_pool_C \<Rightarrow> bool" 486where 487 "casid_pool_relation asid_pool casid_pool \<equiv> 488 case asid_pool of ASIDPool pool \<Rightarrow> 489 case casid_pool of asid_pool_C cpool \<Rightarrow> 490 array_relation ((=) \<circ> option_to_ptr) (2^asid_low_bits - 1) pool cpool" 491 492definition 493 cvcpu_regs_relation :: "vcpu \<Rightarrow> vcpu_C \<Rightarrow> bool" 494where 495 "cvcpu_regs_relation vcpu cvcpu \<equiv> 496 \<forall>r. regs_C cvcpu.[fromEnum r] = vcpuRegs vcpu r" 497 498definition 499 virq_to_H :: "virq_C \<Rightarrow> virq" 500where 501 "virq_to_H virq = (virq_C.words_C virq).[0]" 502 503definition 504 cvgic_relation :: "gicvcpuinterface \<Rightarrow> gicVCpuIface_C \<Rightarrow> bool" 505where 506 "cvgic_relation vgic cvgic \<equiv> 507 gicVCpuIface_C.hcr_C cvgic = vgicHCR vgic 508 \<and> gicVCpuIface_C.vmcr_C cvgic = vgicVMCR vgic 509 \<and> gicVCpuIface_C.apr_C cvgic = vgicAPR vgic 510 \<and> (\<forall>i\<le>63. vgicLR vgic i = virq_to_H ((gicVCpuIface_C.lr_C cvgic).[i])) 511 \<and> (\<forall>i\<ge>64. vgicLR vgic i = 0)" 512(* FIXME ARM_HYP: if we know the range is 64, we should change the index type from nat to 6 word *) 513 514definition 515 cvcpu_relation :: "vcpu \<Rightarrow> vcpu_C \<Rightarrow> bool" 516where 517 "cvcpu_relation vcpu cvcpu \<equiv> 518 vcpuTCB_C cvcpu = option_to_ctcb_ptr (vcpuTCBPtr vcpu) 519 \<and> cvcpu_regs_relation vcpu cvcpu 520 \<and> cvgic_relation (vcpuVGIC vcpu) (vgic_C cvcpu)" 521 522definition 523 cuser_user_data_relation :: "(10 word \<Rightarrow> word32) \<Rightarrow> user_data_C \<Rightarrow> bool" 524where 525 "cuser_user_data_relation f ud \<equiv> \<forall>off. f off = index (user_data_C.words_C ud) (unat off)" 526 527definition 528 cuser_user_data_device_relation :: "(10 word \<Rightarrow> word32) \<Rightarrow> user_data_device_C \<Rightarrow> bool" 529where 530 "cuser_user_data_device_relation f ud \<equiv> True" 531 532abbreviation 533 "cpspace_cte_relation ah ch \<equiv> cmap_relation (map_to_ctes ah) (clift ch) Ptr ccte_relation" 534 535abbreviation 536 "cpspace_tcb_relation ah ch \<equiv> cmap_relation (map_to_tcbs ah) (clift ch) tcb_ptr_to_ctcb_ptr ctcb_relation" 537 538abbreviation 539 "cpspace_ep_relation ah ch \<equiv> cmap_relation (map_to_eps ah) (clift ch) Ptr (cendpoint_relation (clift ch))" 540 541abbreviation 542 "cpspace_ntfn_relation ah ch \<equiv> cmap_relation (map_to_ntfns ah) (clift ch) Ptr (cnotification_relation (clift ch))" 543 544abbreviation 545 "cpspace_pde_relation ah ch \<equiv> cmap_relation (map_to_pdes ah) (clift ch) Ptr cpde_relation" 546 547abbreviation 548 "cpspace_pte_relation ah ch \<equiv> cmap_relation (map_to_ptes ah) (clift ch) Ptr cpte_relation" 549 550abbreviation 551 "cpspace_asidpool_relation ah ch \<equiv> cmap_relation (map_to_asidpools ah) (clift ch) Ptr casid_pool_relation" 552 553abbreviation 554 "cpspace_vcpu_relation ah ch \<equiv> cmap_relation (map_to_vcpus ah) (clift ch) Ptr cvcpu_relation" 555 556 557abbreviation 558 "cpspace_user_data_relation ah bh ch \<equiv> cmap_relation (heap_to_user_data ah bh) (clift ch) Ptr cuser_user_data_relation" 559 560abbreviation 561 "cpspace_device_data_relation ah bh ch \<equiv> cmap_relation (heap_to_device_data ah bh) (clift ch) Ptr cuser_user_data_device_relation" 562 563 564abbreviation 565 pd_Ptr :: "32 word \<Rightarrow> (pde_C[2048]) ptr" where "pd_Ptr == Ptr" 566 567abbreviation 568 "cpspace_pde_array_relation ah ch \<equiv> carray_map_relation pdBits (map_to_pdes ah) (h_t_valid (hrs_htd ch) c_guard) pd_Ptr" 569 570abbreviation 571 pt_Ptr :: "32 word \<Rightarrow> (pte_C[512]) ptr" where "pt_Ptr == Ptr" 572 573abbreviation 574 "cpspace_pte_array_relation ah ch \<equiv> carray_map_relation ptBits (map_to_ptes ah) (h_t_valid (hrs_htd ch) c_guard) pt_Ptr" 575 576 577definition 578 cpspace_relation :: "(word32 \<rightharpoonup> Structures_H.kernel_object) \<Rightarrow> (word32 \<Rightarrow> word8) \<Rightarrow> heap_raw_state \<Rightarrow> bool" 579where 580 "cpspace_relation ah bh ch \<equiv> 581 cpspace_cte_relation ah ch \<and> cpspace_tcb_relation ah ch \<and> cpspace_ep_relation ah ch \<and> cpspace_ntfn_relation ah ch \<and> 582 cpspace_pde_relation ah ch \<and> cpspace_pte_relation ah ch \<and> cpspace_asidpool_relation ah ch \<and> 583 cpspace_user_data_relation ah bh ch \<and> cpspace_device_data_relation ah bh ch \<and> 584 cpspace_pde_array_relation ah ch \<and> cpspace_pte_array_relation ah ch \<and> 585 cpspace_vcpu_relation ah ch" 586 587abbreviation 588 "sched_queue_relation' \<equiv> tcb_queue_relation' tcbSchedNext_C tcbSchedPrev_C" 589 590abbreviation 591 end_C :: "tcb_queue_C \<Rightarrow> tcb_C ptr" 592where 593 "end_C == tcb_queue_C.end_C" 594 595definition 596 cready_queues_index_to_C :: "domain \<Rightarrow> priority \<Rightarrow> nat" 597where 598 "cready_queues_index_to_C qdom prio \<equiv> (unat qdom) * numPriorities + (unat prio)" 599 600definition 601 cready_queues_relation :: "tcb_C typ_heap \<Rightarrow> (tcb_queue_C[4096]) \<Rightarrow> (domain \<times> priority \<Rightarrow> ready_queue) \<Rightarrow> bool" 602where 603 "cready_queues_relation h_tcb queues aqueues \<equiv> 604 \<forall>qdom prio. ((qdom \<ge> ucast minDom \<and> qdom \<le> ucast maxDom \<and> 605 prio \<ge> ucast minPrio \<and> prio \<le> ucast maxPrio) \<longrightarrow> 606 (let cqueue = index queues (cready_queues_index_to_C qdom prio) in 607 sched_queue_relation' h_tcb (aqueues (qdom, prio)) (head_C cqueue) (end_C cqueue))) 608 \<and> (\<not> (qdom \<ge> ucast minDom \<and> qdom \<le> ucast maxDom \<and> 609 prio \<ge> ucast minPrio \<and> prio \<le> ucast maxPrio) \<longrightarrow> aqueues (qdom, prio) = [])" 610 611 612abbreviation 613 "cte_array_relation astate cstate 614 \<equiv> cvariable_array_map_relation (gsCNodes astate) (\<lambda>n. 2 ^ n) 615 cte_Ptr (hrs_htd (t_hrs_' cstate))" 616 617abbreviation 618 "tcb_cte_array_relation astate cstate 619 \<equiv> cvariable_array_map_relation (map_to_tcbs (ksPSpace astate)) 620 (\<lambda>x. 5) cte_Ptr (hrs_htd (t_hrs_' cstate))" 621 622fun 623 irqstate_to_C :: "irqstate \<Rightarrow> word32" 624 where 625 "irqstate_to_C IRQInactive = scast Kernel_C.IRQInactive" 626 | "irqstate_to_C IRQSignal = scast Kernel_C.IRQSignal" 627 | "irqstate_to_C IRQTimer = scast Kernel_C.IRQTimer" 628 | "irqstate_to_C irqstate.IRQReserved = scast Kernel_C.IRQReserved" 629 630definition 631 cinterrupt_relation :: "interrupt_state \<Rightarrow> cte_C ptr \<Rightarrow> (word32[192]) \<Rightarrow> bool" 632where 633 "cinterrupt_relation airqs cnode cirqs \<equiv> 634 cnode = Ptr (intStateIRQNode airqs) \<and> 635 (\<forall>irq \<le> (ucast Kernel_C.maxIRQ). 636 irqstate_to_C (intStateIRQTable airqs irq) = index cirqs (unat irq))" 637 638definition 639 cscheduler_action_relation :: "Structures_H.scheduler_action \<Rightarrow> tcb_C ptr \<Rightarrow> bool" 640where 641 "cscheduler_action_relation a p \<equiv> case a of 642 ResumeCurrentThread \<Rightarrow> p = NULL 643 | ChooseNewThread \<Rightarrow> p = Ptr 1 644 | SwitchToThread p' \<Rightarrow> p = tcb_ptr_to_ctcb_ptr p'" 645 646definition 647 dom_schedule_entry_relation :: "8 word \<times> 32 word \<Rightarrow> dschedule_C \<Rightarrow> bool" 648where 649 "dom_schedule_entry_relation adomSched cdomSched \<equiv> 650 ucast (fst adomSched) = dschedule_C.domain_C cdomSched \<and> 651 (snd adomSched) = dschedule_C.length_C cdomSched" 652 653definition 654 cdom_schedule_relation :: "(8 word \<times> 32 word) list \<Rightarrow> (dschedule_C['b :: finite]) \<Rightarrow> bool" 655where 656 "cdom_schedule_relation adomSched cdomSched \<equiv> 657 length adomSched = card (UNIV :: 'b set) \<and> 658 (\<forall>n \<le> length adomSched. dom_schedule_entry_relation (adomSched ! n) (index cdomSched n))" 659 660definition 661 ghost_size_rel :: "cghost_state \<Rightarrow> nat \<Rightarrow> bool" 662where 663 "ghost_size_rel gs maxSize = ((gs_get_assn cap_get_capSizeBits_'proc gs = 0 664 \<and> maxSize = card (UNIV :: word32 set)) 665 \<or> (maxSize > 0 \<and> maxSize = unat (gs_get_assn cap_get_capSizeBits_'proc gs)))" 666 667definition 668 cbitmap_L1_relation :: "machine_word['dom::finite] \<Rightarrow> (domain \<Rightarrow> machine_word) \<Rightarrow> bool" 669where 670 "cbitmap_L1_relation cbitmap1 abitmap1 \<equiv> 671 \<forall>d. (d \<le> maxDomain \<longrightarrow> cbitmap1.[unat d] = abitmap1 d) \<and> 672 (\<not> d \<le> maxDomain \<longrightarrow> abitmap1 d = 0)" 673 674definition 675 cbitmap_L2_relation :: "machine_word['i::finite]['dom::finite] 676 \<Rightarrow> ((domain \<times> nat) \<Rightarrow> machine_word) \<Rightarrow> bool" 677where 678 "cbitmap_L2_relation cbitmap2 abitmap2 \<equiv> 679 \<forall>d i. ((d \<le> maxDomain \<and> i < l2BitmapSize) 680 \<longrightarrow> cbitmap2.[unat d].[i] = abitmap2 (d, i)) \<and> 681 ((\<not> (d \<le> maxDomain \<and> i < l2BitmapSize)) 682 \<longrightarrow> abitmap2 (d, i) = 0)" 683 684end (* interpretation Arch . (*FIXME: arch_split*) *) 685 686definition 687 region_is_bytes' :: "word32 \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool" 688where 689 "region_is_bytes' ptr sz htd \<equiv> \<forall>z\<in>{ptr ..+ sz}. \<forall> td. td \<noteq> typ_uinfo_t TYPE (word8) \<longrightarrow> 690 (\<forall>n b. snd (htd z) n \<noteq> Some (td, b))" 691 692abbreviation 693 region_is_bytes :: "word32 \<Rightarrow> nat \<Rightarrow> globals myvars \<Rightarrow> bool" 694where 695 "region_is_bytes ptr sz s \<equiv> region_is_bytes' ptr sz (hrs_htd (t_hrs_' (globals s)))" 696 697abbreviation(input) 698 "heap_list_is_zero hp ptr n \<equiv> heap_list hp n ptr = replicate n 0" 699 700abbreviation 701 "region_is_zero_bytes ptr n x \<equiv> region_is_bytes ptr n x 702 \<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals x))) ptr n" 703 704definition 705 region_actually_is_bytes' :: "addr \<Rightarrow> nat \<Rightarrow> heap_typ_desc \<Rightarrow> bool" 706where 707 "region_actually_is_bytes' ptr len htd 708 = (\<forall>x \<in> {ptr ..+ len}. htd x 709 = (True, [0 \<mapsto> (typ_uinfo_t TYPE(8 word), True)]))" 710 711abbreviation 712 "region_actually_is_bytes ptr len s 713 \<equiv> region_actually_is_bytes' ptr len (hrs_htd (t_hrs_' (globals s)))" 714 715lemmas region_actually_is_bytes_def = region_actually_is_bytes'_def 716 717abbreviation 718 "region_actually_is_zero_bytes ptr len s 719 \<equiv> region_actually_is_bytes ptr len s 720 \<and> heap_list_is_zero (hrs_mem (t_hrs_' (globals s))) ptr len" 721 722definition 723 zero_ranges_are_zero 724where 725 "zero_ranges_are_zero rs hrs 726 = (\<forall>(start, end) \<in> rs. region_actually_is_bytes' start (unat ((end + 1) - start)) (hrs_htd hrs) 727 \<and> heap_list_is_zero (hrs_mem hrs) start (unat ((end + 1) - start)))" 728 729definition (in state_rel) 730 cstate_relation :: "KernelStateData_H.kernel_state \<Rightarrow> globals \<Rightarrow> bool" 731where 732 cstate_relation_def: 733 "cstate_relation astate cstate \<equiv> 734 let cheap = t_hrs_' cstate in 735 cpspace_relation (ksPSpace astate) (underlying_memory (ksMachineState astate)) cheap \<and> 736 cready_queues_relation (clift cheap) 737 (ksReadyQueues_' cstate) 738 (ksReadyQueues astate) \<and> 739 zero_ranges_are_zero (gsUntypedZeroRanges astate) cheap \<and> 740 cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cstate) (ksReadyQueuesL1Bitmap astate) \<and> 741 cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cstate) (ksReadyQueuesL2Bitmap astate) \<and> 742 ksCurThread_' cstate = (tcb_ptr_to_ctcb_ptr (ksCurThread astate)) \<and> 743 ksIdleThread_' cstate = (tcb_ptr_to_ctcb_ptr (ksIdleThread astate)) \<and> 744 cinterrupt_relation (ksInterruptState astate) (intStateIRQNode_' cstate) (intStateIRQTable_' cstate) \<and> 745 cscheduler_action_relation (ksSchedulerAction astate) 746 (ksSchedulerAction_' cstate) \<and> 747 carch_state_relation (ksArchState astate) cstate \<and> 748 cmachine_state_relation (ksMachineState astate) cstate \<and> 749 cte_array_relation astate cstate \<and> 750 tcb_cte_array_relation astate cstate \<and> 751 apsnd fst (ghost'state_' cstate) = (gsUserPages astate, gsCNodes astate) \<and> 752 ghost_size_rel (ghost'state_' cstate) (gsMaxObjectSize astate) \<and> 753 ksWorkUnitsCompleted_' cstate = ksWorkUnitsCompleted astate \<and> 754 h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard 755 (ptr_coerce (intStateIRQNode_' cstate) :: (cte_C[256]) ptr) \<and> 756 {ptr_val (intStateIRQNode_' cstate) ..+ 2 ^ (8 + cte_level_bits)} \<subseteq> kernel_data_refs \<and> 757 h_t_valid (hrs_htd (t_hrs_' cstate)) c_guard 758 (pd_Ptr (symbol_table ''armUSGlobalPD'')) \<and> 759 ptr_span (pd_Ptr (symbol_table ''armUSGlobalPD'')) \<subseteq> kernel_data_refs \<and> 760 htd_safe domain (hrs_htd (t_hrs_' cstate)) \<and> 761 kernel_data_refs = (- domain) \<and> 762 globals_list_distinct (- kernel_data_refs) symbol_table globals_list \<and> 763 cdom_schedule_relation (ksDomSchedule astate) 764 Kernel_C.kernel_all_global_addresses.ksDomSchedule \<and> 765 ksDomScheduleIdx_' cstate = of_nat (ksDomScheduleIdx astate) \<and> 766 ksCurDomain_' cstate = ucast (ksCurDomain astate) \<and> 767 ksDomainTime_' cstate = ksDomainTime astate" 768 769definition 770 ccap_relation :: "capability \<Rightarrow> cap_C \<Rightarrow> bool" 771where 772 "ccap_relation acap ccap \<equiv> (Some acap = option_map cap_to_H (cap_lift ccap)) 773 \<and> (c_valid_cap ccap)" 774 775lemma ccap_relation_c_valid_cap: "ccap_relation c c' \<Longrightarrow> c_valid_cap c'" 776 by (simp add: ccap_relation_def) 777 778context begin interpretation Arch . 779fun 780 arch_fault_to_fault_tag :: "arch_fault \<Rightarrow> word32" 781 where 782 "arch_fault_to_fault_tag (VMFault a b) = scast seL4_Fault_VMFault" 783| "arch_fault_to_fault_tag (VCPUFault a) = scast seL4_Fault_VCPUFault" 784| "arch_fault_to_fault_tag (VGICMaintenance a) = scast seL4_Fault_VGICMaintenance" 785end 786 787fun 788 fault_to_fault_tag :: "fault \<Rightarrow> word32" 789where 790 " fault_to_fault_tag (CapFault a b c) = scast seL4_Fault_CapFault" 791 | "fault_to_fault_tag (ArchFault f) = arch_fault_to_fault_tag f" 792 | "fault_to_fault_tag (UnknownSyscallException a) = scast seL4_Fault_UnknownSyscall" 793 | "fault_to_fault_tag (UserException a b) = scast seL4_Fault_UserException" 794 795lemmas seL4_Faults = seL4_Fault_UserException_def 796 seL4_Fault_UnknownSyscall_def 797 seL4_Fault_CapFault_def 798 799lemmas seL4_Arch_Faults = seL4_Fault_VMFault_def 800 seL4_Fault_VCPUFault_def 801 seL4_Fault_VGICMaintenance_def 802 803(* Return relations *) 804 805record errtype = 806 errfault :: "seL4_Fault_CL option" 807 errlookup_fault :: "lookup_fault_CL option" 808 errsyscall :: syscall_error_C 809 810primrec 811 lookup_failure_rel :: "lookup_failure \<Rightarrow> word32 \<Rightarrow> errtype \<Rightarrow> bool" 812where 813 "lookup_failure_rel InvalidRoot fl es = (fl = scast EXCEPTION_LOOKUP_FAULT \<and> errlookup_fault es = Some Lookup_fault_invalid_root)" 814| "lookup_failure_rel (GuardMismatch bl gf sz) fl es = (fl = scast EXCEPTION_LOOKUP_FAULT \<and> 815 (\<exists>lf. errlookup_fault es = Some (Lookup_fault_guard_mismatch lf) \<and> 816 guardFound_CL lf = gf \<and> unat (bitsLeft_CL lf) = bl \<and> unat (bitsFound_CL lf) = sz))" 817| "lookup_failure_rel (DepthMismatch bl bf) fl es = (fl = scast EXCEPTION_LOOKUP_FAULT \<and> 818 (\<exists>lf. errlookup_fault es = Some (Lookup_fault_depth_mismatch lf) \<and> 819 unat (lookup_fault_depth_mismatch_CL.bitsLeft_CL lf) = bl 820 \<and> unat (lookup_fault_depth_mismatch_CL.bitsFound_CL lf) = bf))" 821| "lookup_failure_rel (MissingCapability bl) fl es = (fl = scast EXCEPTION_LOOKUP_FAULT \<and> 822 (\<exists>lf. errlookup_fault es = Some (Lookup_fault_missing_capability lf) \<and> 823 unat (lookup_fault_missing_capability_CL.bitsLeft_CL lf) = bl))" 824 825 826definition 827 syscall_error_to_H :: "syscall_error_C \<Rightarrow> lookup_fault_CL option \<Rightarrow> syscall_error option" 828where 829 "syscall_error_to_H se lf \<equiv> 830 if type_C se = scast seL4_InvalidArgument 831 then Some (InvalidArgument (unat (invalidArgumentNumber_C se))) 832 else if type_C se = scast seL4_InvalidCapability 833 then Some (InvalidCapability (unat (invalidCapNumber_C se))) 834 else if type_C se = scast seL4_IllegalOperation then Some IllegalOperation 835 else if type_C se = scast seL4_RangeError 836 then Some (RangeError (rangeErrorMin_C se) (rangeErrorMax_C se)) 837 else if type_C se = scast seL4_AlignmentError then Some AlignmentError 838 else if type_C se = scast seL4_FailedLookup 839 then option_map (FailedLookup (to_bool (failedLookupWasSource_C se)) 840 o lookup_fault_to_H) lf 841 else if type_C se = scast seL4_TruncatedMessage then Some TruncatedMessage 842 else if type_C se = scast seL4_DeleteFirst then Some DeleteFirst 843 else if type_C se = scast seL4_RevokeFirst then Some RevokeFirst 844 else if type_C se = scast seL4_NotEnoughMemory then Some (NotEnoughMemory (memoryLeft_C se)) 845 else None" 846 847lemmas syscall_error_type_defs 848 = seL4_AlignmentError_def seL4_DeleteFirst_def seL4_FailedLookup_def 849 seL4_IllegalOperation_def seL4_InvalidArgument_def seL4_InvalidCapability_def 850 seL4_NotEnoughMemory_def seL4_RangeError_def seL4_RevokeFirst_def 851 seL4_TruncatedMessage_def 852 853lemma 854 syscall_error_to_H_cases: 855 "type_C se = scast seL4_InvalidArgument 856 \<Longrightarrow> syscall_error_to_H se lf = Some (InvalidArgument (unat (invalidArgumentNumber_C se)))" 857 "type_C se = scast seL4_InvalidCapability 858 \<Longrightarrow> syscall_error_to_H se lf = Some (InvalidCapability (unat (invalidCapNumber_C se)))" 859 "type_C se = scast seL4_IllegalOperation 860 \<Longrightarrow> syscall_error_to_H se lf = Some IllegalOperation" 861 "type_C se = scast seL4_RangeError 862 \<Longrightarrow> syscall_error_to_H se lf = Some (RangeError (rangeErrorMin_C se) (rangeErrorMax_C se))" 863 "type_C se = scast seL4_AlignmentError 864 \<Longrightarrow> syscall_error_to_H se lf = Some AlignmentError" 865 "type_C se = scast seL4_FailedLookup 866 \<Longrightarrow> syscall_error_to_H se lf = option_map (FailedLookup (to_bool (failedLookupWasSource_C se)) 867 o lookup_fault_to_H) lf" 868 "type_C se = scast seL4_TruncatedMessage 869 \<Longrightarrow> syscall_error_to_H se lf = Some TruncatedMessage" 870 "type_C se = scast seL4_DeleteFirst 871 \<Longrightarrow> syscall_error_to_H se lf = Some DeleteFirst" 872 "type_C se = scast seL4_RevokeFirst 873 \<Longrightarrow> syscall_error_to_H se lf = Some RevokeFirst" 874 "type_C se = scast seL4_NotEnoughMemory 875 \<Longrightarrow> syscall_error_to_H se lf = Some (NotEnoughMemory (memoryLeft_C se))" 876 by (simp add: syscall_error_to_H_def syscall_error_type_defs)+ 877 878definition 879 syscall_error_rel :: "syscall_error \<Rightarrow> word32 \<Rightarrow> errtype \<Rightarrow> bool" where 880 "syscall_error_rel se fl es \<equiv> fl = scast EXCEPTION_SYSCALL_ERROR 881 \<and> syscall_error_to_H (errsyscall es) (errlookup_fault es) 882 = Some se" 883 884(* cap rights *) 885definition 886 "cap_rights_to_H rs \<equiv> CapRights (to_bool (capAllowWrite_CL rs)) 887 (to_bool (capAllowRead_CL rs)) 888 (to_bool (capAllowGrant_CL rs))" 889 890definition 891 "ccap_rights_relation cr cr' \<equiv> cr = cap_rights_to_H (seL4_CapRights_lift cr')" 892 893lemma (in kernel) syscall_error_to_H_cases_rev: 894 "\<And>n. syscall_error_to_H e lf = Some (InvalidArgument n) \<Longrightarrow> 895 type_C e = scast seL4_InvalidArgument" 896 "\<And>n. syscall_error_to_H e lf = Some (InvalidCapability n) \<Longrightarrow> 897 type_C e = scast seL4_InvalidCapability" 898 "syscall_error_to_H e lf = Some IllegalOperation \<Longrightarrow> 899 type_C e = scast seL4_IllegalOperation" 900 "\<And>w1 w2. syscall_error_to_H e lf = Some (RangeError w1 w2) \<Longrightarrow> 901 type_C e = scast seL4_RangeError" 902 "syscall_error_to_H e lf = Some AlignmentError \<Longrightarrow> 903 type_C e = scast seL4_AlignmentError" 904 "\<And>b lf'. syscall_error_to_H e lf = Some (FailedLookup b lf') \<Longrightarrow> 905 type_C e = scast seL4_FailedLookup" 906 "syscall_error_to_H e lf = Some TruncatedMessage \<Longrightarrow> 907 type_C e = scast seL4_TruncatedMessage" 908 "syscall_error_to_H e lf = Some DeleteFirst \<Longrightarrow> 909 type_C e = scast seL4_DeleteFirst" 910 "syscall_error_to_H e lf = Some RevokeFirst \<Longrightarrow> 911 type_C e = scast seL4_RevokeFirst" 912 by (clarsimp simp: syscall_error_to_H_def syscall_error_type_defs 913 split: if_split_asm)+ 914 915definition 916 syscall_from_H :: "syscall \<Rightarrow> word32" 917where 918 "syscall_from_H c \<equiv> case c of 919 SysSend \<Rightarrow> scast Kernel_C.SysSend 920 | SysNBSend \<Rightarrow> scast Kernel_C.SysNBSend 921 | SysCall \<Rightarrow> scast Kernel_C.SysCall 922 | SysRecv \<Rightarrow> scast Kernel_C.SysRecv 923 | SysReply \<Rightarrow> scast Kernel_C.SysReply 924 | SysReplyRecv \<Rightarrow> scast Kernel_C.SysReplyRecv 925 | SysNBRecv \<Rightarrow> scast Kernel_C.SysNBRecv 926 | SysYield \<Rightarrow> scast Kernel_C.SysYield" 927 928lemma (in kernel) cmap_relation_cs_atD: 929 "\<lbrakk> cmap_relation as cs addr_fun rel; cs (addr_fun x) = Some y; inj addr_fun \<rbrakk> \<Longrightarrow> 930 \<exists>ko. as x = Some ko \<and> rel ko y" 931 apply (clarsimp simp: cmap_relation_def) 932 apply (subgoal_tac "x \<in> dom as") 933 apply (drule (1) bspec) 934 apply (clarsimp simp: dom_def) 935 apply (subgoal_tac "addr_fun x \<in> addr_fun ` dom as") 936 prefer 2 937 apply fastforce 938 apply (erule imageE) 939 apply (drule (1) injD) 940 apply simp 941 done 942 943end 944