theory CNode_DR

lemma delete_cap_corres':
  "dcorres (dc \<oplus> dc) (\<lambda>_. True) (cte_at (a,b) and invs and emptyable (a,b)
                                     and not_idle_thread a and valid_pdpt_objs and valid_etcbs)
             (delete_cap (transform_cslot_ptr (a, b))) (cap_delete (a, b))" apply (simp add:delete_cap_def cap_delete_def) apply (subst rec_del_simps_ext) apply (simp add:bindE_assoc) apply (rule corres_guard_imp) apply (rule corres_splitEE[OF dcorres_finalise_slot]) apply (clarsimp simp:bindE_assoc when_def) apply (rule empty_slot_corres) apply wp+ apply (rule validE_validE_R) apply (simp add:validE_def weak_valid_mdb_def) apply (rule hoare_drop_imp) apply (rule_tac Q = "\<lambda>r. invs and not_idle_thread a and valid_etcbs" in hoare_strengthen_post) apply (wp rec_del_invs) apply (simp add:not_idle_thread_def validE_def) apply wp apply (clarsimp simp:invs_def valid_state_def valid_mdb_def) apply (clarsimp simp:not_idle_thread_def)+ done

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