theory Finalise_DR

lemma dcorres_finalise_slot:
  "dcorres (dc \<oplus> dc) \<top> (invs and cte_at slot and valid_etcbs and valid_pdpt_objs and emptyable slot
                            and not_idle_thread (fst slot))
    (CSpace_D.finalise_slot (transform_cslot_ptr slot))
    (rec_del (FinaliseSlotCall slot True))" apply (rule corres_use_cutMon) apply (cut_tac b="\<lambda>_. returnOk ()" and d="\<lambda>_. returnOk ()" and r=dc
                and args4="FinaliseSlotCall slot True"
                and S4="({(transform_cslot_ptr slot, False)}, {})" and s4=s
            in corres_splitEE[OF dcorres_rec_del _ wp_post_tautE wp_post_tautE]) apply (simp_all add: bindE_assoc CSpace_D.finalise_slot_def split_def) apply (simp_all add: liftME_def[symmetric]) apply (simp add: returnOk_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable slot and not_idle_thread (fst slot)) (CSpace_D.finalise_slot (transform_cslot_ptr slot)) (rec_del (FinaliseSlotCall slot True)) proof (prove)
goal (1 subgoal):
 1. \<And>s. dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable slot and not_idle_thread (fst slot)) (CSpace_D.finalise_slot (transform_cslot_ptr slot)) (cutMon ((=) s) (rec_del (FinaliseSlotCall slot True))) proof (prove)
goal (5 subgoals):
 1. \<And>s. case FinaliseSlotCall slot True of CTEDeleteCall slot e \<Rightarrow> \<not> e | _ \<Rightarrow> True
 2. \<And>s. (transform_cslot_ptr (slot_rdcall (FinaliseSlotCall slot True)), \<not> exposed_rdcall (FinaliseSlotCall slot True)) \<in> fst ({(transform_cslot_ptr slot, False)}, {})
 3. \<And>s. case FinaliseSlotCall slot True of ReduceZombieCall (Zombie p zbits 0) x xa \<Rightarrow> True | ReduceZombieCall (Zombie p zbits (Suc n)) x xa \<Rightarrow> (transform_cslot_ptr (p, replicate (zombie_cte_bits zbits) False), True) \<in> fst ({(transform_cslot_ptr slot, False)}, {}) \<and> (transform_cslot_ptr (p, nat_to_cref (zombie_cte_bits zbits) n), True) \<in> fst ({(transform_cslot_ptr slot, False)}, {}) | ReduceZombieCall _ x xa \<Rightarrow> True | _ \<Rightarrow> True
 4. \<And>s rv rv'. (case FinaliseSlotCall slot True of FinaliseSlotCall x xa \<Rightarrow> fst rv' \<longrightarrow> (\<exists>v. (transform_cslot_ptr (slot_rdcall (FinaliseSlotCall slot True)), v) \<in> snd rv \<and> (\<not> exposed_rdcall (FinaliseSlotCall slot True) \<longrightarrow> v)) | _ \<Rightarrow> True) \<and> fst ({(transform_cslot_ptr slot, False)}, {}) \<subseteq> fst rv \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (returnOk ()) (returnOk ())
 5. \<And>s. dcorres (dc \<oplus> dc) ((\<lambda>_. True) and (\<lambda>_. True)) (invs and valid_rec_del_call (FinaliseSlotCall slot True) and cte_wp_at (\<lambda>_. True) (slot_rdcall (FinaliseSlotCall slot True)) and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable (slot_rdcall (FinaliseSlotCall slot True)) and not_idle_thread (fst (slot_rdcall (FinaliseSlotCall slot True))) and (\<lambda>s. \<not> exposed_rdcall (FinaliseSlotCall slot True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (FinaliseSlotCall slot True)) s) and (\<lambda>s. case FinaliseSlotCall slot True of ReduceZombieCall cap sl ex \<Rightarrow> \<forall>t\<in>obj_refs cap. halted_if_tcb t s | _ \<Rightarrow> True) and (\<lambda>_. True)) (doE rv <- doE S' <- monadic_trancl_preemptible finalise_slot_inner2 ({(transform_cslot_ptr slot, False)}, {});
whenE ((case FinaliseSlotCall slot True of ReduceZombieCall x xa xb \<Rightarrow> False | _ \<Rightarrow> True) \<and> exposed_rdcall (FinaliseSlotCall slot True) \<and> transform_cslot_ptr (slot_rdcall (FinaliseSlotCall slot True)) \<notin> fst ` snd S') throw;
returnOk S'
odE;
returnOk ()
odE) (doE rv' <- cutMon ((=) s) (rec_del (FinaliseSlotCall slot True));
returnOk ()
odE) \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable slot and not_idle_thread (fst slot)) (CSpace_D.finalise_slot (transform_cslot_ptr slot)) (cutMon ((=) s) (rec_del (FinaliseSlotCall slot True))) proof (prove)
goal (2 subgoals):
 1. \<And>rv rv'. (fst rv' \<longrightarrow> (\<exists>v. (transform_cslot_ptr slot, v) \<in> snd rv)) \<and> (transform_cslot_ptr slot, False) \<in> fst rv \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (returnOk ()) (returnOk ())
 2. \<And>s. dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs and (\<lambda>s. Ball (ran (kheap s)) obj_valid_pdpt) and emptyable slot and not_idle_thread (fst slot)) (doE x <- monadic_trancl_preemptible finalise_slot_inner2 ({(transform_cslot_ptr slot, False)}, {});
whenE (transform_cslot_ptr slot \<notin> fst ` snd x) throw
odE) (doE rv' <- cutMon ((=) s) (rec_del (FinaliseSlotCall slot True));
returnOk ()
odE) \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (invs and cte_wp_at (\<lambda>_. True) slot and valid_etcbs and (\<lambda>s. \<forall>x\<in>ran (kheap s). obj_valid_pdpt x) and emptyable slot and not_idle_thread (fst slot)) (doE p <- monadic_trancl_preemptible finalise_slot_inner2 ({(transform_cslot_ptr slot, False)}, {});
whenE (transform_cslot_ptr slot \<notin> fst ` snd p) throw
odE) (cutMon ((=) s) (rec_del (FinaliseSlotCall slot True))) proof (prove)
goal (1 subgoal):
 1. \<And>rv rv'. (fst rv' \<longrightarrow> (\<exists>v. (transform_cslot_ptr slot, v) \<in> snd rv)) \<and> (transform_cslot_ptr slot, False) \<in> fst rv \<Longrightarrow> dcorres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (returnOk ()) (returnOk ()) proof (prove)
goal:
No subgoals!