theory Intent_DR

lemma ex_cte_cap_wp_to_not_idle:
  "\<lbrakk> ex_cte_cap_wp_to P r s; valid_global_refs s; valid_objs s;
             valid_idle s; valid_irq_node  s\<rbrakk>
         \<Longrightarrow> not_idle_thread (fst r) s" apply (clarsimp simp:ex_cte_cap_wp_to_def) apply (simp add:valid_global_refs_def valid_refs_def not_idle_thread_def) apply (drule_tac x = a in spec, drule_tac x = b in spec) apply (clarsimp simp:global_refs_def cte_wp_at_cases dest!:get_tcb_SomeD split:if_splits) apply (erule disjE) apply clarsimp apply (case_tac cap) apply (clarsimp simp:cap_range_def)+ apply (rename_tac word) apply (clarsimp simp:valid_idle_def valid_irq_node_def) apply (drule_tac x = word in spec) apply (clarsimp simp:pred_tcb_at_def obj_at_def is_cap_table_def) apply (clarsimp simp:cap_range_def)+ apply (case_tac "get tcb") apply clarsimp+ apply (rename_tac word) apply (clarsimp simp:valid_idle_def valid_irq_node_def) apply (drule_tac x = word in spec) apply (clarsimp simp:st_tcb_at_def pred_tcb_at_def obj_at_def is_cap_table_def) apply clarsimp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ex_cte_cap_wp_to P r s; valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s\<rbrakk> \<Longrightarrow> not_idle_thread (fst r) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_global_refs s; valid_objs s; valid_idle s; valid_irq_node s; cte_wp_at (\<lambda>c. P c \<and> r \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrakk> \<Longrightarrow> not_idle_thread (fst r) s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>\<forall>a b. \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s; valid_objs s; valid_idle s; valid_irq_node s; cte_wp_at (\<lambda>c. P c \<and> r \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrakk> \<Longrightarrow> fst r \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; cte_wp_at (\<lambda>c. P c \<and> r \<in> cte_refs c (interrupt_irq_node s)) (a, b) s; \<not> cte_wp_at (\<lambda>c. global_refs s \<inter> cap_range c \<noteq> {}) (a, b) s\<rbrakk> \<Longrightarrow> fst r \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; (\<exists>sz fun. kheap s a = Some (kernel_object.CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> P cap \<and> r \<in> cte_refs cap (interrupt_irq_node s))) \<or> (\<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))); \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>sz fun. kheap s a = Some (kernel_object.CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> (\<exists>cap. fun b = Some cap \<and> P cap \<and> r \<in> cte_refs cap (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (13 subgoals):
 1. \<And>a b sz fun cap. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>a b sz fun cap x21 x22 x23 x24. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> False
 3. \<And>a b sz fun cap x31 x32 x33. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>a b sz fun cap x41 x42 x43. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> False
 5. \<And>a b sz fun cap x51 x52 x53. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> False
 6. \<And>a b sz fun cap x61 x62 x63. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> False
 7. \<And>a b sz fun cap x7. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> False
 8. \<And>a b sz fun cap. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = cap.DomainCap\<rbrakk> \<Longrightarrow> False
 9. \<And>a b sz fun cap. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = IRQControlCap\<rbrakk> \<Longrightarrow> False
 10. \<And>a b sz fun cap x10. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False
A total of 13 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>a b sz fun x10. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; interrupt_irq_node s x10 = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some (IRQHandlerCap x10); P (IRQHandlerCap x10); r = (idle_thread s, [])\<rbrakk> \<Longrightarrow> False
 2. \<And>a b sz fun cap x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b sz fun cap x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b sz fun word. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; interrupt_irq_node s word = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some (IRQHandlerCap word); P (IRQHandlerCap word); r = (idle_thread s, [])\<rbrakk> \<Longrightarrow> False
 2. \<And>a b sz fun cap x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b sz fun cap x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b sz fun word. \<lbrakk>valid_objs s; interrupt_irq_node s word = idle_thread_ptr; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some (IRQHandlerCap word); P (IRQHandlerCap word); r = (idle_thread_ptr, []); idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b sz fun cap x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b sz fun cap x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>a b sz fun word. \<lbrakk>valid_objs s; interrupt_irq_node s word = idle_thread_ptr; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some (IRQHandlerCap word); P (IRQHandlerCap word); r = (idle_thread_ptr, []); idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; inj (interrupt_irq_node s); cap_table_at 0 (interrupt_irq_node s word) s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b sz fun cap x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b sz fun cap x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False
 4. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b sz fun cap x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 2. \<And>a b sz fun cap x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun b = Some cap; P cap; r \<in> cte_refs cap (interrupt_irq_node s); idle_thread s \<notin> cap_range cap; arm_global_pd (arch_state s) \<notin> cap_range cap; (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}; cap = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False
 3. \<And>a b. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; \<forall>sz fun. well_formed_cnode_n sz fun \<longrightarrow> kheap s a = Some (kernel_object.CNode sz fun) \<longrightarrow> (\<forall>cap. fun b = Some cap \<longrightarrow> idle_thread s \<notin> cap_range cap \<and> arm_global_pd (arch_state s) \<notin> cap_range cap \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range cap = {}); \<forall>tcb. kheap s a = Some (TCB tcb) \<longrightarrow> (\<forall>get. (\<forall>set restr. tcb_cap_cases b \<noteq> Some (get, set, restr)) \<or> idle_thread s \<notin> cap_range (get tcb) \<and> arm_global_pd (arch_state s) \<notin> cap_range (get tcb) \<and> (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> cap_range (get tcb) = {}); fst r = idle_thread s; \<exists>tcb. kheap s a = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases b = Some (get, set, restr)) \<and> P (get tcb) \<and> r \<in> cte_refs (get tcb) (interrupt_irq_node s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b tcb get seta restr. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (12 subgoals):
 1. \<And>a b tcb get seta restr. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.NullCap\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get seta restr x21 x22 x23 x24. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get seta restr x31 x32 x33. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> False
 4. \<And>a b tcb get seta restr x41 x42 x43. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> False
 5. \<And>a b tcb get seta restr x51 x52 x53. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> False
 6. \<And>a b tcb get seta restr x61 x62 x63. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> False
 7. \<And>a b tcb get seta restr x7. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = ThreadCap x7\<rbrakk> \<Longrightarrow> False
 8. \<And>a b tcb get seta restr. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = cap.DomainCap\<rbrakk> \<Longrightarrow> False
 9. \<And>a b tcb get seta restr. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = IRQControlCap\<rbrakk> \<Longrightarrow> False
 10. \<And>a b tcb get seta restr x10. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False
A total of 12 subgoals... proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr x10. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; interrupt_irq_node s x10 = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); P (IRQHandlerCap x10); r = (idle_thread s, []); get tcb = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get seta restr x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get seta restr x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr word. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; interrupt_irq_node s word = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); P (IRQHandlerCap word); r = (idle_thread s, []); get tcb = IRQHandlerCap word\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get seta restr x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get seta restr x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr word. \<lbrakk>valid_objs s; interrupt_irq_node s word = idle_thread_ptr; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); P (IRQHandlerCap word); r = (idle_thread_ptr, []); get tcb = IRQHandlerCap word; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get seta restr x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get seta restr x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>a b tcb get set restr word. \<lbrakk>valid_objs s; interrupt_irq_node s word = idle_thread_ptr; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, set, restr); P (IRQHandlerCap word); r = (idle_thread_ptr, []); get tcb = IRQHandlerCap word; idle_tcb_at (\<lambda>(st, ab). idle st \<and> (case ab of (ntfn, arch) \<Rightarrow> ntfn = None \<and> valid_arch_idle arch)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; inj (interrupt_irq_node s); cap_table_at 0 (interrupt_irq_node s word) s\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get seta restr x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 3. \<And>a b tcb get seta restr x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b tcb get seta restr x111 x112 x113. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = Zombie x111 x112 x113\<rbrakk> \<Longrightarrow> False
 2. \<And>a b tcb get seta restr x12. \<lbrakk>valid_objs s; valid_idle s; valid_irq_node s; fst r = idle_thread s; kheap s a = Some (TCB tcb); tcb_cap_cases b = Some (get, seta, restr); P (get tcb); r \<in> cte_refs (get tcb) (interrupt_irq_node s); idle_thread s \<notin> untyped_range (get tcb); idle_thread s \<notin> obj_refs (get tcb); arm_global_pd (arch_state s) \<notin> untyped_range (get tcb); arm_global_pd (arch_state s) \<notin> obj_refs (get tcb); (range (interrupt_irq_node s) \<union> set (arm_global_pts (arch_state s))) \<inter> (untyped_range (get tcb) \<union> obj_refs (get tcb)) = {}; get tcb = ArchObjectCap x12\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!