theory Finalise_R

lemma emptySlot_ifunsafe'[wp]:
  "\<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace>
     emptySlot sl opt
   \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" apply (simp add: ifunsafe'_def3) apply (rule hoare_pre, rule hoare_use_eq_irq_node'[OF emptySlot_irq_node']) apply (simp add: emptySlot_def case_Null_If) apply (wp opt_return_pres_lift | simp add: o_def)+ apply (wp getCTE_cteCap_wp clearUntypedFreeIndex_cteCaps_of)+ apply (clarsimp simp: tree_cte_cteCap_eq[unfolded o_def]
                        modify_map_same
                        modify_map_comp[symmetric]
                 split: option.split_asm if_split_asm
                 dest!: modify_map_K_D) apply (clarsimp simp: modify_map_def) apply (drule_tac x=cref in spec, clarsimp) apply (case_tac "cref' \<noteq> sl") apply (rule_tac x=cref' in exI) apply (clarsimp simp: modify_map_def) apply (simp add: removeable'_def) apply (erule disjE) apply (clarsimp simp: modify_map_def) apply (subst(asm) tree_cte_cteCap_eq[unfolded o_def]) apply (clarsimp split: option.split_asm dest!: capMaster_same_refs) apply fastforce apply clarsimp apply (drule(1) bspec) apply (clarsimp simp: cte_wp_at_ctes_of cteCaps_of_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. if_unsafe_then_cap' s \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P6 f\<rbrace> emptySlot sl opt \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' f)\<rbrace>
 2. \<And>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s \<Longrightarrow> ?P6 (irq_node' s) s proof (prove)
goal (2 subgoals):
 1. \<And>f. \<lbrace>?P6 f\<rbrace> do y <- clearUntypedFreeIndex sl;
newCTE <- getCTE sl;
if cteCap newCTE = capability.NullCap then return () else do y <- updateMDB (mdbPrev (cteMDBNode newCTE)) (mdbNext_update (\<lambda>_. mdbNext (cteMDBNode newCTE)));
y <- updateMDB (mdbNext (cteMDBNode newCTE)) (\<lambda>mdb. mdbFirstBadged_update (\<lambda>_. mdbFirstBadged mdb \<or> mdbFirstBadged (cteMDBNode newCTE)) (mdbPrev_update (\<lambda>_. mdbPrev (cteMDBNode newCTE)) mdb));
y <- updateCap sl capability.NullCap;
y <- updateMDB sl (const nullMDBNode);
global.postCapDeletion opt
od
od \<lbrace>\<lambda>rv s. \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' f)\<rbrace>
 2. \<And>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s \<Longrightarrow> ?P6 (irq_node' s) s proof (prove)
goal (3 subgoals):
 1. \<And>f. \<lbrace>?B17 f ()\<rbrace> getCTE sl \<lbrace>\<lambda>newCTE s. (cteCap newCTE = capability.NullCap \<longrightarrow> (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' f))) \<and> (cteCap newCTE \<noteq> capability.NullCap \<longrightarrow> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' f)))\<rbrace>
 2. \<And>f. \<lbrace>?P6 f\<rbrace> clearUntypedFreeIndex sl \<lbrace>?B17 f\<rbrace>
 3. \<And>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s \<Longrightarrow> ?P6 (irq_node' s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) \<and> cte_wp_at' (\<lambda>cte. removeable' sl s (cteCap cte)) sl s \<Longrightarrow> case cteCaps_of s sl of None \<Rightarrow> True | Some cap \<Rightarrow> (cap = capability.NullCap \<longrightarrow> (\<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) \<and> (cap \<noteq> capability.NullCap \<longrightarrow> (\<forall>cref. (\<exists>cap. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cref cap. \<lbrakk>cteCaps_of s sl = Some x2; \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap\<rbrakk> \<Longrightarrow> \<exists>cref' cap'. modify_map (cteCaps_of s) sl (\<lambda>a. capability.NullCap) cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cref cap. \<lbrakk>cteCaps_of s sl = Some x2; \<forall>cref. (\<exists>cap. cteCaps_of s cref = Some cap \<and> cap \<noteq> capability.NullCap) \<longrightarrow> (\<exists>cref' cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)); removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some x2; removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cteCaps_of s cref' = Some cap'; cref \<in> cte_refs' cap' (irq_node' s)\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some x2; removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cteCaps_of s cref' = Some cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' \<noteq> sl\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some x2; removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cteCaps_of s cref' = Some cap'; cref \<in> cte_refs' cap' (irq_node' s); \<not> cref' \<noteq> sl\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some x2; removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cteCaps_of s cref' = Some cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' \<noteq> sl\<rbrakk> \<Longrightarrow> cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some x2; removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cteCaps_of s cref' = Some cap'; cref \<in> cte_refs' cap' (irq_node' s); \<not> cref' \<noteq> sl\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some x2; removeable' sl s x2; x2 \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cteCaps_of s cref' = Some cap'; cref \<in> cte_refs' cap' (irq_node' s); \<not> cref' \<noteq> sl\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; (\<exists>p. p \<noteq> sl \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap cap') p s) \<or> (\<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl; \<exists>p. p \<noteq> sl \<and> cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap cap') p s\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl; (\<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cap cap' p. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cref \<in> cte_refs' cap' (irq_node' s); p \<noteq> sl; cte_wp_at' (\<lambda>cte. capMasterCap (cteCap cte) = capMasterCap cap') p s\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl; (\<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cap cap' p. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cref \<in> cte_refs' cap' (irq_node' s); p \<noteq> sl; case cteCaps_of s p of None \<Rightarrow> False | Some a \<Rightarrow> capMasterCap a = capMasterCap cap'\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl; (\<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (2 subgoals):
 1. \<And>s cref cap cap' p x2. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cref \<in> cte_refs' cap' (irq_node' s); p \<noteq> sl; cteCaps_of s p = Some x2; cte_refs' x2 = cte_refs' cap'; zobj_refs' x2 = zobj_refs' cap'\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s)))
 2. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl; (\<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 cref cap cref' cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; x2 = cap'; cref \<in> cte_refs' cap' (irq_node' s); cref' = sl; (\<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s) \<and> (\<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s) \<and> (\<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cap cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cref \<in> cte_refs' cap' (irq_node' s); \<forall>p\<in>cte_refs' cap' (irq_node' s). p \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) p s; \<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s; \<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal (1 subgoal):
 1. \<And>s cref cap cap'. \<lbrakk>cteCaps_of s sl = Some cap'; cap' \<noteq> capability.NullCap; cap \<noteq> capability.NullCap; cref \<noteq> sl; cteCaps_of s cref = Some cap; cref \<in> cte_refs' cap' (irq_node' s); \<forall>p\<in>zobj_refs' cap'. ko_wp_at' (Not \<circ> live') p s; \<forall>t\<in>threadCapRefs cap'. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); cref \<noteq> sl \<longrightarrow> cte_wp_at' (\<lambda>cte. cteCap cte = capability.NullCap) cref s\<rbrakk> \<Longrightarrow> \<exists>cref'. cref' \<noteq> sl \<and> (cref' \<noteq> sl \<longrightarrow> (\<exists>cap'. cteCaps_of s cref' = Some cap' \<and> cref \<in> cte_refs' cap' (irq_node' s))) proof (prove)
goal:
No subgoals!