theory ArchFinalise_AI

lemma (* get_irq_slot_fast_finalisable *)[wp,Finalise_AI_asms]:
  "\<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>cte_wp_at can_fast_finalise\<rbrace>" apply (simp add: get_irq_slot_def) apply wp apply (clarsimp simp: invs_def valid_state_def valid_irq_node_def) apply (drule spec[where x=irq], drule cap_table_at_cte_at[where offset="[]"]) apply simp apply (clarsimp simp: cte_wp_at_caps_of_state) apply (case_tac "cap = cap.NullCap") apply (simp add: can_fast_finalise_def) apply (frule(1) if_unsafe_then_capD [OF caps_of_state_cteD]) apply simp apply (clarsimp simp: ex_cte_cap_wp_to_def) apply (drule cte_wp_at_norm, clarsimp) apply (drule(1) valid_global_refsD [OF _ _ irq_node_global_refs_ARCH[where irq=irq]]) apply (case_tac c, simp_all) apply (clarsimp simp: cap_range_def) apply (clarsimp simp: cap_range_def) apply (clarsimp simp: appropriate_cte_cap_def can_fast_finalise_def split: cap.split_asm) apply (clarsimp simp: cap_range_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> get_irq_slot irq \<lbrace>cte_wp_at can_fast_finalise\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> gets (\<lambda>st. (interrupt_irq_node st irq, [])) \<lbrace>cte_wp_at can_fast_finalise\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> cte_wp_at can_fast_finalise (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> cte_wp_at can_fast_finalise (interrupt_irq_node s irq, []) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> length [] = 0
 2. \<And>s. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> cte_wp_at can_fast_finalise (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; cte_wp_at (\<lambda>_. True) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> cte_wp_at can_fast_finalise (interrupt_irq_node s irq, []) s proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap = NullCap\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 2. \<And>s cap. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (2 subgoals):
 1. \<And>s cap capa. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cap = capa\<rbrakk> \<Longrightarrow> capa \<noteq> NullCap
 2. \<And>s cap. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; ex_cte_cap_wp_to (\<lambda>capa. \<exists>cap'. cap = cap' \<and> appropriate_cte_cap cap' capa) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; ex_cte_cap_wp_to (\<lambda>capa. \<exists>cap'. cap = cap' \<and> appropriate_cte_cap cap' capa) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at (\<lambda>c. appropriate_cte_cap cap c \<and> (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s)) (a, b) s\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b c. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) c) (a, b) s; appropriate_cte_cap cap c; (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b c. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) c) (a, b) s; appropriate_cte_cap cap c; (interrupt_irq_node s irq, []) \<in> cte_refs c (interrupt_irq_node s); interrupt_irq_node s irq \<notin> cap_range c\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (4 subgoals):
 1. \<And>s cap a b c x61 x63. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (x61, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (CNodeCap x61 0 x63)) (a, b) s; interrupt_irq_node s irq = x61; x61 \<notin> cap_range (CNodeCap x61 0 x63); c = CNodeCap x61 0 x63\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 2. \<And>s cap a b c. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (ThreadCap (interrupt_irq_node s irq))) (a, b) s; [] \<in> dom tcb_cap_cases; interrupt_irq_node s irq \<notin> cap_range (ThreadCap (interrupt_irq_node s irq)); c = ThreadCap (interrupt_irq_node s irq)\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 3. \<And>s cap a b c x10. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s x10, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (IRQHandlerCap x10)) (a, b) s; appropriate_cte_cap cap (IRQHandlerCap x10); interrupt_irq_node s irq = interrupt_irq_node s x10; interrupt_irq_node s x10 \<notin> cap_range (IRQHandlerCap x10); c = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 4. \<And>s cap a b c x112 x113. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (Zombie (interrupt_irq_node s irq) x112 x113)) (a, b) s; zombie_cte_bits x112 = 0 \<and> 0 < x113; interrupt_irq_node s irq \<notin> cap_range (Zombie (interrupt_irq_node s irq) x112 x113); c = Zombie (interrupt_irq_node s irq) x112 x113\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (3 subgoals):
 1. \<And>s cap a b c. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (ThreadCap (interrupt_irq_node s irq))) (a, b) s; [] \<in> dom tcb_cap_cases; interrupt_irq_node s irq \<notin> cap_range (ThreadCap (interrupt_irq_node s irq)); c = ThreadCap (interrupt_irq_node s irq)\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 2. \<And>s cap a b c x10. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s x10, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (IRQHandlerCap x10)) (a, b) s; appropriate_cte_cap cap (IRQHandlerCap x10); interrupt_irq_node s irq = interrupt_irq_node s x10; interrupt_irq_node s x10 \<notin> cap_range (IRQHandlerCap x10); c = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 3. \<And>s cap a b c x112 x113. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (Zombie (interrupt_irq_node s irq) x112 x113)) (a, b) s; zombie_cte_bits x112 = 0 \<and> 0 < x113; interrupt_irq_node s irq \<notin> cap_range (Zombie (interrupt_irq_node s irq) x112 x113); c = Zombie (interrupt_irq_node s irq) x112 x113\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (2 subgoals):
 1. \<And>s cap a b c x10. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s x10, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (IRQHandlerCap x10)) (a, b) s; appropriate_cte_cap cap (IRQHandlerCap x10); interrupt_irq_node s irq = interrupt_irq_node s x10; interrupt_irq_node s x10 \<notin> cap_range (IRQHandlerCap x10); c = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> can_fast_finalise cap
 2. \<And>s cap a b c x112 x113. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (Zombie (interrupt_irq_node s irq) x112 x113)) (a, b) s; zombie_cte_bits x112 = 0 \<and> 0 < x113; interrupt_irq_node s irq \<notin> cap_range (Zombie (interrupt_irq_node s irq) x112 x113); c = Zombie (interrupt_irq_node s irq) x112 x113\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal (1 subgoal):
 1. \<And>s cap a b c x112 x113. \<lbrakk>valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_arch_state s; inj (interrupt_irq_node s); valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; caps_of_state s (interrupt_irq_node s irq, []) = Some cap; cap \<noteq> NullCap; cte_wp_at ((=) (Zombie (interrupt_irq_node s irq) x112 x113)) (a, b) s; zombie_cte_bits x112 = 0 \<and> 0 < x113; interrupt_irq_node s irq \<notin> cap_range (Zombie (interrupt_irq_node s irq) x112 x113); c = Zombie (interrupt_irq_node s irq) x112 x113\<rbrakk> \<Longrightarrow> can_fast_finalise cap proof (prove)
goal:
No subgoals!