theory Interrupt_DR

lemma irq_state_IRQSignal_NullCap:
  "\<lbrakk> caps_of_state s (interrupt_irq_node s irq, []) \<noteq> None;
     interrupt_states s irq \<noteq> irq_state.IRQSignal;
     if_unsafe_then_cap s; valid_global_refs s;
     valid_irq_node s; valid_irq_handlers s \<rbrakk>
      \<Longrightarrow> caps_of_state s (interrupt_irq_node s irq, []) = Some cap.NullCap" apply (rule ccontr, clarsimp) apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD]) apply simp apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply (frule(1) valid_global_refsD2) apply (case_tac cap, simp_all add: cap_range_def global_refs_def) apply (safe, simp_all) apply (clarsimp simp: valid_irq_node_def inj_on_eq_iff[where f="interrupt_irq_node s"]) apply (simp add: valid_irq_handlers_def) apply (drule bspec, erule ranI) apply (simp add: irq_issued_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>caps_of_state s (interrupt_irq_node s irq, []) \<noteq> None; interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s\<rbrakk> \<Longrightarrow> caps_of_state s (interrupt_irq_node s irq, []) = Some cap.NullCap proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (interrupt_irq_node s irq, []) = Some y\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y cap. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; y = cap\<rbrakk> \<Longrightarrow> cap \<noteq> cap.NullCap
 2. \<And>y. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. y = cap' \<and> appropriate_cte_cap cap' cap) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; ex_cte_cap_wp_to (\<lambda>cap. \<exists>cap'. y = cap' \<and> appropriate_cte_cap cap' cap) (interrupt_irq_node s irq, []) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some cap; appropriate_cte_cap y cap; (interrupt_irq_node s irq, []) \<in> cte_refs cap (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b cap. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some cap; appropriate_cte_cap y cap; (interrupt_irq_node s irq, []) \<in> cte_refs cap (interrupt_irq_node s); global_refs s \<inter> cap_range cap = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>y a b cap x61 x63. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some (cap.CNodeCap x61 0 x63); interrupt_irq_node s irq = x61; x61 \<noteq> idle_thread s \<and> x61 \<noteq> arm_global_pd (arch_state s) \<and> x61 \<notin> range (interrupt_irq_node s) \<and> x61 \<notin> set (arm_global_pts (arch_state s)); cap = cap.CNodeCap x61 0 x63\<rbrakk> \<Longrightarrow> False
 2. \<And>y a b cap x10. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap x10); appropriate_cte_cap y (IRQHandlerCap x10); interrupt_irq_node s irq = interrupt_irq_node s x10; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b x10. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_node s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap x10); appropriate_cte_cap y (IRQHandlerCap x10); interrupt_irq_node s irq = interrupt_irq_node s x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; valid_irq_handlers s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap irq); appropriate_cte_cap y (IRQHandlerCap irq); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; \<forall>cap\<in>ran (caps_of_state s). \<forall>irq\<in>cap_irqs cap. irq_issued irq s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap irq); appropriate_cte_cap y (IRQHandlerCap irq); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>y a b. \<lbrakk>interrupt_states s irq \<noteq> IRQSignal; if_unsafe_then_cap s; valid_global_refs s; y \<noteq> cap.NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap irq); appropriate_cte_cap y (IRQHandlerCap irq); inj (interrupt_irq_node s); \<forall>irq. cap_table_at 0 (interrupt_irq_node s irq) s; \<forall>irq\<in>cap_irqs (IRQHandlerCap irq). irq_issued irq s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!