theory CNodeInv_R

lemma cteDelete_corres:
  "corres (dc \<oplus> dc)
      (einvs and simple_sched_action and cte_at ptr and emptyable ptr)
      (invs' and sch_act_simple and cte_at' (cte_map ptr))
      (cap_delete ptr) (cteDelete (cte_map ptr) True)" unfolding cap_delete_def using rec_del_corres[where args="CTEDeleteCall ptr True"] apply (simp add: spec_corres_liftME2 liftME_def[symmetric]) apply (erule use_spec_corres) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and simple_sched_action and cte_wp_at (\<lambda>_. True) ptr and emptyable ptr) (invs' and sch_act_simple and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (cap_delete ptr) (cteDelete (cte_map ptr) True) proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and simple_sched_action and cte_wp_at (\<lambda>_. True) ptr and emptyable ptr) (invs' and sch_act_simple and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (doE rec_del (CTEDeleteCall ptr True);
returnOk ()
odE) (cteDelete (cte_map ptr) True) proof (prove)
using this:
\<forall>C\<in>rec_del_concrete (CTEDeleteCall ptr True). spec_corres ?s (dc \<oplus> (case CTEDeleteCall ptr True of FinaliseSlotCall x xa \<Rightarrow> \<lambda>r r'. fst r = fst r' \<and> cap_relation (snd r) (snd r') | _ \<Rightarrow> dc)) (einvs and simple_sched_action and valid_rec_del_call (CTEDeleteCall ptr True) and cte_wp_at (\<lambda>_. True) (slot_rdcall (CTEDeleteCall ptr True)) and emptyable (slot_rdcall (CTEDeleteCall ptr True)) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall ptr True) \<longrightarrow> ex_cte_cap_wp_to (\<lambda>cp. cap_irqs cp = {}) (slot_rdcall (CTEDeleteCall ptr True)) s) and (\<lambda>s. case CTEDeleteCall ptr True of ReduceZombieCall cap sl ex \<Rightarrow> \<forall>t\<in>obj_refs cap. halted_if_tcb t s | _ \<Rightarrow> True)) (invs' and sch_act_simple and cte_wp_at' (\<lambda>_. True) (cte_map (slot_rdcall (CTEDeleteCall ptr True))) and (\<lambda>s. \<not> exposed_rdcall (CTEDeleteCall ptr True) \<longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) (cte_map (slot_rdcall (CTEDeleteCall ptr True))) s) and (\<lambda>s. case CTEDeleteCall ptr True of ReduceZombieCall cap sl ex \<Rightarrow> \<exists>cp'. cap_relation cap cp' \<and> (cte_wp_at' (\<lambda>cte. cteCap cte = cp') (cte_map sl) and (\<lambda>s. \<not> capRemovable cp' (cte_map sl) \<and> (\<not> ex \<longrightarrow> \<not> capCyclicZombie cp' (cte_map sl)))) s | _ \<Rightarrow> True)) (rec_del (CTEDeleteCall ptr True)) C

goal (1 subgoal):
 1. corres (dc \<oplus> dc) (einvs and simple_sched_action and cte_wp_at (\<lambda>_. True) ptr and emptyable ptr) (invs' and sch_act_simple and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (doE rec_del (CTEDeleteCall ptr True);
returnOk ()
odE) (cteDelete (cte_map ptr) True) proof (prove)
goal (1 subgoal):
 1. (\<And>s. spec_corres s (dc \<oplus> dc) (einvs and simple_sched_action and cte_wp_at (\<lambda>_. True) ptr and emptyable ptr) (invs' and sch_act_simple and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (rec_del (CTEDeleteCall ptr True)) (cteDelete (cte_map ptr) True)) \<Longrightarrow> corres (dc \<oplus> dc) (einvs and simple_sched_action and cte_wp_at (\<lambda>_. True) ptr and emptyable ptr) (invs' and sch_act_simple and cte_wp_at' (\<lambda>_. True) (cte_map ptr)) (rec_del (CTEDeleteCall ptr True)) (cteDelete (cte_map ptr) True) proof (prove)
goal:
No subgoals!