theory Finalise_R

lemma finaliseCap_valid_cap[wp]:
  "\<lbrace>valid_cap' cap\<rbrace> finaliseCap cap final flag \<lbrace>\<lambda>rv. valid_cap' (fst rv)\<rbrace>" apply (simp add: finaliseCap_def Let_def
                   getThreadCSpaceRoot
                   ARM_H.finaliseCap_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp | simp only: valid_NullCap o_def fst_conv | wpc)+ apply simp apply (intro conjI impI) apply (clarsimp simp: valid_cap'_def isCap_simps capAligned_def
                         objBits_simps shiftL_nat)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<rbrace> global.finaliseCap cap final flag \<lbrace>\<lambda>rv. valid_cap' (fst rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<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 <- Arch.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 ARM_H.isASIDPoolCap (capCap cap) \<and> final then do y <- ARM_H.deleteASIDPool (ARM_H.capASIDBase (capCap cap)) (ARM_H.capASIDPool (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if ARM_H.isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. ARM_H.capPDMappedASID (capCap cap) = Some y) then do y <- ARM_H.deleteASID (the (ARM_H.capPDMappedASID (capCap cap))) (ARM_H.capPDBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if ARM_H.isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. ARM_H.capPTMappedAddress (capCap cap) = Some (a, b)) then case the (ARM_H.capPTMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- ARM_H.unmapPageTable a v (ARM_H.capPTBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if ARM_H.isPageCap (capCap cap) \<and> (\<exists>a b. ARM_H.capVPMappedAddress (capCap cap) = Some (a, b)) then case the (ARM_H.capVPMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- ARM_H.unmapPage (ARM_H.capVPSize (capCap cap)) a v (ARM_H.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. valid_cap' (fst rv)\<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 <- Arch.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 ARM_H.isASIDPoolCap (capCap cap) \<and> final then do y <- ARM_H.deleteASIDPool (ARM_H.capASIDBase (capCap cap)) (ARM_H.capASIDPool (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if ARM_H.isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. ARM_H.capPDMappedASID (capCap cap) = Some y) then do y <- ARM_H.deleteASID (the (ARM_H.capPDMappedASID (capCap cap))) (ARM_H.capPDBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if ARM_H.isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. ARM_H.capPTMappedAddress (capCap cap) = Some (a, b)) then case the (ARM_H.capPTMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- ARM_H.unmapPageTable a v (ARM_H.capPTBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if ARM_H.isPageCap (capCap cap) \<and> (\<exists>a b. ARM_H.capVPMappedAddress (capCap cap) = Some (a, b)) then case the (ARM_H.capVPMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- ARM_H.unmapPage (ARM_H.capVPSize (capCap cap)) a v (ARM_H.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. valid_cap' (fst rv)\<rbrace>
 2. \<And>s. valid_cap' cap s \<Longrightarrow> ?Q31 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_cap' cap s \<Longrightarrow> (isEndpointCap cap \<longrightarrow> (if final then \<lambda>s. True else (\<lambda>a. True)) s) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (if final then \<lambda>s. True else (\<lambda>a. True)) s) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> True) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> True) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> True) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (flag \<longrightarrow> True) \<and> (\<not> flag \<longrightarrow> (isCNodeCap cap \<and> final \<longrightarrow> valid_cap' (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) s) \<and> (\<not> (isCNodeCap cap \<and> final) \<longrightarrow> (isThreadCap cap \<and> final \<longrightarrow> valid_cap' (capability.Zombie (capTCBPtr cap) ZombieTCB 5) s) \<and> (\<not> (isThreadCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> final \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> final) \<longrightarrow> (isArchObjectCap cap \<longrightarrow> (ARM_H.isASIDPoolCap (capCap cap) \<and> final \<longrightarrow> True) \<and> (\<not> (ARM_H.isASIDPoolCap (capCap cap) \<and> final) \<longrightarrow> (ARM_H.isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. ARM_H.capPDMappedASID (capCap cap) = Some y) \<longrightarrow> True) \<and> (\<not> (ARM_H.isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. ARM_H.capPDMappedASID (capCap cap) = Some y)) \<longrightarrow> (ARM_H.isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. ARM_H.capPTMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (ARM_H.capPTMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> True)) \<and> (\<not> (ARM_H.isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. ARM_H.capPTMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> (ARM_H.isPageCap (capCap cap) \<and> (\<exists>a b. ARM_H.capVPMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (ARM_H.capVPMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> True)) \<and> (\<not> (ARM_H.isPageCap (capCap cap) \<and> (\<exists>a b. ARM_H.capVPMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> True))))) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<and> final \<longrightarrow> True) \<and> (\<not> (isIRQHandlerCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> \<not> final \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> \<not> final) \<longrightarrow> True)))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_cap' cap s \<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> valid_cap' (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) s) \<and> ((isCNodeCap cap \<longrightarrow> \<not> final) \<longrightarrow> isThreadCap cap \<and> final \<longrightarrow> valid_cap' (capability.Zombie (capTCBPtr cap) ZombieTCB 5) s) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_cap' cap s; \<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> valid_cap' (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) s
 2. \<And>s. \<lbrakk>valid_cap' cap s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> final; isThreadCap cap \<and> final\<rbrakk> \<Longrightarrow> valid_cap' (capability.Zombie (capTCBPtr cap) ZombieTCB 5) s proof (prove)
goal:
No subgoals!