theory TcbAcc_AI

lemma sts_invs_minor:
  "\<lbrace>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t
     and (\<lambda>s. \<not> halted st \<longrightarrow> ex_nonz_cap_to t s)
     and (\<lambda>s. \<forall>a data. st = Structures_A.BlockedOnReceive a data \<longrightarrow>
                    cte_wp_at ((=) cap.NullCap) (t, tcb_cnode_index 3) s)
     and (\<lambda>s. t \<noteq> idle_thread s)
     and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or>
                    cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t)
                              (t, tcb_cnode_index 2) s)
     and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st)
     and (\<lambda>s. \<not> awaiting_reply st \<longrightarrow> \<not> has_reply_cap t s)
     and K (\<not>idle st)
     and invs\<rbrace>
     set_thread_state t st
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre) apply (wp valid_irq_node_typ sts_only_idle | simp)+ apply clarsimp apply (rule conjI) apply (simp add: pred_tcb_at_def, erule(1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def
                  split: Structures_A.thread_state.splits) apply (clarsimp elim!: rsubst[where P=sym_refs]
                 intro!: ext
                  dest!: st_tcb_at_state_refs_ofD) apply (cases st) apply simp_all by (fastforce simp: tcb_ntfn_is_bound_def tcb_bound_refs_def
                   elim: obj_at_valid_objsE
                  split: option.splits)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t and (\<lambda>s. \<not> halted st \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. \<forall>a data. st = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) and (\<lambda>s. t \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st) and (\<lambda>s. st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) and K (st \<noteq> IdleThreadState) and invs\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t and (\<lambda>s. \<not> halted st \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) and (\<lambda>s. t \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st) and (\<lambda>s. st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) and (\<lambda>y. st \<noteq> IdleThreadState) 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> set_thread_state t st \<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. \<lbrace>?Q5\<rbrace> set_thread_state t st \<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>s. (st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t and (\<lambda>s. \<not> halted st \<longrightarrow> ex_nonz_cap_to t s) and (\<lambda>s. (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) and (\<lambda>s. t \<noteq> idle_thread s) and (\<lambda>s. st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) and (\<lambda>s. \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st) and (\<lambda>s. st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) and (\<lambda>y. st \<noteq> IdleThreadState) 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 \<Longrightarrow> ?Q5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t s \<and> (\<not> halted st \<longrightarrow> ex_nonz_cap_to t s) \<and> ((\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) \<and> t \<noteq> idle_thread s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st) \<and> (st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s) \<and> st \<noteq> IdleThreadState \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> if_live_then_nonz_cap s \<and> zombies_final s \<and> sym_refs (state_refs_of s) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc 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 \<Longrightarrow> valid_tcb_state st s \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t s; \<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; 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\<rbrakk> \<Longrightarrow> valid_tcb_state st s \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t s; \<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; 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\<rbrakk> \<Longrightarrow> valid_tcb_state st s
 2. \<And>s. \<lbrakk>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t s; \<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>s ko. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> \<not> halted (tcb_state tcb)) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; 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; kheap s t = Some ko; \<exists>tcb. ko = TCB tcb \<and> tcb_st_refs_of (tcb_state tcb) = tcb_st_refs_of st; valid_obj t ko s\<rbrakk> \<Longrightarrow> valid_tcb_state st s
 2. \<And>s. \<lbrakk>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t s; \<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>st_tcb_at (\<lambda>st'. tcb_st_refs_of st' = tcb_st_refs_of st) t s; \<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; 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\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of st \<union> {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>s ts ntfnptr. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound} proof (prove)
goal (8 subgoals):
 1. \<And>s ts ntfnptr. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; st = Running\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 2. \<And>s ts ntfnptr. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; inactive st\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 3. \<And>s ts ntfnptr. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; st = Restart\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 4. \<And>s ts ntfnptr x41 x42. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; st = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 5. \<And>s ts ntfnptr x51 x52. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; st = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 6. \<And>s ts ntfnptr. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; awaiting_reply st\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 7. \<And>s ts ntfnptr x7. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; st = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 8. \<And>s ts ntfnptr. \<lbrakk>\<not> halted st \<longrightarrow> ex_nonz_cap_to t s; (\<exists>a data. st = BlockedOnReceive a data) \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted st \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<forall>typ. (idle_thread s, typ) \<notin> tcb_st_refs_of st; st \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t s; st \<noteq> IdleThreadState; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = tcb_st_refs_of st; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr; idle st\<rbrakk> \<Longrightarrow> tcb_st_refs_of st \<union> tcb_bound_refs ntfnptr = tcb_st_refs_of st \<union> {r. (r \<in> tcb_st_refs_of st \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound} proof (prove)
goal (7 subgoals):
 1. \<And>s ts ntfnptr. \<lbrakk>ex_nonz_cap_to t s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<not> has_reply_cap t s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_bound_refs ntfnptr; st = Running\<rbrakk> \<Longrightarrow> tcb_bound_refs ntfnptr = {r \<in> tcb_bound_refs ntfnptr. snd r = TCBBound}
 2. \<And>s ts ntfnptr. \<lbrakk>t \<noteq> idle_thread s; \<not> has_reply_cap t s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_bound_refs ntfnptr; inactive st\<rbrakk> \<Longrightarrow> tcb_bound_refs ntfnptr = {r \<in> tcb_bound_refs ntfnptr. snd r = TCBBound}
 3. \<And>s ts ntfnptr. \<lbrakk>ex_nonz_cap_to t s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; \<not> has_reply_cap t s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_bound_refs ntfnptr; st = Restart\<rbrakk> \<Longrightarrow> tcb_bound_refs ntfnptr = {r \<in> tcb_bound_refs ntfnptr. snd r = TCBBound}
 4. \<And>s ts ntfnptr x41 x42. \<lbrakk>ex_nonz_cap_to t s; cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; idle_thread s \<noteq> x41; \<not> has_reply_cap t s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {(x41, TCBBlockedRecv)}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (x41, TCBBlockedRecv) (tcb_bound_refs ntfnptr); st = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> insert (x41, TCBBlockedRecv) (tcb_bound_refs ntfnptr) = insert (x41, TCBBlockedRecv) {r. (r = (x41, TCBBlockedRecv) \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 5. \<And>s ts ntfnptr x51 x52. \<lbrakk>ex_nonz_cap_to t s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; idle_thread s \<noteq> x51; \<not> has_reply_cap t s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {(x51, TCBBlockedSend)}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (x51, TCBBlockedSend) (tcb_bound_refs ntfnptr); st = BlockedOnSend x51 x52\<rbrakk> \<Longrightarrow> insert (x51, TCBBlockedSend) (tcb_bound_refs ntfnptr) = insert (x51, TCBBlockedSend) {r. (r = (x51, TCBBlockedSend) \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}
 6. \<And>s ts ntfnptr. \<lbrakk>ex_nonz_cap_to t s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = tcb_bound_refs ntfnptr; awaiting_reply st\<rbrakk> \<Longrightarrow> tcb_bound_refs ntfnptr = {r \<in> tcb_bound_refs ntfnptr. snd r = TCBBound}
 7. \<And>s ts ntfnptr x7. \<lbrakk>ex_nonz_cap_to t s; t \<noteq> idle_thread s; st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s; idle_thread s \<noteq> x7; \<not> has_reply_cap t s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final 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; tcb_st_refs_of ts = {(x7, TCBSignal)}; obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (x7, TCBSignal) (tcb_bound_refs ntfnptr); st = BlockedOnNotification x7\<rbrakk> \<Longrightarrow> insert (x7, TCBSignal) (tcb_bound_refs ntfnptr) = insert (x7, TCBSignal) {r. (r = (x7, TCBSignal) \<or> r \<in> tcb_bound_refs ntfnptr) \<and> snd r = TCBBound}