theory Ipc_C

lemma receiveIPC_block_ccorres_helper:
  "ccorres dc xfdc (tcb_at' thread and valid_queues and valid_objs' and
                    sch_act_not thread and ep_at' epptr and
                    (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
                     (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and
                    K (epptr = epptr && ~~ mask 4) and
                    K (isEndpointCap cap \<and> ccap_relation cap cap'))
                   UNIV hs
           (setThreadState (Structures_H.thread_state.BlockedOnReceive
                                epptr (capEPCanGrant cap)) thread)
           (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_tsType(Ptr
              &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),
              scast ThreadState_BlockedOnReceive));;
            Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingObject(Ptr
                           &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),
              ucast (ptr_val (ep_Ptr epptr))));;
           \<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant(cap');;
           (Guard C_Guard \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingIPCCanGrant(Ptr
              &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),
              \<acute>ret__unsigned)));;
            CALL scheduleTCB(tcb_ptr_to_ctcb_ptr thread))" unfolding K_def setThreadState_def apply (intro ccorres_gen_asm) apply (rule ccorres_guard_imp) apply (rule ccorres_split_nothrow_novcg) apply (rule_tac P=\<top> and P'="tcb_at' thread"
                     in threadSet_ccorres_lemma3) apply vcg apply clarsimp apply (frule(1) tcb_at_h_t_valid) apply (frule h_t_valid_c_guard) apply (clarsimp simp: typ_heap_simps' rf_sr_tcb_update_twice cap_get_tag_isCap) apply (erule(1) rf_sr_tcb_update_no_queue_gen, (simp add: typ_heap_simps)+) apply (simp add: tcb_cte_cases_def) apply (simp add: ctcb_relation_def cthread_state_relation_def ccap_relation_ep_helpers
                         ThreadState_BlockedOnReceive_def mask_def cap_get_tag_isCap) apply ceqv apply clarsimp apply ctac apply (wp threadSet_valid_queues hoare_vcg_all_lift threadSet_valid_objs'
               threadSet_weak_sch_act_wf_runnable') apply (clarsimp simp: guard_is_UNIV_def) apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def
                         tcb_cte_cases_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and K (epptr = epptr && ~~ mask 4) and K (isEndpointCap cap \<and> ccap_relation cap cap')) UNIV hs (setThreadState (Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) thread) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr))));;
\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant_'proc(cap');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),\<acute>ret__unsigned));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and (\<lambda>y. epptr = epptr && ~~ mask 4) and (\<lambda>y. isEndpointCap cap \<and> ccap_relation cap cap')) UNIV hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr))));;
\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant_'proc(cap');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),\<acute>ret__unsigned));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) UNIV hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr))));;
\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant_'proc(cap');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),\<acute>ret__unsigned));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q2 ?Q'2 hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr))));;
\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant_'proc(cap');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),\<acute>ret__unsigned));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> ?Q2 s
 3. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'2 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ccorres ?r'6 ?xf'6 ?P6 ?Q'2 [] (threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr))));;
\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant_'proc(cap');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),\<acute>ret__unsigned)))
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ?xf'6 rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; ?r'6 rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV ?r'6 ?xf'6 ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (?P6 and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'2 proof (prove)
goal (8 subgoals):
 1. \<And>s tcb. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q12 s tcb) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr))));;
\<acute>ret__unsigned :== CALL cap_endpoint_cap_get_capCanGrant_'proc(cap');;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),\<acute>ret__unsigned)) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>s s' tcb tcb'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q12 s tcb
 3. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 4. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 6. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 8. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. sa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> sa \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift sa (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift sa (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals sa))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> t \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingObject_CL := UCAST(32 \<rightarrow> 32) (ptr_val (ep_Ptr epptr)) && ~~ mask 4\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals t))) \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<and> (\<forall>t. ret__unsigned_' t = capCanGrant_CL (cap_endpoint_cap_lift cap') \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> ta \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && mask 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals ta))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb))\<rparr>, sa\<lparr>ret__unsigned_' := capCanGrant_CL (cap_endpoint_cap_lift cap'), globals := globals sa\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))))}
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingObject_CL := epptr\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<and> ((\<exists>t. ret__unsigned_' t = capCanGrant_CL (cap_endpoint_cap_lift cap')) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb))\<rparr>, s'\<lparr>ret__unsigned_' := capCanGrant_CL (cap_endpoint_cap_lift cap'), globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))))
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'; s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingObject_CL := epptr\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<and> ((\<exists>t. ret__unsigned_' t = capCanGrant_CL (cap_endpoint_cap_lift cap')) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb))\<rparr>, s'\<lparr>ret__unsigned_' := capCanGrant_CL (cap_endpoint_cap_lift cap'), globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))))
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'; s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread; c_guard (tcb_ptr_to_ctcb_ptr thread)\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingObject_CL := epptr\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> cap_get_tag cap' = SCAST(32 signed \<rightarrow> 32) cap_endpoint_cap \<and> ((\<exists>t. ret__unsigned_' t = capCanGrant_CL (cap_endpoint_cap_lift cap')) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb))\<rparr>, s'\<lparr>ret__unsigned_' := capCanGrant_CL (cap_endpoint_cap_lift cap'), globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>) \<in> rf_sr))))
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb' t thread_state ta thread_statea tb tc thread_stateb. \<lbrakk>epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); ret__unsigned_' tb = capCanGrant_CL (cap_endpoint_cap_lift cap'); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr, blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb))\<rparr>, s'\<lparr>ret__unsigned_' := capCanGrant_CL (cap_endpoint_cap_lift cap'), globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>s s' tcb tcb' t thread_state ta thread_statea tb tc thread_stateb. \<lbrakk>epptr = epptr && ~~ mask 4; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); ret__unsigned_' tb = capCanGrant_CL (cap_endpoint_cap_lift cap'); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr, blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) = getF tcb
 2. \<And>s s' tcb tcb' t thread_state ta thread_statea tb tc thread_stateb. \<lbrakk>epptr = epptr && ~~ mask 4; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); ret__unsigned_' tb = capCanGrant_CL (cap_endpoint_cap_lift cap'); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr, blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))\<rbrakk> \<Longrightarrow> ctcb_relation (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')
 3. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 4. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 6. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 8. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb' t thread_state ta thread_statea tb tc thread_stateb. \<lbrakk>epptr = epptr && ~~ mask 4; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; isEndpointCap cap; ccap_relation cap cap'; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); ret__unsigned_' tb = capCanGrant_CL (cap_endpoint_cap_lift cap'); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnReceive && mask 4, blockingObject_CL := epptr, blockingIPCCanGrant_CL := capCanGrant_CL (cap_endpoint_cap_lift cap') && 1\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))\<rbrakk> \<Longrightarrow> ctcb_relation (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')
 2. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 3. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 5. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 7. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>rv' t t'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'6 rv')
 2. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'6 rv')
 3. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 4. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 5. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 6. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 rv) (?Q'6 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 3. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 4. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 5. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv'. \<lbrakk>epptr = epptr && ~~ mask 4; isEndpointCap cap; ccap_relation cap cap'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q6 ()) (?Q'6 () rv') hs (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>?Q6\<rbrace>
 3. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'6
 4. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 5. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> \<lbrace>?R6\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) thread \<lbrace>\<lambda>a. tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 2. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>})
 3. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R6) s
 4. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (3 subgoals):
 1. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>})
 2. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and (\<lambda>s. obj_at' (\<lambda>obj. if thread = thread then True else True) thread s \<and> ((ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' (Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb)))) thread s \<longrightarrow> thread \<notin> set (ksReadyQueues s (d, p)))) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) s)) s)) s
 3. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and (\<lambda>s. obj_at' (\<lambda>obj. if thread = thread then True else True) thread s \<and> ((ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' (Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap))) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb)))) thread s \<longrightarrow> thread \<notin> set (ksReadyQueues s (d, p)))) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnReceive epptr (capEPCanGrant cap)) tcb) s)) s)) s
 2. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>isEndpointCap cap \<and> ccap_relation cap cap'; epptr = epptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal:
No subgoals!