theory IpcCancel_AI

lemma cancel_badged_sends_filterM_helper':
  "\<forall>ys.
   \<lbrace>\<lambda>s. all_invs_but_sym_refs s  \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s
           \<and> ex_nonz_cap_to epptr s
           \<and> sym_refs ((state_refs_of s) (epptr := ((set (xs @ ys)) \<times> {EPSend})))
           \<and> (\<forall>x \<in> set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace>
      filterM (\<lambda>t. do st \<leftarrow> get_thread_state t;
                      if blocking_ipc_badge st = badge
                      then do y \<leftarrow> set_thread_state t Structures_A.thread_state.Restart;
                              y \<leftarrow> do_extended_op (tcb_sched_action action t);
                              return False
                      od
                      else return True
                   od) xs
   \<lbrace>\<lambda>rv s. all_invs_but_sym_refs s \<and> sym_refs (state_hyp_refs_of s)
            \<and> ep_at epptr s \<and> (\<forall>x \<in> set (xs @ ys). tcb_at x s)
            \<and> ex_nonz_cap_to epptr s
            \<and> (\<forall>y \<in> set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})
            \<and> distinct rv \<and> distinct (xs @ ys) \<and> (set rv \<subseteq> set xs)
            \<and> sym_refs ((state_refs_of s) (epptr := ((set rv \<union> set ys) \<times> {EPSend})))\<rbrace>" apply (rule rev_induct[where xs=xs]) apply (rule allI, simp) apply wp apply clarsimp apply (drule(1) bspec, drule singleton_eqD, clarsimp, drule state_refs_of_elemD) apply (clarsimp simp: st_tcb_at_refs_of_rev pred_tcb_at_def is_tcb
                  elim!: obj_at_weakenE) apply (clarsimp simp: filterM_append bind_assoc simp del: set_append distinct_append) apply (drule spec, erule hoare_seq_ext[rotated]) apply (rule hoare_seq_ext [OF _ gts_sp]) apply (rule hoare_pre,
         wpsimp wp: valid_irq_node_typ sts_only_idle hoare_vcg_const_Ball_lift) apply (clarsimp simp: valid_tcb_state_def) apply (rule conjI[rotated]) apply blast apply clarsimp apply (thin_tac "obj_at f epptr s" for f s) apply (thin_tac "tcb_at x s" for x s) apply (thin_tac "sym_refs (state_hyp_refs_of s)" for s) apply (frule singleton_eqD, clarify, drule state_refs_of_elemD) apply (frule(1) if_live_then_nonz_capD) apply (rule refs_of_live, clarsimp) apply (clarsimp simp: st_tcb_at_refs_of_rev) apply (clarsimp simp: pred_tcb_def2 valid_idle_def) apply (rule conjI, clarsimp) apply (rule conjI, clarsimp) apply (drule(1) valid_reply_capsD, clarsimp simp: st_tcb_def2) apply (rule conjI, blast) apply (rule conjI, blast) apply (erule delta_sym_refs) apply (auto dest!: get_tcb_ko_atD ko_at_state_refs_ofD symreftype_inverse'
                      refs_in_tcb_bound_refs
               split: if_split_asm)[2] done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ([] @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ([] @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ([] @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) [] \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ([] @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ([] @ ys) \<and> set rv \<subseteq> set [] \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace>
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ((xs @ [x]) @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ys. \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ys \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set ys \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set ys. {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> return [] \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ys. tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ys \<and> rv = [] \<and> sym_refs (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of s a)\<rbrace>
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ((xs @ [x]) @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ys s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ys \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set ys \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set ys. {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<Longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ys. tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct [] \<and> distinct ys \<and> [] = [] \<and> sym_refs (\<lambda>a. if a = epptr then (set [] \<union> set ys) \<times> {EPSend} else state_refs_of s a)
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ((xs @ [x]) @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ys s x. \<lbrakk>x \<in> set ys; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); distinct ys; ep_at epptr s; ex_nonz_cap_to epptr s; sym_refs (\<lambda>a. if a = epptr then set ys \<times> {EPSend} else state_refs_of s a); \<forall>x\<in>set ys. {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}\<rbrakk> \<Longrightarrow> tcb_at x s
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ((xs @ [x]) @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ys s x. \<lbrakk>x \<in> set ys; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); distinct ys; ep_at epptr s; ex_nonz_cap_to epptr s; sym_refs (\<lambda>a. if a = epptr then set ys \<times> {EPSend} else state_refs_of s a); obj_at (\<lambda>obj. (epptr, TCBBlockedSend) \<in> refs_of obj) x s\<rbrakk> \<Longrightarrow> tcb_at x s
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ((xs @ [x]) @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set (xs @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct ((xs @ [x]) @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := set ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) (xs @ [x]) \<lbrace>\<lambda>rv s. (valid_objs and pspace_aligned and pspace_distinct and valid_ioc and if_live_then_nonz_cap and zombies_final and valid_mdb and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_machine_state and valid_irq_states and valid_irq_node and valid_irq_handlers and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_ioports and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb) s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set ((xs @ [x]) @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs ((state_refs_of s)(epptr := (set rv \<union> set ys) \<times> {EPSend}))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys. \<forall>ys. \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set (xs @ ys) \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set (xs @ ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> sym_refs (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of s a)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> distinct (xs @ x # ys) \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set (xs @ x # ys) \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set (xs @ x # ys). {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace> do xs' <- filterM (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do y <- set_thread_state t Restart;
y <- do_extended_op (tcb_sched_action action t);
return False
od else return True
od) xs;
xa <- get_thread_state x;
b <- if blocking_ipc_badge xa = badge then do y <- set_thread_state x Restart;
y <- do_extended_op (tcb_sched_action action x);
return False
od else return True;
return (xs' @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of s a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa. \<lbrace>\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set (x # ys). {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct xa \<and> distinct (xs @ x # ys) \<and> set xa \<subseteq> set xs \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set (x # ys)) \<times> {EPSend} else state_refs_of s a)\<rbrace> do xb <- get_thread_state x;
b <- if blocking_ipc_badge xb = badge then do y <- set_thread_state x Restart;
y <- do_extended_op (tcb_sched_action action x);
return False
od else return True;
return (xa @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of s a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb. \<lbrace>st_tcb_at ((=) xb) x and (\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set (x # ys). {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct xa \<and> distinct (xs @ x # ys) \<and> set xa \<subseteq> set xs \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set (x # ys)) \<times> {EPSend} else state_refs_of s a))\<rbrace> do b <- if blocking_ipc_badge xb = badge then do y <- set_thread_state x Restart;
y <- do_extended_op (tcb_sched_action action x);
return False
od else return True;
return (xa @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> sym_refs (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of s a)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. (st_tcb_at ((=) xb) x and (\<lambda>s. valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set (x # ys). {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct xa \<and> distinct (xs @ x # ys) \<and> set xa \<subseteq> set xs \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set (x # ys)) \<times> {EPSend} else state_refs_of s a))) s \<Longrightarrow> (blocking_ipc_badge xb = badge \<longrightarrow> (valid_objs and valid_tcb_state Restart and (\<lambda>s. (\<forall>a data. Restart = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (x, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> halted Restart \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s))) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> ((\<not> halted Restart \<longrightarrow> ex_nonz_cap_to x s) \<and> if_live_then_nonz_cap s) \<and> zombies_final s \<and> valid_mdb s \<and> (valid_idle and (\<lambda>s. x = idle_thread s \<longrightarrow> idle Restart)) s \<and> (only_idle and (\<lambda>s. idle Restart \<longrightarrow> x = idle_thread s)) s \<and> if_unsafe_then_cap s \<and> (valid_reply_caps s \<and> (Restart \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap x s)) \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>xa\<in>set ys. {r \<in> ((state_refs_of s)(x := tcb_st_refs_of Restart \<union> {r \<in> state_refs_of s x. snd r = TCBBound})) xa. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct (xa @ (if False then [x] else [])) \<and> distinct (xs @ x # ys) \<and> set (xa @ (if False then [x] else [])) \<subseteq> set (xs @ [x]) \<and> sym_refs (\<lambda>a. if a = epptr then (set (xa @ (if False then [x] else [])) \<union> set ys) \<times> {EPSend} else ((state_refs_of s)(x := tcb_st_refs_of Restart \<union> {r \<in> state_refs_of s x. snd r = TCBBound})) a)) \<and> (blocking_ipc_badge xb \<noteq> badge \<longrightarrow> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> valid_mdb s \<and> valid_idle s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_machine_state s \<and> valid_irq_states s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_vspace_objs s \<and> valid_arch_caps s \<and> valid_global_objs s \<and> valid_kernel_mappings s \<and> equal_kernel_mappings s \<and> valid_asid_map s \<and> valid_ioports s \<and> valid_global_vspace_mappings s \<and> pspace_in_kernel_window s \<and> cap_refs_in_kernel_window s \<and> pspace_respects_device_region s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> sym_refs (state_hyp_refs_of s) \<and> ep_at epptr s \<and> (\<forall>x\<in>set (xs @ x # ys). tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> (\<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}) \<and> distinct (xa @ (if True then [x] else [])) \<and> distinct (xs @ x # ys) \<and> set (xa @ (if True then [x] else [])) \<subseteq> set (xs @ [x]) \<and> sym_refs (\<lambda>a. if a = epptr then (set (xa @ (if True then [x] else [])) \<union> set ys) \<times> {EPSend} else state_refs_of s a)) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); ep_at epptr s; tcb_at x s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a)\<rbrakk> \<Longrightarrow> (blocking_ipc_badge xb = badge \<longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a)) \<and> (blocking_ipc_badge xb \<noteq> badge \<longrightarrow> x \<notin> set xa \<and> set xa \<subseteq> insert x (set xs)) proof (prove)
goal (2 subgoals):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); ep_at epptr s; tcb_at x s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a)\<rbrakk> \<Longrightarrow> blocking_ipc_badge xb \<noteq> badge \<longrightarrow> x \<notin> set xa \<and> set xa \<subseteq> insert x (set xs)
 2. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); ep_at epptr s; tcb_at x s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a)\<rbrakk> \<Longrightarrow> blocking_ipc_badge xb = badge \<longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); ep_at epptr s; tcb_at x s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a)\<rbrakk> \<Longrightarrow> blocking_ipc_badge xb = badge \<longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); ep_at epptr s; tcb_at x s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); tcb_at x s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; sym_refs (state_hyp_refs_of s); \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb; snd (epptr, TCBBlockedSend) \<noteq> TCBBound; obj_at (\<lambda>obj. (epptr, TCBBlockedSend) \<in> refs_of obj) x s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xs ys xa xb s obj. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb; snd (epptr, TCBBlockedSend) \<noteq> TCBBound; obj_at (\<lambda>obj. (epptr, TCBBlockedSend) \<in> refs_of obj) x s; (epptr, TCBBlockedSend) \<in> refs_of obj; kheap s x = Some obj\<rbrakk> \<Longrightarrow> live obj
 2. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb; snd (epptr, TCBBlockedSend) \<noteq> TCBBound; obj_at (\<lambda>obj. (epptr, TCBBlockedSend) \<in> refs_of obj) x s; ex_nonz_cap_to x s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb; snd (epptr, TCBBlockedSend) \<noteq> TCBBound; obj_at (\<lambda>obj. (epptr, TCBBlockedSend) \<in> refs_of obj) x s; ex_nonz_cap_to x s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> ex_nonz_cap_to x s \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb s. \<lbrakk>st_tcb_at ((=) xb) x s; valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = blocking_ipc_badge xb; st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend epptr pl) x s; ex_nonz_cap_to x s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) x s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = x) (x, tcb_cnode_index 2) s) \<and> x \<noteq> idle_thread s \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb)\<rbrakk> \<Longrightarrow> x \<noteq> idle_thread_ptr \<and> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb)\<rbrakk> \<Longrightarrow> \<not> has_reply_cap x s \<and> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb); has_reply_cap x s\<rbrakk> \<Longrightarrow> False
 2. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb)\<rbrakk> \<Longrightarrow> (\<forall>xa\<in>set ys. xa \<noteq> x) \<and> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb)\<rbrakk> \<Longrightarrow> set xa \<subseteq> insert x (set xs) \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa s tcb tcbb pl. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s a); badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb)\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>x xs ys xa s tcb tcbb pl xb y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb); (y, tp) \<in> (if xb = epptr then (set xa \<union> set ys) \<times> {EPSend} else if xb = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s xb); (y, tp) \<notin> (if xb = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s xb)\<rbrakk> \<Longrightarrow> (xb, symreftype tp) \<in> (if y = epptr then (set xa \<union> set ys) \<times> {EPSend} else if y = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s y)
 2. \<And>x xs ys xa s tcb tcbb pl xb y tp. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; valid_ioc s; if_live_then_nonz_cap s; zombies_final s; valid_mdb s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_machine_state s; valid_irq_states s; valid_irq_node s; valid_irq_handlers s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_ioports s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>x\<in>set xs \<union> set ys. tcb_at x s; ex_nonz_cap_to epptr s; {r \<in> state_refs_of s x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; \<forall>y\<in>set ys. {r \<in> state_refs_of s y. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; badge = sender_badge pl; ex_nonz_cap_to x s; idle_thread s = idle_thread_ptr; get_tcb x s = Some tcb; tcb_state tcb = BlockedOnSend epptr pl; get_tcb idle_thread_ptr s = Some tcbb; idle (tcb_state tcbb); tcb_bound_notification tcbb = None; valid_arch_idle (tcb_iarch tcbb); (y, tp) \<in> (if xb = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of s xb); (y, tp) \<notin> (if xb = epptr then (set xa \<union> set ys) \<times> {EPSend} else if xb = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s xb)\<rbrakk> \<Longrightarrow> (xb, symreftype tp) \<notin> (if y = epptr then (set xa \<union> set ys) \<times> {EPSend} else if y = x then {r \<in> state_refs_of s x. snd r = TCBBound} else state_refs_of s y) proof (prove)
goal:
No subgoals!