theory IpcCancel_AI

lemma cancel_badged_sends_invs[wp]:
  "\<lbrace>invs\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: cancel_badged_sends_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac ep; simp) apply wpsimp apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wpsimp wp: valid_irq_node_typ valid_ioports_lift) apply (simp add: fun_upd_def[symmetric] ep_redux_simps ep_at_def2[symmetric, simplified]
                cong: list.case_cong) apply (rule hoare_strengthen_post,
            rule cancel_badged_sends_filterM_helper[where epptr=epptr]) apply (auto intro:obj_at_weakenE)[1] apply (wpsimp wp: valid_irq_node_typ set_endpoint_ep_at valid_ioports_lift) apply (clarsimp simp: valid_ep_def conj_comms) apply (subst obj_at_weakenE, simp, fastforce) apply (clarsimp simp: is_ep_def) apply (frule(1) sym_refs_ko_atD, clarsimp) apply (frule(1) if_live_then_nonz_capD, (clarsimp simp: live_def)+) apply (erule(1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_ep_def st_tcb_at_refs_of_rev) apply (simp add: fun_upd_idem obj_at_def is_ep_def | subst fun_upd_def[symmetric])+ apply (clarsimp, drule(1) bspec) apply (drule st_tcb_at_state_refs_ofD) apply (clarsimp simp only: cancel_badged_sends_invs_helper Un_iff, clarsimp) apply (simp add: set_eq_subset) apply wpsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> cancel_badged_sends epptr badge \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> do ep <- get_endpoint epptr;
case ep of SendEP queue \<Rightarrow> do set_endpoint epptr IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. \<lbrace>ko_at (Endpoint ep) epptr and invs\<rbrace> case ep of SendEP queue \<Rightarrow> do set_endpoint epptr IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- get_thread_state t;
if blocking_ipc_badge st = badge then do set_thread_state t Restart;
do_extended_op (tcb_sched_action tcb_sched_enqueue t);
return False
od else return True
od);
ep' <- return (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
set_endpoint epptr ep';
do_extended_op reschedule_required
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>ko_at (Endpoint IdleEP) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) epptr and invs\<rbrace> do y <- set_endpoint epptr IdleEP;
queue' <- 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 tcb_sched_enqueue t);
return False
od else return True
od) x2;
y <- set_endpoint epptr (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
do_extended_op reschedule_required
od \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) epptr and invs\<rbrace> do y <- set_endpoint epptr IdleEP;
queue' <- 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 tcb_sched_enqueue t);
return False
od else return True
od) x2;
y <- set_endpoint epptr (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
do_extended_op reschedule_required
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>ko_at (Endpoint (SendEP x2)) 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)\<rbrace> do y <- set_endpoint epptr IdleEP;
queue' <- 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 tcb_sched_enqueue t);
return False
od else return True
od) x2;
y <- set_endpoint epptr (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue');
do_extended_op reschedule_required
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>
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrace>?B51 (SendEP x2) x2 ()\<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 tcb_sched_enqueue t);
return False
od else return True
od) x2 \<lbrace>\<lambda>queue' s. valid_objs s \<and> valid_ep (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue') s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> (live (Endpoint (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue')) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = epptr then ep_q_refs_of (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP queue') else state_refs_of s a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr 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_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>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?Q18 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>?B51 ep x2\<rbrace>
 3. \<And>ep x2 s. \<lbrakk>ep = SendEP x2; (ko_at (Endpoint (SendEP x2)) 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)) s\<rbrakk> \<Longrightarrow> ?Q18 ep x2 s
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2. \<lbrace>?B51 (SendEP x2) x2 ()\<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 tcb_sched_enqueue t);
return False
od else return True
od) x2 \<lbrace>\<lambda>queue' s. valid_objs s \<and> distinct queue' \<and> (\<forall>t\<in>set queue'. tcb_at t s) \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> (live (Endpoint (case queue' of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (a # list))) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> zombies_final s \<and> sym_refs ((state_refs_of s)(epptr := set queue' \<times> {EPSend})) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> ep_at epptr 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_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>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?Q18 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>?B51 ep x2\<rbrace>
 3. \<And>ep x2 s. \<lbrakk>ep = SendEP x2; (ko_at (Endpoint (SendEP x2)) 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)) s\<rbrakk> \<Longrightarrow> ?Q18 ep x2 s
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x2 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 x2. tcb_at x s) \<and> ex_nonz_cap_to epptr s \<and> distinct rv \<and> distinct x2 \<and> set rv \<subseteq> set x2 \<and> sym_refs ((state_refs_of s)(epptr := set rv \<times> {EPSend})) \<Longrightarrow> valid_objs s \<and> distinct rv \<and> (\<forall>t\<in>set rv. tcb_at t s) \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> (live (Endpoint (case rv of [] \<Rightarrow> IdleEP | a # list \<Rightarrow> SendEP (a # list))) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> zombies_final s \<and> sym_refs ((state_refs_of s)(epptr := set rv \<times> {EPSend})) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> ep_at epptr 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_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>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?Q18 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a b. valid_objs b \<and> pspace_aligned b \<and> pspace_distinct b \<and> valid_ioc b \<and> if_live_then_nonz_cap b \<and> zombies_final b \<and> valid_mdb b \<and> valid_idle b \<and> only_idle b \<and> if_unsafe_then_cap b \<and> valid_reply_caps b \<and> valid_reply_masters b \<and> valid_global_refs b \<and> valid_arch_state b \<and> valid_machine_state b \<and> valid_irq_states b \<and> valid_irq_node b \<and> valid_irq_handlers b \<and> valid_vspace_objs b \<and> valid_arch_caps b \<and> valid_global_objs b \<and> valid_kernel_mappings b \<and> equal_kernel_mappings b \<and> valid_asid_map b \<and> valid_ioports b \<and> valid_global_vspace_mappings b \<and> pspace_in_kernel_window b \<and> cap_refs_in_kernel_window b \<and> pspace_respects_device_region b \<and> cap_refs_respects_device_region b \<and> cur_tcb b \<and> sym_refs (state_hyp_refs_of b) \<and> distinct x2 \<and> ep_at epptr b \<and> ex_nonz_cap_to epptr b \<and> sym_refs ((state_refs_of b)(epptr := set x2 \<times> {EPSend})) \<and> (\<forall>x\<in>set x2. {r \<in> state_refs_of b x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace>
 3. \<And>ep x2 s. \<lbrakk>ep = SendEP x2; (ko_at (Endpoint (SendEP x2)) 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)) s\<rbrakk> \<Longrightarrow> ?Q18 ep x2 s
 4. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep x2. ep = SendEP x2 \<Longrightarrow> \<lbrace>?Q18 ep x2\<rbrace> set_endpoint epptr IdleEP \<lbrace>\<lambda>a b. valid_objs b \<and> pspace_aligned b \<and> pspace_distinct b \<and> valid_ioc b \<and> if_live_then_nonz_cap b \<and> zombies_final b \<and> valid_mdb b \<and> valid_idle b \<and> only_idle b \<and> if_unsafe_then_cap b \<and> valid_reply_caps b \<and> valid_reply_masters b \<and> valid_global_refs b \<and> valid_arch_state b \<and> valid_machine_state b \<and> valid_irq_states b \<and> valid_irq_node b \<and> valid_irq_handlers b \<and> valid_vspace_objs b \<and> valid_arch_caps b \<and> valid_global_objs b \<and> valid_kernel_mappings b \<and> equal_kernel_mappings b \<and> valid_asid_map b \<and> valid_ioports b \<and> valid_global_vspace_mappings b \<and> pspace_in_kernel_window b \<and> cap_refs_in_kernel_window b \<and> pspace_respects_device_region b \<and> cap_refs_respects_device_region b \<and> cur_tcb b \<and> sym_refs (state_hyp_refs_of b) \<and> distinct x2 \<and> ep_at epptr b \<and> ex_nonz_cap_to epptr b \<and> sym_refs ((state_refs_of b)(epptr := set x2 \<times> {EPSend})) \<and> (\<forall>x\<in>set x2. {r \<in> state_refs_of b x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})\<rbrace>
 2. \<And>ep x2 s. \<lbrakk>ep = SendEP x2; (ko_at (Endpoint (SendEP x2)) 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)) s\<rbrakk> \<Longrightarrow> ?Q18 ep x2 s
 3. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ep x2 s. \<lbrakk>ep = SendEP x2; (ko_at (Endpoint (SendEP x2)) 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)) s\<rbrakk> \<Longrightarrow> (valid_objs and valid_simple_obj (Endpoint IdleEP) and K (is_simple_type (Endpoint IdleEP))) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_ioc s \<and> (if_live_then_nonz_cap s \<and> (live (Endpoint IdleEP) \<longrightarrow> ex_nonz_cap_to epptr s)) \<and> zombies_final s \<and> valid_mdb s \<and> (obj_at (\<lambda>ko. partial_inv Endpoint ko \<noteq> None) epptr 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 x2 \<and> ep_at epptr s \<and> ex_nonz_cap_to epptr s \<and> sym_refs ((state_refs_of s)(epptr := ep_q_refs_of IdleEP, epptr := set x2 \<times> {EPSend})) \<and> (\<forall>x\<in>set x2. {r \<in> ((state_refs_of s)(epptr := ep_q_refs_of IdleEP)) x. snd r \<noteq> TCBBound} = {(epptr, TCBBlockedSend)})
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x2)) epptr s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ex_nonz_cap_to epptr s \<and> ep_at epptr s \<and> (live (Endpoint IdleEP) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Endpoint y = ko) epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x2)) epptr s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ex_nonz_cap_to epptr s \<and> ep_at epptr s \<and> (live (Endpoint IdleEP) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> True \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x2)) epptr s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ex_nonz_cap_to epptr s \<and> ep_at epptr s \<and> (live (Endpoint IdleEP) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x2)) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ex_nonz_cap_to epptr s \<and> ep_at epptr s \<and> (live (Endpoint IdleEP) \<longrightarrow> ex_nonz_cap_to epptr s) \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); ko_at (Endpoint (SendEP x2)) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s; ex_nonz_cap_to epptr s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ep_at epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ko. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. obj_at (\<lambda>ko. (epptr, TCBBlockedSend) \<in> refs_of ko) x s; ex_nonz_cap_to epptr s; kheap s epptr = Some ko; Endpoint (SendEP x2) = ko; valid_obj epptr ko s\<rbrakk> \<Longrightarrow> distinct x2 \<and> ep_at epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend epptr pl) x s; ex_nonz_cap_to epptr s; kheap s epptr = Some (Endpoint (SendEP x2)); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2\<rbrakk> \<Longrightarrow> ep_at epptr s \<and> sym_refs (\<lambda>a. if a = epptr then set x2 \<times> {EPSend} else state_refs_of s a) \<and> (\<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)}))
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); state_refs_of s epptr = set x2 \<times> {EPSend}; \<forall>x\<in>set x2. st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend epptr pl) x s; ex_nonz_cap_to epptr s; kheap s epptr = Some (Endpoint (SendEP x2)); x2 \<noteq> []; \<forall>t\<in>set x2. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; distinct x2\<rbrakk> \<Longrightarrow> \<forall>x\<in>set x2. x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)})
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s x. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); state_refs_of s epptr = set x2 \<times> {EPSend}; ex_nonz_cap_to epptr s; kheap s epptr = Some (Endpoint (SendEP x2)); x2 \<noteq> []; \<forall>t\<in>set x2. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; distinct x2; x \<in> set x2; st_tcb_at (\<lambda>ts. \<exists>pl. ts = BlockedOnSend epptr pl) x s\<rbrakk> \<Longrightarrow> x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)})
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s x. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); state_refs_of s epptr = set x2 \<times> {EPSend}; ex_nonz_cap_to epptr s; kheap s epptr = Some (Endpoint (SendEP x2)); x2 \<noteq> []; \<forall>t\<in>set x2. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; distinct x2; x \<in> set x2; \<exists>ts ntfnptr. (\<exists>pl. ts = BlockedOnSend epptr pl) \<and> obj_at (tcb_ntfn_is_bound ntfnptr) x s \<and> state_refs_of s x = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> x \<noteq> epptr \<and> (x \<noteq> epptr \<longrightarrow> {r. snd r \<noteq> TCBBound \<and> r \<in> state_refs_of s x} = {(epptr, TCBBlockedSend)})
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ntfnptr. \<lbrakk>equal_kernel_mappings s; pspace_in_kernel_window s; valid_arch_caps s; valid_arch_state s; valid_asid_map s; valid_global_objs s; valid_global_vspace_mappings s; valid_ioports s; valid_kernel_mappings s; valid_vspace_objs s; pspace_aligned s; pspace_distinct s; cap_refs_in_kernel_window s; cap_refs_respects_device_region s; cur_tcb s; if_live_then_nonz_cap s; if_unsafe_then_cap s; only_idle s; pspace_respects_device_region s; valid_global_refs s; valid_idle s; valid_ioc s; valid_irq_handlers s; valid_irq_node s; valid_irq_states s; valid_machine_state s; valid_mdb s; valid_objs s; valid_reply_caps s; valid_reply_masters s; zombies_final s; sym_refs (state_hyp_refs_of s); sym_refs (state_refs_of s); insert (epptr, TCBBlockedSend) (tcb_bound_refs ntfnptr) = set x2 \<times> {EPSend}; ex_nonz_cap_to epptr s; kheap s epptr = Some (Endpoint (SendEP x2)); x2 \<noteq> []; \<forall>t\<in>set x2. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; distinct x2; epptr \<in> set x2; obj_at (tcb_ntfn_is_bound ntfnptr) epptr s; state_refs_of s epptr = set x2 \<times> {EPSend}\<rbrakk> \<Longrightarrow> False
 2. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. ep = RecvEP x3 \<Longrightarrow> \<lbrace>ko_at (Endpoint (RecvEP x3)) epptr and invs\<rbrace> return () \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal:
No subgoals!