theory Invoke_C

lemma invokeCNodeCancelBadgedSends_ccorres:
  "ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
     (invs' and sch_act_simple and valid_cap' cap and K (isEndpointCap cap)) (UNIV \<inter> {s. ccap_relation cap (cap_' s)}) []
     (invokeCNode (CancelBadgedSends cap))
     (Call invokeCNodeCancelBadgedSends_'proc)" apply (simp) apply (rule ccorres_gen_asm) apply (clarsimp simp: isCap_simps) apply (cinit lift: cap_' simp del: return_bind cong:call_ignore_cong) apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (simp add: cap_get_tag_EndpointCap del: Collect_const) apply csymbr apply csymbr apply (simp add: unless_def liftE_def when_def Collect_True del: Collect_const) apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg) apply (rule_tac R=\<top> in ccorres_cond2) apply (clarsimp simp: cap_get_tag_isCap[symmetric] simp del: Collect_const dest!: cap_get_tag_to_H) apply (rule ccorres_rhs_assoc | csymbr)+ apply (ctac add: cancelBadgedSends_ccorres) apply (rule ccorres_return_Skip) apply ceqv apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre,vcg) apply clarsimp apply (simp add: return_def) apply wp apply (simp add: guard_is_UNIV_def) apply (frule cap_get_tag_isCap_unfolded_H_cap) apply (clarsimp simp: valid_cap_simps' cap_get_tag_EndpointCap) 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 and valid_cap' cap and K (isEndpointCap cap)) (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace>) [] (invokeCNode (CancelBadgedSends cap)) (Call invokeCNodeCancelBadgedSends_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and sch_act_simple and valid_cap' cap and (\<lambda>y. isEndpointCap cap)) \<lbrace>ccap_relation cap \<acute>cap\<rbrace> [] (invokeCNode (CancelBadgedSends cap)) (Call invokeCNodeCancelBadgedSends_'proc) proof (prove)
goal (1 subgoal):
 1. isEndpointCap cap \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and sch_act_simple and valid_cap' cap) \<lbrace>ccap_relation cap \<acute>cap\<rbrace> [] (invokeCNode (CancelBadgedSends cap)) (Call invokeCNodeCancelBadgedSends_'proc) proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3 v4 v5. cap = capability.EndpointCap v0 v1 v2 v3 v4 v5 \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) \<lbrace>ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) \<acute>cap\<rbrace> [] (invokeCNode (CancelBadgedSends (capability.EndpointCap v0 v1 v2 v3 v4 v5))) (Call invokeCNodeCancelBadgedSends_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>v0 v1 v2 v3 v4 v5 capa. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q177 v0 v1 v2 v3 v4 v5 capa) (?Q'177 v0 v1 v2 v3 v4 v5 capa) [SKIP] (liftE (unless (v1 = 0) (cancelBadgedSends v0 v1))) (\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPBadge_'proc(capa);;
(\<acute>badge :== \<acute>ret__unsigned;;
(IF \<acute>badge \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,\<acute>badge)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 v0 v1 v2 v3 v4 v5 capa s \<and> s' \<in> ?Q'177 v0 v1 v2 v3 v4 v5 capa proof (prove)
goal (2 subgoals):
 1. \<And>v0 v1 v2 v3 v4 v5 capa. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q177 v0 v1 v2 v3 v4 v5 capa) (?Q'177 v0 v1 v2 v3 v4 v5 capa) [SKIP] (liftE (unless (v1 = 0) (cancelBadgedSends v0 v1))) (\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPBadge_'proc(capa);;
(\<acute>badge :== \<acute>ret__unsigned;;
(IF \<acute>badge \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,\<acute>badge)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 v0 v1 v2 v3 v4 v5 capa s \<and> s' \<in> ?Q'177 v0 v1 v2 v3 v4 v5 capa proof (prove)
goal (2 subgoals):
 1. \<And>v0 capa. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q177 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Q'177 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) [SKIP] (liftE (unless (capEPBadge_CL (cap_endpoint_cap_lift capa) = 0) (cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa))))) (\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPBadge_'proc(capa);;
(\<acute>badge :== \<acute>ret__unsigned;;
(IF \<acute>badge \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))))
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 v0 v1 v2 v3 v4 v5 capa s \<and> s' \<in> ?Q'177 v0 v1 v2 v3 v4 v5 capa proof (prove)
goal (2 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q177 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?G'245 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa ret__unsigned) [SKIP] (liftE (unless (capEPBadge_CL (cap_endpoint_cap_lift capa) = 0) (cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa))))) (\<acute>badge :== ret__unsigned;;
(IF \<acute>badge \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)))
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 v0 v1 v2 v3 v4 v5 capa s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> ?G'245 v0 v1 v2 v3 v4 v5 capa v}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (2 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q177 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?G'365 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa ret__unsigned) [SKIP] (liftE (unless (capEPBadge_CL (cap_endpoint_cap_lift capa) = 0) (cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa))))) (IF ret__unsigned \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,ret__unsigned)
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 v0 v1 v2 v3 v4 v5 capa s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> ?G'365 v0 v1 v2 v3 v4 v5 capa v}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (2 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q177 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?G'365 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [SKIP] (do r <- if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return ();
return (Inr ())
od) (IF capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,capEPBadge_CL (cap_endpoint_cap_lift capa))
FI;;
return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q177 v0 v1 v2 v3 v4 v5 capa s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> ?G'365 v0 v1 v2 v3 v4 v5 capa v}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (6 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P489 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?G'365 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return ()) (IF capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 THEN
  \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,capEPBadge_CL (cap_endpoint_cap_lift capa))
FI)
 2. \<And>v0 capa ret__unsigned rv' t t'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'481 v0 capa ret__unsigned rv')
 3. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (?d'481 v0 capa ret__unsigned rv')
 4. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 5. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 6. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P489 v0 v1 v2 v3 v4 v5 capa and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> ?G'365 v0 v1 v2 v3 v4 v5 capa v}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (8 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0) = (s' \<in> \<lbrace>capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0\<rbrace>)
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt504 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Rt500 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa))) (\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,capEPBadge_CL (cap_endpoint_cap_lift capa)))
 3. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Rf498 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (return ()) SKIP
 4. \<And>v0 capa ret__unsigned rv' t t'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'481 v0 capa ret__unsigned rv')
 5. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (?d'481 v0 capa ret__unsigned rv')
 6. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 7. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 8. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> ?Pt504 v0 v1 v2 v3 v4 v5 capa s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> ?Pf502 v0 v1 v2 v3 v4 v5 capa s) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt500 v0 v1 v2 v3 v4 v5 capa v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf498 v0 v1 v2 v3 v4 v5 capa v)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (7 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt504 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Rt500 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa))) (\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capEPPtr_'proc(capa);;
\<acute>ep :== ep_Ptr \<acute>ret__unsigned;;
CALL cancelBadgedSends_'proc(\<acute>ep,capEPBadge_CL (cap_endpoint_cap_lift capa)))
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Rf498 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (return ()) SKIP
 3. \<And>v0 capa ret__unsigned rv' t t'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'481 v0 capa ret__unsigned rv')
 4. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (?d'481 v0 capa ret__unsigned rv')
 5. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 6. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 7. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> ?Pt504 v0 v1 v2 v3 v4 v5 capa s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> ?Pf502 v0 v1 v2 v3 v4 v5 capa s) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt500 v0 v1 v2 v3 v4 v5 capa v) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf498 v0 v1 v2 v3 v4 v5 capa v)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (7 subgoals):
 1. \<And>v0 capa ret__unsigneda ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigneda = capEPBadge_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPPtr_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt504 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?G'589 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa)) ret__unsigned) [] (cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa))) (CALL cancelBadgedSends_'proc(ep_Ptr ret__unsigned,capEPBadge_CL (cap_endpoint_cap_lift capa)))
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Rf498 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (return ()) SKIP
 3. \<And>v0 capa ret__unsigned rv' t t'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'481 v0 capa ret__unsigned rv')
 4. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (?d'481 v0 capa ret__unsigned rv')
 5. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 6. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 7. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> ?Pt504 v0 v1 v2 v3 v4 v5 capa s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> ?Pf502 v0 v1 v2 v3 v4 v5 capa s) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> ?G'589 v0 v1 v2 v3 v4 v5 capa v va}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf498 v0 v1 v2 v3 v4 v5 capa v)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (6 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa) (?Rf498 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa (capEPBadge_CL (cap_endpoint_cap_lift capa))) [] (return ()) SKIP
 2. \<And>v0 capa ret__unsigned rv' t t'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'481 v0 capa ret__unsigned rv')
 3. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (?d'481 v0 capa ret__unsigned rv')
 4. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 5. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 6. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> ?Pf502 v0 v1 v2 v3 v4 v5 capa s) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rf498 v0 v1 v2 v3 v4 v5 capa v)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (5 subgoals):
 1. \<And>v0 capa ret__unsigned rv' t t'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE)) (?d'481 v0 capa ret__unsigned rv')
 2. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (?d'481 v0 capa ret__unsigned rv')
 3. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 4. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 5. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (4 subgoals):
 1. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> ccorres (cintr \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') (?Q481 v0 capa ret__unsigned rv) (?Q'481 v0 capa ret__unsigned rv rv') [SKIP] (return (Inr ())) (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE))
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>?Q481 v0 capa ret__unsigned\<rbrace>
 3. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'481 v0 capa ret__unsigned)
 4. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (4 subgoals):
 1. \<And>v0 capa ret__unsigned rv rv'. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE) {},{s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' s)}
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 4. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (4 subgoals):
 1. \<And>v0 capa ret__unsigned rv rv' \<sigma>. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa); dc rv rv'\<rbrakk> \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (return (Inr ()) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (K ()) ret__unsigned_long_' (s\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))}
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 4. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (4 subgoals):
 1. \<And>capa \<sigma> x. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>xa\<in>fst (return (Inr ()) \<sigma>). case xa of (rv, \<sigma>') \<Rightarrow> (\<sigma>', x) \<in> rf_sr \<and> (cintr \<currency> dc) rv (liftxf errstate id (\<lambda>y. ()) ret__unsigned_long_' (x\<lparr>ret__unsigned_long_' := SCAST(32 signed \<rightarrow> 32) EXCEPTION_NONE, global_exn_var_' := Return\<rparr>))
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 4. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (3 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> \<lbrace>?R487 (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))) capa\<rbrace> if capEPBadge_CL (cap_endpoint_cap_lift capa) \<noteq> 0 then cancelBadgedSends (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) else return () \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 3. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and ?R487 v0 v1 v2 v3 v4 v5 capa) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (2 subgoals):
 1. \<And>v0 capa ret__unsigned. \<lbrakk>cap = capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa))); ccap_relation (capability.EndpointCap (capEPPtr_CL (cap_endpoint_cap_lift capa)) (capEPBadge_CL (cap_endpoint_cap_lift capa)) (to_bool (capCanSend_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanReceive_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrant_CL (cap_endpoint_cap_lift capa))) (to_bool (capCanGrantReply_CL (cap_endpoint_cap_lift capa)))) capa; v0 = capEPPtr_CL (cap_endpoint_cap_lift capa); ret__unsigned = capEPBadge_CL (cap_endpoint_cap_lift capa)\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>rv rv'. UNIV)
 2. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and (\<lambda>a. True)) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and (\<lambda>a. True)) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal (1 subgoal):
 1. \<And>v0 v1 v2 v3 v4 v5 capa s s'. \<lbrakk>cap = capability.EndpointCap v0 v1 v2 v3 v4 v5; ccap_relation (capability.EndpointCap v0 v1 v2 v3 v4 v5) capa; (s, s') \<in> rf_sr; (invs' and sch_act_simple and valid_cap' (capability.EndpointCap v0 v1 v2 v3 v4 v5)) s; s' \<in> UNIV; cap_get_tag capa = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. v1 \<noteq> 0 \<longrightarrow> (invs' and ep_at' v0) s) and (\<lambda>s. \<not> v1 \<noteq> 0 \<longrightarrow> True) and (\<lambda>a. True)) s \<and> s' \<in> {s. \<forall>v v'. v = capEPBadge_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := v\<rparr> \<in> {s. s \<in> {s. badge_'_update (\<lambda>_. v) s \<in> {s. (s \<in> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. \<forall>va v'. va = capEPPtr_CL (cap_endpoint_cap_lift (cap_' (cap_'_update (\<lambda>_. capa) s))) \<longrightarrow> s\<lparr>ret__unsigned_' := va\<rparr> \<in> {s. s \<in> {s. ep_'_update (\<lambda>_. ep_Ptr va) s \<in> {s. badge_'_update (\<lambda>x. v) (epptr_'_update (\<lambda>_. ep_Ptr va) s) \<in> UNIV \<inter> \<lbrace>\<acute>epptr = ep_Ptr v0\<rbrace> \<inter> \<lbrace>\<acute>badge = v\<rbrace>}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap}) \<and> (s \<notin> \<lbrace>v \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)}}}} \<inter> {s. cap_get_tag (cap_' (cap_'_update (\<lambda>_. capa) s)) = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap} proof (prove)
goal:
No subgoals!