theory Finalise_R

lemma arch_finaliseCap_cte_wp_at[wp]:
  "\<lbrace>cte_wp_at' P p\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>" apply (simp add: ARM_H.finaliseCap_def) apply (safe ; wpsimp wp: unmapPage_cte_wp_at') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' P p\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace> proof (prove)
goal (1 subgoal):
 1. (isPageCap cap \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> (isPageTableCap cap \<and> fin \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> (isPageDirectoryCap cap \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>)) \<and> ((isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<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. cte_wp_at' P p\<rbrace>))) \<and> ((fin \<longrightarrow> isPageTableCap cap \<longrightarrow> capPTMappedAddress cap = None) \<longrightarrow> (isPageDirectoryCap cap \<and> fin \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>)) \<and> ((fin \<longrightarrow> isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<and> fin \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> ((isASIDPoolCap cap \<longrightarrow> \<not> fin) \<longrightarrow> \<lbrace>cte_wp_at' P p\<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. cte_wp_at' P p\<rbrace>)))) \<and> ((isPageCap cap \<longrightarrow> capVPMappedAddress cap = None) \<longrightarrow> (isPageTableCap cap \<and> fin \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> (isPageDirectoryCap cap \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>)) \<and> ((isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<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. cte_wp_at' P p\<rbrace>))) \<and> ((fin \<longrightarrow> isPageTableCap cap \<longrightarrow> capPTMappedAddress cap = None) \<longrightarrow> (isPageDirectoryCap cap \<and> fin \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>)) \<and> ((fin \<longrightarrow> isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> isASIDPoolCap cap \<and> fin \<longrightarrow> \<lbrace>cte_wp_at' P p\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. cte_wp_at' P p\<rbrace>))) proof (prove)
goal:
No subgoals!