theory Untyped_R

lemma cte_cap_in_untyped_range:
  "\<lbrakk> ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; cte_wp_at' (\<lambda>cte. cteCap cte = UntypedCap d ptr bits idx) cref s;
     descendants_of' cref (ctes_of s) = {}; invs' s;
     ex_cte_cap_to' x s; valid_global_refs' s \<rbrakk> \<Longrightarrow> False" apply (clarsimp simp: ex_cte_cap_to'_def cte_wp_at_ctes_of) apply (case_tac ctea, simp) apply (rename_tac cap node) apply (frule ctes_of_valid_cap', clarsimp) apply (case_tac "\<exists>irq. cap = IRQHandlerCap irq") apply (drule (1) equals0D[where a=x, OF valid_global_refsD2'[where p=cref]]) apply (clarsimp simp: irq_nodes_global) apply (frule_tac p=crefa and p'=cref in caps_containedD', assumption) apply (clarsimp dest!: isCapDs) apply (rule_tac x=x in notemptyI) apply (simp add: subsetD [OF cte_refs_capRange]) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) apply (frule_tac p=cref and p'=crefa in untyped_mdbD', assumption) apply (simp_all add: isUntypedCap_def) apply (frule valid_capAligned) apply (frule capAligned_capUntypedPtr) apply (case_tac cap; simp) apply blast apply (case_tac cap; simp) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def valid_mdb'_def valid_mdb_ctes_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap d ptr bits idx) cref s; descendants_of' cref (ctes_of s) = {}; invs' s; ex_cte_cap_wp_to' (\<lambda>_. True) x s; valid_global_refs' s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some ctea; x \<in> cte_refs' (cteCap ctea) (irq_node' s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea x1 x2. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE x1 x2); x \<in> cte_refs' x1 (irq_node' s); ctea = CTE x1 x2\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<exists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<exists>irq. cap = capability.IRQHandlerCap irq; x \<notin> global_refs' s \<inter> capRange (cteCap cte)\<rbrakk> \<Longrightarrow> False
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> capRange (cteCap (CTE cap node)) \<inter> untypedRange (cteCap cte) \<noteq> {}
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> caps_contained' (ctes_of s)
 4. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> capRange (cteCap (CTE cap node)) \<inter> untypedRange (cteCap cte) \<noteq> {}
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> caps_contained' (ctes_of s)
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> x \<in> capRange (cteCap (CTE cap node)) \<inter> untypedRange (cteCap cte)
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> caps_contained' (ctes_of s)
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq\<rbrakk> \<Longrightarrow> caps_contained' (ctes_of s)
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> capRange (cteCap (CTE cap node)) \<inter> untypedRange (cteCap cte) \<noteq> {}
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> \<not> isUntypedCap (cteCap (CTE cap node))
 4. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte)\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s)
 5. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<nexists>irq. cap = capability.IRQHandlerCap irq; capRange (cteCap (CTE cap node)) \<subseteq> untypedRange (cteCap cte); crefa \<in> descendants_of' cref (ctes_of s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> capRange cap \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> \<not> (case cap of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s) proof (prove)
goal (3 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}; capAligned cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> \<not> (case cap of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s) proof (prove)
goal (4 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}; capAligned cap\<rbrakk> \<Longrightarrow> capClass cap = PhysicalClass
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}; capAligned cap; global.capUntypedPtr cap \<in> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> \<not> (case cap of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False)
 4. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s) proof (prove)
goal (3 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}; capAligned cap; global.capUntypedPtr cap \<in> capRange cap\<rbrakk> \<Longrightarrow> capRange cap \<inter> {ptr..ptr + 2 ^ bits - 1} \<noteq> {}
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> \<not> (case cap of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False)
 3. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> \<not> (case cap of capability.UntypedCap v0 v1 v2 v3 \<Rightarrow> True | _ \<Rightarrow> False)
 2. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>cte crefa ctea cap node. \<lbrakk>ptr \<le> x; x \<le> ptr + 2 ^ bits - 1; descendants_of' cref (ctes_of s) = {}; invs' s; valid_global_refs' s; ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d ptr bits idx; ctes_of s crefa = Some (CTE cap node); x \<in> cte_refs' cap (irq_node' s); ctea = CTE cap node; valid_cap' cap s; \<forall>irq. cap \<noteq> capability.IRQHandlerCap irq; capRange cap \<subseteq> {ptr..ptr + 2 ^ bits - 1}\<rbrakk> \<Longrightarrow> untyped_mdb' (ctes_of s) proof (prove)
goal:
No subgoals!