theory Orphanage

lemma arch_finaliseCap_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<rbrace>
   Arch.finaliseCap cap fin
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding ARM_H.finaliseCap_def apply (wpsimp simp: isCap_simps) apply (safe; wpsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<rbrace> Arch.finaliseCap cap fin \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans\<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. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. ((\<exists>v0 v1. cap = arch_capability.PageTableCap v0 v1) \<and> fin \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.PageDirectoryCap v0 v1) \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>))) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>))) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageTableCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the None) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>))) \<and> (capPTMappedAddress cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the None) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)))) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>))) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageTableCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capPTMappedAddress cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> case the None of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>))) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>))) \<and> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageTableCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capPTMappedAddress cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> case the None of (a, v) \<Rightarrow> do y <- unmapPageTable a v (capPTBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)))) \<and> ((fin \<longrightarrow> (\<forall>v0 v1. cap \<noteq> arch_capability.PageTableCap v0 v1) \<or> capPTMappedAddress cap = None) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.PageDirectoryCap v0 v1) \<and> fin \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.PageTableCap v0 v1) \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>))) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)))) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageTableCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the None) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>))) \<and> (capPTMappedAddress cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the None) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)))) \<and> ((fin \<longrightarrow> (\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<or> capPDMappedASID cap = None) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.PageTableCap v0 v1) \<and> fin \<and> (\<exists>a b. capPTMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.PageDirectoryCap v0 v1) \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>))) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.PageDirectoryCap v0 v1) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>))) \<and> (capPDMappedASID cap = None \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)))) \<and> ((\<exists>v0 v1. cap = arch_capability.PageDirectoryCap v0 v1) \<and> fin \<and> (\<exists>y. capPDMappedASID cap = Some y) \<longrightarrow> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>)) \<and> (capVPMappedAddress cap = None \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASID (the (capPDMappedASID cap)) (capPDBasePtr cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>))) \<and> ((\<exists>d v0 v1 v2 v3. cap = arch_capability.PageCap d v0 v1 v2 v3) \<and> (\<exists>a b. capVPMappedAddress cap = Some (a, b)) \<longrightarrow> ((\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<and> fin \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> ((\<forall>v0 v1. cap \<noteq> arch_capability.ASIDPoolCap v0 v1) \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>) \<and> (\<not> fin \<longrightarrow> \<lbrace>no_orphans\<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. no_orphans\<rbrace>)) \<and> ((\<forall>d v0 v1 v2 v3. cap \<noteq> arch_capability.PageCap d v0 v1 v2 v3) \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<and> fin \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>) \<and> (capVPMappedAddress cap = None \<longrightarrow> (\<exists>v0 v1. cap = arch_capability.ASIDPoolCap v0 v1) \<and> fin \<longrightarrow> \<lbrace>no_orphans\<rbrace> do y <- deleteASIDPool (capASIDBase cap) (capASIDPool cap);
return (capability.NullCap, capability.NullCap)
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>))) proof (prove)
goal:
No subgoals!