theory Finalise_DR

lemma zombie_cap_has_all:
  "\<lbrakk>valid_objs s;if_unsafe_then_cap s; zombies_final s;valid_global_refs s;
    caps_of_state s slot = Some (cap.Zombie w option n);
    (w,x) \<notin> cte_refs (cap.Zombie w option n) f  \<rbrakk>
    \<Longrightarrow>  caps_of_state s (w,x) = None \<or> caps_of_state s (w,x) = Some cap.NullCap" apply (clarsimp simp:if_unsafe_then_cap_def valid_cap_def split:option.splits) apply (drule_tac x = w in spec,drule_tac x = x in spec) apply (rule ccontr) apply clarsimp apply (clarsimp simp:ex_cte_cap_wp_to_def appropriate_cte_cap_def) apply (drule iffD1[OF cte_wp_at_caps_of_state]) apply clarsimp apply (frule_tac p = slot and p'="(a,b)" in zombies_final_ccontr) apply simp+ apply (simp add:is_zombie_def) apply simp+ apply (case_tac cap; simp) apply (case_tac y; simp) apply (frule_tac p = "(a,b)" in caps_of_state_valid_cap) apply simp apply (frule_tac p = slot in caps_of_state_valid_cap) apply simp apply (rename_tac word w2 w3 rights) apply (clarsimp simp:valid_cap_def tcb_at_def dest!:get_tcb_SomeD) apply (drule_tac p = "(interrupt_irq_node s word,[])" in caps_of_state_cteD) apply (clarsimp simp:cte_wp_at_cases) apply (clarsimp simp:obj_at_def tcb_cap_cases_def tcb_cnode_index_def to_bl_1 split:if_splits) apply (drule valid_globals_irq_node[OF _ caps_of_state_cteD]) apply simp apply (fastforce simp:cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; if_unsafe_then_cap s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); (w, x) \<notin> cte_refs (Zombie w option n) f\<rbrakk> \<Longrightarrow> caps_of_state s (w, x) = None \<or> caps_of_state s (w, x) = Some cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (a, b) s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; caps_of_state s (w, x) \<noteq> Some cap.NullCap\<rbrakk> \<Longrightarrow> caps_of_state s (w, x) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; caps_of_state s (w, x) \<noteq> Some cap.NullCap; \<forall>cap. caps_of_state s (w, x) = Some cap \<longrightarrow> cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (w, x) s\<rbrakk> \<Longrightarrow> caps_of_state s (w, x) = None proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; caps_of_state s (w, x) \<noteq> Some cap.NullCap; \<forall>cap. caps_of_state s (w, x) = Some cap \<longrightarrow> cap \<noteq> cap.NullCap \<longrightarrow> ex_cte_cap_wp_to (appropriate_cte_cap cap) (w, x) s; caps_of_state s (w, x) \<noteq> None\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; ex_cte_cap_wp_to (appropriate_cte_cap y) (w, x) s; caps_of_state s (w, x) = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; cte_wp_at (\<lambda>c. (case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs c = {}) \<and> (w, x) \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; \<exists>cap. caps_of_state s (a, b) = Some cap \<and> (case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}) \<and> (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (5 subgoals):
 1. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> ?r15 y a b cap \<in> obj_refs (Zombie w option n)
 2. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> is_zombie (Zombie w option n)
 3. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> zombies_final s
 4. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some (?cap'15 y a b cap)
 5. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s); ?r15 y a b cap \<in> obj_refs (?cap'15 y a b cap) \<longrightarrow> is_zombie (?cap'15 y a b cap) \<and> slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> is_zombie (Zombie w option n)
 2. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> zombies_final s
 3. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some (?cap'15 y a b cap)
 4. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s); w \<in> obj_refs (?cap'15 y a b cap) \<longrightarrow> is_zombie (?cap'15 y a b cap) \<and> slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> zombies_final s
 2. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> caps_of_state s (a, b) = Some (?cap'15 y a b cap)
 3. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s); w \<in> obj_refs (?cap'15 y a b cap) \<longrightarrow> is_zombie (?cap'15 y a b cap) \<and> slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie w option n); length x = zombie_cte_bits option \<longrightarrow> \<not> unat (of_bl x) < n; y \<noteq> cap.NullCap; caps_of_state s (w, x) = Some y; caps_of_state s (a, b) = Some cap; case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; (w, x) \<in> cte_refs cap (interrupt_irq_node s); w \<in> obj_refs cap \<longrightarrow> is_zombie cap \<and> slot = (a, b)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap x10. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; y \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s x10, []) = Some y; caps_of_state s (a, b) = Some (IRQHandlerCap x10); case y of cap.NullCap \<Rightarrow> True | cap.NotificationCap x xa xb \<Rightarrow> True | _ \<Rightarrow> cap_irqs cap = {}; w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43; s \<turnstile> IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43; s \<turnstile> IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43; s \<turnstile> IRQHandlerCap x10\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43; s \<turnstile> IRQHandlerCap x10; s \<turnstile> Zombie (interrupt_irq_node s x10) option n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap x10 x41 x42 x43. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s x10) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s x10, []) = Some (cap.NotificationCap x41 x42 x43); caps_of_state s (a, b) = Some (IRQHandlerCap x10); w = interrupt_irq_node s x10 \<and> x = []; cap = IRQHandlerCap x10; y = cap.NotificationCap x41 x42 x43; s \<turnstile> IRQHandlerCap x10; s \<turnstile> Zombie (interrupt_irq_node s x10) option n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap word w2 w3 rights. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s word, []) = Some (cap.NotificationCap w2 w3 rights); caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word \<and> x = []; cap = IRQHandlerCap word; y = cap.NotificationCap w2 w3 rights; s \<turnstile> IRQHandlerCap word; s \<turnstile> Zombie (interrupt_irq_node s word) option n\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b word w2 w3 rights. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (interrupt_irq_node s word, []) = Some (cap.NotificationCap w2 w3 rights); caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b word w2 w3 rights. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0; cte_wp_at ((=) (cap.NotificationCap w2 w3 rights)) (interrupt_irq_node s word, []) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b word w2 w3 rights. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0; (\<exists>sz fun. kheap s (interrupt_irq_node s word) = Some (kernel_object.CNode sz fun) \<and> well_formed_cnode_n sz fun \<and> fun [] = Some (cap.NotificationCap w2 w3 rights)) \<or> (\<exists>tcb. kheap s (interrupt_irq_node s word) = Some (TCB tcb) \<and> (\<exists>get. (\<exists>set restr. tcb_cap_cases [] = Some (get, set, restr)) \<and> cap.NotificationCap w2 w3 rights = get tcb))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b word w2 w3 rights sz fun. \<lbrakk>valid_objs s; zombies_final s; valid_global_refs s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0; kheap s (interrupt_irq_node s word) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun [] = Some (cap.NotificationCap w2 w3 rights)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>a b word w2 w3 rights sz fun. \<lbrakk>valid_objs s; zombies_final s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0; kheap s (interrupt_irq_node s word) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun [] = Some (cap.NotificationCap w2 w3 rights)\<rbrakk> \<Longrightarrow> caps_of_state s (?ptr88 a b word w2 w3 rights sz fun) = Some (?cap88 a b word w2 w3 rights sz fun)
 2. \<And>a b word w2 w3 rights sz fun. \<lbrakk>valid_objs s; zombies_final s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0; kheap s (interrupt_irq_node s word) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun [] = Some (cap.NotificationCap w2 w3 rights); interrupt_irq_node s (?irq88 a b word w2 w3 rights sz fun) \<notin> cap_range (?cap88 a b word w2 w3 rights sz fun)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b word w2 w3 rights sz fun. \<lbrakk>valid_objs s; zombies_final s; caps_of_state s slot = Some (Zombie (interrupt_irq_node s word) option n); zombie_cte_bits option = 0 \<longrightarrow> n = 0; caps_of_state s (a, b) = Some (IRQHandlerCap word); w = interrupt_irq_node s word; x = []; cap_aligned (IRQHandlerCap word); word \<le> maxIRQ; cap_aligned (Zombie (interrupt_irq_node s word) option n); case option of None \<Rightarrow> tcb_at (interrupt_irq_node s word) s \<and> n \<le> 5 | Some b \<Rightarrow> cap_table_at b (interrupt_irq_node s word) s \<and> n \<le> 2 ^ b \<and> b \<noteq> 0; kheap s (interrupt_irq_node s word) = Some (kernel_object.CNode sz fun); well_formed_cnode_n sz fun; fun [] = Some (cap.NotificationCap w2 w3 rights); interrupt_irq_node s (?irq88 a b word w2 w3 rights sz fun) \<notin> cap_range (Zombie (interrupt_irq_node s word) option n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!