theory Tcb_AI

lemma bind_notification_invs:
  shows
  "\<lbrace>bound_tcb_at ((=) None) tcbptr
    and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None)
                           \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr
    and invs
    and ex_nonz_cap_to ntfnptr
    and ex_nonz_cap_to tcbptr\<rbrace>
     bind_notification tcbptr ntfnptr
   \<lbrace>\<lambda>_. invs\<rbrace>" apply (simp add: bind_notification_def invs_def valid_state_def valid_pspace_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (wp valid_irq_node_typ set_simple_ko_valid_objs simple_obj_set_prop_at valid_ioports_lift
         | clarsimp simp:idle_no_ex_cap split del: if_split)+ apply (intro conjI;
    (clarsimp simp: is_ntfn idle_no_ex_cap elim!: obj_at_weakenE)?) apply (erule (1) obj_at_valid_objsE) apply (clarsimp simp: valid_obj_def valid_ntfn_def pred_tcb_at_tcb_at
                  elim!: obj_atE
                  split: ntfn.splits) apply (rule conjI) apply (clarsimp simp: obj_at_def pred_tcb_at_def2) apply (rule impI, erule delta_sym_refs) apply (fastforce dest!: symreftype_inverse'
                     simp: ntfn_q_refs_of_def obj_at_def
                    split: ntfn.splits if_split_asm) apply (fastforce simp: state_refs_of_def pred_tcb_at_def2 obj_at_def
                         tcb_st_refs_of_def
                  split: thread_state.splits if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at ((=) None) tcbptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr and invs and ex_nonz_cap_to ntfnptr and ex_nonz_cap_to tcbptr\<rbrace> bind_notification tcbptr ntfnptr \<lbrace>\<lambda>_. invs\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>bound_tcb_at ((=) None) tcbptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr 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 ex_nonz_cap_to ntfnptr and ex_nonz_cap_to tcbptr\<rbrace> do ntfn <- get_notification ntfnptr;
y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn (Some tcbptr));
set_bound_notification tcbptr (Some ntfnptr)
od \<lbrace>\<lambda>_. 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>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (bound_tcb_at ((=) None) tcbptr and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr 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 ex_nonz_cap_to ntfnptr and ex_nonz_cap_to tcbptr)\<rbrace> do y <- set_notification ntfnptr (ntfn_set_bound_tcb ntfn (Some tcbptr));
set_bound_notification tcbptr (Some ntfnptr)
od \<lbrace>\<lambda>_. 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>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn (Some tcbptr)) s \<and> is_ntfn (Notification (ntfn_set_bound_tcb ntfn (Some tcbptr))) \<and> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> if tcbptr = ntfnptr then insert (ntfnptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfnptr s \<and> tcbptr \<noteq> idle_thread s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn (Some tcbptr)) s
 2. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of s a)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s a)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s ko. \<lbrakk>bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s; kheap s ntfnptr = Some ko; Notification ntfn = ko; valid_obj ntfnptr ko s\<rbrakk> \<Longrightarrow> valid_ntfn (ntfn_set_bound_tcb ntfn (Some tcbptr)) s
 2. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of s a)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s a)) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> (tcbptr = ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of s a)) \<and> (tcbptr \<noteq> ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s a)) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> tcbptr = ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = ntfnptr then insert (ntfnptr, TCBBound) {r. (r = (ntfnptr, NTFNBound) \<or> r \<in> ntfn_q_refs_of (ntfn_obj ntfn)) \<and> snd r \<noteq> TCBBound} else state_refs_of s a)
 2. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s a) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) 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; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s\<rbrakk> \<Longrightarrow> tcbptr \<noteq> ntfnptr \<longrightarrow> sym_refs (\<lambda>a. if a = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if a = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s a) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> (if x = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if x = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s x); (y, tp) \<notin> state_refs_of s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if y = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s y)
 2. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if x = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if y = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s y) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s x y tp. \<lbrakk>ko_at (Notification ntfn) ntfnptr s; bound_tcb_at ((=) None) tcbptr s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> ntfn_bound_tcb ntfn = None \<and> (\<forall>q. ntfn_obj ntfn \<noteq> WaitingNtfn q)) ntfnptr s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_hyp_refs_of s); valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_ioports s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; ex_nonz_cap_to ntfnptr s; ex_nonz_cap_to tcbptr s; tcbptr \<noteq> ntfnptr; (y, tp) \<in> state_refs_of s x; (y, tp) \<notin> (if x = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if x = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = tcbptr then insert (ntfnptr, TCBBound) {r \<in> state_refs_of s tcbptr. snd r \<noteq> TCBBound} else if y = ntfnptr then insert (tcbptr, NTFNBound) (ntfn_q_refs_of (ntfn_obj ntfn)) else state_refs_of s y) proof (prove)
goal:
No subgoals!