theory Finalise_R

lemma finaliseCap_invs:
  "\<lbrace>invs' and sch_act_simple and valid_cap' cap
         and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace>
     finaliseCap cap fin flag
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: finaliseCap_def Let_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp hoare_drop_imps hoare_vcg_all_lift | simp only: o_def | wpc)+ apply clarsimp apply (intro conjI impI) apply (clarsimp dest!: isCapDs simp: valid_cap'_def) apply (drule invs_valid_global', drule(1) valid_globals_cte_wpD') apply (drule valid_capAligned, drule capAligned_capUntypedPtr) apply (clarsimp dest!: isCapDs) apply (clarsimp dest!: isCapDs) apply (clarsimp dest!: isCapDs) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and valid_cap' cap and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl\<rbrace> global.finaliseCap cap fin flag \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and sch_act_simple and valid_cap' cap and 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 <- 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. invs'\<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 <- 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. invs'\<rbrace>
 2. \<And>s. (invs' and sch_act_simple and valid_cap' cap and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl) s \<Longrightarrow> ?Q26 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and sch_act_simple and valid_cap' cap and cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl) s \<Longrightarrow> (isEndpointCap cap \<longrightarrow> (if fin then invs' else invs') s) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> (if fin then invs' else invs') s) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> invs' s) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> invs' s) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> invs' s) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (flag \<longrightarrow> True) \<and> (\<not> flag \<longrightarrow> (isCNodeCap cap \<and> fin \<longrightarrow> invs' s) \<and> (\<not> (isCNodeCap cap \<and> fin) \<longrightarrow> (isThreadCap cap \<and> fin \<longrightarrow> invs' s \<and> sch_act_simple s \<and> tcb_at' (capTCBPtr cap) s \<and> capTCBPtr cap \<noteq> ksIdleThread s) \<and> (\<not> (isThreadCap cap \<and> fin) \<longrightarrow> (isZombie cap \<and> fin \<longrightarrow> invs' s) \<and> (\<not> (isZombie cap \<and> fin) \<longrightarrow> (isArchObjectCap cap \<longrightarrow> (invs' and valid_cap' (capability.ArchObjectCap (capCap cap))) s) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<and> fin \<longrightarrow> invs' s) \<and> (\<not> (isIRQHandlerCap cap \<and> fin) \<longrightarrow> (isZombie cap \<and> \<not> fin \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> \<not> fin) \<longrightarrow> invs' s)))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin\<rbrakk> \<Longrightarrow> (isThreadCap cap \<and> fin \<longrightarrow> tcb_at' (capTCBPtr cap) s \<and> capTCBPtr cap \<noteq> ksIdleThread s) \<and> ((isThreadCap cap \<longrightarrow> \<not> fin) \<longrightarrow> (isZombie cap \<longrightarrow> \<not> fin) \<longrightarrow> isArchObjectCap cap \<longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin\<rbrakk> \<Longrightarrow> tcb_at' (capTCBPtr cap) s
 2. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin\<rbrakk> \<Longrightarrow> capTCBPtr cap \<noteq> ksIdleThread s
 3. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<longrightarrow> \<not> fin; isZombie cap \<longrightarrow> \<not> fin; isArchObjectCap cap\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin\<rbrakk> \<Longrightarrow> capTCBPtr cap \<noteq> ksIdleThread s
 2. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<longrightarrow> \<not> fin; isZombie cap \<longrightarrow> \<not> fin; isArchObjectCap cap\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin; \<exists>cte. cteCap cte = cap \<and> ksIdleThread s \<notin> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> capTCBPtr cap \<noteq> ksIdleThread s
 2. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<longrightarrow> \<not> fin; isZombie cap \<longrightarrow> \<not> fin; isArchObjectCap cap\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin; \<exists>cte. cteCap cte = cap \<and> ksIdleThread s \<notin> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
 2. \<And>s. \<lbrakk>sch_act_simple s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin; \<exists>cte. cteCap cte = cap \<and> ksIdleThread s \<notin> capRange (cteCap cte); global.capUntypedPtr cap \<in> capRange cap\<rbrakk> \<Longrightarrow> capTCBPtr cap \<noteq> ksIdleThread s
 3. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<longrightarrow> \<not> fin; isZombie cap \<longrightarrow> \<not> fin; isArchObjectCap cap\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<and> fin; \<exists>cte. cteCap cte = cap \<and> ksIdleThread s \<notin> capRange (cteCap cte); global.capUntypedPtr cap \<in> capRange cap\<rbrakk> \<Longrightarrow> capTCBPtr cap \<noteq> ksIdleThread s
 2. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<longrightarrow> \<not> fin; isZombie cap \<longrightarrow> \<not> fin; isArchObjectCap cap\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; valid_cap' cap s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) sl s; \<not> isEndpointCap cap; \<not> isNotificationCap cap; \<not> isReplyCap cap; cap \<noteq> capability.NullCap; cap \<noteq> capability.DomainCap; \<not> flag; isCNodeCap cap \<longrightarrow> \<not> fin; isThreadCap cap \<longrightarrow> \<not> fin; isZombie cap \<longrightarrow> \<not> fin; isArchObjectCap cap\<rbrakk> \<Longrightarrow> valid_cap' (capability.ArchObjectCap (capCap cap)) s proof (prove)
goal:
No subgoals!