theory Invoke_C

lemma invokeCNodeDelete_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
       (\<lambda>s. invs' s \<and> sch_act_simple s)
       (UNIV \<inter> {s. destSlot_' s = Ptr destSlot}) []
       (invokeCNode (Delete destSlot))
  (Call invokeCNodeDelete_'proc)" apply (cinit lift: destSlot_' simp del: return_bind cong:call_ignore_cong) apply (rule ccorres_trim_returnE, simp, simp) apply (rule ccorres_callE) apply (rule cteDelete_ccorres[simplified]) apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (\<lambda>s. invs' s \<and> sch_act_simple s) (UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace>) [] (invokeCNode (Delete destSlot)) (Call invokeCNodeDelete_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>destSlota. destSlota = cte_Ptr destSlot \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q58 destSlota) (?Q'58 destSlota) [SKIP] (cteDelete destSlot True) (\<acute>ret__unsigned_long :== CALL cteDelete_'proc(destSlota,SCAST(32 signed \<rightarrow> 32) true);;
return_C ret__unsigned_long_'_update ret__unsigned_long_')
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q58 destSlota s \<and> s' \<in> ?Q'58 destSlota proof (prove)
goal (2 subgoals):
 1. \<And>destSlota. destSlota = cte_Ptr destSlot \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q58 destSlota) (?Q'58 destSlota) [SKIP] (cteDelete destSlot True) (\<acute>ret__unsigned_long :== CALL cteDelete_'proc(destSlota,SCAST(32 signed \<rightarrow> 32) true))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q58 destSlota s \<and> s' \<in> ?Q'58 destSlota proof (prove)
goal (6 subgoals):
 1. \<And>destSlota. destSlota = cte_Ptr destSlot \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) (?xf''68 destSlota)) (?Q58 destSlota) (?C'68 destSlota) [] (cteDelete destSlot True) (Call cteDelete_'proc)
 2. \<And>destSlota s ta sa. destSlota = cte_Ptr destSlot \<Longrightarrow> globals (sa\<lparr>ret__unsigned_long_' := ret__unsigned_long_' ta\<rparr>) = globals sa
 3. \<And>destSlota a s t. destSlota = cte_Ptr destSlot \<Longrightarrow> errstate (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = errstate t
 4. \<And>destSlota a s t. destSlota = cte_Ptr destSlot \<Longrightarrow> ret__unsigned_long_' (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = ?xf''68 destSlota t
 5. \<And>destSlota s. destSlota = cte_Ptr destSlot \<Longrightarrow> globals (exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (slot_'_update (\<lambda>_. destSlota) s)) = globals s
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q58 destSlota s \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (slot_'_update (\<lambda>_. destSlota) s) \<in> ?C'68 destSlota} proof (prove)
goal (5 subgoals):
 1. \<And>destSlota s ta sa. destSlota = cte_Ptr destSlot \<Longrightarrow> globals (sa\<lparr>ret__unsigned_long_' := ret__unsigned_long_' ta\<rparr>) = globals sa
 2. \<And>destSlota a s t. destSlota = cte_Ptr destSlot \<Longrightarrow> errstate (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = errstate t
 3. \<And>destSlota a s t. destSlota = cte_Ptr destSlot \<Longrightarrow> ret__unsigned_long_' (s\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr>) = ret__unsigned_long_' t
 4. \<And>destSlota s. destSlota = cte_Ptr destSlot \<Longrightarrow> globals (exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (slot_'_update (\<lambda>_. destSlota) s)) = globals s
 5. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; invs' s \<and> sch_act_simple s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' s \<and> sch_act_simple s \<and> (True \<or> ex_cte_cap_wp_to' (\<lambda>_. True) destSlot s)) \<and> s' \<in> {s. exposed_'_update (\<lambda>_. SCAST(32 signed \<rightarrow> 32) true) (slot_'_update (\<lambda>_. destSlota) s) \<in> \<lbrace>\<acute>slot = cte_Ptr destSlot\<rbrace> \<inter> \<lbrace>\<acute>exposed = from_bool True\<rbrace>} proof (prove)
goal:
No subgoals!