theory Invoke_C

lemma invokeCNodeRevoke_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
         (invs' and sch_act_simple)
         (UNIV \<inter> {s. destSlot_' s = cte_Ptr destSlot}) []
       (invokeCNode (Revoke destSlot))
  (Call invokeCNodeRevoke_'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 cteRevoke_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_') (invs' and sch_act_simple) (UNIV \<inter> \<lbrace>\<acute>destSlot = cte_Ptr destSlot\<rbrace>) [] (invokeCNode (Revoke destSlot)) (Call invokeCNodeRevoke_'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] (cteRevoke destSlot) (\<acute>ret__unsigned_long :== CALL cteRevoke_'proc(destSlota);;
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' 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] (cteRevoke destSlot) (\<acute>ret__unsigned_long :== CALL cteRevoke_'proc(destSlota))
 2. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (invs' 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) [] (cteRevoke destSlot) (Call cteRevoke_'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 (slot_'_update (\<lambda>_. destSlota) s) = globals s
 6. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q58 destSlota s \<and> s' \<in> {s. 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 (slot_'_update (\<lambda>_. destSlota) s) = globals s
 5. \<And>destSlota s s'. \<lbrakk>destSlota = cte_Ptr destSlot; (s, s') \<in> rf_sr; (invs' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (invs' and sch_act_simple) s \<and> s' \<in> {s. slot_'_update (\<lambda>_. destSlota) s \<in> \<lbrace>\<acute>slot = cte_Ptr destSlot\<rbrace>} proof (prove)
goal:
No subgoals!