theory Ipc_IF

lemma update_waiting_ntfn_equiv_but_for_labels:
  "\<lbrace>equiv_but_for_labels aag L st and pas_refined aag and pspace_aligned and valid_vspace_objs and
    valid_arch_state and valid_objs and ko_at (Notification ntfn) nptr and sym_refs \<circ> state_refs_of and
    (\<lambda>s. \<forall>t\<in> set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and
    K (ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag nptr \<in> L \<and>
       all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L \<and>
       \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L)\<rbrace>
   update_waiting_ntfn nptr list boundtcb badge
   \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace>" unfolding update_waiting_ntfn_def apply (wp hoare_weak_lift_imp as_user_equiv_but_for_labels set_thread_state_runnable_equiv_but_for_labels
            set_thread_state_pas_refined set_notification_equiv_but_for_labels
            set_simple_ko_pred_tcb_at set_simple_ko_pas_refined
            hoare_vcg_disj_lift possible_switch_to_equiv_but_for_labels
         | wpc | simp add: split_def)+ apply clarsimp apply (frule_tac P="receive_blocked_on nptr" and t="hd list" in ntfn_queued_st_tcb_at') apply (fastforce) apply assumption apply assumption apply simp apply (subgoal_tac "pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag nptr)") apply (fastforce) apply (clarsimp simp: all_with_auth_to_def) apply (erule pas_refined_mem[rotated]) apply (rule sta_ts) apply (clarsimp simp: thread_st_auth_def tcb_states_of_state_def st_tcb_def2) apply (case_tac "tcb_state tcb", simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and ko_at (Notification ntfn) nptr and sym_refs \<circ> state_refs_of and (\<lambda>s. \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and K (ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag nptr \<in> L \<and> all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L)\<rbrace> update_waiting_ntfn nptr list boundtcb badge \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>equiv_but_for_labels aag L st and pas_refined aag and pspace_aligned and valid_vspace_objs and valid_arch_state and valid_objs and ko_at (Notification ntfn) nptr and sym_refs \<circ> state_refs_of and (\<lambda>s. \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) and K (ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag nptr \<in> L \<and> all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L)\<rbrace> do assert (list \<noteq> []);
(dest, rest) <- return $ (hd list, tl list);
set_notification nptr $ \<lparr>ntfn_obj = case rest of [] \<Rightarrow> IdleNtfn | a # list \<Rightarrow> WaitingNtfn rest, ntfn_bound_tcb = boundtcb\<rparr>;
set_thread_state dest Running;
as_user dest $ setRegister badge_register badge;
do_extended_op (possible_switch_to dest)
od \<lbrace>\<lambda>_. equiv_but_for_labels aag L st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. equiv_but_for_labels aag L st s \<and> pas_refined aag s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> valid_arch_state s \<and> valid_objs s \<and> ko_at (Notification ntfn) nptr s \<and> sym_refs (state_refs_of s) \<and> (\<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s) \<and> ntfn_obj ntfn = WaitingNtfn list \<and> pasObjectAbs aag nptr \<in> L \<and> all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L \<and> \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L \<Longrightarrow> list \<noteq> [] \<longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (5 subgoals):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> (hd list, ?rt113 s) \<in> ntfn_q_refs_of (ntfn_obj ntfn)
 2. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> valid_objs s
 3. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 4. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on nptr (BlockedOnNotification nptr)
 5. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 3. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on nptr (BlockedOnNotification nptr)
 4. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of s)
 2. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on nptr (BlockedOnNotification nptr)
 3. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on nptr (BlockedOnNotification nptr)
 2. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s; pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag nptr)\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> L
 2. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag nptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; all_with_auth_to aag Receive (pasObjectAbs aag nptr) \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` all_with_auth_to aag Receive (pasObjectAbs aag nptr)) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd list) \<in> all_with_auth_to aag Receive (pasObjectAbs aag nptr) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pas_refined aag s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag} \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag}) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (hd list), Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag} \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag}) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> (hd list, Receive, nptr) \<in> state_objs_to_policy s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>equiv_but_for_labels aag L st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag} \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag}) \<subseteq> L; list \<noteq> []; st_tcb_at (receive_blocked_on nptr) (hd list) s\<rbrakk> \<Longrightarrow> (nptr, Receive) \<in> thread_st_auth s (hd list) proof (prove)
goal (1 subgoal):
 1. \<And>s tcb. \<lbrakk>equiv_but_for_labels aag L st s; pspace_aligned s; valid_vspace_objs s; valid_arch_state s; valid_objs s; ko_at (Notification ntfn) nptr s; sym_refs (state_refs_of s); \<forall>t\<in>set list. etcb_at (\<lambda>etcb. tcb_domain etcb \<noteq> cur_domain s) t s; ntfn_obj ntfn = WaitingNtfn list; pasObjectAbs aag nptr \<in> L; {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag} \<subseteq> L; \<Union> (all_to_which_has_auth aag Write ` {x. (x, Receive, pasObjectAbs aag nptr) \<in> pasPolicy aag}) \<subseteq> L; list \<noteq> []; get_tcb (hd list) s = Some tcb; receive_blocked_on nptr (tcb_state tcb)\<rbrakk> \<Longrightarrow> (nptr, Receive) \<in> tcb_st_to_auth (tcb_state tcb) proof (prove)
goal:
No subgoals!