theory Finalise_R

lemma finaliseCap_cte_cap_wp_to[wp]:
  "\<lbrace>ex_cte_cap_wp_to' P sl\<rbrace> finaliseCap cap fin flag \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P sl\<rbrace>" apply (simp add: ex_cte_cap_to'_def) apply (rule hoare_pre, rule hoare_use_eq_irq_node' [OF finaliseCap_irq_node']) apply (simp add: finaliseCap_def Let_def
              cong: if_cong split del: if_split) apply (wp suspend_cte_wp_at'
             deletingIRQHandler_cte_preserved
             hoare_vcg_ex_lift
                 | clarsimp simp: finaliseCap_def isCap_simps
                 | rule conjI
                 | wpc)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_cte_cap_wp_to' P sl\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' P sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) cref s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) f) cref s\<rbrace>
 2. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P3 f\<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 <- Arch.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 s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) f) cref s\<rbrace>
 2. \<And>s. \<exists>cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> ?P3 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s cref. cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) cref s \<Longrightarrow> \<exists>x. ((\<exists>v0 v1 v2 v3 v4 v5. cap = capability.EndpointCap v0 v1 v2 v3 v4 v5) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2 v3 v4 v5. cap \<noteq> capability.EndpointCap v0 v1 v2 v3 v4 v5) \<longrightarrow> ((\<exists>v0 v1 v2 v3. cap = capability.NotificationCap v0 v1 v2 v3) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2 v3. cap \<noteq> capability.NotificationCap v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1 v2. cap = capability.ReplyCap v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.ReplyCap v0 v1 v2) \<longrightarrow> (cap = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> ((\<exists>v0 v1 v2 v3. cap = capability.CNodeCap v0 v1 v2 v3) \<and> fin \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2 v3. cap \<noteq> capability.CNodeCap v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0. cap = capability.ThreadCap v0) \<and> fin \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> sl \<in> cte_refs' (cteCap cte) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ThreadCap v0) \<longrightarrow> ((\<exists>v0 v1 v2. cap = capability.Zombie v0 v1 v2) \<and> fin \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<exists>v0. cap = capability.IRQHandlerCap v0) \<and> fin \<longrightarrow> cte_wp_at' (\<lambda>cte. P (cteCap cte) \<and> sl \<in> cte_refs' (cteCap cte) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s \<and> (fin \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)) \<and> (\<not> fin \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s))) \<and> (\<not> fin \<longrightarrow> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> (\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)))) \<and> (\<not> fin \<longrightarrow> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)) \<and> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> (\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)))) \<and> (\<not> fin \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.ThreadCap v0) \<longrightarrow> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)) \<and> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> (\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s))) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)) \<and> ((\<exists>v0. cap = capability.ArchObjectCap v0) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0. cap \<noteq> capability.ArchObjectCap v0) \<longrightarrow> ((\<forall>v0. cap \<noteq> capability.IRQHandlerCap v0) \<longrightarrow> (\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s) \<and> ((\<forall>v0 v1 v2. cap \<noteq> capability.Zombie v0 v1 v2) \<longrightarrow> cte_wp_at' (\<lambda>c. P (cteCap c) \<and> sl \<in> cte_refs' (cteCap c) (irq_node' s)) x s)))))))) proof (prove)
goal:
No subgoals!