theory CSpace1_R

lemma src_no_mdb_parent:
  "isMDBParentOf (CTE src_cap src_node) cte = False" using no_child partial_is_derived' apply clarsimp apply (case_tac cte) apply (clarsimp simp: isMDBParentOf_CTE is_derived'_def badge_derived'_def) apply (erule sameRegionAsE) apply (clarsimp simp add: sameRegionAs_def3) apply (cases src_cap,auto simp:capMasterCap_def revokable'_def vsCapRef_def freeIndex_update_def
         isCap_simps split:capability.splits arch_capability.splits)[1] apply (clarsimp simp: isCap_simps sameRegionAs_def3 capMasterCap_def freeIndex_update_def
       split:capability.splits arch_capability.splits) apply (clarsimp simp: isCap_simps sameRegionAs_def3 freeIndex_update_def
                         capRange_def vsCapRef_def split:capability.splits
               simp del: Int_atLeastAtMost atLeastAtMost_iff) apply auto[1] apply (clarsimp simp: isCap_simps sameRegionAs_def3) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. isMDBParentOf (CTE src_cap src_node) cte = False proof (prove)
using this:
\<not> isMDBParentOf (CTE src_cap src_node) (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node))))
is_derived' m src c' src_cap

goal (1 subgoal):
 1. isMDBParentOf (CTE src_cap src_node) cte = False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<not> isMDBParentOf (CTE src_cap src_node) (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))); is_derived' m src c' src_cap; isMDBParentOf (CTE src_cap src_node) cte\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>\<not> isMDBParentOf (CTE src_cap src_node) (CTE c' (mdbFirstBadged_update (\<lambda>a. revokable' src_cap c') (mdbRevocable_update (\<lambda>a. revokable' src_cap c') (mdbPrev_update (\<lambda>a. src) src_node)))); is_derived' m src c' src_cap; isMDBParentOf (CTE src_cap src_node) cte; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; global.sameRegionAs src_cap x1; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capMasterCap src_cap = capMasterCap x1; \<not> isNullCap src_cap; \<not> isZombie src_cap; \<not> isUntypedCap src_cap; \<not> isArchPageCap src_cap\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap x1\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isIRQControlCap src_cap; isIRQHandlerCap x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>x1 x2. \<lbrakk>cte = CTE x1 x2; c' \<noteq> capability.NullCap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap x1 = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capMasterCap src_cap = capMasterCap c'; src_cap \<noteq> capability.NullCap; \<not> isZombie src_cap; \<not> isUntypedCap src_cap; \<not> isArchPageCap src_cap; \<not> isZombie c' \<and> \<not> isUntypedCap c' \<and> \<not> isArchPageCap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); isIRQControlCap src_cap \<and> isIRQHandlerCap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c')\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap x1\<rbrakk> \<Longrightarrow> False
 4. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isIRQControlCap src_cap; isIRQHandlerCap x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isUntypedCap src_cap\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap x1\<rbrakk> \<Longrightarrow> False
 3. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isIRQControlCap src_cap; isIRQHandlerCap x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); capRange x1 \<noteq> {}; capRange x1 \<subseteq> capRange src_cap; isArchPageCap src_cap; isArchPageCap x1\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isIRQControlCap src_cap; isIRQHandlerCap x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x2 d da ref refa rghts rghtsa sz sza data dataa rghtsb mapdata. \<lbrakk>refa \<le> refa + 2 ^ pageBitsForSize sza - 1; cte = CTE (capability.ArchObjectCap (arch_capability.PageCap da refa rghtsa sza dataa)) x2; mdbRevocable src_node; d; ref \<le> ref + 2 ^ pageBitsForSize sz - 1 \<longrightarrow> All Not; c' = capability.ArchObjectCap (arch_capability.PageCap True ref rghtsb sz mapdata); src_cap = capability.ArchObjectCap (arch_capability.PageCap True ref rghts sz data); ref \<le> refa; refa + 2 ^ pageBitsForSize sza - 1 \<le> ref + 2 ^ pageBitsForSize sz - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isIRQControlCap src_cap; isIRQHandlerCap x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x1 x2. \<lbrakk>global.sameRegionAs src_cap c' \<longrightarrow> (capBadge src_cap, capBadge c') \<notin> capBadge_ordering (revokable' src_cap c'); cte = CTE x1 x2; c' \<noteq> capability.NullCap; \<not> isZombie src_cap; mdbRevocable src_node; (capBadge src_cap, capBadge x1) \<in> capBadge_ordering (mdbFirstBadged x2); \<not> isIRQControlCap c'; capMasterCap src_cap = capMasterCap c'; (capBadge src_cap, capBadge c') \<in> capBadge_ordering False; isUntypedCap src_cap \<longrightarrow> descendants_of' src m = {}; isReplyCap src_cap = isReplyCap c'; isReplyCap c' \<longrightarrow> capReplyMaster src_cap; isReplyCap c' \<longrightarrow> \<not> capReplyMaster c'; vsCapRef src_cap = vsCapRef c' \<or> isArchCap isPageCap c'; isArchCap isPageTableCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isArchCap isPageDirectoryCap src_cap \<longrightarrow> capASID src_cap = capASID c' \<and> (\<exists>y. capASID src_cap = Some y); isIRQControlCap src_cap; isIRQHandlerCap x1\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!