theory Untyped_AI

lemma ex_cte_no_overlap:
  "\<And>P slot. ex_cte_cap_wp_to P slot s \<Longrightarrow> fst slot \<notin> usable_range" using cte_wp_at apply clarsimp apply (drule ex_cte_cap_to_obj_ref_disj,erule disjE) using misc apply clarsimp apply (rule_tac ptr' = "(aa,b)" in untyped_children_in_mdbEE[OF invs_untyped_children]) apply simp+ apply (clarsimp simp:untyped_range.simps) apply (drule_tac B'="usable_range" in disjoint_subset2[rotated]) apply (clarsimp simp:blah word_and_le2) apply blast apply (drule descendants_range_inD[OF descendants_range(1)]) apply (simp add:cte_wp_at_caps_of_state)+ apply (clarsimp simp:cap_range_def) apply blast apply clarsimp apply (drule_tac irq = irq in valid_globals_irq_node[rotated]) using misc apply (clarsimp simp: invs_def valid_state_def ) apply (clarsimp simp:untyped_range.simps) apply (drule_tac B = "{ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}" in subsetD[rotated]) apply (clarsimp simp:blah word_and_le2) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>P slot. ex_cte_cap_wp_to P slot s \<Longrightarrow> fst slot \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
using this:
cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s

goal (1 subgoal):
 1. \<And>P slot. ex_cte_cap_wp_to P slot s \<Longrightarrow> fst slot \<notin> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>P a b. \<lbrakk>ex_cte_cap_wp_to P (a, b) s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr'. cte_wp_at (\<lambda>cap. fst (a, b) \<in> obj_refs cap) ptr' s\<rbrakk> \<Longrightarrow> False
 2. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
ct_active s
invs s

goal (2 subgoals):
 1. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr'. cte_wp_at (\<lambda>cap. fst (a, b) \<in> obj_refs cap) ptr' s\<rbrakk> \<Longrightarrow> False
 2. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a aa b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s\<rbrakk> \<Longrightarrow> False
 2. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (7 subgoals):
 1. \<And>a aa b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s\<rbrakk> \<Longrightarrow> invs (?s12 a aa b)
 2. \<And>a aa b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s\<rbrakk> \<Longrightarrow> cte_wp_at ((=) (?cap12 a aa b)) (?ptr12 a aa b) (?s12 a aa b)
 3. \<And>a aa b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s\<rbrakk> \<Longrightarrow> is_untyped_cap (?cap12 a aa b)
 4. \<And>a aa b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (?P12 a aa b) (aa, b) (?s12 a aa b)
 5. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) (?s12 a aa b); ?P12 a aa b cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (?cap12 a aa b) \<noteq> {}
 6. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) (?s12 a aa b); cap_range cap' \<inter> untyped_range (?cap12 a aa b) \<noteq> {}; (aa, b) \<in> descendants_of (?ptr12 a aa b) (cdt (?s12 a aa b))\<rbrakk> \<Longrightarrow> False
 7. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; a \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> obj_refs cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}
 2. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; (aa, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; a \<in> obj_refs cap'; obj_refs cap' \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; (aa, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; a \<in> obj_refs cap'\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; a \<in> obj_refs cap'; obj_refs cap' \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; (aa, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> False
 4. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; a \<in> obj_refs cap'; obj_refs cap' \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; (aa, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> False
 3. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; (aa, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> False
 2. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}\<rbrakk> \<Longrightarrow> caps_of_state s (aa, b) = Some (?cap26 a aa b cap')
 2. \<And>a aa b cap'. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; cte_wp_at (\<lambda>cap. a \<in> obj_refs cap) (aa, b) s; cte_wp_at ((=) cap') (aa, b) s; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; cap_range (?cap26 a aa b cap') \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; a \<in> obj_refs cap'; caps_of_state s (aa, b) = Some cap'; cap_range cap' \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; cap_range cap' \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a aa b cap'. \<lbrakk>caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ct_active s; invs s; a \<in> obj_refs cap'; caps_of_state s (aa, b) = Some cap'; (untyped_range cap' \<union> obj_refs cap') \<inter> untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<noteq> {}; (untyped_range cap' \<union> obj_refs cap') \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>P a b. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; a \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; \<exists>ptr' irq. cte_wp_at ((=) (IRQHandlerCap irq)) ptr' s \<and> (a, b) = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa ba irq. \<lbrakk>cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s; interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa ba irq. \<lbrakk>interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>aa ba irq. \<lbrakk>interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
ct_active s
invs s

goal (2 subgoals):
 1. \<And>aa ba irq. \<lbrakk>interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s\<rbrakk> \<Longrightarrow> valid_global_refs s
 2. \<And>aa ba irq. \<lbrakk>interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa ba irq. \<lbrakk>interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> cap_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa ba irq. \<lbrakk>interrupt_irq_node s irq \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>aa ba irq. \<lbrakk>cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>aa ba irq. \<lbrakk>cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; interrupt_irq_node s irq \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>aa ba irq. \<lbrakk>cte_wp_at ((=) (IRQHandlerCap irq)) (aa, ba) s; interrupt_irq_node s irq \<notin> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; interrupt_irq_node s irq \<in> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!