theory ArchFinalise_AI

lemma (* deleting_irq_handler_slot_not_irq_node *)[Finalise_AI_asms]:
  "\<lbrace>if_unsafe_then_cap and valid_global_refs
           and cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) sl\<rbrace>
     deleting_irq_handler irq
   \<lbrace>\<lambda>rv s. (interrupt_irq_node s irq, []) \<noteq> sl\<rbrace>" apply (simp add: deleting_irq_handler_def) apply wp apply clarsimp apply (drule(1) if_unsafe_then_capD) apply clarsimp apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply (drule cte_refs_obj_refs_elem) apply (erule disjE) apply simp apply (drule(1) valid_global_refsD[OF _ caps_of_state_cteD]) prefer 2 apply (erule notE, simp add: cap_range_def, erule disjI2) apply (simp add: global_refs_def) apply (clarsimp simp: appropriate_cte_cap_def split: cap.split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and valid_global_refs and cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) sl\<rbrace> deleting_irq_handler irq \<lbrace>\<lambda>rv s. (interrupt_irq_node s irq, []) \<noteq> sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap and valid_global_refs and cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) sl\<rbrace> get_irq_slot irq >>= cap_delete_one \<lbrace>\<lambda>rv s. (interrupt_irq_node s irq, []) \<noteq> sl\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (if_unsafe_then_cap and valid_global_refs and cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) sl) s \<Longrightarrow> (interrupt_irq_node s irq, []) \<noteq> sl proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; cte_wp_at (\<lambda>cp. cap_irqs cp \<noteq> {}) (interrupt_irq_node s irq, []) s; sl = (interrupt_irq_node s irq, [])\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s cap. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); cap_irqs cap \<noteq> {}\<rbrakk> \<Longrightarrow> cap \<noteq> NullCap
 2. \<And>s. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap_irqs cap' \<noteq> {} \<and> appropriate_cte_cap cap' cap) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. cap_irqs cap' \<noteq> {} \<and> appropriate_cte_cap cap' cap) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; (interrupt_irq_node s irq, []) \<in> cte_refs cap (interrupt_irq_node s); cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; fst (interrupt_irq_node s irq, []) \<in> obj_refs cap \<or> (\<exists>irq. cap = IRQHandlerCap irq)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; fst (interrupt_irq_node s irq, []) \<in> obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; interrupt_irq_node s irq \<in> obj_refs cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; interrupt_irq_node s irq \<in> obj_refs cap\<rbrakk> \<Longrightarrow> ?r31 s a b cap cap' \<in> global_refs s
 2. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; interrupt_irq_node s irq \<in> obj_refs cap; ?r31 s a b cap cap' \<notin> cap_range cap\<rbrakk> \<Longrightarrow> False
 3. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; interrupt_irq_node s irq \<in> obj_refs cap; ?r31 s a b cap cap' \<notin> cap_range cap\<rbrakk> \<Longrightarrow> False
 2. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; interrupt_irq_node s irq \<in> obj_refs cap\<rbrakk> \<Longrightarrow> ?r31 s a b cap cap' \<in> global_refs s
 3. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; interrupt_irq_node s irq \<in> obj_refs cap\<rbrakk> \<Longrightarrow> interrupt_irq_node s irq \<in> global_refs s
 2. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s a b cap cap'. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; sl = (interrupt_irq_node s irq, []); caps_of_state s (a, b) = Some cap; cap_irqs cap' \<noteq> {}; appropriate_cte_cap cap' cap; \<exists>irq. cap = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!