theory IpcCancel_R

lemma cancelBadgedSends_corres:
  "corres dc (invs and valid_sched and ep_at epptr) (invs' and ep_at' epptr)
         (cancel_badged_sends epptr bdg) (cancelBadgedSends epptr bdg)" apply (simp add: cancel_badged_sends_def cancelBadgedSends_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getEndpoint_corres _ get_simple_ko_sp get_ep_sp',
                                 where Q="invs and valid_sched" and Q'=invs']) apply simp_all apply (case_tac ep, simp_all add: ep_relation_def) apply (simp add: filterM_mapM list_case_return cong: list.case_cong) apply (rule corres_guard_imp) apply (rule corres_split_nor[OF setEndpoint_corres]) apply (simp add: ep_relation_def) apply (rule corres_split_eqr[OF _ _ _ hoare_post_add[where R="\<lambda>_. valid_objs'"]]) apply (rule_tac S="(=)"
                     and Q="\<lambda>xs s. (\<forall>x \<in> set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s"
                    and Q'="\<lambda>xs s. (\<forall>x \<in> set xs. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s"
                     in corres_mapM_list_all2[where r'="(=)"],
                simp_all add: list_all2_refl)[1] apply (clarsimp simp: liftM_def[symmetric] o_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getThreadState_corres]) apply (rule_tac F="\<exists>pl. st = Structures_A.BlockedOnSend epptr pl"
                            in corres_gen_asm) apply (clarsimp simp: o_def dc_def[symmetric] liftM_def) apply (rule corres_split[OF setThreadState_corres]) apply simp apply (rule corres_split[OF tcbSchedEnqueue_corres]) apply (rule corres_trivial) apply simp apply (wp sts_valid_queues gts_st_tcb_at)+ apply (clarsimp simp: valid_tcb_state_def tcb_at_def st_tcb_def2
                                  st_tcb_at_refs_of_rev
                           dest!: state_refs_of_elemD elim!: tcb_at_is_etcb_at[rotated]) apply (simp add: is_tcb_def) apply (wp hoare_vcg_const_Ball_lift gts_wp | clarsimp)+ apply (wp gts_st_tcb_at hoare_vcg_imp_lift
                      sts_st_tcb' sts_valid_queues
                      | clarsimp simp: valid_tcb_state'_def)+ apply (rule corres_split[OF _ rescheduleRequired_corres]) apply (rule setEndpoint_corres) apply (simp split: list.split add: ep_relation_def) apply (wp weak_sch_act_wf_lift_linear)+ apply (wp gts_st_tcb_at hoare_vcg_imp_lift mapM_wp'
                 sts_st_tcb' sts_valid_queues
                 set_thread_state_runnable_weak_valid_sched_action
                 | clarsimp simp: valid_tcb_state'_def)+ apply (wp hoare_vcg_const_Ball_lift  set_ep_valid_objs')+ apply (clarsimp simp: conj_comms) apply (frule sym_refs_ko_atD, clarsimp+) apply (rule obj_at_valid_objsE, assumption+, clarsimp+) apply (clarsimp simp: valid_obj_def valid_ep_def valid_sched_def valid_sched_action_def) apply (rule conjI, erule obj_at_weakenE, clarsimp simp: is_ep) apply (clarsimp simp: st_tcb_at_refs_of_rev) apply (drule(1) bspec, drule st_tcb_at_state_refs_ofD, clarsimp) apply (simp add: set_eq_subset) apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]) apply (drule ko_at_valid_objs', clarsimp) apply (simp add: projectKOs) apply (clarsimp simp: valid_obj'_def valid_ep'_def invs_weak_sch_act_wf
                        invs'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at epptr) (invs' and ep_at' epptr) (cancel_badged_sends epptr bdg) (cancelBadgedSends epptr bdg) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched and ep_at epptr) (invs' and ep_at' epptr) (do ep <- get_endpoint epptr;
case ep of Structures_A.endpoint.SendEP queue \<Rightarrow> do set_endpoint epptr Structures_A.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = bdg then do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od) (do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = bdg then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ()
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do ep <- get_endpoint epptr;
case ep of Structures_A.endpoint.SendEP queue \<Rightarrow> do set_endpoint epptr Structures_A.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = bdg then do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od) (do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = bdg then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ()
od)
 2. \<And>s. (invs and valid_sched and ep_at epptr) s \<Longrightarrow> ?Q s
 3. \<And>s. (invs' and ep_at' epptr) s \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<And>ep epa. ep_relation ep epa \<Longrightarrow> corres dc (ko_at (Endpoint ep) epptr and (invs and valid_sched)) (invs' and ko_at' epa epptr) (case ep of Structures_A.endpoint.SendEP queue \<Rightarrow> do set_endpoint epptr Structures_A.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = bdg then do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()) (case epa of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = bdg then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ())
 2. \<And>s. (invs and valid_sched and ep_at epptr) s \<Longrightarrow> (ep_at epptr and (invs and valid_sched)) s
 3. \<And>s. (invs' and ep_at' epptr) s \<Longrightarrow> (ep_at' epptr and invs') s proof (prove)
goal (1 subgoal):
 1. \<And>ep epa. ep_relation ep epa \<Longrightarrow> corres dc (ko_at (Endpoint ep) epptr and (invs and valid_sched)) (invs' and ko_at' epa epptr) (case ep of Structures_A.endpoint.SendEP queue \<Rightarrow> do set_endpoint epptr Structures_A.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = bdg then do set_thread_state t Structures_A.thread_state.Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()) (case epa of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = bdg then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ()) proof (prove)
goal (1 subgoal):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) (do y <- set_endpoint epptr Structures_A.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = bdg then do y <- set_thread_state t Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue t;
return False
od else return True
od) x2;
y <- set_endpoint epptr (case queue' of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP queue');
reschedule_required
od) (do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x2;
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
y <- setEndpoint epptr ep';
rescheduleRequired
od) proof (prove)
goal (1 subgoal):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) (do y <- set_endpoint epptr Structures_A.endpoint.IdleEP;
ys <- mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
ys <- mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od) proof (prove)
goal (3 subgoals):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?Q10 ep epa x2) (?Q'10 ep epa x2) (do y <- set_endpoint epptr Structures_A.endpoint.IdleEP;
ys <- mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
ys <- mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> ?Q10 ep epa x2 s
 3. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> ?Q'10 ep epa x2 s proof (prove)
goal (6 subgoals):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> ep_relation Structures_A.endpoint.IdleEP Structures_H.endpoint.IdleEP
 2. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R14 ep epa x2) (?R'14 ep epa x2) (do ys <- mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do ys <- mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 3. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. ?R14 ep epa x2\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. ?R'14 ep epa x2\<rbrace>
 5. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 6. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (5 subgoals):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R14 ep epa x2) (?R'14 ep epa x2) (do ys <- mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do ys <- mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2;
y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 2. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. ?R14 ep epa x2\<rbrace>
 3. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. ?R'14 ep epa x2\<rbrace>
 4. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 5. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (8 subgoals):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres (=) (?P20 ep epa x2) (?P'20 ep epa x2) (mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2) (mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2)
 2. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 3. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. ?P20 ep epa x2 and ?Q20 ep epa x2\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. ?P'20 ep epa x2 and ?Q'20 ep epa x2\<rbrace>
 7. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 8. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (10 subgoals):
 1. \<And>ep epa x2 x xs y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; list_all2 (=) xs ys\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s) (\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) (do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od) (do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od)
 2. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 3. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 4. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 9. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 10. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (10 subgoals):
 1. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> corres (=) (\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s) (\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) (do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
liftM (\<lambda>y. False) (tcb_sched_action tcb_sched_enqueue y)
od else return True
od) (do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
liftM (\<lambda>y. False) (tcbSchedEnqueue y)
od else return True
od)
 2. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 3. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 4. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 9. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 10. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (12 subgoals):
 1. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> corres (=) (?Q37 xs y ys) (?Q'37 xs y ys) (do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
liftM (\<lambda>y. False) (tcb_sched_action tcb_sched_enqueue y)
od else return True
od) (do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
liftM (\<lambda>y. False) (tcbSchedEnqueue y)
od else return True
od)
 2. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> ?Q37 xs y ys s
 3. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> ?Q'37 xs y ys s
 4. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 5. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 6. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 10. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
A total of 12 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>xs y ys st sta. \<lbrakk>list_all2 (=) xs ys; thread_state_relation st sta\<rbrakk> \<Longrightarrow> corres (=) (?R41 xs y ys st) (?R'41 xs y ys sta) (if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
liftM (\<lambda>y. False) (tcb_sched_action tcb_sched_enqueue y)
od else return True) (if blockingIPCBadge sta = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
liftM (\<lambda>y. False) (tcbSchedEnqueue y)
od else return True)
 2. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>?R41 xs y ys\<rbrace>
 3. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>?R'41 xs y ys\<rbrace>
 4. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 5. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 6. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 7. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 8. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 10. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>xs y ys st sta. \<lbrakk>list_all2 (=) xs ys; thread_state_relation st sta; \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl\<rbrakk> \<Longrightarrow> corres (=) (?P47 xs y ys st) (?R'41 xs y ys sta) (if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
liftM (\<lambda>y. False) (tcb_sched_action tcb_sched_enqueue y)
od else return True) (if blockingIPCBadge sta = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
liftM (\<lambda>y. False) (tcbSchedEnqueue y)
od else return True)
 2. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. ?P47 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 3. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>?R'41 xs y ys\<rbrace>
 4. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 5. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 6. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 7. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 8. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 10. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> corres (=) (?P47 xs y ys (Structures_A.thread_state.BlockedOnSend epptr pl)) (?R'41 xs y ys (Structures_H.thread_state.BlockedOnSend epptr (sender_badge pl) (sender_can_grant pl) (sender_can_grant_reply pl) (sender_is_call pl))) (do ya <- set_thread_state y Structures_A.thread_state.Restart;
x <- tcb_sched_action tcb_sched_enqueue y;
return False
od) (do ya <- setThreadState Structures_H.thread_state.Restart y;
x <- tcbSchedEnqueue y;
return False
od)
 2. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. ?P47 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 3. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>?R'41 xs y ys\<rbrace>
 4. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 5. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 6. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 7. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 8. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 10. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
A total of 14 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> thread_state_relation Structures_A.thread_state.Restart Structures_H.thread_state.Restart
 2. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> corres (=) (?R69 xs y ys pl ya) (?R'69 xs y ys pl yb) (do x <- tcb_sched_action tcb_sched_enqueue y;
return False
od) (do x <- tcbSchedEnqueue y;
return False
od)
 3. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q74 xs y ys (Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace> set_thread_state y Structures_A.thread_state.Restart \<lbrace>?R69 xs y ys pl\<rbrace>
 4. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q'73 xs y ys (Structures_H.thread_state.BlockedOnSend epptr (sender_badge pl) (sender_can_grant pl) (sender_can_grant_reply pl) (sender_is_call pl))\<rbrace> setThreadState Structures_H.thread_state.Restart y \<lbrace>?R'69 xs y ys pl\<rbrace>
 5. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. tcb_at y and ?Q74 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 6. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>\<lambda>a. tcb_at' y and ?Q'73 xs y ys a\<rbrace>
 7. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 8. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 9. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 10. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
A total of 17 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> corres (=) (?R69 xs y ys pl ya) (?R'69 xs y ys pl yb) (do x <- tcb_sched_action tcb_sched_enqueue y;
return False
od) (do x <- tcbSchedEnqueue y;
return False
od)
 2. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q74 xs y ys (Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace> set_thread_state y Structures_A.thread_state.Restart \<lbrace>?R69 xs y ys pl\<rbrace>
 3. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q'73 xs y ys (Structures_H.thread_state.BlockedOnSend epptr (sender_badge pl) (sender_can_grant pl) (sender_can_grant_reply pl) (sender_is_call pl))\<rbrace> setThreadState Structures_H.thread_state.Restart y \<lbrace>?R'69 xs y ys pl\<rbrace>
 4. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. tcb_at y and ?Q74 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 5. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>\<lambda>a. tcb_at' y and ?Q'73 xs y ys a\<rbrace>
 6. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 7. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 8. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 9. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 10. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
A total of 16 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>xs y ys pl ya yb rv rv'. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb; dc rv rv'\<rbrakk> \<Longrightarrow> corres (=) (?R79 xs y ys pl ya yb rv) (?R'79 xs y ys pl ya yb rv') (return False) (return False)
 2. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q82 xs y ys pl ya\<rbrace> tcb_sched_action tcb_sched_enqueue y \<lbrace>?R79 xs y ys pl ya yb\<rbrace>
 3. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 xs y ys pl yb\<rbrace> tcbSchedEnqueue y \<lbrace>?R'79 xs y ys pl ya yb\<rbrace>
 4. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q74 xs y ys (Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace> set_thread_state y Structures_A.thread_state.Restart \<lbrace>\<lambda>ya. is_etcb_at y and ?Q82 xs y ys pl ya\<rbrace>
 5. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q'73 xs y ys (Structures_H.thread_state.BlockedOnSend epptr (sender_badge pl) (sender_can_grant pl) (sender_can_grant_reply pl) (sender_is_call pl))\<rbrace> setThreadState Structures_H.thread_state.Restart y \<lbrace>\<lambda>yb. tcb_at' y and Invariants_H.valid_queues and valid_queues' and ?Q'84 xs y ys pl yb\<rbrace>
 6. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. tcb_at y and ?Q74 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 7. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>\<lambda>a. tcb_at' y and ?Q'73 xs y ys a\<rbrace>
 8. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 9. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 10. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
A total of 18 subgoals... proof (prove)
goal (18 subgoals):
 1. \<And>xs y ys pl ya yb rv rv'. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb; dc rv rv'\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (return False) (return False)
 2. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q82 xs y ys pl ya\<rbrace> tcb_sched_action tcb_sched_enqueue y \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 xs y ys pl yb\<rbrace> tcbSchedEnqueue y \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q74 xs y ys (Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace> set_thread_state y Structures_A.thread_state.Restart \<lbrace>\<lambda>ya. is_etcb_at y and ?Q82 xs y ys pl ya\<rbrace>
 5. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q'73 xs y ys (Structures_H.thread_state.BlockedOnSend epptr (sender_badge pl) (sender_can_grant pl) (sender_can_grant_reply pl) (sender_is_call pl))\<rbrace> setThreadState Structures_H.thread_state.Restart y \<lbrace>\<lambda>yb. tcb_at' y and Invariants_H.valid_queues and valid_queues' and ?Q'84 xs y ys pl yb\<rbrace>
 6. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. tcb_at y and ?Q74 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 7. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>\<lambda>a. tcb_at' y and ?Q'73 xs y ys a\<rbrace>
 8. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 9. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 10. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
A total of 18 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q82 xs y ys pl ya\<rbrace> tcb_sched_action tcb_sched_enqueue y \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>xs y ys pl ya yb. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl; dc ya yb\<rbrakk> \<Longrightarrow> \<lbrace>?Q'84 xs y ys pl yb\<rbrace> tcbSchedEnqueue y \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q74 xs y ys (Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace> set_thread_state y Structures_A.thread_state.Restart \<lbrace>\<lambda>ya. is_etcb_at y and ?Q82 xs y ys pl ya\<rbrace>
 4. \<And>xs y ys pl. \<lbrakk>list_all2 (=) xs ys; bdg = sender_badge pl\<rbrakk> \<Longrightarrow> \<lbrace>?Q'73 xs y ys (Structures_H.thread_state.BlockedOnSend epptr (sender_badge pl) (sender_can_grant pl) (sender_can_grant_reply pl) (sender_is_call pl))\<rbrace> setThreadState Structures_H.thread_state.Restart y \<lbrace>\<lambda>yb. tcb_at' y and Invariants_H.valid_queues and valid_queues' and ?Q'84 xs y ys pl yb\<rbrace>
 5. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q41 xs y ys\<rbrace> get_thread_state y \<lbrace>\<lambda>st. tcb_at y and ?Q74 xs y ys st and (\<lambda>s. \<exists>pl. st = Structures_A.thread_state.BlockedOnSend epptr pl)\<rbrace>
 6. \<And>xs y ys. list_all2 (=) xs ys \<Longrightarrow> \<lbrace>?Q'41 xs y ys\<rbrace> getThreadState y \<lbrace>\<lambda>a. tcb_at' y and ?Q'73 xs y ys a\<rbrace>
 7. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and ?Q41 xs y ys) s
 8. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and ?Q'41 xs y ys) s
 9. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 10. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
A total of 17 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrakk> \<Longrightarrow> (tcb_at y and (\<lambda>s. (tcb_at y and (\<lambda>a. is_etcb_at y a \<and> True)) s \<and> st_tcb_at (\<lambda>rv. \<exists>pl. rv = Structures_A.thread_state.BlockedOnSend epptr pl) y s)) s
 2. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and (tcb_at' y and (\<lambda>a. tcb_at' y a \<and> (Invariants_H.valid_queues a \<and> ((\<exists>p. y \<in> set (ksReadyQueues a p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart)) \<and> valid_queues' a \<and> True))) s
 3. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 4. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 5. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 10. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>xs y ys s tcb pl. \<lbrakk>list_all2 (=) xs ys; \<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x; y \<notin> set xs; distinct xs; tcb_state tcb = Structures_A.thread_state.BlockedOnSend epptr pl; get_tcb y s = Some tcb\<rbrakk> \<Longrightarrow> is_tcb (TCB tcb)
 2. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and (tcb_at' y and (\<lambda>a. tcb_at' y a \<and> (Invariants_H.valid_queues a \<and> ((\<exists>p. y \<in> set (ksReadyQueues a p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart)) \<and> valid_queues' a \<and> True))) s
 3. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 4. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 5. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 10. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>xs y ys s. \<lbrakk>list_all2 (=) xs ys; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (tcb_at' y and (tcb_at' y and (\<lambda>a. tcb_at' y a \<and> (Invariants_H.valid_queues a \<and> ((\<exists>p. y \<in> set (ksReadyQueues a p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart)) \<and> valid_queues' a \<and> True))) s
 2. \<And>ep epa x2 x xs y. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # xs) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (epptr, TCBBlockedSend) \<in> state_refs_of s y \<and> (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> y \<notin> set xs \<and> distinct xs \<and> valid_etcbs s\<rbrace> do v <- do st <- get_thread_state y;
if blocking_ipc_badge st = bdg then do ya <- set_thread_state y Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set xs. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct xs \<and> valid_etcbs s\<rbrace>
 3. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace> do v <- do st <- getThreadState y;
if blockingIPCBadge st = bdg then do ya <- setThreadState Structures_H.thread_state.Restart y;
y <- tcbSchedEnqueue y;
return False
od else return True
od;
return (y, v)
od \<lbrace>\<lambda>r s. (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrace>
 4. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 9. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 10. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (11 subgoals):
 1. \<And>x2 y ys st. \<lbrakk>suffix (y # ys) x2; bdg = blockingIPCBadge st\<rbrakk> \<Longrightarrow> \<lbrace>?P'220 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 y y ys st\<rbrace> setThreadState Structures_H.thread_state.Restart y \<lbrace>\<lambda>rv s. Invariants_H.valid_queues s \<and> st_tcb_at' runnable' y s \<and> valid_objs' s \<and> valid_queues' s \<and> st_tcb_at' runnable' y s \<and> valid_objs' s\<rbrace>
 2. \<And>ep epa x2 x y ys st. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2; blockingIPCBadge st \<noteq> bdg\<rbrakk> \<Longrightarrow> \<lbrace>?R209 ep epa x2 x y ys st\<rbrace> return True \<lbrace>\<lambda>v a. weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> valid_objs' a\<rbrace>
 3. \<And>ep epa x2 x y ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2\<rbrakk> \<Longrightarrow> \<lbrace>?P'184 ep epa x2 x y ys\<rbrace> getThreadState y \<lbrace>\<lambda>st s. (blockingIPCBadge st = bdg \<longrightarrow> (weak_sch_act_wf (ksSchedulerAction s) s \<and> (ksSchedulerAction s = SwitchToThread y \<longrightarrow> runnable' Structures_H.thread_state.Restart)) \<and> ?P'220 ep epa x2 x y ys st s) \<and> (blockingIPCBadge st \<noteq> bdg \<longrightarrow> ?R209 ep epa x2 x y ys st s)\<rbrace>
 4. \<And>ep epa x2 x y ys s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; x = y; suffix (y # ys) x2; tcb_at' y s \<and> (\<forall>x\<in>set ys. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set ys. tcb_at' x s) \<and> ?P'184 ep epa x2 x y ys s
 5. \<And>ep epa x2 ys. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> corres dc (?R20 ep epa x2 ys) (?R'20 ep epa x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 8. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 9. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 10. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
A total of 11 subgoals... proof (prove)
goal (7 subgoals):
 1. \<And>x2 ys. corres dc (?R20 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys) (?R'20 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys) (do y <- set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list));
reschedule_required
od) (do y <- setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list));
rescheduleRequired
od)
 2. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>?R20 ep epa x2\<rbrace>
 3. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> ?R'20 ep epa x2 r s\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 6. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 7. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (9 subgoals):
 1. \<And>x2 ys. corres (?r'272 x2 ys) (?P281 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys) (?P'279 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys) (set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list))) (setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)))
 2. \<And>x2 ys. \<lbrace>?Q280 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys\<rbrace> set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list)) \<lbrace>\<lambda>y. weak_valid_sched_action and valid_etcbs\<rbrace>
 3. \<And>x2 ys. \<lbrace>?Q'278 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys\<rbrace> setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) \<lbrace>\<lambda>y. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>a. ?P281 ep epa x2 a and ?Q280 ep epa x2 a\<rbrace>
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> (?P'279 ep epa x2 r and ?Q'278 ep epa x2 r) s\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 8. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 9. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (9 subgoals):
 1. \<And>x2 ys. ep_relation (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list)) (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list))
 2. \<And>x2 ys. \<lbrace>?Q280 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys\<rbrace> set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list)) \<lbrace>\<lambda>y. weak_valid_sched_action and valid_etcbs\<rbrace>
 3. \<And>x2 ys. \<lbrace>?Q'278 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys\<rbrace> setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) \<lbrace>\<lambda>y. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>a. ep_at epptr and ?Q280 ep epa x2 a\<rbrace>
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> (ep_at' epptr and ?Q'278 ep epa x2 r) s\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 7. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 8. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 9. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (8 subgoals):
 1. \<And>x2 ys. \<lbrace>?Q280 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys\<rbrace> set_endpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_A.endpoint.IdleEP | a # list \<Rightarrow> Structures_A.endpoint.SendEP (a # list)) \<lbrace>\<lambda>y. weak_valid_sched_action and valid_etcbs\<rbrace>
 2. \<And>x2 ys. \<lbrace>?Q'278 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2 ys\<rbrace> setEndpoint epptr (case map fst (filter snd ys) of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) \<lbrace>\<lambda>y. Invariants_H.valid_queues and valid_queues' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>a. ep_at epptr and ?Q280 ep epa x2 a\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> (ep_at' epptr and ?Q'278 ep epa x2 r) s\<rbrace>
 5. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 6. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 7. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 8. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (6 subgoals):
 1. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- get_thread_state x;
if blocking_ipc_badge st = bdg then do y <- set_thread_state x Structures_A.thread_state.Restart;
y <- tcb_sched_action tcb_sched_enqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>rv s. ep_at epptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s\<rbrace>
 2. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'20 ep epa x2\<rbrace> mapM (\<lambda>x. do v <- do st <- getThreadState x;
if blockingIPCBadge st = bdg then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True
od;
return (x, v)
od) x2 \<lbrace>\<lambda>r s. valid_objs' s \<and> (ep_at' epptr and (\<lambda>a. Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s\<rbrace>
 3. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q14 ep epa x2\<rbrace> set_endpoint epptr Structures_A.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> state_refs_of s x) \<and> distinct x2 \<and> valid_etcbs s) and ?Q20 ep epa x2\<rbrace>
 4. \<And>ep epa x2. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q'14 ep epa x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x. (\<lambda>s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s) and ?Q'20 ep epa x2\<rbrace>
 5. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and ?Q14 ep epa x2) s
 6. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (3 subgoals):
 1. \<And>x2. \<lbrace>?Q'14 (Structures_A.endpoint.SendEP x2) (Structures_H.endpoint.SendEP x2) x2\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>x s. (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s \<and> ep_at' epptr s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> ((state_refs_of s)(epptr := ep_q_refs_of Structures_A.endpoint.IdleEP)) x) \<and> distinct x2 \<and> valid_etcbs s \<and> ep_at epptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)) s
 3. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and ?Q'14 ep epa x2) s proof (prove)
goal (2 subgoals):
 1. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr and (invs and valid_sched)) s\<rbrakk> \<Longrightarrow> (ep_at epptr and (\<lambda>s. (\<forall>x\<in>set x2. (epptr, TCBBlockedSend) \<in> ((state_refs_of s)(epptr := ep_q_refs_of Structures_A.endpoint.IdleEP)) x) \<and> distinct x2 \<and> valid_etcbs s \<and> ep_at epptr s \<and> weak_valid_sched_action s \<and> valid_etcbs s)) s
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; valid_sched s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ep_at epptr s \<and> valid_etcbs s \<and> weak_valid_sched_action s \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> (epptr, TCBBlockedSend) \<in> state_refs_of s x))
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; valid_sched s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ep_at epptr s \<and> valid_etcbs s \<and> weak_valid_sched_action s \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> (epptr, TCBBlockedSend) \<in> state_refs_of s x))
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; valid_sched s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s; kheap s epptr = Some (Endpoint (Structures_A.endpoint.SendEP x2)); valid_obj epptr (Endpoint (Structures_A.endpoint.SendEP x2)) s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ep_at epptr s \<and> valid_etcbs s \<and> weak_valid_sched_action s \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> (epptr, TCBBlockedSend) \<in> state_refs_of s x))
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s; kheap s epptr = Some (Endpoint (Structures_A.endpoint.SendEP x2)); valid_etcbs s; x2 \<noteq> []; DetSchedInvs_AI.valid_queues s; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ct_not_in_q s; is_activatable (cur_thread s) s; weak_valid_sched_action s; switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> (epptr, TCBBlockedSend) \<in> state_refs_of s x))
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s; kheap s epptr = Some (Endpoint (Structures_A.endpoint.SendEP x2)); valid_etcbs s; x2 \<noteq> []; DetSchedInvs_AI.valid_queues s; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ct_not_in_q s; is_activatable (cur_thread s) s; weak_valid_sched_action s; switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> (epptr, TCBBlockedSend) \<in> state_refs_of s x)
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s x. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. st_tcb_at (\<lambda>ts. \<exists>pl. ts = Structures_A.thread_state.BlockedOnSend epptr pl) x s; kheap s epptr = Some (Endpoint (Structures_A.endpoint.SendEP x2)); valid_etcbs s; x2 \<noteq> []; DetSchedInvs_AI.valid_queues s; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ct_not_in_q s; is_activatable (cur_thread s) s; weak_valid_sched_action s; switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; x \<in> set x2\<rbrakk> \<Longrightarrow> x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> (epptr, TCBBlockedSend) \<in> state_refs_of s x)
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ntfnptr. \<lbrakk>invs s; ko_at (Endpoint (Structures_A.endpoint.SendEP x2)) epptr s; insert (epptr, TCBBlockedSend) (tcb_bound_refs ntfnptr) = set x2 \<times> {EPSend}; kheap s epptr = Some (Endpoint (Structures_A.endpoint.SendEP x2)); valid_etcbs s; x2 \<noteq> []; DetSchedInvs_AI.valid_queues s; \<forall>t\<in>set x2. tcb_at t s; distinct x2; ct_not_in_q s; is_activatable (cur_thread s) s; weak_valid_sched_action s; switch_in_cur_domain s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; epptr \<in> set x2; obj_at (tcb_ntfn_is_bound ntfnptr) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}\<rbrakk> \<Longrightarrow> False
 2. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (1 subgoal):
 1. \<And>ep epa x2 s. \<lbrakk>epa = Structures_H.endpoint.SendEP x2; ep = Structures_A.endpoint.SendEP x2; (invs' and ko_at' (Structures_H.endpoint.SendEP x2) epptr) s\<rbrakk> \<Longrightarrow> (ep_at' epptr and (\<lambda>a. (\<forall>x\<in>set x2. tcb_at' x a) \<and> weak_sch_act_wf (ksSchedulerAction a) a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> (valid_objs' and valid_ep' Structures_H.endpoint.IdleEP) a \<and> ep_at' epptr a \<and> Invariants_H.valid_queues a \<and> valid_queues' a \<and> weak_sch_act_wf (ksSchedulerAction a) a)) s proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>invs' s; ko_at' (Structures_H.endpoint.SendEP x2) epptr s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ko. \<lbrakk>invs' s; projectKO_opt ko = Some (Structures_H.endpoint.SendEP x2)\<rbrakk> \<Longrightarrow> injectKO (Structures_H.endpoint.SendEP x2) = ko
 2. \<And>x2 s. \<lbrakk>invs' s; valid_obj' (injectKO (Structures_H.endpoint.SendEP x2)) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal (1 subgoal):
 1. \<And>x2 s. \<lbrakk>invs' s; valid_obj' (injectKO (Structures_H.endpoint.SendEP x2)) s\<rbrakk> \<Longrightarrow> (\<forall>x\<in>set x2. tcb_at' x s) \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> valid_objs' s \<and> valid_ep' Structures_H.endpoint.IdleEP s \<and> Invariants_H.valid_queues s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!