theory Finalise_R

lemma arch_finaliseCap_invs[wp]:
  "\<lbrace>invs' and valid_cap' (ArchObjectCap cap)\<rbrace>
     Arch.finaliseCap cap fin
   \<lbrace>\<lambda>rv. invs'\<rbrace>" unfolding ARM_H.finaliseCap_def apply clarsimp apply (safe ; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> let (cap, bl) = (cap, fin) in if isASIDPoolCap cap \<and> bl then let b = capASIDBase cap; ptr = capASIDPool cap in do deleteASIDPool b ptr;
return (capability.NullCap, capability.NullCap)
od else if isPageDirectoryCap cap \<and> bl \<and> capPDMappedASID cap \<noteq> None then let a = the (capPDMappedASID cap); ptr = capPDBasePtr cap in do deleteASID a ptr;
return (capability.NullCap, capability.NullCap)
od else if isPageTableCap cap \<and> bl \<and> capPTMappedAddress cap \<noteq> None then let (a, v) = the (capPTMappedAddress cap); ptr = capPTBasePtr cap in do unmapPageTable a v ptr;
return (capability.NullCap, capability.NullCap)
od else if isPageCap cap \<and> capVPMappedAddress cap \<noteq> None then let (a, v) = the (capVPMappedAddress cap); s = capVPSize cap; ptr = capVPBasePtr cap in do unmapPage s a v ptr;
return (capability.NullCap, capability.NullCap)
od else return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv. invs'\<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>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> ((isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<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. invs'\<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>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> ((fin \<longrightarrow> isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<and> fin \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> ((isASIDPoolCap cap \<longrightarrow> \<not> fin) \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<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. invs'\<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>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> ((isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<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. invs'\<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>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> (\<not> isASIDPoolCap cap \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>)) \<and> ((fin \<longrightarrow> isPageDirectoryCap cap \<longrightarrow> capPDMappedASID cap = None) \<longrightarrow> (isASIDPoolCap cap \<and> fin \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. invs'\<rbrace>) \<and> ((isASIDPoolCap cap \<longrightarrow> \<not> fin) \<longrightarrow> \<lbrace>invs' and valid_cap' (capability.ArchObjectCap cap)\<rbrace> return (capability.NullCap, capability.NullCap) \<lbrace>\<lambda>rv. invs'\<rbrace>)))) proof (prove)
goal:
No subgoals!