theory IpcCancel_C

lemma ep_blocked_in_queueD:
  "\<lbrakk> st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st)
                      \<and> blockingObject st = ep) thread \<sigma>;
               ko_at' ep' ep \<sigma>; invs' \<sigma> \<rbrakk>
   \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep')" apply (drule sym_refs_st_tcb_atD') apply clarsimp apply (clarsimp simp: refs_of_rev' obj_at'_def ko_wp_at'_def projectKOs) apply (clarsimp simp: isTS_defs split: Structures_H.thread_state.split_asm) apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] apply (cases ep', simp_all add: isSendEP_def isRecvEP_def)[1] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st) \<and> blockingObject st = ep) thread \<sigma>; ko_at' ep' ep \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep') proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ko_at' ep' ep \<sigma>; invs' \<sigma>\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of' \<sigma>)
 2. \<lbrakk>ko_at' ep' ep \<sigma>; invs' \<sigma>; \<exists>ts ntfnptr. ((isBlockedOnSend ts \<or> isBlockedOnReceive ts) \<and> blockingObject ts = ep) \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) thread \<sigma> \<and> state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (thread, symreftype tp) \<in> refs_of' ko) x \<sigma>)\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep') proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ko_at' ep' ep \<sigma>; invs' \<sigma>; \<exists>ts ntfnptr. ((isBlockedOnSend ts \<or> isBlockedOnReceive ts) \<and> blockingObject ts = ep) \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) thread \<sigma> \<and> state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr \<and> (\<forall>(x, tp)\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. ko_wp_at' (\<lambda>ko. (thread, symreftype tp) \<in> refs_of' ko) x \<sigma>)\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep') proof (prove)
goal (1 subgoal):
 1. \<And>ts ntfnptr obj. \<lbrakk>invs' \<sigma>; ksPSpace \<sigma> (blockingObject ts) = Some (KOEndpoint ep'); isBlockedOnSend ts \<or> isBlockedOnReceive ts; is_aligned (blockingObject ts) (objBitsKO (KOEndpoint ep')); ps_clear (blockingObject ts) (objBitsKO (KOEndpoint ep')) \<sigma>; ep = blockingObject ts; state_refs_of' \<sigma> thread = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; \<forall>x\<in>tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>; ksPSpace \<sigma> thread = Some (KOTCB obj); is_aligned thread (objBitsKO (KOTCB obj)); tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep') proof (prove)
goal (2 subgoals):
 1. \<And>ntfnptr obj. \<lbrakk>is_aligned ep (objBitsKO (KOEndpoint ep')); ps_clear ep (objBitsKO (KOEndpoint ep')) \<sigma>; state_refs_of' \<sigma> thread = insert (ep, TCBBlockedRecv) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); is_aligned thread (objBitsKO (KOTCB obj)); tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>; invs' \<sigma>; ksPSpace \<sigma> ep = Some (KOEndpoint ep'); (thread, EPRecv) \<in> ep_q_refs_of' ep'; \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep')
 2. \<And>ntfnptr obj. \<lbrakk>is_aligned ep (objBitsKO (KOEndpoint ep')); ps_clear ep (objBitsKO (KOEndpoint ep')) \<sigma>; state_refs_of' \<sigma> thread = insert (ep, TCBBlockedSend) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); is_aligned thread (objBitsKO (KOTCB obj)); tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>; invs' \<sigma>; ksPSpace \<sigma> ep = Some (KOEndpoint ep'); (thread, EPSend) \<in> ep_q_refs_of' ep'; \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep') proof (prove)
goal (1 subgoal):
 1. \<And>ntfnptr obj. \<lbrakk>is_aligned ep (objBitsKO (KOEndpoint ep')); ps_clear ep (objBitsKO (KOEndpoint ep')) \<sigma>; state_refs_of' \<sigma> thread = insert (ep, TCBBlockedSend) (tcb_bound_refs' ntfnptr); ksPSpace \<sigma> thread = Some (KOTCB obj); is_aligned thread (objBitsKO (KOTCB obj)); tcb_ntfn_is_bound' ntfnptr obj; ps_clear thread (objBitsKO (KOTCB obj)) \<sigma>; invs' \<sigma>; ksPSpace \<sigma> ep = Some (KOEndpoint ep'); (thread, EPSend) \<in> ep_q_refs_of' ep'; \<forall>x\<in>tcb_bound_refs' ntfnptr. case x of (x, tp) \<Rightarrow> \<exists>ko. ksPSpace \<sigma> x = Some ko \<and> is_aligned x (objBitsKO ko) \<and> (thread, symreftype tp) \<in> refs_of' ko \<and> ps_clear x (objBitsKO ko) \<sigma>\<rbrakk> \<Longrightarrow> thread \<in> set (epQueue ep') \<and> (isSendEP ep' \<or> isRecvEP ep') proof (prove)
goal:
No subgoals!