theory Ipc_IF

lemma send_signal_reads_respects:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  notes set_thread_state_owned_reads_respects[wp del]
        cancel_ipc_pas_refined[wp del]
  shows
    "reads_respects aag l
       (pas_refined aag and pas_cur_domain aag and pspace_aligned
                        and valid_vspace_objs and valid_arch_state
                        and (\<lambda>s. is_subject aag (cur_thread s))
                        and valid_etcbs and ct_active
                        and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs
                        and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))
       (send_signal ntfnptr badge)" unfolding send_signal_def fun_app_def subgoal proof (cases "aag_can_read aag ntfnptr \<or> aag_can_affect aag l ntfnptr") case True note visible = this show ?thesis apply (rule pre_ev) apply (simp split del: if_split
            | rule_tac ntfnptr=ntfnptr in blocked_cancel_ipc_nosts_reads_respects
            | rule cancel_ipc_reads_respects_rewrite
            | wp (once) set_simple_ko_reads_respects possible_switch_to_reads_respects
                        as_user_set_register_reads_respects' set_thread_state_pas_refined
                        set_simple_ko_reads_respects cancel_ipc_receive_blocked_pas_refined
                        gts_reads_respects gts_wp hoare_vcg_imp_lift get_simple_ko_wp
                        get_simple_ko_reads_respects update_waiting_ntfn_reads_respects
            | wpc
            | simp )+ apply (insert visible) apply clarsimp apply (rule conjI[rotated]) apply fastforce apply (rule disjI2) apply (intro impI allI) apply (simp add: obj_at_def) apply (rule conjI) apply (frule (3) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl]) apply (frule (1) bound_tcb_at_implies_receive) apply (elim disjE) apply (rule disjI1) apply (fastforce dest:read_sync_ep_read_receivers) apply (rule disjI2) apply (fastforce dest:read_sync_ep_read_receivers) apply (clarsimp) apply (frule (1) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)",OF _ _ _ _ refl]) apply (fastforce simp: obj_at_def) apply assumption apply (rule conjI) apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def) apply (rule conjI[rotated]) apply (frule (1) bound_tcb_at_implies_receive) apply (frule (1) bound_tcb_at_implies_reset) apply (clarsimp simp: pred_tcb_at_def get_tcb_def obj_at_def) apply (rule context_conjI) apply (fastforce dest!: receive_blockedD intro: BlockedOnReceive_inj) apply (frule_tac t=x and tcb=tcb and ep = "case (tcb_state tcb) of BlockedOnReceive a pl \<Rightarrow> a"
                   in get_tcb_recv_blocked_implies_receive) apply (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def) apply (fastforce simp: receive_blocked_def split:thread_state.splits) apply (fastforce simp: receive_blocked_def intro!: BlockedOnReceive_inj) by (fastforce simp: pred_tcb_at_def get_tcb_def obj_at_def receive_blocked_def ct_in_state_def) next case False note invisible = this show ?thesis apply (insert label_is_invisible[THEN iffD2, OF invisible]) apply (rule gen_asm_ev) apply (drule (1) invisible_ntfn_invisible_receivers_and_receivers) apply simp apply (rule ev2_invisible_simple[OF domains_distinct],assumption) apply (rule modifies_at_mostI) apply (simp split del: if_split
            | rule cancel_ipc_valid_rewrite
            | wp (once) set_thread_state_pas_refined set_notification_equiv_but_for_labels
                        possible_switch_to_equiv_but_for_labels as_user_equiv_but_for_labels
                        set_thread_state_runnable_equiv_but_for_labels get_simple_ko_wp
                        gts_wp update_waiting_ntfn_equiv_but_for_labels
                        blocked_cancel_ipc_nosts_equiv_but_for_labels
            | wpc
            | wps)+ apply (elim conjE) apply (match premises in "ntfn_bound_tcb _ = _" \<Rightarrow> \<open>fail\<close>
                                               \<bar> _ \<Rightarrow> \<open>rule allI impI conjI\<close>)+ prefer 2 apply (intro conjI allI impI; fastforce?) subgoal waiting_ntfn apply clarsimp apply (rule ccontr) apply (frule (3) not_etcb_at_not_cdom_can_read[OF domains_distinct, rotated 2]) apply (rule tcb_at_ntfn_queue;assumption) apply (frule (7) read_queued_thread_reads_ntfn) using invisible by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def) apply (frule (1) ntfn_bound_tcb_at[where P="(=) (Some ntfnptr)", OF _ _ _ _ refl]) apply (fastforce simp: obj_at_def) apply assumption apply (intro allI conjI impI) apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def
                            split: thread_state.splits
                           intro!: BlockedOnReceive_inj) apply assumption apply distinct_subgoals apply (fold_subgoals (prefix)) apply (frule st_tcb_at_tcb_at) subgoal bound_ntfn premises prems for st s ntfn x sta prefer 2 apply (rule disjI2) apply (rule disjI1) subgoal bound_tcb_can_receive using prems apply (clarsimp simp: all_with_auth_to_def obj_at_def) by (rule bound_tcb_at_implies_receive;assumption) apply (rule disjI2) apply (rule disjI2) apply (rule disjI1) subgoal bound_ep_can_receive apply (rule bexI[OF _ bound_tcb_can_receive]) apply (simp add: all_with_auth_to_def all_to_which_has_auth_def) using prems apply (case_tac sta; (clarsimp simp: pred_tcb_at_def obj_at_def receive_blocked_def)) apply (rule get_tcb_recv_blocked_implies_receive, assumption) apply (fastforce simp: get_tcb_def) by (fastforce split: thread_state.splits) apply (rule ccontr) apply (insert prems) apply (frule (4) not_etcb_at_not_cdom_can_read[OF domains_distinct]) using bound_tcb_can_receive apply (fastforce simp: labels_are_invisible_def all_with_auth_to_def all_to_which_has_auth_def) apply (fastforce simp: pred_tcb_at_def receive_blocked_def obj_at_def) apply (rule ccontr) apply clarsimp using invisible bound_tcb_can_receive reads_ep by (fastforce simp add: all_with_auth_to_def all_to_which_has_auth_def) done qed done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (send_signal ntfnptr badge) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (state)
goal (2 subgoals):
 1. aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od)
 2. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (state)
this:
aag_can_read_or_affect aag l ntfnptr

goal (2 subgoals):
 1. aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od)
 2. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (state)
this:
aag_can_read_or_affect aag l ntfnptr

goal (2 subgoals):
 1. aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od)
 2. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (2 subgoals):
 1. reads_respects aag l ?Q (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od)
 2. \<And>s. (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> valid_etcbs s \<and> ct_active s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<Longrightarrow> aag_can_read_or_affect aag l ntfnptr \<and> ((\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_obj ntfn \<noteq> IdleNtfn) \<or> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag)))) \<and> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn122 ntfn x)) ntfnptr s \<and> ntfn_obj (?ntfn122 ntfn x) = WaitingNtfn x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> valid_etcbs s \<and> ct_active s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_read_or_affect aag l ntfnptr\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l ntfnptr \<and> ((\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_obj ntfn \<noteq> IdleNtfn) \<or> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag)))) \<and> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn122 ntfn x)) ntfnptr s \<and> ntfn_obj (?ntfn122 ntfn x) = WaitingNtfn x)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> ((\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_obj ntfn \<noteq> IdleNtfn) \<or> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag)))) \<and> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn122 ntfn x)) ntfnptr s \<and> ntfn_obj (?ntfn122 ntfn x) = WaitingNtfn x)) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn122 ntfn x)) ntfnptr s \<and> ntfn_obj (?ntfn122 ntfn x) = WaitingNtfn x)
 2. \<And>s. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_obj ntfn \<noteq> IdleNtfn) \<or> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> ntfn_obj ntfn \<noteq> IdleNtfn) \<or> (\<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag)) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ko_at (Notification ntfn) ntfnptr s; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x \<and> (\<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 2. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 2. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 2. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_read aag ntfnptr\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 2. \<And>s ntfn x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_affect aag l ntfnptr\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 3. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_read aag ntfnptr\<rbrakk> \<Longrightarrow> aag_can_read aag x
 2. \<And>s ntfn x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_affect aag l ntfnptr\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 3. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_affect aag l ntfnptr\<rbrakk> \<Longrightarrow> aag_can_read_or_affect aag l x
 2. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x. \<lbrakk>pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; aag_can_affect aag l ntfnptr\<rbrakk> \<Longrightarrow> aag_can_affect aag l x
 2. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) x s \<longrightarrow> receive_blocked st \<longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> kheap s ntfnptr = Some (Notification (?ntfn202 s ntfn x st))
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> ntfn_bound_tcb (?ntfn202 s ntfn x st) = Some (?tcbptr202 s ntfn x st)
 3. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) (?tcbptr202 s ntfn x st) s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st\<rbrakk> \<Longrightarrow> ntfn_bound_tcb ntfn = Some (?tcbptr202 s ntfn x st)
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) (?tcbptr202 s ntfn x st) s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x \<and> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s; (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>sta. sta = BlockedOnReceive (?x86 ntfn x st) (?pl86 ntfn x st)) x s \<and> bound_tcb_at ((=) (Some ntfnptr)) x s \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x st)) \<in> pasPolicy aag
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb\<rbrakk> \<Longrightarrow> tcb_state tcb = BlockedOnReceive (?x86 ntfn x (tcb_state tcb)) (?pl86 ntfn x (tcb_state tcb)) \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x (tcb_state tcb))) \<in> pasPolicy aag
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb\<rbrakk> \<Longrightarrow> tcb_state tcb = BlockedOnReceive (?x86 ntfn x (tcb_state tcb)) (?pl86 ntfn x (tcb_state tcb))
 2. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (?x86 ntfn x (tcb_state tcb)) (?pl86 ntfn x (tcb_state tcb))\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag (?x86 ntfn x (tcb_state tcb))) \<in> pasPolicy aag
 3. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl)\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x)) \<in> pasPolicy aag
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (4 subgoals):
 1. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl)\<rbrakk> \<Longrightarrow> get_tcb x s = Some tcb
 2. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl)\<rbrakk> \<Longrightarrow> ep_recv_blocked (case tcb_state tcb of BlockedOnReceive a pl \<Rightarrow> a) (tcb_state tcb)
 3. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl); (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive a pl \<Rightarrow> a)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x)) \<in> pasPolicy aag
 4. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (3 subgoals):
 1. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl)\<rbrakk> \<Longrightarrow> ep_recv_blocked (case tcb_state tcb of BlockedOnReceive a pl \<Rightarrow> a) (tcb_state tcb)
 2. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl); (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive a pl \<Rightarrow> a)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x)) \<in> pasPolicy aag
 3. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>s ntfn x tcb. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; receive_blocked (tcb_state tcb); (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; (pasObjectAbs aag x, Reset, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s x = Some (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; tcb_state tcb = BlockedOnReceive (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x) (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> pl); (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive a pl \<Rightarrow> a)) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag (case tcb_state tcb of BlockedOnReceive x pl \<Rightarrow> x)) \<in> pasPolicy aag
 2. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<And>s ntfn x st. \<lbrakk>aag_can_read_or_affect aag l ntfnptr; pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; kheap s ntfnptr = Some (Notification ntfn); ntfn_bound_tcb ntfn = Some x; st_tcb_at ((=) st) x s; receive_blocked st; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (state)
this:
reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od)

goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (state)
goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (state)
this:
\<not> aag_can_read_or_affect aag l ntfnptr

goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (state)
this:
\<not> aag_can_read_or_affect aag l ntfnptr

goal (1 subgoal):
 1. \<not> aag_can_read_or_affect aag l ntfnptr \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. labels_are_invisible aag l {pasObjectAbs aag ntfnptr} \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>labels_are_invisible aag l {pasObjectAbs aag ntfnptr}; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (2 subgoals):
 1. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<Longrightarrow> Notify \<in> {Notify, Receive, SyncSend}
 2. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))\<rbrakk> \<Longrightarrow> reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))\<rbrakk> \<Longrightarrow> modifies_at_most aag ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od) proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))\<rbrakk> \<Longrightarrow> \<lbrace>pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and equiv_but_for_labels aag ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) st\<rbrace> do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od \<lbrace>\<lambda>_. equiv_but_for_labels aag ({pasObjectAbs aag ntfnptr} \<union> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st s. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s \<and> pas_cur_domain aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> is_subject aag (cur_thread s) \<and> valid_etcbs s \<and> ct_active s \<and> sym_refs (state_refs_of s) \<and> valid_objs s \<and> equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn138 st ntfn x)) ntfnptr s \<and> (\<forall>t\<in>set x. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) \<and> ntfn_obj (?ntfn138 st ntfn x) = WaitingNtfn x \<and> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) proof (prove)
goal (1 subgoal):
 1. \<And>st s. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s\<rbrakk> \<Longrightarrow> \<forall>ntfn. ko_at (Notification ntfn) ntfnptr s \<longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> (\<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x))) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn138 st ntfn x)) ntfnptr s \<and> (\<forall>t\<in>set x. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) \<and> ntfn_obj (?ntfn138 st ntfn x) = WaitingNtfn x \<and> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) proof (prove)
goal (2 subgoals):
 1. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x
 2. \<And>st s ntfn. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn138 st ntfn x)) ntfnptr s \<and> (\<forall>t\<in>set x. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) \<and> ntfn_obj (?ntfn138 st ntfn x) = WaitingNtfn x \<and> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) proof (prove)
goal (2 subgoals):
 1. \<And>st s ntfn. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ko_at (Notification (?ntfn138 st ntfn x)) ntfnptr s \<and> (\<forall>t\<in>set x. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) \<and> ntfn_obj (?ntfn138 st ntfn x) = WaitingNtfn x \<and> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))) \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<subseteq> insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))
 2. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = WaitingNtfn x\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s
 2. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_\<rbrakk> \<Longrightarrow> \<forall>t\<in>set x_. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_ proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_ proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_; \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_; \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_\<rbrakk> \<Longrightarrow> tcb_at t s_
 2. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_; \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_; aag_can_read aag t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_; \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_; aag_can_read aag t\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_; \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_; aag_can_read aag t; aag_can_read aag ntfnptr\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<not> aag_can_read_or_affect aag l ntfnptr

goal (1 subgoal):
 1. \<And>t. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s_; pas_cur_domain aag s_; pspace_aligned s_; valid_vspace_objs s_; valid_arch_state s_; is_subject aag (cur_thread s_); valid_etcbs s_; ct_active s_; sym_refs (state_refs_of s_); valid_objs s_; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st_ s_; ko_at (Notification ntfn_) ntfnptr s_; ntfn_obj ntfn_ = WaitingNtfn x_; t \<in> set x_; \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s_) t s_; aag_can_read aag t; aag_can_read aag ntfnptr\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x proof (prove)
goal (3 subgoals):
 1. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> kheap s ntfnptr = Some (Notification (?ntfn904 st s ntfn x))
 2. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> ntfn_bound_tcb (?ntfn904 st s ntfn x) = Some (?tcbptr904 st s ntfn x)
 3. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) (?tcbptr904 st s ntfn x) s\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> ntfn_bound_tcb ntfn = Some (?tcbptr904 st s ntfn x)
 2. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) (?tcbptr904 st s ntfn x) s\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<And>st s ntfn x. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s\<rbrakk> \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) x s \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s \<and> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s \<and> (pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)) \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<and> (pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)) \<and> st_tcb_at receive_blocked x s \<and> cur_thread s \<noteq> x proof (prove)
goal (8 subgoals):
 1. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> st_tcb_at (\<lambda>stb. stb = BlockedOnReceive (?x96 st ntfn x sta) (?pl96 st ntfn x sta)) x s
 2. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s
 3. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag (?x96 st ntfn x sta) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (?x96 st ntfn x sta) \<in> all_to_which_has_auth aag Write xa)
 4. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 5. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 6. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 7. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 8. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (7 subgoals):
 1. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some (?ntfnptr96 st ntfn x sta))) x s
 2. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 3. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 4. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 5. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 6. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 7. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (6 subgoals):
 1. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 2. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 3. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 4. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 5. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 6. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (5 subgoals):
 1. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 2. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 3. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 4. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 5. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta\<rbrakk> \<Longrightarrow> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x) &&& pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa) &&& etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s &&& st_tcb_at receive_blocked x s &&& cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<And>st s ntfn x sta. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x) &&& pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa) &&& etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s &&& st_tcb_at receive_blocked x s &&& cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x) &&& pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa) &&& etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s &&& st_tcb_at receive_blocked x s &&& cur_thread s \<noteq> x proof (prove)
goal (5 subgoals):
 1. pasObjectAbs aag x = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 2. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 3. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 4. st_tcb_at receive_blocked x s
 5. cur_thread s \<noteq> x proof (prove)
goal (5 subgoals):
 1. pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Receive xa) \<or> (\<exists>xa\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag x \<in> all_to_which_has_auth aag Write xa)
 2. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 3. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 4. st_tcb_at receive_blocked x s
 5. cur_thread s \<noteq> x proof (prove)
goal (5 subgoals):
 1. pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)
 2. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 3. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 4. st_tcb_at receive_blocked x s
 5. cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) proof (prove)
using this:
(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))))
pas_refined aag s
pas_cur_domain aag s
pspace_aligned s
valid_vspace_objs s
valid_arch_state s
is_subject aag (cur_thread s)
valid_etcbs s
ct_active s
sym_refs (state_refs_of s)
valid_objs s
equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s
ko_at (Notification ntfn) ntfnptr s
ntfn_obj ntfn = IdleNtfn
ntfn_bound_tcb ntfn = Some x
bound_tcb_at ((=) (Some ntfnptr)) x s
st_tcb_at ((=) sta) x s
receive_blocked sta
tcb_at x s

goal (1 subgoal):
 1. pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>ko. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) ({x. (x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag} \<union> \<Union> (all_to_which_has_auth aag Receive ` {x. (x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag}) \<union> \<Union> (all_to_which_has_auth aag Write ` {x. (x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag}))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) ({x. (x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag} \<union> \<Union> (all_to_which_has_auth aag Receive ` {x. (x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag}) \<union> \<Union> (all_to_which_has_auth aag Write ` {x. (x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag}))) st s; kheap s ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; kheap s x = Some ko; is_tcb ko\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) = pasObjectAbs aag ntfnptr \<or> pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 2. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 3. st_tcb_at receive_blocked x s
 4. cur_thread s \<noteq> x proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 2. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 3. st_tcb_at receive_blocked x s
 4. cur_thread s \<noteq> x proof (prove)
goal (4 subgoals):
 1. (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x) \<or> (\<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Write x)
 2. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 3. st_tcb_at receive_blocked x s
 4. cur_thread s \<noteq> x proof (prove)
goal (4 subgoals):
 1. \<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x
 2. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 3. st_tcb_at receive_blocked x s
 4. cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<exists>x\<in>all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr). pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive x proof (prove)
goal (1 subgoal):
 1. pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x) \<in> all_to_which_has_auth aag Receive (pasObjectAbs aag x) proof (prove)
goal (1 subgoal):
 1. (pasObjectAbs aag x, Receive, pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x)) \<in> pasPolicy aag proof (prove)
using this:
(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr))))
pas_refined aag s
pas_cur_domain aag s
pspace_aligned s
valid_vspace_objs s
valid_arch_state s
is_subject aag (cur_thread s)
valid_etcbs s
ct_active s
sym_refs (state_refs_of s)
valid_objs s
equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s
ko_at (Notification ntfn) ntfnptr s
ntfn_obj ntfn = IdleNtfn
ntfn_bound_tcb ntfn = Some x
bound_tcb_at ((=) (Some ntfnptr)) x s
st_tcb_at ((=) sta) x s
receive_blocked sta
tcb_at x s

goal (1 subgoal):
 1. (pasObjectAbs aag x, Receive, pasObjectAbs aag (case sta of BlockedOnReceive x pl \<Rightarrow> x)) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 tcb. \<lbrakk>kheap s ntfnptr = Some (Notification ntfn); sta = tcb_state tcb; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; kheap s x = Some (TCB tcb); is_tcb (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; BlockedOnReceive x41 x42 = tcb_state tcb\<rbrakk> \<Longrightarrow> (pasObjectAbs aag x, Receive, pasObjectAbs aag x41) \<in> pasPolicy aag proof (prove)
goal (2 subgoals):
 1. \<And>x41 x42 tcb. \<lbrakk>kheap s ntfnptr = Some (Notification ntfn); sta = tcb_state tcb; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; kheap s x = Some (TCB tcb); is_tcb (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; BlockedOnReceive x41 x42 = tcb_state tcb\<rbrakk> \<Longrightarrow> get_tcb x s = Some (?tcb216 x41 x42 tcb)
 2. \<And>x41 x42 tcb. \<lbrakk>kheap s ntfnptr = Some (Notification ntfn); sta = tcb_state tcb; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; kheap s x = Some (TCB tcb); is_tcb (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; BlockedOnReceive x41 x42 = tcb_state tcb\<rbrakk> \<Longrightarrow> ep_recv_blocked x41 (tcb_state (?tcb216 x41 x42 tcb)) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 tcb. \<lbrakk>kheap s ntfnptr = Some (Notification ntfn); sta = tcb_state tcb; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; kheap s x = Some (TCB tcb); is_tcb (TCB tcb); Some ntfnptr = tcb_bound_notification tcb; BlockedOnReceive x41 x42 = tcb_state tcb\<rbrakk> \<Longrightarrow> ep_recv_blocked x41 (tcb_state tcb) proof (prove)
goal (3 subgoals):
 1. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s
 2. st_tcb_at receive_blocked x s
 3. cur_thread s \<noteq> x proof (prove)
goal (3 subgoals):
 1. \<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s \<Longrightarrow> False
 2. st_tcb_at receive_blocked x s
 3. cur_thread s \<noteq> x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 3. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (3 subgoals):
 1. \<lbrakk>\<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s; aag_can_read aag x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 3. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
using this:
pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)

goal (3 subgoals):
 1. \<lbrakk>\<not> etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) x s; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s; aag_can_read aag x\<rbrakk> \<Longrightarrow> False
 2. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 3. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked x s
 2. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s\<rbrakk> \<Longrightarrow> cur_thread s \<noteq> x proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some x; bound_tcb_at ((=) (Some ntfnptr)) x s; st_tcb_at ((=) sta) x s; receive_blocked sta; tcb_at x s; \<not> cur_thread s \<noteq> x\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some (cur_thread s); bound_tcb_at ((=) (Some ntfnptr)) (cur_thread s) s; st_tcb_at ((=) sta) (cur_thread s) s; receive_blocked sta; tcb_at (cur_thread s) s; x = cur_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
\<not> aag_can_read_or_affect aag l ntfnptr
pasObjectAbs aag x \<in> all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)
\<lbrakk>(?l, ?auth, ?ep) \<in> ?g; ?auth \<in> {SyncSend, Receive}\<rbrakk> \<Longrightarrow> ?ep \<in> subjectReads ?g ?l

goal (1 subgoal):
 1. \<lbrakk>(pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; labels_are_invisible aag l (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))); pas_refined aag s; pas_cur_domain aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; is_subject aag (cur_thread s); valid_etcbs s; ct_active s; sym_refs (state_refs_of s); valid_objs s; equiv_but_for_labels aag (insert (pasObjectAbs aag ntfnptr) (all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr) \<union> \<Union> (all_to_which_has_auth aag Receive ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)) \<union> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag ntfnptr)))) st s; ko_at (Notification ntfn) ntfnptr s; ntfn_obj ntfn = IdleNtfn; ntfn_bound_tcb ntfn = Some (cur_thread s); bound_tcb_at ((=) (Some ntfnptr)) (cur_thread s) s; st_tcb_at ((=) sta) (cur_thread s) s; receive_blocked sta; tcb_at (cur_thread s) s; x = cur_thread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals! proof (state)
this:
reads_respects aag l (pas_refined aag and pas_cur_domain aag and pspace_aligned and valid_vspace_objs and valid_arch_state and (\<lambda>s. is_subject aag (cur_thread s)) and valid_etcbs and ct_active and (\<lambda>s. sym_refs (state_refs_of s)) and valid_objs and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)) (do ntfn <- get_notification ntfnptr;
case (ntfn_obj ntfn, ntfn_bound_tcb ntfn) of (IdleNtfn, None) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) | (IdleNtfn, Some tcb) \<Rightarrow> do st <- get_thread_state tcb;
if receive_blocked st then do cancel_ipc tcb;
set_thread_state tcb Running;
as_user tcb (setRegister badge_register badge);
do_extended_op (possible_switch_to tcb)
od else set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge))
od | (WaitingNtfn queue, bound_tcb) \<Rightarrow> update_waiting_ntfn ntfnptr queue bound_tcb badge | (ActiveNtfn badge', bound_tcb) \<Rightarrow> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn (combine_ntfn_badges badge badge')))
od)

goal:
No subgoals! proof (prove)
goal:
No subgoals!