theory IpcCancel_AI

lemma cancel_signal_invs:
  "\<lbrace>invs and st_tcb_at ((=) (Structures_A.BlockedOnNotification ntfn)) t\<rbrace>
  cancel_signal t ntfn
  \<lbrace>\<lambda>rv. invs\<rbrace>" apply (simp add: cancel_signal_def
                   invs_def valid_state_def valid_pspace_def) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac "ntfn_obj ntfna", simp_all)[1] apply (rule hoare_pre) apply (wp set_simple_ko_valid_objs valid_irq_node_typ sts_only_idle valid_ioports_lift
           | simp add: valid_tcb_state_def
           | strengthen reply_cap_doesnt_exist_strg
           | wpc)+ apply (clarsimp simp: ep_redux_simps cong: list.case_cong if_cong) apply (frule(1) if_live_then_nonz_capD, (clarsimp simp: live_def)+) apply (frule ko_at_state_refs_ofD) apply (frule st_tcb_at_state_refs_ofD) apply (erule(1) obj_at_valid_objsE, clarsimp simp: valid_obj_def valid_ntfn_def) apply (case_tac ntfna) apply clarsimp apply (rule conjI) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply clarsimp apply (rule conjI) apply (clarsimp split:option.split) apply (rule conjI, erule delta_sym_refs) apply (clarsimp split: if_split_asm)+ apply (fastforce dest: refs_in_tcb_bound_refs refs_in_ntfn_bound_refs symreftype_inverse') apply (fastforce simp: obj_at_def is_ntfn idle_not_queued
                   dest: idle_no_refs elim: pred_tcb_weakenE) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and st_tcb_at ((=) (BlockedOnNotification ntfn)) t\<rbrace> cancel_signal t ntfn \<lbrace>\<lambda>rv. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and st_tcb_at ((=) (BlockedOnNotification ntfn)) t\<rbrace> do ntfna <- get_notification ntfn;
queue <- case ntfn_obj ntfna of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna. \<lbrace>ko_at (Notification ntfna) ntfn and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and st_tcb_at ((=) (BlockedOnNotification ntfn)) t)\<rbrace> do queue <- case ntfn_obj ntfna of WaitingNtfn queue \<Rightarrow> return queue | _ \<Rightarrow> fail;
y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t queue of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t queue)));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>ko_at (Notification ntfna) ntfn and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and st_tcb_at ((=) (BlockedOnNotification ntfn)) t)\<rbrace> do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfna x2. ntfn_obj ntfna = WaitingNtfn x2 \<Longrightarrow> \<lbrace>?Q7 ntfna x2\<rbrace> do y <- set_notification ntfn (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)));
set_thread_state t Inactive
od \<lbrace>\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb\<rbrace>
 2. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; (ko_at (Notification ntfna) ntfn and (valid_objs and pspace_aligned and pspace_distinct and if_live_then_nonz_cap and zombies_final and (\<lambda>s. sym_refs (state_refs_of s)) and (\<lambda>s. sym_refs (state_hyp_refs_of s)) and valid_mdb and valid_ioc and valid_idle and only_idle and if_unsafe_then_cap and valid_reply_caps and valid_reply_masters and valid_global_refs and valid_arch_state and valid_irq_node and valid_irq_handlers and valid_irq_states and valid_ioports and valid_machine_state and valid_vspace_objs and valid_arch_caps and valid_global_objs and valid_kernel_mappings and equal_kernel_mappings and valid_asid_map and valid_global_vspace_mappings and pspace_in_kernel_window and cap_refs_in_kernel_window and pspace_respects_device_region and cap_refs_respects_device_region and cur_tcb and st_tcb_at ((=) (BlockedOnNotification ntfn)) t)) s\<rbrakk> \<Longrightarrow> ?Q7 ntfna x2 s proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; ko_at (Notification ntfna) ntfn s \<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 \<and> st_tcb_at ((=) (BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2))) s \<and> (live (Notification (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)))) \<longrightarrow> ex_nonz_cap_to ntfn s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> ((state_refs_of s)(ntfn := ntfn_q_refs_of (ntfn_obj (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)))) \<union> ntfn_bound_refs (ntfn_bound_tcb (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)))))) t. snd r = TCBBound} else ((state_refs_of s)(ntfn := ntfn_q_refs_of (ntfn_obj (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)))) \<union> ntfn_bound_refs (ntfn_bound_tcb (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (remove1 t x2)))))) a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> distinct (remove1 ntfn x2) \<and> (\<forall>t\<in>set (remove1 ntfn x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> (live (Notification (ntfn_set_obj ntfna (case remove1 ntfn x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list)))) \<longrightarrow> ex_nonz_cap_to ntfn s) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb ntfna)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> distinct (remove1 t x2) \<and> (\<forall>t\<in>set (remove1 t x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> (live (Notification (ntfn_set_obj ntfna (case remove1 t x2 of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn (a # list)))) \<longrightarrow> ex_nonz_cap_to ntfn s) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> distinct (remove1 ntfn x2) \<and> (\<forall>t\<in>set (remove1 ntfn x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb ntfna)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> distinct (remove1 t x2) \<and> (\<forall>t\<in>set (remove1 t x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = refs_of (Notification ntfna)\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> distinct (remove1 ntfn x2) \<and> (\<forall>t\<in>set (remove1 ntfn x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb ntfna)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> distinct (remove1 t x2) \<and> (\<forall>t\<in>set (remove1 t x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; ko_at (Notification ntfna) ntfn s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = refs_of (Notification ntfna); \<exists>ts ntfnptr. BlockedOnNotification ntfn = ts \<and> obj_at (tcb_ntfn_is_bound ntfnptr) t s \<and> state_refs_of s t = tcb_st_refs_of ts \<union> tcb_bound_refs ntfnptr\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> distinct (remove1 ntfn x2) \<and> (\<forall>t\<in>set (remove1 ntfn x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb ntfna)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> distinct (remove1 t x2) \<and> (\<forall>t\<in>set (remove1 t x2). tcb_at t s) \<and> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s ntfnptr. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna); kheap s ntfn = Some (Notification ntfna); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfna) s\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb ntfna)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (1 subgoal):
 1. \<And>ntfna x2 s ntfnptr ntfn_obja ntfn_bound_tcba. \<lbrakk>ntfn_obj ntfna = WaitingNtfn x2; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna); kheap s ntfn = Some (Notification ntfna); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb ntfna) s; ntfna = \<lparr>ntfn_obj = ntfn_obja, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb ntfna)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> (case ntfn_bound_tcb ntfna of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb ntfna) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (1 subgoal):
 1. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s\<rbrakk> \<Longrightarrow> (t = ntfn \<longrightarrow> (case ntfn_bound_tcba of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s) \<and> (t \<noteq> ntfn \<longrightarrow> (case ntfn_bound_tcba of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s) proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s\<rbrakk> \<Longrightarrow> t = ntfn \<longrightarrow> (case ntfn_bound_tcba of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = ntfn then {r. (r \<in> set (remove1 ntfn x2) \<times> {NTFNSignal} \<or> r \<in> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>)) \<and> snd r = TCBBound} else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> ntfn \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) ntfn s
 2. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s\<rbrakk> \<Longrightarrow> t \<noteq> ntfn \<longrightarrow> (case ntfn_bound_tcba of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (1 subgoal):
 1. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s\<rbrakk> \<Longrightarrow> t \<noteq> ntfn \<longrightarrow> (case ntfn_bound_tcba of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (1 subgoal):
 1. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> (case ntfn_bound_tcba of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])) \<and> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ntfnptr ntfn_bound_tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcb; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcb\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcb s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> case ntfn_bound_tcb of None \<Rightarrow> True | Some ta \<Rightarrow> tcb_at ta s \<and> (case remove1 t x2 of [] \<Rightarrow> True | a # list \<Rightarrow> remove1 t x2 = [ta])
 2. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (1 subgoal):
 1. \<And>x2 s ntfnptr ntfn_bound_tcba. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if a = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (3 subgoals):
 1. \<And>x2 s ntfnptr ntfn_bound_tcba x y 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; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s; t \<noteq> ntfn; (y, tp) \<in> (if x = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if x = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s x); (y, tp) \<notin> state_refs_of s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if y = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s y)
 2. \<And>x2 s ntfnptr ntfn_bound_tcba x y 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; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcba; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcba of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcba s; t \<noteq> ntfn; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if x = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = t then {r \<in> state_refs_of s t. snd r = TCBBound} else if y = ntfn then set (remove1 t x2) \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcba\<rparr>) else state_refs_of s y)
 3. \<And>x2 s ntfnptr ntfn_bound_tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcb; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcb\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcb s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (2 subgoals):
 1. \<And>x2 s ntfnptr ntfn_bound_tcb y 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; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcb; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcb\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcb s; t \<noteq> ntfn; y = ntfn \<and> tp = TCBSignal \<or> (y, tp) \<in> tcb_bound_refs ntfnptr; tp \<noteq> TCBBound\<rbrakk> \<Longrightarrow> (y = ntfn \<longrightarrow> (t, symreftype tp) \<notin> ntfn_bound_refs ntfn_bound_tcb) \<and> (y \<noteq> ntfn \<longrightarrow> (y = t \<longrightarrow> (t, symreftype tp) \<in> tcb_bound_refs ntfnptr \<longrightarrow> symreftype tp \<noteq> TCBBound) \<and> (y \<noteq> t \<longrightarrow> (t, symreftype tp) \<notin> state_refs_of s y))
 2. \<And>x2 s ntfnptr ntfn_bound_tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcb; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcb\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcb s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal (1 subgoal):
 1. \<And>x2 s ntfnptr ntfn_bound_tcb. \<lbrakk>valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; st_tcb_at ((=) (BlockedOnNotification ntfn)) t s; ex_nonz_cap_to ntfn s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs ntfn_bound_tcb; kheap s ntfn = Some (Notification \<lparr>ntfn_obj = WaitingNtfn x2, ntfn_bound_tcb = ntfn_bound_tcb\<rparr>); obj_at (tcb_ntfn_is_bound ntfnptr) t s; state_refs_of s t = insert (ntfn, TCBSignal) (tcb_bound_refs ntfnptr); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb ntfn_bound_tcb s; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> st_tcb_at (Not \<circ> awaiting_reply) t s proof (prove)
goal:
No subgoals!