theory Ipc_AI

lemma update_waiting_invs:
  notes if_split[split del]
  shows
  "\<lbrace>ko_at (Notification ntfn) ntfnptr and invs
     and K (ntfn_obj ntfn = ntfn.WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)\<rbrace>
     update_waiting_ntfn ntfnptr q bound_tcb bdg
   \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: update_waiting_ntfn_def) apply (rule hoare_seq_ext[OF _ assert_sp]) apply (rule hoare_pre) apply (wp |simp)+ apply (simp add: invs_def valid_state_def valid_pspace_def) apply (wp valid_irq_node_typ sts_only_idle) apply (simp add: valid_tcb_state_def conj_comms) apply (simp add: cte_wp_at_caps_of_state) apply (wp set_simple_ko_valid_objs hoare_post_imp [OF disjI1]
            valid_irq_node_typ valid_ioports_lift | assumption | simp |
            strengthen reply_cap_doesnt_exist_strg)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def
                        ep_redux_simps neq_Nil_conv
                  cong: list.case_cong if_cong) apply (frule(1) sym_refs_obj_atD, clarsimp simp: st_tcb_at_refs_of_rev) apply (frule (1) if_live_then_nonz_capD) apply (clarsimp simp: live_def) apply (frule(1) st_tcb_ex_cap) apply simp apply (simp add: st_tcb_at_tcb_at) apply (frule ko_at_state_refs_ofD) apply (frule st_tcb_at_state_refs_ofD) apply (erule(1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_ntfn_def obj_at_def is_ntfn_def) apply (rule conjI, clarsimp simp: obj_at_def split: option.splits list.splits) apply (rule conjI, clarsimp elim!: pred_tcb_weakenE) apply (rule conjI, clarsimp dest!: idle_no_ex_cap) apply (rule conjI, erule delta_sym_refs) apply (clarsimp dest!: refs_in_ntfn_bound_refs
                    split: if_split_asm if_split) apply (simp only: tcb_bound_refs_eq_restr, simp) apply (fastforce dest!: refs_in_ntfn_bound_refs symreftype_inverse'
                    simp: valid_obj_def valid_ntfn_def obj_at_def is_tcb
                   split: if_split_asm) apply (clarsimp elim!: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at (Notification ntfn) ntfnptr and invs and K (ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)\<rbrace> update_waiting_ntfn ntfnptr q bound_tcb bdg \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)\<rbrace> do y <- assert (q \<noteq> []);
y <- set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr>;
y <- set_thread_state (hd q) Running;
y <- as_user (hd q) (setRegister badge_register bdg);
do_extended_op (possible_switch_to (hd q))
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>y. \<lbrace>\<lambda>s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> []\<rbrace> do y <- set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr>;
y <- set_thread_state (hd q) Running;
y <- as_user (hd q) (setRegister badge_register bdg);
do_extended_op (possible_switch_to (hd q))
od \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?Q4 y\<rbrace> do y <- set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr>;
y <- set_thread_state (hd q) Running;
y <- as_user (hd q) (setRegister badge_register bdg);
do_extended_op (possible_switch_to (hd q))
od \<lbrace>\<lambda>rv. invs\<rbrace>
 2. \<And>y s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> [] \<Longrightarrow> ?Q4 y s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B8 () ()\<rbrace> set_thread_state (hd q) Running \<lbrace>\<lambda>yb. invs\<rbrace>
 2. \<And>y. \<lbrace>?Q4 y\<rbrace> set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>?B8 y\<rbrace>
 3. \<And>y s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> [] \<Longrightarrow> ?Q4 y s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?B8 () ()\<rbrace> set_thread_state (hd q) Running \<lbrace>\<lambda>yb. 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>y. \<lbrace>?Q4 y\<rbrace> set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>?B8 y\<rbrace>
 3. \<And>y s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> [] \<Longrightarrow> ?Q4 y s proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?Q4 y\<rbrace> set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>a b. (valid_objs and valid_tcb_state Running and (\<lambda>s. (\<forall>a data. Running = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (hd q, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) (hd q) s \<or> halted Running \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = hd q) (hd q, tcb_cnode_index 2) s))) b \<and> pspace_aligned b \<and> pspace_distinct b \<and> ((\<not> halted Running \<longrightarrow> ex_nonz_cap_to (hd q) b) \<and> if_live_then_nonz_cap b) \<and> zombies_final b \<and> sym_refs ((state_refs_of b)(hd q := tcb_st_refs_of Running \<union> {r \<in> state_refs_of b (hd q). snd r = TCBBound})) \<and> sym_refs (state_hyp_refs_of b) \<and> valid_mdb b \<and> valid_ioc b \<and> (valid_idle and (\<lambda>s. hd q = idle_thread s \<longrightarrow> idle Running)) b \<and> (only_idle and (\<lambda>s. idle Running \<longrightarrow> hd q = idle_thread s)) b \<and> if_unsafe_then_cap b \<and> (valid_reply_caps b \<and> (Running \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap (hd q) b)) \<and> valid_reply_masters b \<and> valid_global_refs b \<and> valid_arch_state b \<and> valid_irq_node b \<and> valid_irq_handlers b \<and> valid_irq_states b \<and> valid_ioports b \<and> valid_machine_state 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_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\<rbrace>
 2. \<And>y s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> [] \<Longrightarrow> ?Q4 y s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4 ()\<rbrace> set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>a b. equal_kernel_mappings b \<and> pspace_in_kernel_window b \<and> valid_arch_caps b \<and> valid_arch_state b \<and> valid_asid_map b \<and> valid_global_objs b \<and> valid_global_vspace_mappings b \<and> valid_ioports b \<and> valid_kernel_mappings b \<and> valid_vspace_objs b \<and> pspace_aligned b \<and> pspace_distinct b \<and> cap_refs_in_kernel_window b \<and> cap_refs_respects_device_region b \<and> cur_tcb b \<and> if_live_then_nonz_cap b \<and> if_unsafe_then_cap b \<and> only_idle b \<and> pspace_respects_device_region b \<and> valid_global_refs b \<and> valid_idle b \<and> valid_ioc b \<and> valid_irq_handlers b \<and> valid_irq_node b \<and> valid_irq_states b \<and> valid_machine_state b \<and> valid_mdb b \<and> valid_objs b \<and> valid_reply_caps b \<and> valid_reply_masters b \<and> zombies_final b \<and> sym_refs (state_hyp_refs_of b) \<and> ex_nonz_cap_to (hd q) b \<and> \<not> has_reply_cap (hd q) b \<and> hd q \<noteq> idle_thread b \<and> sym_refs (\<lambda>a. if a = hd q then {r. snd r = TCBBound \<and> r \<in> state_refs_of b (hd q)} else state_refs_of b a) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) (hd q) b \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = hd q) (hd q, tcb_cnode_index 2) b)\<rbrace>
 2. \<And>y s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> [] \<Longrightarrow> ?Q4 y s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q4 ()\<rbrace> set_notification ntfnptr \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr> \<lbrace>\<lambda>a b. equal_kernel_mappings b \<and> pspace_in_kernel_window b \<and> valid_arch_caps b \<and> valid_arch_state b \<and> valid_asid_map b \<and> valid_global_objs b \<and> valid_global_vspace_mappings b \<and> valid_ioports b \<and> valid_kernel_mappings b \<and> valid_vspace_objs b \<and> pspace_aligned b \<and> pspace_distinct b \<and> cap_refs_in_kernel_window b \<and> cap_refs_respects_device_region b \<and> cur_tcb b \<and> if_live_then_nonz_cap b \<and> if_unsafe_then_cap b \<and> only_idle b \<and> pspace_respects_device_region b \<and> valid_global_refs b \<and> valid_idle b \<and> valid_ioc b \<and> valid_irq_handlers b \<and> valid_irq_node b \<and> valid_irq_states b \<and> valid_machine_state b \<and> valid_mdb b \<and> valid_objs b \<and> valid_reply_caps b \<and> valid_reply_masters b \<and> zombies_final b \<and> sym_refs (state_hyp_refs_of b) \<and> ex_nonz_cap_to (hd q) b \<and> \<not> has_reply_cap (hd q) b \<and> hd q \<noteq> idle_thread b \<and> sym_refs (\<lambda>a. if a = hd q then {r. snd r = TCBBound \<and> r \<in> state_refs_of b (hd q)} else state_refs_of b a) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) (hd q) b \<or> (\<exists>cap. caps_of_state b (hd q, tcb_cnode_index 2) = Some cap \<and> is_master_reply_cap cap \<and> obj_ref_of cap = hd q))\<rbrace>
 2. \<And>y s. (ko_at (Notification ntfn) ntfnptr and invs and (\<lambda>y. ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb)) s \<and> q \<noteq> [] \<Longrightarrow> ?Q4 y s proof (prove)
goal (1 subgoal):
 1. \<And>s. ko_at (Notification ntfn) ntfnptr s \<and> invs s \<and> ntfn_obj ntfn = WaitingNtfn q \<and> ntfn_bound_tcb ntfn = bound_tcb \<and> q \<noteq> [] \<Longrightarrow> equal_kernel_mappings s \<and> pspace_in_kernel_window s \<and> valid_arch_caps s \<and> valid_arch_state s \<and> valid_asid_map s \<and> valid_global_objs s \<and> valid_global_vspace_mappings s \<and> valid_ioports s \<and> valid_kernel_mappings s \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> cap_refs_in_kernel_window s \<and> cap_refs_respects_device_region s \<and> cur_tcb s \<and> if_live_then_nonz_cap s \<and> (live (Notification \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> if_unsafe_then_cap s \<and> only_idle s \<and> pspace_respects_device_region s \<and> valid_global_refs s \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_idle s \<and> valid_ioc s \<and> valid_irq_handlers s \<and> valid_irq_node s \<and> valid_irq_states s \<and> valid_machine_state s \<and> valid_mdb s \<and> valid_objs s \<and> valid_ntfn \<lparr>ntfn_obj = case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q), ntfn_bound_tcb = bound_tcb\<rparr> s \<and> valid_reply_caps s \<and> valid_reply_masters s \<and> zombies_final s \<and> sym_refs (state_hyp_refs_of s) \<and> ex_nonz_cap_to (hd q) s \<and> valid_reply_caps s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) (hd q) s \<and> hd q \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = hd q then {r. snd r = TCBBound \<and> r \<in> (if hd q = ntfnptr then ntfn_q_refs_of (case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q)) \<union> ntfn_bound_refs bound_tcb else state_refs_of s (hd q))} else if a = ntfnptr then ntfn_q_refs_of (case tl q of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (tl q)) \<union> ntfn_bound_refs bound_tcb else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) (hd q) s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys\<rbrakk> \<Longrightarrow> (live (Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> ex_nonz_cap_to y s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s\<rbrakk> \<Longrightarrow> (live (Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> ex_nonz_cap_to y s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (2 subgoals):
 1. \<And>s y ys obj. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; Notification ntfn = obj; kheap s ntfnptr = Some obj\<rbrakk> \<Longrightarrow> live obj
 2. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s\<rbrakk> \<Longrightarrow> (live (Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> ex_nonz_cap_to y s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s\<rbrakk> \<Longrightarrow> (live (Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> ex_nonz_cap_to y s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (2 subgoals):
 1. \<And>s y ys st. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; st = BlockedOnNotification ntfnptr\<rbrakk> \<Longrightarrow> \<not> halted st
 2. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s\<rbrakk> \<Longrightarrow> (live (Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> ex_nonz_cap_to y s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s\<rbrakk> \<Longrightarrow> (live (Notification \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr>) \<longrightarrow> ex_nonz_cap_to ntfnptr s) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> ex_nonz_cap_to y s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = refs_of (Notification ntfn)\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys. \<lbrakk>ko_at (Notification ntfn) ntfnptr 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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = refs_of (Notification ntfn); \<exists>ts ntfnptra. ts = BlockedOnNotification ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptra) y s \<and> state_refs_of s y = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptra\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys ko. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfnptr, symreftype tp) \<in> refs_of ko) x s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = refs_of (Notification ntfn); \<exists>ts ntfnptra. ts = BlockedOnNotification ntfnptr \<and> obj_at (tcb_ntfn_is_bound ntfnptra) y s \<and> state_refs_of s y = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptra; kheap s ntfnptr = Some ko; Notification ntfn = ko; valid_obj ntfnptr ko s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> valid_ntfn \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> s \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s y)} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> (case case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list) of WaitingNtfn ts \<Rightarrow> ts \<noteq> [] \<and> (\<forall>t\<in>set ts. tcb_at t s) \<and> distinct ts \<and> (case ntfn_bound_tcb \<lparr>ntfn_obj = case ys of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list), ntfn_bound_tcb = ntfn_bound_tcb ntfn\<rparr> of None \<Rightarrow> True | Some tcb \<Rightarrow> ts = [tcb]) | _ \<Rightarrow> True) \<and> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. a \<noteq> BlockedOnReply) y s \<and> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> y \<noteq> idle_thread s \<and> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if a = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s a) \<and> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (3 subgoals):
 1. \<And>s y ys ntfnptra koa x ya tp. \<lbrakk>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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; (ya, tp) \<in> (if x = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if x = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s x); (ya, tp) \<notin> state_refs_of s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if ya = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if ya = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s ya)
 2. \<And>s y ys ntfnptra koa x ya tp. \<lbrakk>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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; (ya, tp) \<in> state_refs_of s x; (ya, tp) \<notin> (if x = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if x = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if ya = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if ya = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s ya)
 3. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (2 subgoals):
 1. \<And>s y ys ntfnptra koa x ya tp. \<lbrakk>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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; (ya, tp) \<in> state_refs_of s x; (ya, tp) \<notin> (if x = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if x = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if ya = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra))} else if ya = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s ya)
 2. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (2 subgoals):
 1. \<And>s y ys ntfnptra koa x ya tp. \<lbrakk>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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) {x \<in> tcb_bound_refs ntfnptra. snd x = TCBBound}; kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s; (ya, tp) \<in> state_refs_of s x; (ya, tp) \<notin> (if x = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) {x \<in> tcb_bound_refs ntfnptra. snd x = TCBBound})} else if x = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if ya = y then {r. snd r = TCBBound \<and> r \<in> (if y = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else insert (ntfnptr, TCBSignal) {x \<in> tcb_bound_refs ntfnptra. snd x = TCBBound})} else if ya = ntfnptr then set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn) else state_refs_of s ya)
 2. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal (1 subgoal):
 1. \<And>s y ys ntfnptra koa. \<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; ntfn_obj ntfn = WaitingNtfn (y # ys); bound_tcb = ntfn_bound_tcb ntfn; q = y # ys; st_tcb_at (\<lambda>ts. ts = BlockedOnNotification ntfnptr) y s; \<forall>x\<in>set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn). case x of (x, tp) \<Rightarrow> \<exists>ko. kheap s x = Some ko \<and> (ntfnptr, symreftype tp) \<in> refs_of ko; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to y s; state_refs_of s ntfnptr = insert (y, NTFNSignal) (set ys \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfn)); kheap s ntfnptr = Some (Notification ntfn); state_refs_of s y = insert (ntfnptr, TCBSignal) (tcb_bound_refs ntfnptra); kheap s y = Some koa; tcb_ntfn_is_bound ntfnptra koa; is_tcb koa; \<forall>t\<in>set ys. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; y \<notin> set ys; distinct ys; case ntfn_bound_tcb ntfn of None \<Rightarrow> True | Some tcb \<Rightarrow> y # ys = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfn) s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>a. \<not> halted a) y s proof (prove)
goal:
No subgoals!