theory KHeap_DR

lemma empty_slot_corres:
  "dcorres dc \<top>
           (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs)
           (PageTableUnmap_D.empty_slot (transform_cslot_ptr slot))
           (IpcCancel_A.empty_slot slot v)" apply (clarsimp simp:PageTableUnmap_D.empty_slot_def IpcCancel_A.empty_slot_def) apply (rule get_cap_no_fail) apply (rule corres_guard_imp) apply (rule corres_split[where r'="%x y. x=transform_cap y"]) apply (rule get_cap_corres) apply simp apply (case_tac "capa = cap.NullCap") apply (subgoal_tac "cap = cdl_cap.NullCap") apply clarsimp apply (clarsimp simp:transform_cap_def split:cap.splits arch_cap.splits) apply (subgoal_tac "cap \<noteq> cdl_cap.NullCap") apply clarsimp 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 corres_add_noop_lhs) apply (rule_tac Q'="\<lambda>_. valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)"
                in corres_split_forwards') apply (rule empty_slot_ext_dcorres) apply (wp empty_slot_ext_valid_etcbs | simp)+ apply (rule corres_guard_imp) apply (rule corres_dummy_return_pl) apply (rule corres_split[OF set_original_dummy_corres]) apply (rule corres_dummy_return_l) apply (rule corres_split[where r'=dc]) apply simp apply (rule set_cap_corres; simp) apply (case_tac "\<exists>irq. v = cap.IRQHandlerCap irq"; clarsimp) apply (clarsimp simp: deleted_irq_handler_def) apply (fold dc_def) apply (rule set_irq_state_dcorres) apply (wp | simp del: fun_upd_apply)+ apply (wp|simp add: set_cdt_def dc_def)+ apply (clarsimp simp:transform_cap_def split:cap.splits arch_cap.splits) apply wp+ apply clarsimp apply (simp add: not_idle_thread_def)+ 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) (PageTableUnmap_D.empty_slot (transform_cslot_ptr slot)) (IpcCancel_A.empty_slot slot v) 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 cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od
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 v
od
od) 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 and cte_wp_at (\<lambda>_. True) slot) (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od
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 v
od
od) proof (prove)
goal (3 subgoals):
 1. dcorres dc ?Q2 ?Q'2 (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od
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 v
od
od)
 2. \<And>s. True \<Longrightarrow> ?Q2 s
 3. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> ?Q'2 s proof (prove)
goal (6 subgoals):
 1. dcorres (\<lambda>x y. x = transform_cap y) ?P6 ?P'6 (KHeap_D.get_cap (transform_cslot_ptr slot)) (CSpaceAcc_A.get_cap slot)
 2. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> (?P6 and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (?P'6 and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. transform_cslot_ptr slot = transform_cslot_ptr slot
 2. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>cap capa. cap = transform_cap capa \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 2. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (7 subgoals):
 1. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa = cap.NullCap; cap = cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa = cap.NullCap\<rbrakk> \<Longrightarrow> cap = cdl_cap.NullCap
 3. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 4. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa = cap.NullCap\<rbrakk> \<Longrightarrow> cap = cdl_cap.NullCap
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 2. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap; cap \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 cap) (?R'6 capa) (if cap = cdl_cap.NullCap then return () else do remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (if capa = 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 v
od)
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 (transform_cap capa)) (?R'6 capa) (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;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ()
od)
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 (transform_cap capa)) (?R'6 capa) (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;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (6 subgoals):
 1. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?R6 (transform_cap capa)) (?R'6 capa) (do y <- remove_parent (transform_cslot_ptr slot);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do a <- do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od;
y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 2. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 3. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>?R6\<rbrace>
 4. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?R'6\<rbrace>
 5. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 6. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (9 subgoals):
 1. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?P50 (transform_cap capa)) (?P'47 capa) (remove_parent (transform_cslot_ptr slot)) (do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od)
 2. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R36 capa slot_p rv) (?R'36 capa slot_p rv') (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 3. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R36 capa slot_p\<rbrace>
 4. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>?R'36 capa slot_p\<rbrace>
 5. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 6. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. ?P50 a and ?Q48 a\<rbrace>
 7. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. ?P'47 a and ?Q'45 a\<rbrace>
 8. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 9. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R36 capa slot_p rv) (?R'36 capa slot_p rv') (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 2. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R36 capa slot_p\<rbrace>
 3. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>?R'36 capa slot_p\<rbrace>
 4. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres dc (?R36 capa slot_p rv) (?R'36 capa slot_p rv') (do _ <- return ();
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do y <- empty_slot_ext slot slot_p;
y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 2. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R36 capa slot_p\<rbrace>
 3. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>?R'36 capa slot_p\<rbrace>
 4. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (11 subgoals):
 1. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> dcorres (?r'59 capa slot_p rv rv') (?R36 capa slot_p rv) (?R'36 capa slot_p rv') (return ()) (empty_slot_ext slot slot_p)
 2. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R36 capa slot_p rv\<rbrace> return () \<lbrace>?Q59 capa slot_p rv rv'\<rbrace>
 3. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'36 capa slot_p rv'\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)\<rbrace>
 4. \<And>capa slot_p rv rv' rva rv'a. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'; ?r'59 capa slot_p rv rv' rva rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?Q59 capa slot_p rv rv' rva) (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 5. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R36 capa slot_p\<rbrace>
 6. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>?R'36 capa slot_p\<rbrace>
 7. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 8. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 9. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 10. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R36 capa slot_p rv\<rbrace> return () \<lbrace>?Q59 capa slot_p rv rv'\<rbrace>
 2. \<And>capa slot_p rv rv'. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R'36 capa slot_p rv'\<rbrace> empty_slot_ext slot slot_p \<lbrace>\<lambda>_. valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)\<rbrace>
 3. \<And>capa slot_p rv rv' rva rv'a. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv rv'; dc rva rv'a\<rbrakk> \<Longrightarrow> dcorres dc (?Q59 capa slot_p rv rv' rva) (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap a \<Rightarrow> deleted_irq_handler a | _ \<Rightarrow> return ()
od)
 4. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>?R36 capa slot_p\<rbrace>
 5. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>?R'36 capa slot_p\<rbrace>
 6. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 7. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (8 subgoals):
 1. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (\<lambda>s. True) (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ()
od)
 2. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 4. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 5. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 6. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 7. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 8. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?Q97 capa) (?Q'97 capa) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (do y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ()
od)
 2. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ?Q97 capa s
 3. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ?Q'97 capa s
 4. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 6. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 7. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (10 subgoals):
 1. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?Q97 capa) (?Q'97 capa) (do return (?b101 capa);
KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap
od) (do y <- set_original slot False;
y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ()
od)
 2. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ?Q97 capa s
 3. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ?Q'97 capa s
 4. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 5. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 6. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 7. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 8. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 9. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 10. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (12 subgoals):
 1. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R103 capa rv) (?R'103 capa y) (K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv) (do y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ()
od)
 2. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>?R103 capa\<rbrace>
 3. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>?R'103 capa\<rbrace>
 4. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 5. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 6. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 7. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 8. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 9. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 10. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R103 capa rv) (?R'103 capa y) (K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv >>= return) (do y <- CSpaceAcc_A.set_cap cap.NullCap slot;
case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ()
od)
 2. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>?R103 capa\<rbrace>
 3. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>?R'103 capa\<rbrace>
 4. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 5. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 6. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 7. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 8. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 9. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 10. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
A total of 12 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> dcorres dc (?P111 capa rv) (?P'113 capa y) (K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv) (CSpaceAcc_A.set_cap cap.NullCap slot)
 2. \<And>capa rv y x ya. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y; dc x ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R110 capa rv y x) (?R'110 capa rv y ya) (return x) (case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ())
 3. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>?R110 capa rv y\<rbrace>
 4. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>?R'110 capa rv y\<rbrace>
 5. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. ?P111 capa rv and ?Q112 capa rv\<rbrace>
 6. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. ?P'113 capa y and ?Q'114 capa y\<rbrace>
 7. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 8. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 9. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 10. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
A total of 15 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>capa rv. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?P111 capa rv) (?P'113 capa ()) (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) (CSpaceAcc_A.set_cap cap.NullCap slot)
 2. \<And>capa rv y x ya. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y; dc x ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R110 capa rv y x) (?R'110 capa rv y ya) (return x) (case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ())
 3. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>?R110 capa rv y\<rbrace>
 4. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>?R'110 capa rv y\<rbrace>
 5. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. ?P111 capa rv and ?Q112 capa rv\<rbrace>
 6. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. ?P'113 capa y and ?Q'114 capa y\<rbrace>
 7. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 8. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 9. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 10. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>capa rv y x ya. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y; dc x ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R110 capa rv y x) (?R'110 capa rv y ya) (return x) (case v of IRQHandlerCap x \<Rightarrow> deleted_irq_handler x | _ \<Rightarrow> return ())
 2. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>?R110 capa rv y\<rbrace>
 3. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>?R'110 capa rv y\<rbrace>
 4. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q112 capa rv\<rbrace>
 5. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. (\<lambda>a. valid_idle a \<and> fst slot \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'114 capa y\<rbrace>
 6. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 7. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 8. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 9. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 10. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>capa rv irq. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; v = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R110 capa rv () ()) (?R'110 capa rv () ()) (return ()) (deleted_irq_handler irq)
 2. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>?R110 capa rv y\<rbrace>
 3. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>?R'110 capa rv y\<rbrace>
 4. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q112 capa rv\<rbrace>
 5. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. (\<lambda>a. valid_idle a \<and> fst slot \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'114 capa y\<rbrace>
 6. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 7. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 8. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 9. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 10. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>capa rv irq. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; v = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> dcorres (\<lambda>a b. True) (?R110 capa rv () ()) (?R'110 capa rv () ()) (return ()) (set_irq_state IRQInactive irq)
 2. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>?R110 capa rv y\<rbrace>
 3. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>?R'110 capa rv y\<rbrace>
 4. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q112 capa rv\<rbrace>
 5. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. (\<lambda>a. valid_idle a \<and> fst slot \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'114 capa y\<rbrace>
 6. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 7. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 8. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>\<lambda>a b. True\<rbrace>
 9. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 10. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>capa rv irq. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; v = IRQHandlerCap irq\<rbrakk> \<Longrightarrow> dcorres dc (?R110 capa rv () ()) (?R'110 capa rv () ()) (return ()) (set_irq_state IRQInactive irq)
 2. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>?R110 capa rv y\<rbrace>
 3. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>?R'110 capa rv y\<rbrace>
 4. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q112 capa rv\<rbrace>
 5. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. (\<lambda>a. valid_idle a \<and> fst slot \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'114 capa y\<rbrace>
 6. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 7. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 8. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>dc\<rbrace>
 9. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 10. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q112 capa rv\<rbrace> K_bind (KHeap_D.set_cap (transform_cslot_ptr slot) cdl_cap.NullCap) rv \<lbrace>\<lambda>a b. True\<rbrace>
 2. \<And>capa rv y. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; dc rv y\<rbrakk> \<Longrightarrow> \<lbrace>?Q'114 capa y\<rbrace> CSpaceAcc_A.set_cap cap.NullCap slot \<lbrace>\<lambda>a b. True\<rbrace>
 3. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q103 capa\<rbrace> return (?b101 capa) \<lbrace>\<lambda>rv. (\<lambda>_. True) and ?Q112 capa rv\<rbrace>
 4. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'103 capa\<rbrace> set_original slot False \<lbrace>\<lambda>y. (\<lambda>a. valid_idle a \<and> fst slot \<noteq> idle_thread a \<and> valid_etcbs a) and ?Q'114 capa y\<rbrace>
 5. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; True\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q103 capa) s
 6. \<And>capa s. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap; (valid_etcbs and valid_idle and (\<lambda>s. fst slot \<noteq> idle_thread s)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q'103 capa) s
 7. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>dc\<rbrace>
 8. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 9. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 10. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
A total of 13 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>capa. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q48 (transform_cap capa)\<rbrace> remove_parent (transform_cslot_ptr slot) \<lbrace>dc\<rbrace>
 2. \<And>capa slot_p. \<lbrakk>capa \<noteq> cap.NullCap; transform_cap capa \<noteq> cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'45 capa\<rbrace> do a <- gets cdt;
set_cdt ((\<lambda>p. if a p = Some slot then a slot else a p)(slot := None))
od \<lbrace>\<lambda>rv' s. valid_etcbs s \<and> valid_idle s \<and> fst slot \<noteq> idle_thread s\<rbrace>
 3. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> cap \<noteq> cdl_cap.NullCap
 4. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 5. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and ?Q'45 a\<rbrace>
 6. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 7. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (5 subgoals):
 1. \<And>cap capa. \<lbrakk>cap = transform_cap capa; capa \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> transform_cap capa \<noteq> cdl_cap.NullCap
 2. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 3. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and (\<lambda>a. valid_etcbs a \<and> valid_idle a \<and> fst slot \<noteq> idle_thread a)\<rbrace>
 4. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 5. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q6\<rbrace> KHeap_D.get_cap (transform_cslot_ptr slot) \<lbrace>\<lambda>a. (\<lambda>a. True) and ?Q48 a\<rbrace>
 2. \<lbrace>?Q'6\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>a. cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and (\<lambda>a. valid_etcbs a \<and> valid_idle a \<and> fst slot \<noteq> idle_thread a)\<rbrace>
 3. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and ?Q6) s
 4. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and ?Q'6) s proof (prove)
goal (2 subgoals):
 1. \<And>s. True \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. opt_cap (transform_cslot_ptr slot) s \<noteq> None \<longrightarrow> ((\<lambda>a. True) and ?Q48 (the (opt_cap (transform_cslot_ptr slot) s))) s)) s
 2. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and (\<lambda>a. valid_etcbs a \<and> valid_idle a \<and> fst slot \<noteq> idle_thread a))) s proof (prove)
goal (2 subgoals):
 1. \<And>s y. opt_cap (transform_cslot_ptr slot) s = Some y \<Longrightarrow> ?Q48 y s
 2. \<And>s. (weak_valid_mdb and valid_idle and not_idle_thread (fst slot) and valid_etcbs and cte_wp_at (\<lambda>_. True) slot) s \<Longrightarrow> (valid_idle and not_idle_thread (fst slot) and valid_etcbs and (cte_wp_at (\<lambda>_. True) slot and weak_valid_mdb and (\<lambda>a. valid_etcbs a \<and> valid_idle a \<and> fst slot \<noteq> idle_thread a))) s proof (prove)
goal:
No subgoals!