theory CSpace_R

lemma irq_control_src:
  "\<lbrakk> isIRQControlCap src_cap;
     m p = Some (CTE cap node);
     sameRegionAs cap c' \<rbrakk> \<Longrightarrow> p = src" using safe_parent src unfolding safe_parent_for'_def apply (clarsimp simp: isCap_simps) apply (clarsimp simp: sameRegionAs_def2 isCap_Master) apply (erule disjE, clarsimp simp: isCap_simps) apply (erule disjE, clarsimp simp: isCap_simps) apply (erule disjE, clarsimp simp: isCap_simps capRange_def) apply (clarsimp simp: isCap_simps) apply (drule (1) irq_controlD, rule irq_control) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isIRQControlCap src_cap; m p = Some (CTE cap node); global.sameRegionAs cap c'\<rbrakk> \<Longrightarrow> p = src proof (prove)
using this:
safe_parent_for' m src c'
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<lbrakk>isIRQControlCap src_cap; m p = Some (CTE cap node); global.sameRegionAs cap c'\<rbrakk> \<Longrightarrow> p = src proof (prove)
using this:
\<exists>parent node. m src = Some (CTE parent node) \<and> global.sameRegionAs parent c' \<and> ((\<exists>irq. c' = capability.IRQHandlerCap irq) \<and> parent = capability.IRQControlCap \<and> (\<forall>p n'. m p \<noteq> Some (CTE c' n')) \<or> isUntypedCap parent \<and> descendants_of' src m = {} \<and> capRange c' \<noteq> {} \<and> capBits c' \<le> capBits parent)
m src = Some (CTE src_cap src_node)

goal (1 subgoal):
 1. \<lbrakk>isIRQControlCap src_cap; m p = Some (CTE cap node); global.sameRegionAs cap c'\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m p = Some (CTE cap node); global.sameRegionAs cap (capability.IRQHandlerCap irq); m src = Some (CTE capability.IRQControlCap src_node); global.sameRegionAs capability.IRQControlCap (capability.IRQHandlerCap irq); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m p = Some (CTE cap node); capMasterCap cap = capability.IRQHandlerCap irq \<and> capMasterCap cap \<noteq> capability.NullCap \<and> \<not> isZombie cap \<and> \<not> isUntypedCap cap \<and> \<not> isArchPageCap cap \<and> \<not> isZombie (capability.IRQHandlerCap irq) \<and> \<not> isArchPageCap (capability.IRQHandlerCap irq) \<or> capRange (capability.IRQHandlerCap irq) \<noteq> {} \<and> capRange (capability.IRQHandlerCap irq) \<subseteq> capRange (capMasterCap cap) \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap (capability.IRQHandlerCap irq)) \<or> isIRQControlCap cap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq); m src = Some (CTE capability.IRQControlCap src_node); capRange (capability.IRQHandlerCap irq) \<noteq> {} \<and> capRange (capability.IRQHandlerCap irq) \<subseteq> capRange capability.IRQControlCap \<and> isArchPageCap capability.IRQControlCap \<and> isArchPageCap (capability.IRQHandlerCap irq) \<or> isIRQControlCap capability.IRQControlCap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m p = Some (CTE cap node); m src = Some (CTE capability.IRQControlCap src_node); capRange (capability.IRQHandlerCap irq) \<noteq> {} \<and> capRange (capability.IRQHandlerCap irq) \<subseteq> capRange capability.IRQControlCap \<and> isArchPageCap capability.IRQControlCap \<and> isArchPageCap (capability.IRQHandlerCap irq) \<or> isIRQControlCap capability.IRQControlCap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq; capRange (capability.IRQHandlerCap irq) \<noteq> {} \<and> capRange (capability.IRQHandlerCap irq) \<subseteq> capRange (capMasterCap cap) \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap (capability.IRQHandlerCap irq)) \<or> isIRQControlCap cap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m p = Some (CTE cap node); m src = Some (CTE capability.IRQControlCap src_node); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq; capRange (capability.IRQHandlerCap irq) \<noteq> {} \<and> capRange (capability.IRQHandlerCap irq) \<subseteq> capRange (capMasterCap cap) \<and> (isUntypedCap cap \<or> isArchPageCap cap \<and> isArchPageCap (capability.IRQHandlerCap irq)) \<or> isIRQControlCap cap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq); isIRQControlCap capability.IRQControlCap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m p = Some (CTE cap node); m src = Some (CTE capability.IRQControlCap src_node); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq; isIRQControlCap capability.IRQControlCap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq); isIRQControlCap cap \<and> isIRQHandlerCap (capability.IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m p = Some (CTE capability.IRQControlCap node); m src = Some (CTE capability.IRQControlCap src_node); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq; cap = capability.IRQControlCap\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal (1 subgoal):
 1. \<And>irq. \<lbrakk>src_cap = capability.IRQControlCap; m src = Some (CTE capability.IRQControlCap src_node); \<forall>p n'. m p \<noteq> Some (CTE (capability.IRQHandlerCap irq) n'); c' = capability.IRQHandlerCap irq; cap = capability.IRQControlCap; src = p\<rbrakk> \<Longrightarrow> p = src proof (prove)
goal:
No subgoals!