theory Finalise_R

lemma (in delete_one_conc_pre) finaliseCap_replaceable:
  "\<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s
       \<and> (final_matters' cap \<longrightarrow> (final = isFinal cap slot (cteCaps_of s)))
       \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
     finaliseCap cap final flag
   \<lbrace>\<lambda>rv s. (isNullCap (fst rv) \<and> removeable' slot s cap
                \<and> (snd rv \<noteq> NullCap \<longrightarrow> snd rv = cap \<and> cap_has_cleanup' cap
                                      \<and> isFinal cap slot (cteCaps_of s)))
        \<or>
          (isZombie (fst rv) \<and> snd rv = NullCap
            \<and> isFinal cap slot (cteCaps_of s)
            \<and> capClass cap = capClass (fst rv)
            \<and> capUntypedPtr (fst rv) = capUntypedPtr cap
            \<and> capBits (fst rv) = capBits cap
            \<and> capRange (fst rv) = capRange cap
            \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap)
            \<and> (\<forall>p \<in> threadCapRefs cap. st_tcb_at' ((=) Inactive) p s
                     \<and> obj_at' (Not \<circ> tcbQueued) p s
                     \<and> bound_tcb_at' ((=) None) p s
                     \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr))))\<rbrace>" apply (simp add: finaliseCap_def Let_def getThreadCSpaceRoot
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp prepares_delete_helper'' [OF cancelAllIPC_unlive]
             prepares_delete_helper'' [OF cancelAllSignals_unlive]
             suspend_isFinal prepareThreadDelete_unqueued prepareThreadDelete_nonq
             prepareThreadDelete_inactive prepareThreadDelete_isFinal
             suspend_makes_inactive suspend_nonq
             deletingIRQHandler_removeable'
             deletingIRQHandler_final[where slot=slot ]
             unbindMaybeNotification_obj_at'_bound
             getNotification_wp
             suspend_bound_tcb_at'
             unbindNotification_bound_tcb_at'
           | simp add: isZombie_Null isThreadCap_threadCapRefs_tcbptr
                       isArchObjectCap_Cap_capCap
           | (rule hoare_strengthen_post [OF arch_finaliseCap_removeable[where slot=slot]],
                  clarsimp simp: isCap_simps)
           | wpc)+ apply clarsimp apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp+) apply (case_tac "cteCap cte",
         simp_all add: isCap_simps capRange_def cap_has_cleanup'_def
                       final_matters'_def objBits_simps
                       not_Final_removeable finaliseCap_def,
         simp_all add: removeable'_def) 
     (* thread *)
      apply (frule capAligned_capUntypedPtr [OF valid_capAligned], simp) apply (clarsimp simp: valid_cap'_def) apply (drule valid_globals_cte_wpD'[rotated], clarsimp) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) apply (clarsimp simp: obj_at'_def | rule conjI)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (final_matters' cap \<longrightarrow> final = isFinal cap slot (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace> global.finaliseCap cap final flag \<lbrace>\<lambda>rv s. isNullCap (fst rv) \<and> removeable' slot s cap \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cap \<and> cap_has_cleanup' cap \<and> isFinal cap slot (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr cap \<and> capBits (fst rv) = capBits cap \<and> capRange (fst rv) = capRange cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap) \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>pr. p \<notin> set (ksReadyQueues s pr)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (final_matters' cap \<longrightarrow> final = isFinal cap slot (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) 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 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 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 s. fst rv = capability.NullCap \<and> removeable' slot s cap \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cap \<and> cap_has_cleanup' cap \<and> isFinal cap slot (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr cap \<and> capBits (fst rv) = capBits cap \<and> capRange (fst rv) = capRange cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap) \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))\<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 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 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 s. fst rv = capability.NullCap \<and> removeable' slot s cap \<and> (snd rv \<noteq> capability.NullCap \<longrightarrow> snd rv = cap \<and> cap_has_cleanup' cap \<and> isFinal cap slot (cteCaps_of s)) \<or> isZombie (fst rv) \<and> snd rv = capability.NullCap \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = capClass (fst rv) \<and> global.capUntypedPtr (fst rv) = global.capUntypedPtr cap \<and> capBits (fst rv) = capBits cap \<and> capRange (fst rv) = capRange cap \<and> (isThreadCap cap \<or> isCNodeCap cap \<or> isZombie cap) \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))\<rbrace>
 2. \<And>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (final_matters' cap \<longrightarrow> final = isFinal cap slot (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> ?Q26 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s \<and> (final_matters' cap \<longrightarrow> final = isFinal cap slot (cteCaps_of s)) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<Longrightarrow> (final \<longrightarrow> (isEndpointCap cap \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {capEPPtr cap} \<and> threadCapRefs cap = {}) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {capNtfnPtr cap} \<and> threadCapRefs cap = {}) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> removeable' slot s capability.NullCap) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> removeable' slot s capability.DomainCap) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> (isCNodeCap cap \<longrightarrow> isZombie (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = PhysicalClass \<and> capCNodePtr cap = global.capUntypedPtr cap \<and> objBits undefined + capCNodeBits cap = capBits cap \<and> capRange (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) = capRange cap \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))) \<and> (\<not> isCNodeCap cap \<longrightarrow> (isThreadCap cap \<longrightarrow> isZombie (capability.Zombie (capTCBPtr cap) ZombieTCB 5) \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = PhysicalClass \<and> capTCBPtr cap = global.capUntypedPtr cap \<and> tcbBlockSizeBits = capBits cap \<and> capRange (capability.Zombie (capTCBPtr cap) ZombieTCB 5) = capRange cap \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> tcb_at' (capTCBPtr cap) s \<and> capTCBPtr cap \<noteq> ksIdleThread s) \<and> (\<not> isThreadCap cap \<longrightarrow> (isZombie cap \<longrightarrow> isFinal cap slot (cteCaps_of s) \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))) \<and> (\<not> isZombie cap \<longrightarrow> (isArchObjectCap cap \<longrightarrow> valid_cap' cap s \<and> (final_matters' cap \<longrightarrow> isFinal cap slot (cteCaps_of s))) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<longrightarrow> isFinal (capability.IRQHandlerCap (capIRQ cap)) slot (cteCaps_of s) \<and> cap = capability.IRQHandlerCap (capIRQ cap) \<and> cap_has_cleanup' cap \<and> isFinal cap slot (cteCaps_of s) \<and> (\<forall>final. global.finaliseCap cap final True = fail)) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> removeable' slot s cap))))))))))) \<and> (\<not> final \<longrightarrow> (isEndpointCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> removeable' slot s capability.NullCap) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> removeable' slot s capability.DomainCap) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> (isArchObjectCap cap \<longrightarrow> valid_cap' cap s) \<and> (\<not> isArchObjectCap cap \<longrightarrow> \<not> isZombie cap \<longrightarrow> removeable' slot s cap))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = cap) slot s; final_matters' cap \<longrightarrow> final = isFinal cap slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s\<rbrakk> \<Longrightarrow> (final \<longrightarrow> (isEndpointCap cap \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {capEPPtr cap} \<and> threadCapRefs cap = {}) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>x. cte_refs' cap x = {}) \<and> zobj_refs' cap = {capNtfnPtr cap} \<and> threadCapRefs cap = {}) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> removeable' slot s capability.NullCap) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> removeable' slot s capability.DomainCap) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> (isCNodeCap cap \<longrightarrow> isZombie (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = PhysicalClass \<and> capCNodePtr cap = global.capUntypedPtr cap \<and> objBits undefined + capCNodeBits cap = capBits cap \<and> capRange (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap))) = capRange cap \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))) \<and> (\<not> isCNodeCap cap \<longrightarrow> (isThreadCap cap \<longrightarrow> isZombie (capability.Zombie (capTCBPtr cap) ZombieTCB 5) \<and> isFinal cap slot (cteCaps_of s) \<and> capClass cap = PhysicalClass \<and> capTCBPtr cap = global.capUntypedPtr cap \<and> tcbBlockSizeBits = capBits cap \<and> capRange (capability.Zombie (capTCBPtr cap) ZombieTCB 5) = capRange cap \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> tcb_at' (capTCBPtr cap) s \<and> capTCBPtr cap \<noteq> ksIdleThread s) \<and> (\<not> isThreadCap cap \<longrightarrow> (isZombie cap \<longrightarrow> isFinal cap slot (cteCaps_of s) \<and> (\<forall>p\<in>threadCapRefs cap. st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))) \<and> (\<not> isZombie cap \<longrightarrow> (isArchObjectCap cap \<longrightarrow> valid_cap' cap s \<and> (final_matters' cap \<longrightarrow> isFinal cap slot (cteCaps_of s))) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<longrightarrow> isFinal (capability.IRQHandlerCap (capIRQ cap)) slot (cteCaps_of s) \<and> cap = capability.IRQHandlerCap (capIRQ cap) \<and> cap_has_cleanup' cap \<and> isFinal cap slot (cteCaps_of s) \<and> (\<forall>final. global.finaliseCap cap final True = fail)) \<and> (\<not> isIRQHandlerCap cap \<longrightarrow> removeable' slot s cap))))))))))) \<and> (\<not> final \<longrightarrow> (isEndpointCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> removeable' slot s cap) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> removeable' slot s capability.NullCap) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> removeable' slot s capability.DomainCap) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> (isArchObjectCap cap \<longrightarrow> valid_cap' cap s) \<and> (\<not> isArchObjectCap cap \<longrightarrow> \<not> isZombie cap \<longrightarrow> removeable' slot s cap))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>invs' s; cte_wp_at' (\<lambda>ctea. cteCap ctea = cteCap cte) slot s; final_matters' (cteCap cte) \<longrightarrow> final = isFinal (cteCap cte) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (cteCap cte) s; cap = cteCap cte\<rbrakk> \<Longrightarrow> (final \<longrightarrow> (isEndpointCap (cteCap cte) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>x. cte_refs' (cteCap cte) x = {}) \<and> zobj_refs' (cteCap cte) = {capEPPtr (cteCap cte)} \<and> threadCapRefs (cteCap cte) = {}) \<and> (\<not> isEndpointCap (cteCap cte) \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>x. cte_refs' (cteCap cte) x = {}) \<and> zobj_refs' (cteCap cte) = {capNtfnPtr (cteCap cte)} \<and> threadCapRefs (cteCap cte) = {}) \<and> (\<not> isNotificationCap (cteCap cte) \<longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> removeable' slot s (cteCap cte)) \<and> (\<not> isReplyCap (cteCap cte) \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> removeable' slot s capability.NullCap) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cteCap cte = capability.DomainCap \<longrightarrow> removeable' slot s capability.DomainCap) \<and> (cteCap cte \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> (isCNodeCap (cteCap cte) \<longrightarrow> isZombie (capability.Zombie (capCNodePtr (cteCap cte)) (ZombieCNode (capCNodeBits (cteCap cte))) (shiftL (Suc 0) (capCNodeBits (cteCap cte)))) \<and> isFinal (cteCap cte) slot (cteCaps_of s) \<and> capClass (cteCap cte) = PhysicalClass \<and> capCNodePtr (cteCap cte) = global.capUntypedPtr (cteCap cte) \<and> objBits undefined + capCNodeBits (cteCap cte) = capBits (cteCap cte) \<and> capRange (capability.Zombie (capCNodePtr (cteCap cte)) (ZombieCNode (capCNodeBits (cteCap cte))) (shiftL (Suc 0) (capCNodeBits (cteCap cte)))) = capRange (cteCap cte) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))) \<and> (\<not> isCNodeCap (cteCap cte) \<longrightarrow> (isThreadCap (cteCap cte) \<longrightarrow> isZombie (capability.Zombie (capTCBPtr (cteCap cte)) ZombieTCB 5) \<and> isFinal (cteCap cte) slot (cteCaps_of s) \<and> capClass (cteCap cte) = PhysicalClass \<and> capTCBPtr (cteCap cte) = global.capUntypedPtr (cteCap cte) \<and> tcbBlockSizeBits = capBits (cteCap cte) \<and> capRange (capability.Zombie (capTCBPtr (cteCap cte)) ZombieTCB 5) = capRange (cteCap cte) \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> tcb_at' (capTCBPtr (cteCap cte)) s \<and> capTCBPtr (cteCap cte) \<noteq> ksIdleThread s) \<and> (\<not> isThreadCap (cteCap cte) \<longrightarrow> (isZombie (cteCap cte) \<longrightarrow> isFinal (cteCap cte) slot (cteCaps_of s) \<and> (\<forall>p\<in>threadCapRefs (cteCap cte). st_tcb_at' ((=) Structures_H.thread_state.Inactive) p s \<and> obj_at' (Not \<circ> tcbQueued) p s \<and> bound_tcb_at' ((=) None) p s \<and> (\<forall>a b. p \<notin> set (ksReadyQueues s (a, b))))) \<and> (\<not> isZombie (cteCap cte) \<longrightarrow> (isArchObjectCap (cteCap cte) \<longrightarrow> final_matters' (cteCap cte) \<longrightarrow> isFinal (cteCap cte) slot (cteCaps_of s)) \<and> (\<not> isArchObjectCap (cteCap cte) \<longrightarrow> (isIRQHandlerCap (cteCap cte) \<longrightarrow> isFinal (capability.IRQHandlerCap (capIRQ (cteCap cte))) slot (cteCaps_of s) \<and> cteCap cte = capability.IRQHandlerCap (capIRQ (cteCap cte)) \<and> cap_has_cleanup' (cteCap cte) \<and> isFinal (cteCap cte) slot (cteCaps_of s) \<and> (\<forall>final. global.finaliseCap (cteCap cte) final True = fail)) \<and> (\<not> isIRQHandlerCap (cteCap cte) \<longrightarrow> removeable' slot s (cteCap cte)))))))))))) \<and> (\<not> final \<longrightarrow> (isEndpointCap (cteCap cte) \<longrightarrow> removeable' slot s (cteCap cte)) \<and> (\<not> isEndpointCap (cteCap cte) \<longrightarrow> (isNotificationCap (cteCap cte) \<longrightarrow> removeable' slot s (cteCap cte)) \<and> (\<not> isNotificationCap (cteCap cte) \<longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> removeable' slot s (cteCap cte)) \<and> (\<not> isReplyCap (cteCap cte) \<longrightarrow> (cteCap cte = capability.NullCap \<longrightarrow> removeable' slot s capability.NullCap) \<and> (cteCap cte \<noteq> capability.NullCap \<longrightarrow> (cteCap cte = capability.DomainCap \<longrightarrow> removeable' slot s capability.DomainCap) \<and> (cteCap cte \<noteq> capability.DomainCap \<longrightarrow> \<not> flag \<longrightarrow> \<not> isArchObjectCap (cteCap cte) \<longrightarrow> \<not> isZombie (cteCap cte) \<longrightarrow> removeable' slot s (cteCap cte))))))) proof (prove)
goal (4 subgoals):
 1. \<And>s cte x1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ThreadCap x1) slot s; final = isFinal (capability.ThreadCap x1) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ThreadCap x1) s; cap = capability.ThreadCap x1; cteCap cte = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> isFinal (capability.ThreadCap x1) slot (cteCaps_of s) \<longrightarrow> \<not> flag \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> tcb_at' x1 s \<and> x1 \<noteq> ksIdleThread s
 2. \<And>s cte x31 x32 x33 x34. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NotificationCap x31 x32 x33 x34) slot s; final = isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.NotificationCap x31 x32 x33 x34) s; cap = capability.NotificationCap x31 x32 x33 x34; cteCap cte = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 3. \<And>s cte x51 x52 x53 x54 x55 x56. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) slot s; final = isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) s; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56; cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 4. \<And>s cte x8. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) slot s; (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> final = isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ArchObjectCap x8) s; cap = capability.ArchObjectCap x8; cteCap cte = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> final \<longrightarrow> \<not> flag \<longrightarrow> (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s) proof (prove)
goal (4 subgoals):
 1. \<And>s cte x1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ThreadCap x1) slot s; final = isFinal (capability.ThreadCap x1) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ThreadCap x1) s; cap = capability.ThreadCap x1; cteCap cte = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> isFinal (capability.ThreadCap x1) slot (cteCaps_of s) \<longrightarrow> \<not> flag \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> tcb_at' x1 s \<and> x1 \<noteq> ksIdleThread s
 2. \<And>s cte x31 x32 x33 x34. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NotificationCap x31 x32 x33 x34) slot s; final = isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.NotificationCap x31 x32 x33 x34) s; cap = capability.NotificationCap x31 x32 x33 x34; cteCap cte = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 3. \<And>s cte x51 x52 x53 x54 x55 x56. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) slot s; final = isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) s; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56; cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 4. \<And>s cte x8. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) slot s; (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> final = isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ArchObjectCap x8) s; cap = capability.ArchObjectCap x8; cteCap cte = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> final \<longrightarrow> \<not> flag \<longrightarrow> (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s) proof (prove)
goal (4 subgoals):
 1. \<And>s cte x1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ThreadCap x1) slot s; final = isFinal (capability.ThreadCap x1) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ThreadCap x1) s; cap = capability.ThreadCap x1; cteCap cte = capability.ThreadCap x1; global.capUntypedPtr (capability.ThreadCap x1) \<in> capRange (capability.ThreadCap x1)\<rbrakk> \<Longrightarrow> isFinal (capability.ThreadCap x1) slot (cteCaps_of s) \<longrightarrow> \<not> flag \<longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> tcb_at' x1 s \<and> x1 \<noteq> ksIdleThread s
 2. \<And>s cte x31 x32 x33 x34. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NotificationCap x31 x32 x33 x34) slot s; final = isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.NotificationCap x31 x32 x33 x34) s; cap = capability.NotificationCap x31 x32 x33 x34; cteCap cte = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 3. \<And>s cte x51 x52 x53 x54 x55 x56. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) slot s; final = isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) s; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56; cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 4. \<And>s cte x8. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) slot s; (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> final = isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ArchObjectCap x8) s; cap = capability.ArchObjectCap x8; cteCap cte = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> final \<longrightarrow> \<not> flag \<longrightarrow> (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s) proof (prove)
goal (4 subgoals):
 1. \<And>s cte x1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ThreadCap x1) slot s; weak_sch_act_wf (ksSchedulerAction s) s; cap = capability.ThreadCap x1; cteCap cte = capability.ThreadCap x1; x1 \<in> capRange (capability.ThreadCap x1); capAligned (capability.ThreadCap x1); tcb_at' x1 s; \<not> flag; final; isFinal (capability.ThreadCap x1) slot (cteCaps_of s)\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> x1 \<noteq> ksIdleThread s
 2. \<And>s cte x31 x32 x33 x34. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NotificationCap x31 x32 x33 x34) slot s; final = isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.NotificationCap x31 x32 x33 x34) s; cap = capability.NotificationCap x31 x32 x33 x34; cteCap cte = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 3. \<And>s cte x51 x52 x53 x54 x55 x56. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) slot s; final = isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) s; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56; cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 4. \<And>s cte x8. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) slot s; (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> final = isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ArchObjectCap x8) s; cap = capability.ArchObjectCap x8; cteCap cte = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> final \<longrightarrow> \<not> flag \<longrightarrow> (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s) proof (prove)
goal (4 subgoals):
 1. \<And>s cte x1. \<lbrakk>invs' s; weak_sch_act_wf (ksSchedulerAction s) s; cap = capability.ThreadCap x1; cteCap cte = capability.ThreadCap x1; x1 \<in> capRange (capability.ThreadCap x1); capAligned (capability.ThreadCap x1); tcb_at' x1 s; \<not> flag; final; isFinal (capability.ThreadCap x1) slot (cteCaps_of s); \<exists>cte. cteCap cte = capability.ThreadCap x1 \<and> ksIdleThread s \<notin> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s \<and> valid_objs' s \<and> x1 \<noteq> ksIdleThread s
 2. \<And>s cte x31 x32 x33 x34. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NotificationCap x31 x32 x33 x34) slot s; final = isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.NotificationCap x31 x32 x33 x34) s; cap = capability.NotificationCap x31 x32 x33 x34; cteCap cte = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 3. \<And>s cte x51 x52 x53 x54 x55 x56. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) slot s; final = isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) s; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56; cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 4. \<And>s cte x8. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) slot s; (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> final = isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ArchObjectCap x8) s; cap = capability.ArchObjectCap x8; cteCap cte = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> final \<longrightarrow> \<not> flag \<longrightarrow> (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s) proof (prove)
goal (3 subgoals):
 1. \<And>s cte x31 x32 x33 x34. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.NotificationCap x31 x32 x33 x34) slot s; final = isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.NotificationCap x31 x32 x33 x34) s; cap = capability.NotificationCap x31 x32 x33 x34; cteCap cte = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> isFinal (capability.NotificationCap x31 x32 x33 x34) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 2. \<And>s cte x51 x52 x53 x54 x55 x56. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56) slot s; final = isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.EndpointCap x51 x52 x53 x54 x55 x56) s; cap = capability.EndpointCap x51 x52 x53 x54 x55 x56; cteCap cte = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> isFinal (capability.EndpointCap x51 x52 x53 x54 x55 x56) slot (cteCaps_of s) \<longrightarrow> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s
 3. \<And>s cte x8. \<lbrakk>invs' s; cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) slot s; (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> final = isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s); weak_sch_act_wf (ksSchedulerAction s) s; valid_cap' (capability.ArchObjectCap x8) s; cap = capability.ArchObjectCap x8; cteCap cte = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> final \<longrightarrow> \<not> flag \<longrightarrow> (case x8 of ARM_H.ASIDControlCap \<Rightarrow> False | ARM_H.PageCap d ref rghts sz mapdata \<Rightarrow> False | _ \<Rightarrow> True) \<longrightarrow> isFinal (capability.ArchObjectCap x8) slot (cteCaps_of s) proof (prove)
goal:
No subgoals!