theory Tcb_DR

lemma dcorres_tcb_empty_slot:
  "(thread,idx) = (transform_cslot_ptr slot)
  \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True)
  (cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and valid_pdpt_objs and valid_etcbs)
  (tcb_empty_thread_slot thread idx) (cap_delete slot)" apply (simp add:liftE_bindE tcb_empty_thread_slot_def) apply (simp add:opt_cap_def gets_the_def assert_opt_def gets_def bind_assoc split_def) apply (rule dcorres_absorb_get_l) apply (clarsimp simp add:cte_at_into_opt_cap) apply (erule impE) apply (clarsimp simp: not_idle_thread_def dest!:invs_valid_idle) apply (simp add:opt_cap_def whenE_def split_def) apply (intro conjI impI) apply (case_tac slot,clarsimp) apply (rule corres_guard_imp) apply (rule delete_cap_corres') apply simp apply (clarsimp simp:cte_wp_at_caps_of_state) apply (simp add:cap_delete_def) apply (subst rec_del_simps_ext) apply (subst rec_del_simps_ext) apply (clarsimp simp:bindE_assoc) apply (subst liftE_bindE) apply (rule corres_guard_imp[OF corres_symb_exec_r]) apply (rule_tac F = "x = cap.NullCap" in corres_gen_asm2) apply (simp add:bindE_assoc when_def) apply (simp add:IpcCancel_A.empty_slot_def returnOk_liftE) apply (rule corres_symb_exec_r) apply (rule_tac F = "cap = cap.NullCap" in corres_gen_asm2) apply (rule corres_trivial) apply simp apply (simp | wp get_cap_wp)+ apply (clarsimp simp:cte_wp_at_caps_of_state) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (thread, idx) = transform_cslot_ptr slot \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (tcb_empty_thread_slot thread idx) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. (thread, idx) = transform_cslot_ptr slot \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (do cap <- KHeap_D.get_cap (transform_cslot_ptr slot);
whenE (cap \<noteq> cdl_cap.NullCap) (delete_cap (transform_cslot_ptr slot))
od) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. (thread, idx) = transform_cslot_ptr slot \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) (do x <- get;
cap <- case slots_of (fst (transform_cslot_ptr slot)) x (snd (transform_cslot_ptr slot)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
whenE (cap \<noteq> cdl_cap.NullCap) (delete_cap (transform_cslot_ptr slot))
od) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; True; (cte_wp_at (\<lambda>_. True) slot and invs and emptyable slot and not_idle_thread (fst slot) and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (do cap <- case slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
whenE (cap \<noteq> cdl_cap.NullCap) (delete_cap (transform_cslot_ptr slot))
od) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; fst slot \<noteq> idle_thread s' \<longrightarrow> opt_cap (transform_cslot_ptr slot) (transform s') = Some (transform_cap cap); emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (do cap <- case slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
whenE (cap \<noteq> cdl_cap.NullCap) (delete_cap (transform_cslot_ptr slot))
od) (cap_delete slot) proof (prove)
goal (2 subgoals):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'\<rbrakk> \<Longrightarrow> fst slot \<noteq> idle_thread s'
 2. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; opt_cap (transform_cslot_ptr slot) (transform s') = Some (transform_cap cap)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (do cap <- case slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
whenE (cap \<noteq> cdl_cap.NullCap) (delete_cap (transform_cslot_ptr slot))
od) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; opt_cap (transform_cslot_ptr slot) (transform s') = Some (transform_cap cap)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (do cap <- case slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) of None \<Rightarrow> fail | Some x \<Rightarrow> return x;
whenE (cap \<noteq> cdl_cap.NullCap) (delete_cap (transform_cslot_ptr slot))
od) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap)\<rbrakk> \<Longrightarrow> (cap \<noteq> cap.NullCap \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (delete_cap (transform_cslot_ptr slot)) (cap_delete slot)) \<and> (cap = cap.NullCap \<longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot)) proof (prove)
goal (2 subgoals):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap \<noteq> cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (delete_cap (transform_cslot_ptr slot)) (cap_delete slot)
 2. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot) proof (prove)
goal (2 subgoals):
 1. \<And>s' cap a b. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (delete_cap (transform_cslot_ptr (a, b))) (cap_delete (a, b))
 2. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot) proof (prove)
goal (4 subgoals):
 1. \<And>s' cap a b. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b)\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q27 s' cap a b) (?Q'27 s' cap a b) (delete_cap (transform_cslot_ptr (a, b))) (cap_delete (a, b))
 2. \<And>s' cap a b s. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b); transform s' = s\<rbrakk> \<Longrightarrow> ?Q27 s' cap a b s
 3. \<And>s' cap a b s. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b); s' = s\<rbrakk> \<Longrightarrow> ?Q'27 s' cap a b s
 4. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot) proof (prove)
goal (3 subgoals):
 1. \<And>s' cap a b s. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b); transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' cap a b s. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b); s' = s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (a, b) and invs and emptyable (a, b) and not_idle_thread a and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s
 3. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot) proof (prove)
goal (2 subgoals):
 1. \<And>s' cap a b s. \<lbrakk>(thread, idx) = transform_cslot_ptr (a, b); invs s'; cte_wp_at ((=) cap) (a, b) s'; emptyable (a, b) s'; not_idle_thread a s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr (a, b))) (transform s') (snd (transform_cslot_ptr (a, b))) = Some (transform_cap cap); cap \<noteq> cap.NullCap; slot = (a, b); s' = s\<rbrakk> \<Longrightarrow> (cte_wp_at (\<lambda>_. True) (a, b) and invs and emptyable (a, b) and not_idle_thread a and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and valid_etcbs) s
 2. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some (transform_cap cap); cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (cap_delete slot) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (doE y <- rec_del (CTEDeleteCall slot True);
returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (doE y <- doE (success, cleanup_info) <- rec_del (FinaliseSlotCall slot True);
without_preemption $ when (True \<or> success) $ IpcCancel_A.empty_slot slot cleanup_info;
returnOk undefined
odE;
returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s' cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (doE y <- doE (success, cleanup_info) <- doE cap <- without_preemption $ CSpaceAcc_A.get_cap slot;
if cap = cap.NullCap then returnOk (True, cap.NullCap) else doE is_final <- without_preemption $ IpcCancel_A.is_final_cap cap;
(remainder, cleanup_info) <- without_preemption $ CSpace_A.finalise_cap cap is_final;
if CSpace_A.cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> True then doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
returnOk (False, cap.NullCap)
odE else doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot True);
Exceptions_A.preemption_point;
rec_del (FinaliseSlotCall slot True)
odE
odE
odE;
without_preemption $ when (True \<or> success) $ IpcCancel_A.empty_slot slot cleanup_info;
returnOk undefined
odE;
returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (doE x <- liftE (CSpaceAcc_A.get_cap slot);
x <- if x = cap.NullCap then returnOk (True, cap.NullCap) else doE is_final <- without_preemption $ IpcCancel_A.is_final_cap x;
(remainder, cleanup_info) <- without_preemption $ CSpace_A.finalise_cap x is_final;
if CSpace_A.cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> True then doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
returnOk (False, cap.NullCap)
odE else doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot True);
Exceptions_A.preemption_point;
rec_del (FinaliseSlotCall slot True)
odE
odE;
y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot slot cleanup_info);
returnOk undefined
odE;
returnOk ()
odE) proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) ((=) (transform s')) ((=) s') (returnOk ()) (do x <- CSpaceAcc_A.get_cap slot;
doE x <- if x = cap.NullCap then returnOk (True, cap.NullCap) else doE is_final <- without_preemption $ IpcCancel_A.is_final_cap x;
(remainder, cleanup_info) <- without_preemption $ CSpace_A.finalise_cap x is_final;
if CSpace_A.cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> True then doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
returnOk (False, cap.NullCap)
odE else doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot True);
Exceptions_A.preemption_point;
rec_del (FinaliseSlotCall slot True)
odE
odE;
y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot slot cleanup_info);
returnOk undefined
odE;
returnOk ()
odE
od) proof (prove)
goal (6 subgoals):
 1. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q36 s') (?Q'37 s' x) (returnOk ()) (doE x <- if x = cap.NullCap then returnOk (True, cap.NullCap) else doE is_final <- without_preemption $ IpcCancel_A.is_final_cap x;
(remainder, cleanup_info) <- without_preemption $ CSpace_A.finalise_cap x is_final;
if CSpace_A.cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> True then doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
returnOk (False, cap.NullCap)
odE else doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot True);
Exceptions_A.preemption_point;
rec_del (FinaliseSlotCall slot True)
odE
odE;
y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot slot cleanup_info);
returnOk undefined
odE;
returnOk ()
odE)
 2. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'37 s'\<rbrace>
 3. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 5. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q36 s' s
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (6 subgoals):
 1. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q36 s') (?P'44 s' x) (returnOk ()) (doE x <- if x = cap.NullCap then returnOk (True, cap.NullCap) else doE is_final <- without_preemption $ IpcCancel_A.is_final_cap x;
(remainder, cleanup_info) <- without_preemption $ CSpace_A.finalise_cap x is_final;
if CSpace_A.cap_removeable remainder slot then returnOk (True, cleanup_info) else if cap_cyclic_zombie remainder slot \<and> \<not> True then doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
returnOk (False, cap.NullCap)
odE else doE without_preemption $ CSpaceAcc_A.set_cap remainder slot;
rec_del (ReduceZombieCall remainder slot True);
Exceptions_A.preemption_point;
rec_del (FinaliseSlotCall slot True)
odE
odE;
y <- case x of (success, cleanup_info) \<Rightarrow> doE y <- liftE (IpcCancel_A.empty_slot slot cleanup_info);
returnOk undefined
odE;
returnOk ()
odE)
 2. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 3. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 5. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q36 s' s
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (6 subgoals):
 1. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres (dc \<oplus> dc) (?Q36 s') (?P'44 s' cap.NullCap) (returnOk ()) (liftE (IpcCancel_A.empty_slot slot cap.NullCap))
 2. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 3. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 5. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q36 s' s
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (6 subgoals):
 1. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q36 s') (?P'44 s' cap.NullCap) (return ()) (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)
 2. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 3. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 5. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q36 s' s
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (9 subgoals):
 1. \<And>s' x cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q36 s') (?Q'47 s' x cap) (return ()) (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>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'44 s' cap.NullCap\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>?Q'47 s' x\<rbrace>
 3. \<And>s' x s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; ?P'44 s' cap.NullCap s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?P'44 s' cap.NullCap) (CSpaceAcc_A.get_cap slot)
 5. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 8. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q36 s' s
 9. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (9 subgoals):
 1. \<And>s' x cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (?Q36 s') (?P'57 s' x cap) (return ()) (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>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'44 s' cap.NullCap\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. ?P'57 s' x cap and (\<lambda>s. cap = cap.NullCap)\<rbrace>
 3. \<And>s' x s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; ?P'44 s' cap.NullCap s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?P'44 s' cap.NullCap) (CSpaceAcc_A.get_cap slot)
 5. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 8. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> ?Q36 s' s
 9. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (9 subgoals):
 1. \<And>s' x cap. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; cap = cap.NullCap\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (\<lambda>_. True) (return ()) (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>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'44 s' cap.NullCap\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. (\<lambda>_. True) and (\<lambda>s. cap = cap.NullCap)\<rbrace>
 3. \<And>s' x s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; ?P'44 s' cap.NullCap s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?P'44 s' cap.NullCap) (CSpaceAcc_A.get_cap slot)
 5. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 6. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 8. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> True
 9. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (8 subgoals):
 1. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?P'44 s' cap.NullCap\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>cap. (\<lambda>_. True) and (\<lambda>s. cap = cap.NullCap)\<rbrace>
 2. \<And>s' x s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; ?P'44 s' cap.NullCap s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s' x. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; x = cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?P'44 s' cap.NullCap) (CSpaceAcc_A.get_cap slot)
 4. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap\<rbrakk> \<Longrightarrow> \<lbrace>?Q'36 s'\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>x. ?P'44 s' x and (\<lambda>s. x = cap.NullCap)\<rbrace>
 5. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; ?Q'36 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> CSpaceAcc_A.get_cap slot \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>s'. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; False\<rbrakk> \<Longrightarrow> no_fail (?Q'36 s') (CSpaceAcc_A.get_cap slot)
 7. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; transform s' = s\<rbrakk> \<Longrightarrow> True
 8. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s'; cte_wp_at ((=) cap.NullCap) slot s'; emptyable slot s'; not_idle_thread (fst slot) s'; \<forall>x\<in>ran (kheap s'). obj_valid_pdpt x; valid_etcbs s'; slots_of (fst (transform_cslot_ptr slot)) (transform s') (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> ?Q'36 s' s proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>(thread, idx) = transform_cslot_ptr slot; invs s; cte_wp_at ((=) cap.NullCap) slot s; emptyable slot s; not_idle_thread (fst slot) s; \<forall>x\<in>ran (kheap s). obj_valid_pdpt x; valid_etcbs s; slots_of (fst (transform_cslot_ptr slot)) (transform s) (snd (transform_cslot_ptr slot)) = Some cdl_cap.NullCap; s' = s\<rbrakk> \<Longrightarrow> \<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> (\<forall>cap. cte_wp_at ((=) cap) slot s \<longrightarrow> cap = cap.NullCap) \<and> cap = cap.NullCap proof (prove)
goal:
No subgoals!