theory Orphanage

lemma finaliseCap_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> valid_cap' cap s \<rbrace>
   finaliseCap cap final flag
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" apply (simp add: finaliseCap_def Let_def
              cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp | clarsimp simp: o_def | wpc)+ apply (auto simp: valid_cap'_def dest!: isCapDs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> valid_cap' cap s\<rbrace> global.finaliseCap cap final flag \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> valid_cap' cap s\<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 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> final then return (cap, capability.NullCap) else if isArchObjectCap cap then Arch.finaliseCap (capCap cap) final 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. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q26\<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 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> final then return (cap, capability.NullCap) else if isArchObjectCap cap then Arch.finaliseCap (capCap cap) final 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. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> sch_act_simple s \<and> valid_cap' cap s \<Longrightarrow> ?Q26 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; sch_act_simple s; valid_cap' cap s; final\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> valid_queues' s \<and> valid_objs' s) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> valid_queues' s \<and> valid_objs' s) \<and> (\<not> isNotificationCap cap \<longrightarrow> \<not> isReplyCap cap \<longrightarrow> cap \<noteq> capability.NullCap \<longrightarrow> cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> \<not> isCNodeCap cap \<longrightarrow> isThreadCap cap \<longrightarrow> tcb_at' (capTCBPtr cap) s)) proof (prove)
goal:
No subgoals!