theory Finalise_R

lemma finaliseCap_equal_cap[wp]:
  "\<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>
     finaliseCap cap fin flag
   \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>" apply (simp add: finaliseCap_def Let_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp suspend_cte_wp_at' deletingIRQHandler_cte_preserved
        | clarsimp simp: finaliseCap_def | wpc)+ apply (case_tac cap) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> if isEndpointCap cap then do y <- when fin (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then do y <- when fin (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> fin then return (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) else if isThreadCap cap \<and> fin then do cte_ptr <- getThreadCSpaceRoot (capTCBPtr cap);
y <- unbindNotification (capTCBPtr cap);
y <- ThreadDecls_H.suspend (capTCBPtr cap);
y <- prepareThreadDelete (capTCBPtr cap);
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if isZombie cap \<and> fin then return (cap, capability.NullCap) else if isArchObjectCap cap then Arch.finaliseCap (capCap cap) fin else if isIRQHandlerCap cap \<and> fin then do y <- deletingIRQHandler (capIRQ cap);
return (capability.NullCap, cap)
od else if isZombie cap \<and> \<not> fin then fail else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q26\<rbrace> if isEndpointCap cap then do y <- when fin (cancelAllIPC (capEPPtr cap));
return (capability.NullCap, capability.NullCap)
od else if isNotificationCap cap then do y <- when fin (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> fin then return (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) else if isThreadCap cap \<and> fin then do cte_ptr <- getThreadCSpaceRoot (capTCBPtr cap);
y <- unbindNotification (capTCBPtr cap);
y <- ThreadDecls_H.suspend (capTCBPtr cap);
y <- prepareThreadDelete (capTCBPtr cap);
return (capability.Zombie cte_ptr ZombieTCB 5, capability.NullCap)
od else if isZombie cap \<and> fin then return (cap, capability.NullCap) else if isArchObjectCap cap then Arch.finaliseCap (capCap cap) fin else if isIRQHandlerCap cap \<and> fin then do y <- deletingIRQHandler (capIRQ cap);
return (capability.NullCap, cap)
od else if isZombie cap \<and> \<not> fin then fail else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s \<Longrightarrow> ?Q26 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s) proof (prove)
goal (12 subgoals):
 1. \<And>s x1. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 2. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.NullCap\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 3. \<And>s x31 x32 x33 x34. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 4. \<And>s x4. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 5. \<And>s x51 x52 x53 x54 x55 x56. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 6. \<And>s. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.DomainCap\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 7. \<And>s x71 x72 x73. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 8. \<And>s x8. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 9. \<And>s x91 x92 x93. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
 10. \<And>s x101 x102 x103 x104. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) sl s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.DomainCap) sl s)
A total of 12 subgoals... proof (prove)
goal:
No subgoals!