theory Finalise_R

lemma finaliseCap_cases[wp]:
  "\<lbrace>\<top>\<rbrace>
     finaliseCap cap final flag
   \<lbrace>\<lambda>rv s. fst rv = NullCap \<and> (snd rv \<noteq> NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd rv = cap)
     \<or>
       isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = NullCap
        \<and> capUntypedPtr (fst rv) = capUntypedPtr cap
        \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace>" apply (simp add: finaliseCap_def ARM_H.finaliseCap_def Let_def
                   getThreadCSpaceRoot
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply ((wp | simp add: isCap_simps split del: if_split
              | wpc
              | simp only: valid_NullCap fst_conv snd_conv)+)[1] apply (simp only: simp_thms fst_conv snd_conv option.simps if_cancel
                    o_def) apply (intro allI impI conjI TrueI) apply (auto simp add: isCap_simps cap_has_cleanup'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> global.finaliseCap cap final flag \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd rv = cap) \<or> isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = capability.NullCap \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>_. True\<rbrace> if isEndpointCap cap then do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap cap then return (capability.NullCap, capability.NullCap) else if cap = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if flag then fail else if isCNodeCap cap \<and> final then return (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) else if isThreadCap cap \<and> final then do y <- unbindNotification (capTCBPtr cap);
y <- ThreadDecls_H.suspend (capTCBPtr cap);
y <- prepareThreadDelete (capTCBPtr cap);
return (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap)
od else if isZombie cap \<and> final then return (cap, capability.NullCap) else if isArchObjectCap cap then if isASIDPoolCap (capCap cap) \<and> final then do y <- deleteASIDPool (capASIDBase (capCap cap)) (capASIDPool (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) then do y <- deleteASID (the (capPDMappedASID (capCap cap))) (capPDBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) then case the (capPTMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) then case the (capVPMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPage (capVPSize (capCap cap)) a v (capVPBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else return (capability.NullCap, capability.NullCap) else if isIRQHandlerCap cap \<and> final then do y <- deletingIRQHandler (capIRQ cap);
return (capability.NullCap, cap)
od else if isZombie cap \<and> \<not> final then fail else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd rv = cap) \<or> isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = capability.NullCap \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q31\<rbrace> if isEndpointCap cap then do y <- when final (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then do y <- when final (do y <- unbindMaybeNotification (capNtfnPtr cap);
cancelAllSignals (capNtfnPtr cap)
od);
return (capability.NullCap, capability.NullCap)
od else if isReplyCap cap then return (capability.NullCap, capability.NullCap) else if cap = capability.NullCap then return (capability.NullCap, capability.NullCap) else if cap = capability.DomainCap then return (capability.NullCap, capability.NullCap) else if flag then fail else if isCNodeCap cap \<and> final then return (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) else if isThreadCap cap \<and> final then do y <- unbindNotification (capTCBPtr cap);
y <- ThreadDecls_H.suspend (capTCBPtr cap);
y <- prepareThreadDelete (capTCBPtr cap);
return (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap)
od else if isZombie cap \<and> final then return (cap, capability.NullCap) else if isArchObjectCap cap then if isASIDPoolCap (capCap cap) \<and> final then do y <- deleteASIDPool (capASIDBase (capCap cap)) (capASIDPool (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) then do y <- deleteASID (the (capPDMappedASID (capCap cap))) (capPDBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) then case the (capPTMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) then case the (capVPMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPage (capVPSize (capCap cap)) a v (capVPBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else return (capability.NullCap, capability.NullCap) else if isIRQHandlerCap cap \<and> final then do y <- deletingIRQHandler (capIRQ cap);
return (capability.NullCap, cap)
od else if isZombie cap \<and> \<not> final then fail else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd rv = cap) \<or> isZombie (fst rv) \<and> final \<and> \<not> flag \<and> snd rv = capability.NullCap \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)\<rbrace>
 2. \<And>s. True \<Longrightarrow> ?Q31 s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> (isEndpointCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (flag \<longrightarrow> True) \<and> (\<not> flag \<longrightarrow> (isCNodeCap cap \<and> final \<longrightarrow> fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) = capability.NullCap \<and> (snd (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) = cap) \<or> isZombie (fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isCNodeCap cap \<and> final) \<longrightarrow> (isThreadCap cap \<and> final \<longrightarrow> fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap) = capability.NullCap \<and> (snd (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap) = cap) \<or> isZombie (fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isThreadCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> final \<longrightarrow> fst (cap, capability.NullCap) = capability.NullCap \<and> (snd (cap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (cap, capability.NullCap) = cap) \<or> isZombie (fst (cap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (cap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (cap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isZombie cap \<and> final) \<longrightarrow> (isArchObjectCap cap \<longrightarrow> (isASIDPoolCap (capCap cap) \<and> final \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isASIDPoolCap (capCap cap) \<and> final) \<longrightarrow> (isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y)) \<longrightarrow> (isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (capPTMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap))) \<and> (\<not> (isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> (isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (capVPMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> (\<exists>v0 v1 v2. fst (capability.NullCap, capability.NullCap) = capability.Zombie v0 v1 v2) \<and> final \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> ((\<exists>v0. cap = capability.ThreadCap v0) \<or> (\<exists>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3) \<or> (\<exists>v0 v1 v2. cap = capability.Zombie v0 v1 v2)))) \<and> (\<not> (isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)))))) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<and> final \<longrightarrow> fst (capability.NullCap, cap) = capability.NullCap \<and> (snd (capability.NullCap, cap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, cap) = cap) \<or> isZombie (fst (capability.NullCap, cap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, cap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, cap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isIRQHandlerCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> \<not> final \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> \<not> final) \<longrightarrow> fst (capability.NullCap, capability.NullCap) = capability.NullCap \<and> (snd (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap \<and> snd (capability.NullCap, capability.NullCap) = cap) \<or> isZombie (fst (capability.NullCap, capability.NullCap)) \<and> final \<and> \<not> flag \<and> snd (capability.NullCap, capability.NullCap) = capability.NullCap \<and> global.capUntypedPtr (fst (capability.NullCap, capability.NullCap)) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap))))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<not> isEndpointCap cap \<longrightarrow> \<not> isNotificationCap cap \<longrightarrow> \<not> isReplyCap cap \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> (isCNodeCap cap \<and> final \<longrightarrow> capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)) = capability.NullCap \<or> isZombie (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) \<and> final \<and> \<not> flag \<and> global.capUntypedPtr (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isCNodeCap cap \<and> final) \<longrightarrow> (isThreadCap cap \<and> final \<longrightarrow> capability.Zombie (capTCBPtr cap) ZombieTCB 5 = capability.NullCap \<or> isZombie (capability.Zombie (capTCBPtr cap) ZombieTCB 5) \<and> final \<and> \<not> flag \<and> global.capUntypedPtr (capability.Zombie (capTCBPtr cap) ZombieTCB 5) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isThreadCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> final \<longrightarrow> cap = capability.NullCap \<or> isZombie cap \<and> final \<and> \<not> flag \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)) \<and> (\<not> (isZombie cap \<and> final) \<longrightarrow> \<not> isArchObjectCap cap \<longrightarrow> isIRQHandlerCap cap \<and> final \<longrightarrow> (cap \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap) \<or> isZombie capability.NullCap \<and> final \<and> \<not> flag \<and> cap = capability.NullCap \<and> global.capUntypedPtr capability.NullCap = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)))) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>True; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<and> final\<rbrakk> \<Longrightarrow> capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)) = capability.NullCap \<or> isZombie (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) \<and> final \<and> \<not> flag \<and> global.capUntypedPtr (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)
 2. \<And>s. \<lbrakk>True; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; \<not> (isCNodeCap cap \<and> final); isThreadCap cap \<and> final\<rbrakk> \<Longrightarrow> capability.Zombie (capTCBPtr cap) ZombieTCB 5 = capability.NullCap \<or> isZombie (capability.Zombie (capTCBPtr cap) ZombieTCB 5) \<and> final \<and> \<not> flag \<and> global.capUntypedPtr (capability.Zombie (capTCBPtr cap) ZombieTCB 5) = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)
 3. \<And>s. \<lbrakk>True; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; \<not> (isCNodeCap cap \<and> final); \<not> (isThreadCap cap \<and> final); isZombie cap \<and> final\<rbrakk> \<Longrightarrow> cap = capability.NullCap \<or> isZombie cap \<and> final \<and> \<not> flag \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)
 4. \<And>s. \<lbrakk>True; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; \<not> (isCNodeCap cap \<and> final); \<not> (isThreadCap cap \<and> final); \<not> (isZombie cap \<and> final); \<not> isArchObjectCap cap; isIRQHandlerCap cap \<and> final\<rbrakk> \<Longrightarrow> (cap \<noteq> capability.NullCap \<longrightarrow> final \<and> cap_has_cleanup' cap) \<or> isZombie capability.NullCap \<and> final \<and> \<not> flag \<and> cap = capability.NullCap \<and> global.capUntypedPtr capability.NullCap = global.capUntypedPtr cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap) proof (prove)
goal:
No subgoals!