theory SyscallArgs_C

lemma ccap_relation_page_is_device:
  "ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3)) c
   \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift c) \<noteq> 0) = d" apply (clarsimp simp: ccap_relation_def Let_def map_option_Some_eq2 cap_to_H_def) apply (case_tac z) apply (auto split: if_splits simp: to_bool_def generic_frame_cap_get_capFIsDevice_CL_def Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccap_relation (capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3)) c \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (cap_lift c) \<noteq> 0) = d proof (prove)
goal (1 subgoal):
 1. \<And>z. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3)\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d proof (prove)
goal (17 subgoals):
 1. \<And>z. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_null_cap\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 2. \<And>z x2. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_untyped_cap x2\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 3. \<And>z x3. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_endpoint_cap x3\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 4. \<And>z x4. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_notification_cap x4\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 5. \<And>z x5. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_reply_cap x5\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 6. \<And>z x6. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_cnode_cap x6\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 7. \<And>z x7. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_thread_cap x7\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 8. \<And>z x8. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_small_frame_cap x8\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 9. \<And>z x9. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_frame_cap x9\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
 10. \<And>z x10. \<lbrakk>c_valid_cap c; cap_lift c = Some z; (case z of Cap_null_cap \<Rightarrow> capability.NullCap | Cap_untyped_cap uc \<Rightarrow> capability.UntypedCap (to_bool (capIsDevice_CL uc)) (capPtr_CL uc) (unat (capBlockSize_CL uc)) (unat (capFreeIndex_CL uc << 4)) | Cap_endpoint_cap ec \<Rightarrow> capability.EndpointCap (capEPPtr_CL ec) (capEPBadge_CL ec) (to_bool (capCanSend_CL ec)) (to_bool (capCanReceive_CL ec)) (to_bool (capCanGrant_CL ec)) (to_bool (capCanGrantReply_CL ec)) | Cap_notification_cap ntfn \<Rightarrow> capability.NotificationCap (capNtfnPtr_CL ntfn) (capNtfnBadge_CL ntfn) (to_bool (capNtfnCanSend_CL ntfn)) (to_bool (capNtfnCanReceive_CL ntfn)) | Cap_reply_cap rc \<Rightarrow> capability.ReplyCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_reply_cap_CL.capTCBPtr_CL rc))) (to_bool (capReplyMaster_CL rc)) (to_bool (capReplyCanGrant_CL rc)) | Cap_cnode_cap ccap \<Rightarrow> capability.CNodeCap (capCNodePtr_CL ccap) (unat (capCNodeRadix_CL ccap)) (capCNodeGuard_CL ccap) (unat (capCNodeGuardSize_CL ccap)) | Cap_thread_cap tc \<Rightarrow> capability.ThreadCap (ctcb_ptr_to_tcb_ptr (tcb_Ptr (cap_thread_cap_CL.capTCBPtr_CL tc))) | Cap_small_frame_cap sfc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_small_frame_cap_CL.capFIsDevice_CL sfc)) (cap_small_frame_cap_CL.capFBasePtr_CL sfc) (vmrights_to_H (cap_small_frame_cap_CL.capFVMRights_CL sfc)) Wellformed_C.ARMSmallPage (if cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc = 0 \<and> cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc = 0 then None else Some ((cap_small_frame_cap_CL.capFMappedASIDHigh_CL sfc << local.asidLowBits) + cap_small_frame_cap_CL.capFMappedASIDLow_CL sfc, cap_small_frame_cap_CL.capFMappedAddress_CL sfc))) | Cap_frame_cap fc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageCap (to_bool (cap_frame_cap_CL.capFIsDevice_CL fc)) (cap_frame_cap_CL.capFBasePtr_CL fc) (vmrights_to_H (cap_frame_cap_CL.capFVMRights_CL fc)) (framesize_to_H (capFSize_CL fc)) (if cap_frame_cap_CL.capFMappedASIDHigh_CL fc = 0 \<and> cap_frame_cap_CL.capFMappedASIDLow_CL fc = 0 then None else Some ((cap_frame_cap_CL.capFMappedASIDHigh_CL fc << local.asidLowBits) + cap_frame_cap_CL.capFMappedASIDLow_CL fc, cap_frame_cap_CL.capFMappedAddress_CL fc))) | Cap_asid_pool_cap apc \<Rightarrow> capability.ArchObjectCap (arch_capability.ASIDPoolCap (capASIDPool_CL apc) (capASIDBase_CL apc)) | Cap_page_table_cap ptc \<Rightarrow> capability.ArchObjectCap (arch_capability.PageTableCap (capPTBasePtr_CL ptc) (if to_bool (capPTIsMapped_CL ptc) then Some (capPTMappedASID_CL ptc, capPTMappedAddress_CL ptc) else None)) | Cap_page_directory_cap pdf \<Rightarrow> capability.ArchObjectCap (arch_capability.PageDirectoryCap (capPDBasePtr_CL pdf) (if to_bool (capPDIsMapped_CL pdf) then Some (capPDMappedASID_CL pdf) else None)) | Cap_asid_control_cap \<Rightarrow> capability.ArchObjectCap arch_capability.ASIDControlCap | Cap_irq_control_cap \<Rightarrow> capability.IRQControlCap | Cap_irq_handler_cap ihc \<Rightarrow> capability.IRQHandlerCap (UCAST(32 \<rightarrow> 10) (capIRQ_CL ihc)) | Cap_zombie_cap zc \<Rightarrow> if isZombieTCB_C (capZombieType_CL zc) then capability.Zombie (capZombieID_CL zc && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zc && mask 5)) else let radix = unat (capZombieType_CL zc) in capability.Zombie (capZombieID_CL zc && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zc && mask (radix + 1))) | Cap_domain_cap \<Rightarrow> capability.DomainCap) = capability.ArchObjectCap (arch_capability.PageCap d v0a v1 v2 v3); z = Cap_asid_pool_cap x10\<rbrakk> \<Longrightarrow> (generic_frame_cap_get_capFIsDevice_CL (Some z) \<noteq> 0) = d
A total of 17 subgoals... proof (prove)
goal:
No subgoals!