theory CSpace1_R

lemma maskedAsFull_revokable:
  "is_derived' x y c' src_cap' \<Longrightarrow>
   revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'" apply (case_tac src_cap') apply (simp_all add:maskedAsFull_def isCap_simps) apply (case_tac c') apply (simp_all add:maskedAsFull_def is_derived'_def isCap_simps vsCapRef_def) apply (simp_all add:badge_derived'_def capMasterCap_simps split:arch_capability.splits) apply (clarsimp split:if_splits simp:revokable'_def isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. is_derived' x y c' src_cap' \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c' proof (prove)
goal (12 subgoals):
 1. \<And>x1. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 2. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.NullCap\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 3. \<And>x31 x32 x33 x34. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 4. \<And>x4. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 5. \<And>x51 x52 x53 x54 x55 x56. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 6. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.DomainCap\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 7. \<And>x71 x72 x73. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 8. \<And>x8. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 9. \<And>x91 x92 x93. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
 10. \<And>x101 x102 x103 x104. \<lbrakk>is_derived' x y c' src_cap'; src_cap' = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> revokable' (maskedAsFull src_cap' a) c' = revokable' src_cap' c'
A total of 12 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>x101 x102 x103 x104. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c' proof (prove)
goal (12 subgoals):
 1. \<And>x101 x102 x103 x104 x1. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 2. \<And>x101 x102 x103 x104. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.NullCap\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 3. \<And>x101 x102 x103 x104 x31 x32 x33 x34. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 4. \<And>x101 x102 x103 x104 x4. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 5. \<And>x101 x102 x103 x104 x51 x52 x53 x54 x55 x56. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 6. \<And>x101 x102 x103 x104. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.DomainCap\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 7. \<And>x101 x102 x103 x104 x71 x72 x73. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 8. \<And>x101 x102 x103 x104 x8. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 9. \<And>x101 x102 x103 x104 x91 x92 x93. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.ReplyCap x91 x92 x93\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
 10. \<And>x101 x102 x103 x104 x101a x102a x103a x104a. \<lbrakk>is_derived' x y c' (capability.UntypedCap x101 x102 x103 x104); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.UntypedCap x101a x102a x103a x104a\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) c' = revokable' (capability.UntypedCap x101 x102 x103 x104) c'
A total of 12 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>x101 x102 x103 x104 x1. \<lbrakk>badge_derived' (capability.ThreadCap x1) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.ThreadCap x1\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.ThreadCap x1) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.ThreadCap x1)
 2. \<And>x101 x102 x103 x104 x31 x32 x33 x34. \<lbrakk>badge_derived' (capability.NotificationCap x31 x32 x33 x34) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.NotificationCap x31 x32 x33 x34\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.NotificationCap x31 x32 x33 x34) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.NotificationCap x31 x32 x33 x34)
 3. \<And>x101 x102 x103 x104 x4. \<lbrakk>badge_derived' (capability.IRQHandlerCap x4) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.IRQHandlerCap x4\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.IRQHandlerCap x4) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.IRQHandlerCap x4)
 4. \<And>x101 x102 x103 x104 x51 x52 x53 x54 x55 x56. \<lbrakk>badge_derived' (capability.EndpointCap x51 x52 x53 x54 x55 x56) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.EndpointCap x51 x52 x53 x54 x55 x56\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.EndpointCap x51 x52 x53 x54 x55 x56) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.EndpointCap x51 x52 x53 x54 x55 x56)
 5. \<And>x101 x102 x103 x104. \<lbrakk>badge_derived' capability.DomainCap (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.DomainCap\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) capability.DomainCap = revokable' (capability.UntypedCap x101 x102 x103 x104) capability.DomainCap
 6. \<And>x101 x102 x103 x104 x71 x72 x73. \<lbrakk>badge_derived' (capability.Zombie x71 x72 x73) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.Zombie x71 x72 x73\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.Zombie x71 x72 x73) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.Zombie x71 x72 x73)
 7. \<And>x101 x102 x103 x104 x8. \<lbrakk>badge_derived' (capability.ArchObjectCap x8) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {} \<and> (None = (case x8 of arch_capability.ASIDPoolCap x asid \<Rightarrow> Some [VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.ASIDControlCap \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb ARMSuperSection None \<Rightarrow> None | arch_capability.PageCap x xa xb ARMSuperSection (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageCap x xa xb _ None \<Rightarrow> None | arch_capability.PageCap x xa xb _ (Some (asid, vptr)) \<Rightarrow> Some [VSRef ((vptr >> 12) && mask 8) (Some APageTable), VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageTableCap x None \<Rightarrow> None | arch_capability.PageTableCap x (Some (asid, vptr)) \<Rightarrow> Some [VSRef (vptr >> 20) (Some APageDirectory), VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None] | arch_capability.PageDirectoryCap x None \<Rightarrow> None | arch_capability.PageDirectoryCap x (Some asid) \<Rightarrow> Some [VSRef (asid && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of asid)) None]) \<or> (\<exists>d v0 v1 v2 v3. x8 = arch_capability.PageCap d v0 v1 v2 v3)); src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.ArchObjectCap x8) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.ArchObjectCap x8)
 8. \<And>x101 x102 x103 x104 x101a x102a x103a x104a. \<lbrakk>badge_derived' (capability.UntypedCap x101a x102a x103a x104a) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.UntypedCap x101a x102a x103a x104a\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.UntypedCap x101a x102a x103a x104a) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.UntypedCap x101a x102a x103a x104a)
 9. \<And>x101 x102 x103 x104 x111 x112 x113 x114. \<lbrakk>badge_derived' (capability.CNodeCap x111 x112 x113 x114) (capability.UntypedCap x101 x102 x103 x104) \<and> descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.CNodeCap x111 x112 x113 x114) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.CNodeCap x111 x112 x113 x114) proof (prove)
goal (1 subgoal):
 1. \<And>x101 x102 x103 x104 x104a. \<lbrakk>descendants_of' y x = {}; src_cap' = capability.UntypedCap x101 x102 x103 x104; c' = capability.UntypedCap x101 x102 x103 x104a\<rbrakk> \<Longrightarrow> revokable' (if (\<exists>d v0 v1 f. a = capability.UntypedCap d v0 v1 f) \<and> x102 = capPtr a \<and> x103 = capBlockSize a then capability.UntypedCap x101 (capPtr a) (capBlockSize a) (max_free_index (capBlockSize a)) else capability.UntypedCap x101 x102 x103 x104) (capability.UntypedCap x101 x102 x103 x104a) = revokable' (capability.UntypedCap x101 x102 x103 x104) (capability.UntypedCap x101 x102 x103 x104a) proof (prove)
goal:
No subgoals!