theory Ipc_AC

lemma send_signal_respects:
  "\<lbrace>integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of
                       and K (aag_has_auth_to aag Notify ntfnptr)\<rbrace>
   send_signal ntfnptr badge
   \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" apply (simp add: send_signal_def) apply (rule hoare_seq_ext[OF _ get_simple_ko_sp]) apply (rule hoare_name_pre_state) apply (case_tac "ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None")
   \<comment> \<open>ntfn-binding case\<close> apply (rule hoare_pre) apply (wp set_notification_respects[where auth=Notify]
                 as_user_set_register_respects_indirect[where ntfnptr=ntfnptr]
                 set_thread_state_integrity' sts_st_tcb_at' hoare_weak_lift_imp
                 cancel_ipc_receive_blocked_respects[where ntfnptr=ntfnptr]
                 gts_wp
               | wpc | simp)+ apply (clarsimp, rule conjI, clarsimp simp: st_tcb_def2) apply (clarsimp simp: receive_blocked_def) apply (simp split: thread_state.split_asm) apply (clarsimp simp: obj_at_def) apply (drule (3) ntfn_bound_tcb_at[where ntfnptr=ntfnptr and P="\<lambda>ntfn. ntfn = Some ntfnptr"], simp+)[1] apply (rule conjI) apply (drule_tac x=ntfnptr and t=y in bound_tcb_at_implies_receive) apply (clarsimp simp: pred_tcb_at_def obj_at_def, simp) apply clarsimp apply (rule conjI) apply (rule_tac s=sa in integrity_receive_blocked_chain') apply (clarsimp simp add: pred_tcb_at_def obj_at_def receive_blocked_def) apply (fastforce split: thread_state.split) apply simp+ apply (rule_tac s=sa in integrity_receive_blocked_chain_bound) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply simp+ apply (rule hoare_pre) apply clarsimp apply (wpc, clarsimp) apply (wp set_notification_respects[where auth=Notify]
               sts_st_tcb_at' as_user_set_register_respects
               set_thread_state_pas_refined set_simple_ko_pas_refined
               set_thread_state_respects_in_signalling [where ntfnptr = ntfnptr]
               set_ntfn_valid_objs_at hoare_vcg_disj_lift hoare_weak_lift_imp
          | wpc
          | simp add: update_waiting_ntfn_def)+ apply clarsimp apply (subgoal_tac "st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa") prefer 2 apply (rule ntfn_queued_st_tcb_at', assumption) apply (fastforce simp: obj_at_def valid_obj_def valid_ntfn_def) apply assumption+ apply simp apply simp apply (intro impI conjI)
   \<comment> \<open>st_tcb_at receive_blocked st\<close> apply (erule (2) integrity_receive_blocked_chain) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and K ((pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> send_signal ntfnptr badge \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag)\<rbrace> do ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge')
od \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn. \<lbrace>ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. (ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 ntfn s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s sa. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None; s = sa\<rbrakk> \<Longrightarrow> ?Q7 ntfn s sa
 3. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s sa. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> valid_objs sa \<and> sym_refs (state_refs_of sa) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<and> (\<exists>y. ntfn_bound_tcb ntfn = Some y); s = sa\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_bound_tcb ntfn = Some x \<longrightarrow> (\<forall>sta. st_tcb_at ((=) sta) x sa \<longrightarrow> receive_blocked sta \<longrightarrow> st_tcb_at receive_blocked x sa \<and> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x sa \<and> (pasObjectAbs aag x, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag x \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked x st \<and> bound_tcb_at ((=) (Some ntfnptr)) x st))
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y sta. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) sta) y sa; receive_blocked sta\<rbrakk> \<Longrightarrow> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa \<and> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st)
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y sta. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) sta) y sa; case sta of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False\<rbrakk> \<Longrightarrow> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa \<and> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st)
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y sta x41 x42. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; sta = BlockedOnReceive x41 x42\<rbrakk> \<Longrightarrow> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa \<and> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st)
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa\<rbrakk> \<Longrightarrow> bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa \<and> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st)
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa\<rbrakk> \<Longrightarrow> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<and> (pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st)
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa\<rbrakk> \<Longrightarrow> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa\<rbrakk> \<Longrightarrow> pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st
 3. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y sa
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> (pasObjectAbs aag y, Receive, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag
 3. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa\<rbrakk> \<Longrightarrow> pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st
 4. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa\<rbrakk> \<Longrightarrow> pasObjectAbs aag y \<noteq> pasSubject aag \<longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked y st \<and> bound_tcb_at ((=) (Some ntfnptr)) y st
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked y st
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y st
 3. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> st_tcb_at receive_blocked y sa
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity (?aag180 ntfn sa y x41 x42) (?X180 ntfn sa y x41 x42) st sa
 3. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> pasObjectAbs (?aag180 ntfn sa y x41 x42) y \<noteq> pasSubject (?aag180 ntfn sa y x41 x42)
 4. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y st
 5. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ntfn sa y x41 x42 tcb. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; pasObjectAbs aag y \<noteq> pasSubject aag; kheap sa y = Some (TCB tcb); BlockedOnReceive x41 x42 = tcb_state tcb; tcb_bound_notification tcb = Some ntfnptr\<rbrakk> \<Longrightarrow> case tcb_state tcb of BlockedOnReceive x xa \<Rightarrow> True | _ \<Rightarrow> False
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity (?aag180 ntfn sa y x41 x42) (?X180 ntfn sa y x41 x42) st sa
 3. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> pasObjectAbs (?aag180 ntfn sa y x41 x42) y \<noteq> pasSubject (?aag180 ntfn sa y x41 x42)
 4. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y st
 5. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity (?aag180 ntfn sa y x41 x42) (?X180 ntfn sa y x41 x42) st sa
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> pasObjectAbs (?aag180 ntfn sa y x41 x42) y \<noteq> pasSubject (?aag180 ntfn sa y x41 x42)
 3. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y st
 4. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y st
 2. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> bound_tcb_at ((=) (Some ntfnptr)) y sa
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity (?aag216 ntfn sa y x41 x42) (?X216 ntfn sa y x41 x42) st sa
 3. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> pasObjectAbs (?aag216 ntfn sa y x41 x42) y \<noteq> pasSubject (?aag216 ntfn sa y x41 x42)
 4. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> integrity (?aag216 ntfn sa y x41 x42) (?X216 ntfn sa y x41 x42) st sa
 2. \<And>ntfn sa y x41 x42. \<lbrakk>kheap sa ntfnptr = Some (Notification ntfn); ntfn_obj ntfn = IdleNtfn; integrity aag X st sa; pas_refined aag sa; valid_objs sa; (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_bound_tcb ntfn = Some y; st_tcb_at ((=) (BlockedOnReceive x41 x42)) y sa; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) y sa; pasObjectAbs aag y \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> pasObjectAbs (?aag216 ntfn sa y x41 x42) y \<noteq> pasSubject (?aag216 ntfn sa y x41 x42)
 3. \<And>ntfn s. \<lbrakk>(ko_at (Notification ntfn) ntfnptr and (integrity aag X st and pas_refined aag and valid_objs and sym_refs \<circ> state_refs_of and (\<lambda>y. (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag))) s; \<not> (ntfn_obj ntfn = IdleNtfn \<and> ntfn_bound_tcb ntfn \<noteq> None)\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>ko_at (Notification ntfn) ntfnptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None\<rbrakk> \<Longrightarrow> \<lbrace>?Q229 ntfn s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s sa. \<lbrakk>ko_at (Notification ntfn) ntfnptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; s = sa\<rbrakk> \<Longrightarrow> ?Q229 ntfn s sa proof (prove)
goal (2 subgoals):
 1. \<And>ntfn s. \<lbrakk>ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; ko_at (Notification ntfn) ntfnptr s; integrity aag X st s; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag\<rbrakk> \<Longrightarrow> \<lbrace>?Q229 ntfn s\<rbrace> case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case ntfn_bound_tcb ntfn of None \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn (ActiveNtfn badge) | 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 \<Rightarrow> update_waiting_ntfn ntfnptr queue (ntfn_bound_tcb ntfn) badge | ActiveNtfn badge' \<Rightarrow> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge badge') \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s sa. \<lbrakk>ko_at (Notification ntfn) ntfnptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; s = sa\<rbrakk> \<Longrightarrow> ?Q229 ntfn s sa proof (prove)
goal (4 subgoals):
 1. \<And>ntfn s. \<lbrakk>ntfn_bound_tcb ntfn = None; ko_at (Notification ntfn) ntfnptr s; integrity aag X st s; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn\<rbrakk> \<Longrightarrow> \<lbrace>?R250 ntfn s\<rbrace> set_notification ntfnptr (ntfn_set_obj ntfn (ActiveNtfn badge)) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 2. \<And>ntfn s x2. \<lbrakk>ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; ko_at (Notification ntfn) ntfnptr s; integrity aag X st s; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x2\<rbrakk> \<Longrightarrow> \<lbrace>?R251 ntfn s x2\<rbrace> update_waiting_ntfn ntfnptr x2 (ntfn_bound_tcb ntfn) badge \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 3. \<And>ntfn s x3. \<lbrakk>ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; ko_at (Notification ntfn) ntfnptr s; integrity aag X st s; pas_refined aag s; valid_objs s; sym_refs (state_refs_of s); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?R252 ntfn s x3\<rbrace> set_notification ntfnptr $ ntfn_set_obj ntfn $ ActiveNtfn (combine_ntfn_badges badge x3) \<lbrace>\<lambda>_. integrity aag X st\<rbrace>
 4. \<And>ntfn s sa. \<lbrakk>ko_at (Notification ntfn) ntfnptr s \<and> integrity aag X st s \<and> pas_refined aag s \<and> valid_objs s \<and> sym_refs (state_refs_of s) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; s = sa\<rbrakk> \<Longrightarrow> (ntfn_obj ntfn = IdleNtfn \<longrightarrow> ?R250 ntfn s sa) \<and> (\<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> ?R251 ntfn s x sa) \<and> (\<forall>x. ntfn_obj ntfn = ActiveNtfn x \<longrightarrow> ?R252 ntfn s x sa) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn s sa. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa \<and> integrity aag X st sa \<and> pas_refined aag sa \<and> valid_objs sa \<and> sym_refs (state_refs_of sa) \<and> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = IdleNtfn \<longrightarrow> ntfn_bound_tcb ntfn = None; s = sa\<rbrakk> \<Longrightarrow> \<forall>x. ntfn_obj ntfn = WaitingNtfn x \<longrightarrow> x \<noteq> [] \<longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag)
 2. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa
 2. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (5 subgoals):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> (hd x, ?rt316 ntfn sa x) \<in> ntfn_q_refs_of (ntfn_obj ntfn)
 2. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> valid_objs sa
 3. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of sa)
 4. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 5. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (4 subgoals):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> valid_objs sa
 2. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> sym_refs (state_refs_of sa)
 3. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 4. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []\<rbrakk> \<Longrightarrow> receive_blocked_on ntfnptr (BlockedOnNotification ntfnptr)
 2. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (is_subject aag (hd x) \<or> st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa) \<and> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (1 subgoal):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (pasObjectAbs aag (hd x) \<noteq> pasSubject aag \<longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st) \<and> ((pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag) proof (prove)
goal (2 subgoals):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa; pasObjectAbs aag (hd x) \<noteq> pasSubject aag\<rbrakk> \<Longrightarrow> st_tcb_at (receive_blocked_on (?ep298 ntfn sa x ())) (hd x) st
 2. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (pasSubject aag, SyncSend, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag (?ep298 ntfn sa x ())) \<in> pasPolicy aag proof (prove)
goal (1 subgoal):
 1. \<And>ntfn sa x. \<lbrakk>ko_at (Notification ntfn) ntfnptr sa; integrity aag X st sa; pas_refined aag sa; valid_objs sa; sym_refs (state_refs_of sa); (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag; ntfn_obj ntfn = WaitingNtfn x; x \<noteq> []; st_tcb_at (receive_blocked_on ntfnptr) (hd x) sa\<rbrakk> \<Longrightarrow> (pasSubject aag, SyncSend, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag \<or> (pasSubject aag, Notify, pasObjectAbs aag ntfnptr) \<in> pasPolicy aag proof (prove)
goal:
No subgoals!