theory KHeap_DR

lemma always_empty_slot_corres:
  "dcorres dc \<top> (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs)
   (always_empty_slot (transform_cslot_ptr slot)) (IpcCancel_A.empty_slot slot cap.NullCap)" apply (clarsimp simp: always_empty_slot_def IpcCancel_A.empty_slot_def) apply (rule corres_symb_exec_r) apply (rule corres_guard_imp) apply (rule_tac R="cap = cap.NullCap" in corres_cases) apply simp apply (rule always_empty_slot_NullCap_corres) apply simp apply (rule dcorres_gets_all_param) apply (rule_tac P="%a. dcorres dc P P' h a" for P P' h in subst[OF bind_assoc[where m="gets cdt"]]) apply (rule corres_split[where r'="dc"]) apply (rule remove_parent_corres) apply (rule dcorres_rhs_noop_above[OF empty_slot_ext_dcorres]) apply (rule corres_bind_ignore_ret_rhs) apply (rule set_cap_null_cap_corres) apply wp+ apply (wp get_cap_wp|simp add: set_cdt_def)+ apply (clarsimp simp: cte_wp_at_def not_idle_thread_def) apply (wp get_cap_wp) apply simp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (always_empty_slot (transform_cslot_ptr slot)) (IpcCancel_A.empty_slot slot cap.NullCap) proof (prove)
goal (1 subgoal):
 1. dcorres dc (\<lambda>_. True) (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do cap <- CSpaceAcc_A.get_cap slot;
if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od
od) proof (prove)
goal (4 subgoals):
 1. \<And>cap. dcorres dc (\<lambda>_. True) (?Q' cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od)
 2. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 3. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (6 subgoals):
 1. \<And>cap. dcorres dc (?Q5 cap) (?Q'5 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od)
 2. \<And>cap s. True \<Longrightarrow> ?Q5 cap s
 3. \<And>cap s. ?Q' cap s \<Longrightarrow> ?Q'5 cap s
 4. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (7 subgoals):
 1. \<And>cap. cap = cap.NullCap \<Longrightarrow> dcorres dc (?P9 cap) (?P'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od)
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?Q9 cap) (?Q'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od)
 3. \<And>cap s. True \<Longrightarrow> (?P9 cap and ?Q9 cap) s
 4. \<And>cap s. ?Q' cap s \<Longrightarrow> (?P'9 cap and ?Q'9 cap) s
 5. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (7 subgoals):
 1. dcorres dc (?P9 cap.NullCap) (?P'9 cap.NullCap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (return ())
 2. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?Q9 cap) (?Q'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od)
 3. \<And>cap s. True \<Longrightarrow> (?P9 cap and ?Q9 cap) s
 4. \<And>cap s. ?Q' cap s \<Longrightarrow> (?P'9 cap and ?Q'9 cap) s
 5. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (6 subgoals):
 1. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?Q9 cap) (?Q'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if cap = cap.NullCap then return () else do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
parent <- return $ cdt slot;
set_cdt ((\<lambda>p. if cdt p = Some slot then parent else cdt p)(slot := None));
do_extended_op (empty_slot_ext slot slot_p);
set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot;
post_cap_deletion cap.NullCap
od)
 2. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ?Q9 cap) s
 3. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and ?Q'9 cap) s
 4. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (6 subgoals):
 1. \<And>cap. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?Q9 cap) (?Q'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do slot_p <- gets (\<lambda>s. cdt s slot);
cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ?Q9 cap) s
 3. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and ?Q'9 cap) s
 4. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (6 subgoals):
 1. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?Q9 cap) (?Q'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do cdt <- gets cdt;
y <- set_cdt ((\<lambda>p. if cdt p = Some slot then cdt slot else cdt p)(slot := None));
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ?Q9 cap) s
 3. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and ?Q'9 cap) s
 4. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (6 subgoals):
 1. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?Q9 cap) (?Q'9 cap) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do y <- do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od;
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ?Q9 cap) s
 3. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and ?Q'9 cap) s
 4. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (9 subgoals):
 1. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> dcorres dc (?P23 cap) (?P'25 cap) (remove_parent (transform_cslot_ptr slot)) (do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od)
 2. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R22 cap slot_p y) (?R'22 cap slot_p ya) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 3. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q24 cap\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R22 cap slot_p\<rbrace>
 4. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q'26 cap\<rbrace> do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od \<lbrace>?R'22 cap slot_p\<rbrace>
 5. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and (?P23 cap and ?Q24 cap)) s
 6. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and (?P'25 cap and ?Q'26 cap)) s
 7. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 8. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (8 subgoals):
 1. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?R22 cap slot_p y) (?R'22 cap slot_p ya) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q24 cap\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R22 cap slot_p\<rbrace>
 3. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q'26 cap\<rbrace> do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od \<lbrace>?R'22 cap slot_p\<rbrace>
 4. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ((\<lambda>_. True) and ?Q24 cap)) s
 5. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'26 cap)) s
 6. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 7. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (10 subgoals):
 1. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?Q33 cap slot_p y ya) (?Q'33 cap slot_p y ya) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?R22 cap slot_p y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q33 cap slot_p y ya\<rbrace>
 3. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'22 cap slot_p ya\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>yb. ?Q'33 cap slot_p y ya\<rbrace>
 4. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q24 cap\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R22 cap slot_p\<rbrace>
 5. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q'26 cap\<rbrace> do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od \<lbrace>?R'22 cap slot_p\<rbrace>
 6. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ((\<lambda>_. True) and ?Q24 cap)) s
 7. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'26 cap)) s
 8. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 9. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (10 subgoals):
 1. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> dcorres dc (?Q33 cap slot_p y ya) (?Q'33 cap slot_p y ya) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do set_original slot False;
CSpaceAcc_A.set_cap cap.NullCap slot
od)
 2. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?R22 cap slot_p y\<rbrace> return () \<lbrace>\<lambda>yb. ?Q33 cap slot_p y ya\<rbrace>
 3. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'22 cap slot_p ya\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>yb. ?Q'33 cap slot_p y ya\<rbrace>
 4. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q24 cap\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R22 cap slot_p\<rbrace>
 5. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q'26 cap\<rbrace> do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od \<lbrace>?R'22 cap slot_p\<rbrace>
 6. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ((\<lambda>_. True) and ?Q24 cap)) s
 7. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'26 cap)) s
 8. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 9. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 10. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (9 subgoals):
 1. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?R22 cap slot_p y\<rbrace> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>cap slot_p y ya. \<lbrakk>cap \<noteq> cap.NullCap; dc y ya\<rbrakk> \<Longrightarrow> \<lbrace>?R'22 cap slot_p ya\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>y. valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s) and valid_etcbs\<rbrace>
 3. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q24 cap\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R22 cap slot_p\<rbrace>
 4. \<And>cap slot_p. cap \<noteq> cap.NullCap \<Longrightarrow> \<lbrace>?Q'26 cap\<rbrace> do x <- gets cdt;
set_cdt ((\<lambda>p. if x p = Some slot then x slot else x p)(slot := None))
od \<lbrace>?R'22 cap slot_p\<rbrace>
 5. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ((\<lambda>_. True) and ?Q24 cap)) s
 6. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'26 cap)) s
 7. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 8. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (5 subgoals):
 1. \<And>cap s. True \<Longrightarrow> ((\<lambda>a. True) and ((\<lambda>_. True) and (\<lambda>_. True))) s
 2. \<And>cap s. ?Q' cap s \<Longrightarrow> (weak_valid_mdb and not_idle_thread (fst slot) and cte_wp_at ((=) cap) slot and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and (\<lambda>a. valid_idle a \<and> fst slot \<noteq> idle_thread a \<and> valid_etcbs a))) s
 3. \<lbrace>weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'\<rbrace>
 4. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (3 subgoals):
 1. \<And>s. weak_valid_mdb s \<and> valid_idle s \<and> not_idle_thread (fst slot) s \<and> valid_etcbs s \<Longrightarrow> (\<exists>cap. cte_wp_at ((=) cap) slot s) \<longrightarrow> cte_wp_at (\<lambda>_. True) slot s \<and> fst slot \<noteq> idle_thread s
 2. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (2 subgoals):
 1. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>(weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) s; s = sa\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot sa \<longrightarrow> s = sa
 2. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal (1 subgoal):
 1. False \<Longrightarrow> no_fail (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs) (CSpaceAcc_A.get_cap slot) proof (prove)
goal:
No subgoals!