theory ArchFinalise_AI

lemma valid_idle_has_null_cap_ARCH[Finalise_AI_asms]:
  "\<lbrakk> if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s\<rbrakk>
   \<Longrightarrow> caps_of_state s (idle_thread s, v) = Some cap
   \<Longrightarrow> cap = NullCap" apply (rule ccontr) apply (drule(1) if_unsafe_then_capD[OF caps_of_state_cteD]) apply clarsimp apply (clarsimp simp: ex_cte_cap_wp_to_def cte_wp_at_caps_of_state) apply (frule(1) valid_global_refsD2) apply (case_tac capa, simp_all add: cap_range_def global_refs_def)[1] apply (clarsimp simp: valid_irq_node_def valid_idle_def pred_tcb_at_def
                        obj_at_def is_cap_table_def) apply (rename_tac word tcb) apply (drule_tac x=word in spec, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; caps_of_state s (idle_thread s, v) = Some cap\<rbrakk> \<Longrightarrow> cap = NullCap proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; caps_of_state s (idle_thread s, v) = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>capa. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; cap \<noteq> NullCap; cap = capa\<rbrakk> \<Longrightarrow> capa \<noteq> NullCap
 2. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; cap \<noteq> NullCap; ex_cte_cap_wp_to (\<lambda>capa. \<exists>cap'. cap = cap' \<and> appropriate_cte_cap cap' capa) (idle_thread s, v) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; cap \<noteq> NullCap; ex_cte_cap_wp_to (\<lambda>capa. \<exists>cap'. cap = cap' \<and> appropriate_cte_cap cap' capa) (idle_thread s, v) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; cap \<noteq> NullCap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (idle_thread s, v) \<in> cte_refs capa (interrupt_irq_node s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; cap \<noteq> NullCap; caps_of_state s (a, b) = Some capa; appropriate_cte_cap cap capa; (idle_thread s, v) \<in> cte_refs capa (interrupt_irq_node s); global_refs s \<inter> cap_range capa = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b capa x10. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; valid_idle s; valid_irq_node s; cap \<noteq> NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap x10); appropriate_cte_cap cap (IRQHandlerCap x10); idle_thread s = interrupt_irq_node s x10 \<and> v = []; capa = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b x10 tcb. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; cap \<noteq> NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap x10); appropriate_cte_cap cap (IRQHandlerCap x10); interrupt_irq_node s x10 = idle_thread_ptr; inj (interrupt_irq_node s); \<forall>irq. \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> (case ko of CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False); idle_thread s = idle_thread_ptr; v = []; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>a b word tcb. \<lbrakk>if_unsafe_then_cap s; valid_global_refs s; cap \<noteq> NullCap; caps_of_state s (a, b) = Some (IRQHandlerCap word); appropriate_cte_cap cap (IRQHandlerCap word); interrupt_irq_node s word = idle_thread_ptr; inj (interrupt_irq_node s); \<forall>irq. \<exists>ko. kheap s (interrupt_irq_node s irq) = Some ko \<and> (case ko of CNode sz cs \<Rightarrow> 0 = sz \<and> well_formed_cnode_n 0 cs | _ \<Rightarrow> False); idle_thread s = idle_thread_ptr; v = []; kheap s idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!