theory Ipc_AI

lemma rai_invs':
  assumes set_notification_Q[wp]: "\<And>a b.\<lbrace> Q\<rbrace> set_notification a b \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes sts_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> set_thread_state a b \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes smi_Q[wp]: "\<And>a b.\<lbrace>Q\<rbrace> set_message_info a b \<lbrace>\<lambda>_.Q\<rbrace>"
  assumes as_user_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> as_user a b \<lbrace>\<lambda>r::unit. Q\<rbrace>"
  assumes set_mrs_Q[wp]: "\<And>a b c. \<lbrace>Q\<rbrace> set_mrs a b c \<lbrace>\<lambda>_.Q\<rbrace>"
  shows
  "\<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t
         and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s)
         and (\<lambda>s. \<exists>ntfnptr. is_ntfn_cap cap \<and> cap_ep_ptr cap = ntfnptr \<and>
                     obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None
                                                          \<or> ntfn_bound_tcb ntfn = Some t)) ntfnptr s)\<rbrace>
     receive_signal t cap is_blocking
   \<lbrace>\<lambda>r (s::'state_ext state). invs s \<and> Q s\<rbrace>" apply (simp add: receive_signal_def) apply (cases cap, simp_all) apply (rename_tac ntfn badge rights) apply (rule hoare_seq_ext [OF _ get_simple_ko_sp]) apply (case_tac "ntfn_obj x") apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre) apply (wp set_simple_ko_valid_objs valid_irq_node_typ sts_only_idle valid_ioports_lift
              sts_ntfn_at_inv[simplified ntfn_at_def2, simplified] | wpc
          | simp add: live_def valid_ntfn_def do_nbrecv_failed_transfer_def)+ apply (clarsimp simp: valid_tcb_state_def st_tcb_at_tcb_at) apply (rule conjI, clarsimp elim!: obj_at_weakenE simp: is_ntfn_def) apply (rule conjI, clarsimp simp: st_tcb_at_reply_cap_valid) apply (rule conjI, clarsimp simp: obj_at_def split: option.splits) apply (rule conjI, clarsimp simp: valid_bound_tcb_def obj_at_def
                                dest!: st_tcb_at_tcb_at
                                split: option.splits) apply (rule conjI) apply (subgoal_tac "t \<noteq> ntfn") apply (drule ko_at_state_refs_ofD) apply (drule active_st_tcb_at_state_refs_ofD) apply (erule delta_sym_refs) apply (clarsimp split: if_split_asm) apply (fastforce simp: pred_tcb_at_def2 tcb_bound_refs_def2 split: if_split_asm) apply (clarsimp simp: obj_at_def pred_tcb_at_def) apply (simp add: is_ntfn obj_at_def) apply (fastforce dest!: idle_no_ex_cap valid_reply_capsD
                    elim!: pred_tcb_weakenE
                    simp: st_tcb_at_reply_cap_valid st_tcb_def2) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre) apply (wpsimp wp: set_simple_ko_valid_objs hoare_vcg_const_Ball_lift sts_only_idle valid_ioports_lift
                      valid_irq_node_typ sts_ntfn_at_inv[simplified ntfn_at_def2, simplified]
               simp: live_def valid_ntfn_def do_nbrecv_failed_transfer_def) apply (clarsimp simp: valid_tcb_state_def st_tcb_at_tcb_at) apply (rule conjI, clarsimp elim!: obj_at_weakenE simp: is_ntfn_def) apply (rule obj_at_valid_objsE, assumption+) apply (clarsimp simp: valid_obj_def valid_ntfn_def) apply (frule(1) sym_refs_ko_atD, simp) apply (frule ko_at_state_refs_ofD) apply (frule active_st_tcb_at_state_refs_ofD) apply (rule conjI, clarsimp simp: st_tcb_at_reply_cap_valid) apply (rule context_conjI, fastforce simp: pred_tcb_at_def obj_at_def tcb_bound_refs_def2
                                               state_refs_of_def) apply (subgoal_tac "ntfn_bound_tcb x = None") apply (rule conjI, clarsimp split: option.splits) apply (rule conjI, erule delta_sym_refs) apply (fastforce simp: pred_tcb_at_def2 obj_at_def symreftype_inverse'
                      split: if_split_asm) apply (fastforce simp: pred_tcb_at_def2 tcb_bound_refs_def2 split: if_split_asm) apply (simp add: obj_at_def is_ntfn idle_not_queued) apply (fastforce dest: idle_no_ex_cap valid_reply_capsD
                    elim!: pred_tcb_weakenE
                     simp: st_tcb_at_reply_cap_valid st_tcb_def2) apply (clarsimp simp: valid_obj_def valid_ntfn_def obj_at_def
                   elim: obj_at_valid_objsE
                  split: option.splits) apply (simp add: invs_def valid_state_def valid_pspace_def) apply (rule hoare_pre) apply (wp set_simple_ko_valid_objs hoare_vcg_const_Ball_lift valid_ioports_lift
             as_user_no_del_ntfn[simplified ntfn_at_def2, simplified]
             valid_irq_node_typ ball_tcb_cap_casesI hoare_weak_lift_imp
             valid_bound_tcb_typ_at[rule_format]
             | simp add: valid_ntfn_def)+ apply clarsimp apply (rule conjI, clarsimp simp: valid_bound_tcb_def obj_at_def pred_tcb_at_def2 is_tcb
                             split: option.splits) apply (frule ko_at_state_refs_ofD) apply (frule active_st_tcb_at_state_refs_ofD) apply (rule conjI, erule delta_sym_refs) apply (clarsimp split: if_split_asm) apply (clarsimp split: if_split_asm) apply (fastforce simp: obj_at_def is_ntfn_def state_refs_of_def
                        valid_idle_def pred_tcb_at_def
                        st_tcb_at_reply_cap_valid
                  dest: valid_reply_capsD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) and (\<lambda>s. \<exists>ntfnptr. is_ntfn_cap cap \<and> cap_ep_ptr cap = ntfnptr \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfnptr s)\<rbrace> receive_signal t cap is_blocking \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) and (\<lambda>s. is_ntfn_cap cap \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) (cap_ep_ptr cap) s)\<rbrace> do ntfnptr <- case cap of NotificationCap ntfnptr badge rights \<Rightarrow> return ntfnptr | _ \<Rightarrow> fail;
ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfnptr);
set_notification ntfnptr $ ntfn_set_obj ntfn $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfnptr);
set_notification ntfnptr $ ntfn_set_obj ntfn $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn IdleNtfn
od
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. cap = NotificationCap x41 x42 x43 \<Longrightarrow> \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to x41 and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) x41\<rbrace> do ntfn <- get_notification x41;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification x41 $ ntfn_set_obj ntfn IdleNtfn
od
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights. cap = NotificationCap ntfn badge rights \<Longrightarrow> \<lbrace>invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn\<rbrace> do ntfna <- get_notification ntfn;
case ntfn_obj ntfna of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj ntfna $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj ntfna $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj ntfna IdleNtfn
od
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x. cap = NotificationCap ntfn badge rights \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>r s. 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> Q s\<rbrace>
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn badge rights x. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn\<rbrakk> \<Longrightarrow> \<lbrace>?Q15 ntfn badge rights x\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>r s. 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> Q s\<rbrace>
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; (ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)) s\<rbrakk> \<Longrightarrow> ?Q15 ntfn badge rights x s
 3. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 4. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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> Q s \<and> st_tcb_at active t s \<and> ex_nonz_cap_to t s \<and> ex_nonz_cap_to ntfn s \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s\<rbrakk> \<Longrightarrow> is_blocking \<longrightarrow> valid_tcb_state (BlockedOnNotification ntfn) s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> tcb_at t s \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> ntfn_at ntfn s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a)
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 3. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 4. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; t \<noteq> ntfn\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a)
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> ntfn
 3. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 4. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 5. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; t \<noteq> ntfn; state_refs_of s ntfn = refs_of (Notification x)\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a)
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> ntfn
 3. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 4. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 5. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; 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; Q s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; t \<noteq> ntfn; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s a)
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> ntfn
 3. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 4. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 5. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ntfn badge rights x s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; 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; Q s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; t \<noteq> ntfn; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; (y, tp) \<in> (if xa = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if xa = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if y = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s y)
 2. \<And>ntfn badge rights x s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; 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; Q s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; t \<noteq> ntfn; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if xa = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if y = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s y)
 3. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> ntfn
 4. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 5. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 6. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn badge rights x s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; 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; Q s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; t \<noteq> ntfn; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if xa = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfn then insert (t, NTFNSignal) (ntfn_bound_refs (ntfn_bound_tcb x)) else if y = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s y)
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> ntfn
 3. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 4. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 5. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> ntfn
 2. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 3. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 4. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = IdleNtfn; kheap s ntfn = Some (Notification x); 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; ntfn_bound_tcb x = None \<or> ntfn_bound_tcb x = Some t; is_blocking\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace>
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (x2 @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>r s. 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> Q s\<rbrace>
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x x2. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?Q3810 ntfn badge rights x x2\<rbrace> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (x2 @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t \<lbrace>\<lambda>r s. 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> Q s\<rbrace>
 2. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; (ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)) s\<rbrakk> \<Longrightarrow> ?Q3810 ntfn badge rights x x2 s
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; (ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)) s\<rbrakk> \<Longrightarrow> (is_blocking = True \<longrightarrow> (valid_objs and valid_tcb_state (BlockedOnNotification ntfn) and (\<lambda>s. (\<forall>a data. BlockedOnNotification ntfn = BlockedOnReceive a data \<longrightarrow> cte_wp_at ((=) NullCap) (t, tcb_cnode_index 3) s) \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> halted (BlockedOnNotification ntfn) \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s))) s \<and> tcb_at t s \<and> (\<forall>x\<in>set x2. tcb_at x s) \<and> distinct x2 \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> pspace_aligned s \<and> pspace_distinct s \<and> ((\<not> halted (BlockedOnNotification ntfn) \<longrightarrow> ex_nonz_cap_to t s) \<and> if_live_then_nonz_cap s) \<and> ex_nonz_cap_to ntfn s \<and> zombies_final s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else ((state_refs_of s)(t := tcb_st_refs_of (BlockedOnNotification ntfn) \<union> {r \<in> state_refs_of s t. snd r = TCBBound})) a) \<and> sym_refs (state_hyp_refs_of s) \<and> valid_mdb s \<and> valid_ioc s \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> (valid_idle and (\<lambda>s. t = idle_thread s \<longrightarrow> idle (BlockedOnNotification ntfn))) s \<and> (only_idle and (\<lambda>s. idle (BlockedOnNotification ntfn) \<longrightarrow> t = idle_thread s)) s \<and> if_unsafe_then_cap s \<and> (valid_reply_caps s \<and> (BlockedOnNotification ntfn \<noteq> BlockedOnReply \<longrightarrow> \<not> has_reply_cap t 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> Q s) \<and> (is_blocking = False \<longrightarrow> 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> Q s)
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> ntfn_at ntfn s \<and> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>x\<in>set x2. tcb_at x s) \<and> distinct x2 \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>x\<in>set x2. tcb_at x s) \<and> distinct x2 \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s ko. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some ko; Notification x = ko; valid_obj ntfn ko s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> (\<forall>x\<in>set x2. tcb_at x s) \<and> distinct x2 \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s)\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x)\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> (st_tcb_at (\<lambda>st. \<not> halted st) t s \<or> cte_wp_at (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t) (t, tcb_cnode_index 2) s) \<and> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> t \<notin> set x2 \<and> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None\<rbrakk> \<Longrightarrow> (case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 @ [t] = [tcb]) \<and> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if a = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} 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> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn badge rights x x2 s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) ntfn 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None; (y, tp) \<in> (if xa = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if xa = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if y = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s y)
 2. \<And>ntfn badge rights x x2 s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) ntfn 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if xa = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if y = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s y)
 3. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 4. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 5. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn badge rights x x2 s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) ntfn 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if xa = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfn then insert (t, NTFNSignal) (set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x)) else if y = t then insert (ntfn, TCBSignal) {r \<in> state_refs_of s t. snd r = TCBBound} else state_refs_of s y)
 2. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 3. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 4. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s \<and> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. \<exists>ko. kheap s t = Some ko \<and> is_tcb ko; distinct x2; \<forall>x\<in>set x2. \<exists>ko. kheap s x = Some ko \<and> (ntfn, TCBSignal) \<in> refs_of ko; state_refs_of s ntfn = set x2 \<times> {NTFNSignal}; bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2; ntfn_bound_tcb x = None\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s \<and> \<not> has_reply_cap t s
 2. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 3. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x2 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = WaitingNtfn x2; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; is_blocking; kheap s ntfn = Some (Notification x); x2 \<noteq> []; \<forall>t\<in>set x2. tcb_at t s; distinct x2; case ntfn_bound_tcb x of None \<Rightarrow> True | Some tcb \<Rightarrow> x2 = [tcb]; valid_bound_tcb (ntfn_bound_tcb x) s; state_refs_of s ntfn = set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x) \<and> (\<forall>x\<in>set x2 \<times> {NTFNSignal} \<union> ntfn_bound_refs (ntfn_bound_tcb x). case x of (x, tp) \<Rightarrow> obj_at (\<lambda>ko. (ntfn, symreftype tp) \<in> refs_of ko) x s); state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; t \<notin> set x2\<rbrakk> \<Longrightarrow> ntfn_bound_tcb x = None
 2. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) ntfn and (invs and Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> case ntfn_obj x of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn [t]
od | False \<Rightarrow> do_nbrecv_failed_transfer t | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state t (BlockedOnNotification ntfn);
set_notification ntfn $ ntfn_set_obj x $ WaitingNtfn (queue @ [t])
od | False \<Rightarrow> do_nbrecv_failed_transfer t | ActiveNtfn badge \<Rightarrow> do as_user t $ setRegister badge_register badge;
set_notification ntfn $ ntfn_set_obj x IdleNtfn
od \<lbrace>\<lambda>r s. invs s \<and> Q s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)\<rbrace> do y <- as_user t (setRegister badge_register x3);
set_notification ntfn (ntfn_set_obj x IdleNtfn)
od \<lbrace>\<lambda>r s. 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> Q s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x3. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q5526 ntfn badge rights x x3\<rbrace> do y <- as_user t (setRegister badge_register x3);
set_notification ntfn (ntfn_set_obj x IdleNtfn)
od \<lbrace>\<lambda>r s. 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> Q s\<rbrace>
 2. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; (ko_at (Notification x) 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 Q and st_tcb_at active t and ex_nonz_cap_to t and ex_nonz_cap_to ntfn and obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn)) s\<rbrakk> \<Longrightarrow> ?Q5526 ntfn badge rights x x3 s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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> Q s \<and> st_tcb_at active t s \<and> ex_nonz_cap_to t s \<and> ex_nonz_cap_to ntfn s \<and> obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s\<rbrakk> \<Longrightarrow> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s\<rbrakk> \<Longrightarrow> valid_bound_tcb (ntfn_bound_tcb x) s \<and> sym_refs (\<lambda>a. if a = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x)\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s a) \<and> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (3 subgoals):
 1. \<And>ntfn badge rights x x3 s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) ntfn 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; (y, tp) \<in> (if xa = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s xa); (y, tp) \<notin> state_refs_of s xa\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<in> (if y = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s y)
 2. \<And>ntfn badge rights x x3 s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) ntfn 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s y)
 3. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (2 subgoals):
 1. \<And>ntfn badge rights x x3 s xa y tp. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) ntfn 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s; (y, tp) \<in> state_refs_of s xa; (y, tp) \<notin> (if xa = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s xa)\<rbrakk> \<Longrightarrow> (xa, symreftype tp) \<notin> (if y = ntfn then ntfn_bound_refs (ntfn_bound_tcb x) else state_refs_of s y)
 2. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal (1 subgoal):
 1. \<And>ntfn badge rights x x3 s. \<lbrakk>cap = NotificationCap ntfn badge rights; ntfn_obj x = ActiveNtfn x3; ko_at (Notification x) 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; Q s; st_tcb_at active t s; ex_nonz_cap_to t s; ex_nonz_cap_to ntfn s; obj_at (\<lambda>ko. \<exists>ntfn. ko = Notification ntfn \<and> (ntfn_bound_tcb ntfn = None \<or> ntfn_bound_tcb ntfn = Some t)) ntfn s; state_refs_of s ntfn = refs_of (Notification x); bound_tcb_at (\<lambda>x. tcb_bound_refs x = state_refs_of s t) t s\<rbrakk> \<Longrightarrow> obj_at (\<lambda>ko. \<exists>y. Notification y = ko) ntfn s proof (prove)
goal:
No subgoals!