theory Finalise_R

lemma finaliseCap_cte_refs:
  "\<lbrace>\<lambda>s. s \<turnstile>' cap\<rbrace>
     finaliseCap cap final flag
   \<lbrace>\<lambda>rv s. fst rv \<noteq> NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace>" apply (simp  add: finaliseCap_def Let_def getThreadCSpaceRoot
                    ARM_H.finaliseCap_def
             cong: if_cong split del: if_split) apply (rule hoare_pre) apply (wp | wpc | simp only: o_def)+ apply (frule valid_capAligned) apply (cases cap, simp_all add: isCap_simps) apply (clarsimp simp: tcb_cte_cases_def word_count_from_top objBits_defs) apply clarsimp apply (rule ext, simp) apply (rule image_cong [OF _ refl]) apply (fastforce simp: capAligned_def objBits_simps shiftL_nat) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<rbrace> global.finaliseCap cap final flag \<lbrace>\<lambda>rv s. fst rv \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_cap' cap\<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 <- 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 if isASIDPoolCap (capCap cap) \<and> final then do y <- deleteASIDPool (capASIDBase (capCap cap)) (capASIDPool (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) then do y <- deleteASID (the (capPDMappedASID (capCap cap))) (capPDBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) then case the (capPTMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) then case the (capVPMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPage (capVPSize (capCap cap)) a v (capVPBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else return (capability.NullCap, capability.NullCap) 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 \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q31\<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 <- 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 if isASIDPoolCap (capCap cap) \<and> final then do y <- deleteASIDPool (capASIDBase (capCap cap)) (capASIDPool (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) then do y <- deleteASID (the (capPDMappedASID (capCap cap))) (capPDBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) then case the (capPTMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else if isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) then case the (capVPMappedAddress (capCap cap)) of (a, v) \<Rightarrow> do y <- unmapPage (capVPSize (capCap cap)) a v (capVPBasePtr (capCap cap));
return (capability.NullCap, capability.NullCap)
od else return (capability.NullCap, capability.NullCap) 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 \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst rv) = cte_refs' cap\<rbrace>
 2. \<And>s. valid_cap' cap s \<Longrightarrow> ?Q31 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_cap' cap s \<Longrightarrow> (isEndpointCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (flag \<longrightarrow> True) \<and> (\<not> flag \<longrightarrow> (isCNodeCap cap \<and> final \<longrightarrow> fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isCNodeCap cap \<and> final) \<longrightarrow> (isThreadCap cap \<and> final \<longrightarrow> fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isThreadCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> final \<longrightarrow> fst (cap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (cap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isZombie cap \<and> final) \<longrightarrow> (isArchObjectCap cap \<longrightarrow> (isASIDPoolCap (capCap cap) \<and> final \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isASIDPoolCap (capCap cap) \<and> final) \<longrightarrow> (isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y)) \<longrightarrow> (isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (capPTMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap)) \<and> (\<not> (isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> (isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (capVPMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap)) \<and> (\<not> (isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap))))) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<and> final \<longrightarrow> fst (capability.NullCap, cap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, cap)) = cte_refs' cap) \<and> (\<not> (isIRQHandlerCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> \<not> final \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> \<not> final) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap)))))))))))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_cap' cap s; capAligned cap\<rbrakk> \<Longrightarrow> (isEndpointCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> isEndpointCap cap \<longrightarrow> (isNotificationCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> isNotificationCap cap \<longrightarrow> (isReplyCap cap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> isReplyCap cap \<longrightarrow> (cap = capability.NullCap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (cap = capability.DomainCap \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (cap \<noteq> capability.DomainCap \<longrightarrow> (flag \<longrightarrow> True) \<and> (\<not> flag \<longrightarrow> (isCNodeCap cap \<and> final \<longrightarrow> fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.Zombie (capCNodePtr cap) (ZombieCNode (capCNodeBits cap)) (shiftL (Suc 0) (capCNodeBits cap)), capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isCNodeCap cap \<and> final) \<longrightarrow> (isThreadCap cap \<and> final \<longrightarrow> fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.Zombie (capTCBPtr cap) ZombieTCB 5, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isThreadCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> final \<longrightarrow> fst (cap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (cap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isZombie cap \<and> final) \<longrightarrow> (isArchObjectCap cap \<longrightarrow> (isASIDPoolCap (capCap cap) \<and> final \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isASIDPoolCap (capCap cap) \<and> final) \<longrightarrow> (isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap) \<and> (\<not> (isPageDirectoryCap (capCap cap) \<and> final \<and> (\<exists>y. capPDMappedASID (capCap cap) = Some y)) \<longrightarrow> (isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (capPTMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap)) \<and> (\<not> (isPageTableCap (capCap cap) \<and> final \<and> (\<exists>a b. capPTMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> (isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b)) \<longrightarrow> (\<forall>x xa. the (capVPMappedAddress (capCap cap)) = (x, xa) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap)) \<and> (\<not> (isPageCap (capCap cap) \<and> (\<exists>a b. capVPMappedAddress (capCap cap) = Some (a, b))) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap))))) \<and> (\<not> isArchObjectCap cap \<longrightarrow> (isIRQHandlerCap cap \<and> final \<longrightarrow> fst (capability.NullCap, cap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, cap)) = cte_refs' cap) \<and> (\<not> (isIRQHandlerCap cap \<and> final) \<longrightarrow> (isZombie cap \<and> \<not> final \<longrightarrow> True) \<and> (\<not> (isZombie cap \<and> \<not> final) \<longrightarrow> fst (capability.NullCap, capability.NullCap) \<noteq> capability.NullCap \<longrightarrow> cte_refs' (fst (capability.NullCap, capability.NullCap)) = cte_refs' cap)))))))))))) proof (prove)
goal (2 subgoals):
 1. \<And>s x1. \<lbrakk>valid_cap' (capability.ThreadCap x1) s; capAligned (capability.ThreadCap x1); cap = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> \<not> flag \<longrightarrow> final \<longrightarrow> (\<lambda>a. (\<lambda>x. x1 + x * 2 ^ cteSizeBits) ` {0..<5}) = (\<lambda>a. (+) x1 ` dom tcb_cte_cases)
 2. \<And>s x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; capAligned (capability.CNodeCap x111 x112 x113 x114); cap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<not> flag \<longrightarrow> final \<longrightarrow> cte_refs' (capability.Zombie x111 (ZombieCNode x112) (shiftL (Suc 0) x112)) = cte_refs' (capability.CNodeCap x111 x112 x113 x114) proof (prove)
goal (1 subgoal):
 1. \<And>s x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; capAligned (capability.CNodeCap x111 x112 x113 x114); cap = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<not> flag \<longrightarrow> final \<longrightarrow> cte_refs' (capability.Zombie x111 (ZombieCNode x112) (shiftL (Suc 0) x112)) = cte_refs' (capability.CNodeCap x111 x112 x113 x114) proof (prove)
goal (1 subgoal):
 1. \<And>s x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; capAligned (capability.CNodeCap x111 x112 x113 x114); cap = capability.CNodeCap x111 x112 x113 x114; \<not> flag; final\<rbrakk> \<Longrightarrow> cte_refs' (capability.Zombie x111 (ZombieCNode x112) (shiftL (Suc 0) x112)) = cte_refs' (capability.CNodeCap x111 x112 x113 x114) proof (prove)
goal (1 subgoal):
 1. \<And>s x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; capAligned (capability.CNodeCap x111 x112 x113 x114); cap = capability.CNodeCap x111 x112 x113 x114; \<not> flag; final\<rbrakk> \<Longrightarrow> (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..<word_of_nat (shiftL (Suc 0) x112)} = (\<lambda>x. x111 + x * 2 ^ cteSizeBits) ` {0..2 ^ x112 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x111 x112 x113 x114. \<lbrakk>valid_cap' (capability.CNodeCap x111 x112 x113 x114) s; capAligned (capability.CNodeCap x111 x112 x113 x114); cap = capability.CNodeCap x111 x112 x113 x114; \<not> flag; final\<rbrakk> \<Longrightarrow> {0..<word_of_nat (shiftL (Suc 0) x112)} = {0..2 ^ x112 - 1} proof (prove)
goal:
No subgoals!