theory IpcCancel_AI

lemma blocked_cancel_ipc_invs:
  "\<lbrace>invs and st_tcb_at ((=) st) t\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: blocked_cancel_ipc_def) apply (rule hoare_seq_ext [OF _ gbi_ep_sp]) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (rule hoare_seq_ext [OF _ get_epq_sp]) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre, wp valid_irq_node_typ sts_only_idle) apply (simp add: valid_tcb_state_def) apply (strengthen reply_cap_doesnt_exist_strg) apply simp apply (wp valid_irq_node_typ valid_ioports_lift) apply (subgoal_tac "ep \<noteq> Structures_A.IdleEP") apply (clarsimp simp: ep_redux_simps2 cong: if_cong) apply (frule(1) if_live_then_nonz_capD, (clarsimp simp: live_def)+) apply (frule ko_at_state_refs_ofD) apply (erule(1) obj_at_valid_objsE, clarsimp simp: valid_obj_def) apply (frule st_tcb_at_state_refs_ofD) apply (subgoal_tac "epptr \<notin> set (remove1 t queue)") apply (case_tac ep, simp_all add: valid_ep_def)[1] apply (auto elim!: delta_sym_refs pred_tcb_weaken_strongerE
                 simp: obj_at_def is_ep_def2 idle_not_queued refs_in_tcb_bound_refs
                 dest: idle_no_refs
                 split: if_split_asm)[2] apply (case_tac ep, simp_all add: valid_ep_def)[1] apply (clarsimp, drule(1) bspec, clarsimp simp: obj_at_def is_tcb_def)+ apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at ((=) st) t\<rbrace> blocked_cancel_ipc st t \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at ((=) st) t\<rbrace> do epptr <- get_blocking_object st;
ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr. \<lbrace>invs and st_tcb_at ((=) st) t and K ((\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))\<rbrace> do ep <- get_endpoint epptr;
queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr ep. \<lbrace>ko_at (Endpoint ep) epptr and (invs and st_tcb_at ((=) st) t and K ((\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d)))\<rbrace> do queue <- get_ep_queue ep;
y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr ep queue. \<lbrace>ko_at (Endpoint ep) epptr and (invs and st_tcb_at ((=) st) t and K ((\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and K (ep \<in> {SendEP queue, RecvEP queue})\<rbrace> do y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>epptr ep queue. \<lbrace>ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)\<rbrace> do y <- set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue. \<lbrace>?P'122 epptr ep queue\<rbrace> set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)) \<lbrace>\<lambda>rv s. valid_tcb_state Inactive s \<and> ((\<forall>a data. Inactive = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted Inactive \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s)) \<and> pspace_aligned s \<and> pspace_distinct s \<and> ((\<not> halted Inactive \<longrightarrow> ex_nonz_cap_to t s) \<and> if_live_then_nonz_cap s) \<and> zombies_final s \<and> sym_refs ((state_refs_of s)(t := tcb_st_refs_of Inactive \<union> {r \<in> state_refs_of s t. snd r = TCBBound})) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> (valid_idle and (\<lambda>s. t = idle_thread s \<longrightarrow> idle Inactive)) s \<and> (only_idle and (\<lambda>s. idle Inactive \<longrightarrow> t = idle_thread s)) s \<and> if_unsafe_then_cap s \<and> (valid_reply_caps s \<and> (Inactive \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s)) \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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\<rbrace>
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) and K (is_simple_type (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))))) s \<and> ?P'122 epptr ep queue s proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue. \<lbrace>?P'122 epptr ep queue\<rbrace> set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)) \<lbrace>\<lambda>rv s. pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> t \<noteq> idle_thread s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> \<not> has_reply_cap t s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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\<rbrace>
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) and K (is_simple_type (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))))) s \<and> ?P'122 epptr ep queue s proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue. \<lbrace>?P'122 epptr ep queue\<rbrace> set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)) \<lbrace>\<lambda>r s. pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> t \<noteq> idle_thread s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> (valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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\<rbrace>
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) and K (is_simple_type (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))))) s \<and> ?P'122 epptr ep queue s proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue. \<lbrace>?P'122 epptr ep queue\<rbrace> set_endpoint epptr (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)) \<lbrace>\<lambda>r s. pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> valid_idle s \<and> t \<noteq> idle_thread s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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\<rbrace>
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) and K (is_simple_type (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))))) s \<and> ?P'122 epptr ep queue s proof (prove)
goal (1 subgoal):
 1. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) and K (is_simple_type (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))))) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (if_live_then_nonz_cap s \<and> (live (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) \<longrightarrow> ex_nonz_cap_to epptr s)) \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of s)(epptr := ep_q_refs_of (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)))) t. snd r = TCBBound} else ((state_refs_of s)(epptr := ep_q_refs_of (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)))) a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> (obj_at (\<lambda>ko. partial_inv Endpoint ko \<noteq> None) epptr and valid_idle) s \<and> t \<noteq> idle_thread s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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 proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>(ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s; ep \<noteq> IdleEP\<rbrakk> \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) and K (is_simple_type (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))))) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> (if_live_then_nonz_cap s \<and> (live (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) \<longrightarrow> ex_nonz_cap_to epptr s)) \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of s)(epptr := ep_q_refs_of (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)))) t. snd r = TCBBound} else ((state_refs_of s)(epptr := ep_q_refs_of (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue)))) a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> (obj_at (\<lambda>ko. partial_inv Endpoint ko \<noteq> None) epptr and valid_idle) s \<and> t \<noteq> idle_thread s \<and> only_idle s \<and> if_unsafe_then_cap s \<and> valid_reply_caps s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s \<and> valid_reply_masters s \<and> valid_global_refs s \<and> valid_arch_state s \<and> valid_irq_node s \<and> valid_irq_handlers s \<and> valid_irq_states s \<and> valid_ioports s \<and> valid_machine_state 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_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
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; ko_at (Endpoint ep) epptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> distinct (remove1 epptr queue) \<and> (\<forall>t\<in>set (remove1 epptr queue). tcb_at t s) \<and> (live (Endpoint (case remove1 epptr queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> distinct (remove1 t queue) \<and> (\<forall>t\<in>set (remove1 t queue). tcb_at t s) \<and> (live (Endpoint (case remove1 t queue of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> update_ep_queue ep (remove1 t queue))) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; ko_at (Endpoint ep) epptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> distinct (remove1 epptr queue) \<and> (\<forall>t\<in>set (remove1 epptr queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> distinct (remove1 t queue) \<and> (\<forall>t\<in>set (remove1 t queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; ko_at (Endpoint ep) epptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = refs_of (Endpoint ep)\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> distinct (remove1 epptr queue) \<and> (\<forall>t\<in>set (remove1 epptr queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> distinct (remove1 t queue) \<and> (\<forall>t\<in>set (remove1 t queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_ep ep s\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> distinct (remove1 epptr queue) \<and> (\<forall>t\<in>set (remove1 epptr queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> distinct (remove1 t queue) \<and> (\<forall>t\<in>set (remove1 t queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_ep ep s; \<exists>ts ntfnptr. st = ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> distinct (remove1 epptr queue) \<and> (\<forall>t\<in>set (remove1 epptr queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> distinct (remove1 t queue) \<and> (\<forall>t\<in>set (remove1 t queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (3 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_ep ep s; \<exists>ts ntfnptr. st = ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr; epptr \<notin> set (remove1 t queue)\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> distinct (remove1 epptr queue) \<and> (\<forall>t\<in>set (remove1 epptr queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> distinct (remove1 t queue) \<and> (\<forall>t\<in>set (remove1 t queue). tcb_at t s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_ep ep s; \<exists>ts ntfnptr. st = ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> epptr \<notin> set (remove1 t queue)
 3. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (4 subgoals):
 1. \<And>epptr ep queue s x2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); x2 = queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = set queue \<times> {EPSend}; kheap s epptr = Some (Endpoint (SendEP queue)); queue \<noteq> [] \<and> (\<forall>t\<in>set queue. tcb_at t s) \<and> distinct queue; \<exists>ntfnptr. obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; epptr \<in> set queue \<longrightarrow> epptr = t; ep = SendEP queue\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 2. \<And>epptr ep queue s x3. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); x3 = queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = set queue \<times> {EPRecv}; kheap s epptr = Some (Endpoint (RecvEP queue)); queue \<noteq> [] \<and> (\<forall>t\<in>set queue. tcb_at t s) \<and> distinct queue; \<exists>ntfnptr. obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; epptr \<in> set queue \<longrightarrow> epptr = t; ep = RecvEP queue\<rbrakk> \<Longrightarrow> (t = epptr \<longrightarrow> sym_refs (\<lambda>a. if a = epptr then {r \<in> set (remove1 epptr queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv}. snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> epptr \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) epptr s) \<and> (t \<noteq> epptr \<longrightarrow> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = epptr then set (remove1 t queue) \<times> {case ep of SendEP xs \<Rightarrow> EPSend | RecvEP xs \<Rightarrow> EPRecv} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s)
 3. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_ep ep s; \<exists>ts ntfnptr. st = ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> epptr \<notin> set (remove1 t queue)
 4. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (2 subgoals):
 1. \<And>epptr ep queue s. \<lbrakk>ep \<noteq> IdleEP; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); ep = SendEP queue \<or> ep = RecvEP queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = ep_q_refs_of ep; kheap s epptr = Some (Endpoint ep); valid_ep ep s; \<exists>ts ntfnptr. st = ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> epptr \<notin> set (remove1 t queue)
 2. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (3 subgoals):
 1. \<And>epptr ep queue s x2. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); x2 = queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = set queue \<times> {EPSend}; kheap s epptr = Some (Endpoint (SendEP queue)); queue \<noteq> [] \<and> (\<forall>t\<in>set queue. tcb_at t s) \<and> distinct queue; \<exists>ntfnptr. obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; ep = SendEP queue\<rbrakk> \<Longrightarrow> epptr \<in> set queue \<longrightarrow> epptr = t
 2. \<And>epptr ep queue s x3. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc 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_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state 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_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; st_tcb_at ((=) st) t s; (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d); x3 = queue; ex_nonz_cap_to epptr s; state_refs_of s epptr = set queue \<times> {EPRecv}; kheap s epptr = Some (Endpoint (RecvEP queue)); queue \<noteq> [] \<and> (\<forall>t\<in>set queue. tcb_at t s) \<and> distinct queue; \<exists>ntfnptr. obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; ep = RecvEP queue\<rbrakk> \<Longrightarrow> epptr \<in> set queue \<longrightarrow> epptr = t
 3. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal (1 subgoal):
 1. \<And>epptr ep queue s. (ko_at (Endpoint ep) epptr and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc 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_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state 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_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 and st_tcb_at ((=) st) t and (\<lambda>y. (\<exists>d. st = BlockedOnReceive epptr d) \<or> (\<exists>d. st = BlockedOnSend epptr d))) and (\<lambda>y. ep = SendEP queue \<or> ep = RecvEP queue)) s \<Longrightarrow> ep \<noteq> IdleEP proof (prove)
goal:
No subgoals!