theory CNode_DR

lemma delete_cap_corres:
  "dcorres (dc \<oplus> dc) (\<lambda>_. True) (cap_table_at (length b) a and invs and valid_etcbs
                                     and valid_pdpt_objs and ct_active)
             (delete_cap (transform_cslot_ptr (a, b))) (cap_delete (a, b))" apply (simp add:delete_cap_def cap_delete_def) apply (subst rec_del_simps_ext) apply (simp add:bindE_assoc) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF dcorres_finalise_slot]) apply (clarsimp simp:bindE_assoc when_def) apply (rule empty_slot_corres) apply wp+ apply (rule validE_validE_R) apply (simp add:validE_def weak_valid_mdb_def) apply (rule hoare_drop_imp) apply (rule_tac Q = "\<lambda>r. invs and not_idle_thread a and valid_etcbs" in hoare_strengthen_post) apply (wp rec_del_invs) apply (simp add:not_idle_thread_def validE_def) apply wp apply (clarsimp simp:invs_def valid_state_def valid_mdb_def) apply clarsimp+ apply (simp add:cap_table_at_cte_at) apply (clarsimp simp:emptyable_def obj_at_def is_cap_table_def) apply (clarsimp simp:is_tcb_def split:Structures_A.kernel_object.splits) apply (clarsimp simp:invs_def valid_state_def) apply (drule cnode_not_idle,simp) apply (simp add:not_idle_thread_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) (delete_cap (transform_cslot_ptr (a, b))) (cap_delete (a, b)) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) (doE y <- CSpace_D.finalise_slot (transform_cslot_ptr (a, b));
liftE (PageTableUnmap_D.empty_slot (transform_cslot_ptr (a, b)))
odE) (doE y <- rec_del (CTEDeleteCall (a, b) True);
returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and ct_active) (doE y <- CSpace_D.finalise_slot (transform_cslot_ptr (a, b));
liftE (PageTableUnmap_D.empty_slot (transform_cslot_ptr (a, b)))
odE) (doE y <- doE (success, cleanup_info) <- rec_del (FinaliseSlotCall (a, b) True);
without_preemption $ when (True \<or> success) $ IpcCancel_A.empty_slot (a, b) cleanup_info;
returnOk undefined
odE;
returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) (doE y <- CSpace_D.finalise_slot (transform_cslot_ptr (a, b));
liftE (PageTableUnmap_D.empty_slot (transform_cslot_ptr (a, b)))
odE) (doE x <- rec_del (FinaliseSlotCall (a, b) True);
y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot (a, b) cleanup_info);
returnOk undefined
odE;
returnOk ()
odE) proof (prove)
goal (3 subgoals):
 1. dcorres (dc \<oplus> dc) ?Q4 ?Q'4 (doE y <- CSpace_D.finalise_slot (transform_cslot_ptr (a, b));
liftE (PageTableUnmap_D.empty_slot (transform_cslot_ptr (a, b)))
odE) (doE x <- rec_del (FinaliseSlotCall (a, b) True);
y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot (a, b) cleanup_info);
returnOk undefined
odE;
returnOk ()
odE)
 2. \<And>s. True \<Longrightarrow> ?Q4 s
 3. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> ?Q'4 s proof (prove)
goal (5 subgoals):
 1. \<And>y x. dc y x \<Longrightarrow> dcorres (dc \<oplus> dc) (?R8 y) (?R'8 x) (liftE (PageTableUnmap_D.empty_slot (transform_cslot_ptr (a, b)))) (doE y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot (a, b) cleanup_info);
returnOk undefined
odE;
returnOk ()
odE)
 2. \<lbrace>?Q8\<rbrace> CSpace_D.finalise_slot (transform_cslot_ptr (a, b)) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and ?Q'8) s proof (prove)
goal (5 subgoals):
 1. \<And>aa ba. dcorres dc (?R8 ()) (?R'8 (aa, ba)) (PageTableUnmap_D.empty_slot (transform_cslot_ptr (a, b))) (IpcCancel_A.empty_slot (a, b) ba)
 2. \<lbrace>?Q8\<rbrace> CSpace_D.finalise_slot (transform_cslot_ptr (a, b)) \<lbrace>?R8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'8\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>?R'8\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 5. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and ?Q'8) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q8\<rbrace> CSpace_D.finalise_slot (transform_cslot_ptr (a, b)) \<lbrace>\<lambda>a b. True\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<lbrace>?Q'8\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>c. weak_valid_mdb and valid_idle and not_idle_thread (fst (a, b)) and valid_etcbs\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q8) s
 4. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and ?Q'8) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'23\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>rv s. weak_valid_mdb s \<and> valid_idle s \<and> not_idle_thread (fst (a, b)) s \<and> valid_etcbs s\<rbrace>, -
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'23\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>rv s. weak_valid_mdb s \<and> valid_idle s \<and> not_idle_thread (fst (a, b)) s \<and> valid_etcbs s\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'23\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>v s. (\<exists>a b. v = Inr (a, b)) \<longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> no_mloop (cdt s) \<and> valid_idle s \<and> not_idle_thread a s \<and> valid_etcbs s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'23\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> no_mloop (cdt s) \<and> valid_idle s \<and> not_idle_thread a s \<and> valid_etcbs s\<rbrace>
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'23\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>r. invs and not_idle_thread a and valid_etcbs\<rbrace>
 2. \<And>rv s. (invs and not_idle_thread a and valid_etcbs) s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> no_mloop (cdt s) \<and> valid_idle s \<and> not_idle_thread a s \<and> valid_etcbs s
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> ?P'23 s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'38\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>rv s. not_idle_thread a s \<and> valid_etcbs s\<rbrace>, \<lbrace>\<lambda>rv s. not_idle_thread a s \<and> valid_etcbs s\<rbrace>
 2. \<And>rv s. (invs and not_idle_thread a and valid_etcbs) s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> no_mloop (cdt s) \<and> valid_idle s \<and> not_idle_thread a s \<and> valid_etcbs s
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> (invs and valid_rec_del_call (FinaliseSlotCall (a, b) True) and (\<lambda>s. \<not> exposed_rdcall (FinaliseSlotCall (a, b) True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (FinaliseSlotCall (a, b) True)) s) and emptyable (slot_rdcall (FinaliseSlotCall (a, b) True)) and (\<lambda>s. case FinaliseSlotCall (a, b) True of ReduceZombieCall cap sl ex \<Rightarrow> \<not> CSpace_A.cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<and> ?P'38 s)) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?P'38\<rbrace> rec_del (FinaliseSlotCall (a, b) True) \<lbrace>\<lambda>v s. a \<noteq> idle_thread s \<and> valid_etcbs s\<rbrace>
 2. \<And>rv s. (invs and not_idle_thread a and valid_etcbs) s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> no_mloop (cdt s) \<and> valid_idle s \<and> not_idle_thread a s \<and> valid_etcbs s
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 4. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> (invs and valid_rec_del_call (FinaliseSlotCall (a, b) True) and (\<lambda>s. \<not> exposed_rdcall (FinaliseSlotCall (a, b) True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (FinaliseSlotCall (a, b) True)) s) and emptyable (slot_rdcall (FinaliseSlotCall (a, b) True)) and (\<lambda>s. case FinaliseSlotCall (a, b) True of ReduceZombieCall cap sl ex \<Rightarrow> \<not> CSpace_A.cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<and> ?P'38 s)) s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (invs and not_idle_thread a and valid_etcbs) s \<Longrightarrow> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) \<and> no_mloop (cdt s) \<and> valid_idle s \<and> not_idle_thread a s \<and> valid_etcbs s
 2. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 3. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> (invs and valid_rec_del_call (FinaliseSlotCall (a, b) True) and (\<lambda>s. \<not> exposed_rdcall (FinaliseSlotCall (a, b) True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (FinaliseSlotCall (a, b) True)) s) and emptyable (slot_rdcall (FinaliseSlotCall (a, b) True)) and (\<lambda>s. case FinaliseSlotCall (a, b) True of ReduceZombieCall cap sl ex \<Rightarrow> \<not> CSpace_A.cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<and> a \<noteq> idle_thread s \<and> valid_etcbs s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. True \<and> True)) s
 2. \<And>s. (cap_table_at (length b) a and invs and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and ct_active) s \<Longrightarrow> (invs and cte_wp_at (\<lambda>_. True) (a, b) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (a, b) and not_idle_thread (fst (a, b)) and (\<lambda>s. True \<and> (invs and valid_rec_del_call (FinaliseSlotCall (a, b) True) and (\<lambda>s. \<not> exposed_rdcall (FinaliseSlotCall (a, b) True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (FinaliseSlotCall (a, b) True)) s) and emptyable (slot_rdcall (FinaliseSlotCall (a, b) True)) and (\<lambda>s. case FinaliseSlotCall (a, b) True of ReduceZombieCall cap sl ex \<Rightarrow> \<not> CSpace_A.cap_removeable cap sl \<and> (\<forall>t\<in>obj_refs cap. halted_if_tcb t s) | _ \<Rightarrow> True)) s \<and> a \<noteq> idle_thread s \<and> valid_etcbs s)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_table_at (length b) a s; invs s; valid_etcbs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ct_active s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>_. True) (a, b) s \<and> emptyable (a, b) s \<and> not_idle_thread a s \<and> emptyable (a, b) s \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>cap_table_at (length b) a s; invs s; valid_etcbs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ct_active s\<rbrakk> \<Longrightarrow> emptyable (a, b) s \<and> not_idle_thread a s \<and> emptyable (a, b) s \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s ko. \<lbrakk>invs s; valid_etcbs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ct_active s; kheap s a = Some ko; case ko of kernel_object.CNode sz cs \<Rightarrow> length b = sz \<and> well_formed_cnode_n (length b) cs | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> (is_tcb ko \<and> b = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted a s) \<and> not_idle_thread a s \<and> (is_tcb ko \<and> b = tcb_cnode_index 2 \<longrightarrow> st_tcb_at halted a s) \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x12. \<lbrakk>invs s; valid_etcbs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ct_active s; kheap s a = Some (kernel_object.CNode (length b) x12); well_formed_cnode_n (length b) x12\<rbrakk> \<Longrightarrow> not_idle_thread a s \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x12. \<lbrakk>valid_etcbs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ct_active s; kheap s a = Some (kernel_object.CNode (length b) x12); well_formed_cnode_n (length b) x12; 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; valid_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> not_idle_thread a s \<and> a \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<And>s x12. \<lbrakk>valid_etcbs s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; ct_active s; kheap s a = Some (kernel_object.CNode (length b) x12); well_formed_cnode_n (length b) x12; valid_pspace s; valid_mdb s; valid_ioc 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; valid_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; not_idle_thread a s\<rbrakk> \<Longrightarrow> not_idle_thread a s \<and> a \<noteq> idle_thread s proof (prove)
goal:
No subgoals!