theory CSpace_C

lemma sameRegionAs_NotificationCap:
  shows "\<lbrakk>ccap_relation capa capc;
          RetypeDecls_H.sameRegionAs
            (capability.NotificationCap x y z  u ) capa\<rbrakk>
         \<Longrightarrow> cap_get_tag capc = scast cap_notification_cap" apply (simp add: sameRegionAs_def  Let_def) apply (case_tac capa;
         simp add: isUntypedCap_def isEndpointCap_def isNotificationCap_def
             isCNodeCap_def isThreadCap_def isReplyCap_def isIRQControlCap_def
             isIRQHandlerCap_def isArchObjectCap_def) apply (clarsimp simp: ccap_relation_def map_option_case) apply (case_tac "cap_lift capc"; simp) apply (simp add: cap_to_H_def) apply (case_tac a; simp) apply (simp add: cap_notification_cap_lift cap_notification_cap_lift_def) apply (rename_tac zombie_cap) apply (case_tac "isZombieTCB_C (capZombieType_CL zombie_cap)"; simp add: Let_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation capa capc; global.sameRegionAs (capability.NotificationCap x y z u) capa\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ccap_relation capa capc; if isEndpointCap (capability.NotificationCap x y z u) \<and> isEndpointCap capa then capEPPtr (capability.NotificationCap x y z u) = capEPPtr capa else if isNotificationCap (capability.NotificationCap x y z u) \<and> isNotificationCap capa then capNtfnPtr (capability.NotificationCap x y z u) = capNtfnPtr capa else if isCNodeCap (capability.NotificationCap x y z u) \<and> isCNodeCap capa then capCNodePtr (capability.NotificationCap x y z u) = capCNodePtr capa \<and> capCNodeBits (capability.NotificationCap x y z u) = capCNodeBits capa else if isThreadCap (capability.NotificationCap x y z u) \<and> isThreadCap capa then capTCBPtr (capability.NotificationCap x y z u) = capTCBPtr capa else if isReplyCap (capability.NotificationCap x y z u) \<and> isReplyCap capa then capTCBPtr (capability.NotificationCap x y z u) = capTCBPtr capa else if isDomainCap (capability.NotificationCap x y z u) \<and> isDomainCap capa then True else if isIRQControlCap (capability.NotificationCap x y z u) \<and> isIRQControlCap capa then True else if isIRQControlCap (capability.NotificationCap x y z u) \<and> isIRQHandlerCap capa then True else if isIRQHandlerCap (capability.NotificationCap x y z u) \<and> isIRQHandlerCap capa then case (capability.NotificationCap x y z u, capa) of (capability.IRQHandlerCap a, capability.IRQHandlerCap x) \<Rightarrow> a = x else if isArchObjectCap (capability.NotificationCap x y z u) \<and> isArchObjectCap capa then case (capability.NotificationCap x y z u, capa) of (capability.ArchObjectCap a, capability.ArchObjectCap x) \<Rightarrow> a `~Arch.sameRegionAs~` x else False\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<And>x31 x32 x33 x34. \<lbrakk>ccap_relation (capability.NotificationCap x31 x32 x33 x34) capc; x = x31; capa = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<And>x32 x33 x34. \<lbrakk>capa = capability.NotificationCap x x32 x33 x34; Some (capability.NotificationCap x x32 x33 x34) = (case cap_lift capc of None \<Rightarrow> None | Some x \<Rightarrow> Some (cap_to_H x)); c_valid_cap capc\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<And>x32 x33 x34 a. \<lbrakk>capa = cap_to_H a; capability.NotificationCap x x32 x33 x34 = cap_to_H a; c_valid_cap capc; cap_lift capc = Some a\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<And>x32 x33 x34 a. \<lbrakk>capa = (case a 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.NotificationCap x x32 x33 x34 = (case a 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); c_valid_cap capc; cap_lift capc = Some a\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (2 subgoals):
 1. \<And>a x4. \<lbrakk>capa = capability.NotificationCap (capNtfnPtr_CL x4) (capNtfnBadge_CL x4) (to_bool (capNtfnCanSend_CL x4)) (to_bool (capNtfnCanReceive_CL x4)); x = capNtfnPtr_CL x4; c_valid_cap capc; cap_lift capc = Some (Cap_notification_cap x4); a = Cap_notification_cap x4\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap
 2. \<And>x32 x33 x34 a x16. \<lbrakk>capa = (if isZombieTCB_C (capZombieType_CL x16) then capability.Zombie (capZombieID_CL x16 && ~~ mask 5) ZombieTCB (unat (capZombieID_CL x16 && mask 5)) else let radix = unat (capZombieType_CL x16) in capability.Zombie (capZombieID_CL x16 && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL x16 && mask (radix + 1)))); capability.NotificationCap x x32 x33 x34 = (if isZombieTCB_C (capZombieType_CL x16) then capability.Zombie (capZombieID_CL x16 && ~~ mask 5) ZombieTCB (unat (capZombieID_CL x16 && mask 5)) else let radix = unat (capZombieType_CL x16) in capability.Zombie (capZombieID_CL x16 && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL x16 && mask (radix + 1)))); c_valid_cap capc; cap_lift capc = Some (Cap_zombie_cap x16); a = Cap_zombie_cap x16\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<And>x32 x33 x34 a x16. \<lbrakk>capa = (if isZombieTCB_C (capZombieType_CL x16) then capability.Zombie (capZombieID_CL x16 && ~~ mask 5) ZombieTCB (unat (capZombieID_CL x16 && mask 5)) else let radix = unat (capZombieType_CL x16) in capability.Zombie (capZombieID_CL x16 && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL x16 && mask (radix + 1)))); capability.NotificationCap x x32 x33 x34 = (if isZombieTCB_C (capZombieType_CL x16) then capability.Zombie (capZombieID_CL x16 && ~~ mask 5) ZombieTCB (unat (capZombieID_CL x16 && mask 5)) else let radix = unat (capZombieType_CL x16) in capability.Zombie (capZombieID_CL x16 && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL x16 && mask (radix + 1)))); c_valid_cap capc; cap_lift capc = Some (Cap_zombie_cap x16); a = Cap_zombie_cap x16\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal (1 subgoal):
 1. \<And>x32 x33 x34 a zombie_cap. \<lbrakk>capa = (if isZombieTCB_C (capZombieType_CL zombie_cap) then capability.Zombie (capZombieID_CL zombie_cap && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zombie_cap && mask 5)) else let radix = unat (capZombieType_CL zombie_cap) in capability.Zombie (capZombieID_CL zombie_cap && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zombie_cap && mask (radix + 1)))); capability.NotificationCap x x32 x33 x34 = (if isZombieTCB_C (capZombieType_CL zombie_cap) then capability.Zombie (capZombieID_CL zombie_cap && ~~ mask 5) ZombieTCB (unat (capZombieID_CL zombie_cap && mask 5)) else let radix = unat (capZombieType_CL zombie_cap) in capability.Zombie (capZombieID_CL zombie_cap && ~~ mask (radix + 1)) (ZombieCNode radix) (unat (capZombieID_CL zombie_cap && mask (radix + 1)))); c_valid_cap capc; cap_lift capc = Some (Cap_zombie_cap zombie_cap); a = Cap_zombie_cap zombie_cap\<rbrakk> \<Longrightarrow> cap_get_tag capc = SCAST(32 signed \<rightarrow> 32) cap_notification_cap proof (prove)
goal:
No subgoals!