theory Finalise_R

lemma arch_finaliseCap_removeable[wp]:
  "\<lbrace>\<lambda>s. s \<turnstile>' ArchObjectCap cap \<and> invs' s
       \<and> (final \<and> final_matters' (ArchObjectCap cap)
            \<longrightarrow> isFinal (ArchObjectCap cap) slot (cteCaps_of s))\<rbrace>
     Arch.finaliseCap cap final
   \<lbrace>\<lambda>rv s. isNullCap (fst rv) \<and> removeable' slot s (ArchObjectCap cap) \<and> isNullCap (snd rv)\<rbrace>" apply (simp add: ARM_H.finaliseCap_def
                   removeable'_def) apply (safe ; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final \<and> final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> Arch.finaliseCap cap final \<lbrace>\<lambda>rv s. isNullCap (fst rv) \<and> removeable' slot s (capability.ArchObjectCap cap) \<and> isNullCap (snd rv)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (isPageCap cap \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> (isPageTableCap cap \<and> final \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> (isPageDirectoryCap cap \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>)) \<and> ((isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> case the (capPTMappedAddress cap) of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>))) \<and> ((final \<longrightarrow> isPageTableCap cap \<longrightarrow> capPTMappedAddress cap = None) \<longrightarrow> (isPageDirectoryCap cap \<and> final \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>)) \<and> ((final \<longrightarrow> isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<and> final \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> ((isASIDPoolCap cap \<longrightarrow> \<not> final) \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final \<and> final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> case the (capVPMappedAddress cap) of (a, v) \<Rightarrow> do y <- unmapPage (capVPSize cap) a v (capVPBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>)))) \<and> ((isPageCap cap \<longrightarrow> capVPMappedAddress cap = None) \<longrightarrow> (isPageTableCap cap \<and> final \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> (isPageDirectoryCap cap \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>)) \<and> ((isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> case the (capPTMappedAddress cap) of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>))) \<and> ((final \<longrightarrow> isPageTableCap cap \<longrightarrow> capPTMappedAddress cap = None) \<longrightarrow> (isPageDirectoryCap cap \<and> final \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>)) \<and> ((final \<longrightarrow> isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<and> final \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>) \<and> ((isASIDPoolCap cap \<longrightarrow> \<not> final) \<longrightarrow> \<lbrace>\<lambda>s. valid_cap' (capability.ArchObjectCap cap) s \<and> invs' s \<and> (final \<and> final_matters' (capability.ArchObjectCap cap) \<longrightarrow> isFinal (capability.ArchObjectCap cap) slot (cteCaps_of s))\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv s. fst rv = capability.NullCap \<and> snd rv = capability.NullCap\<rbrace>)))) proof (prove)
goal:
No subgoals!