theory Ipc_R

lemma receiveSignal_corres:
 "\<lbrakk> is_ntfn_cap cap; cap_relation cap cap' \<rbrakk> \<Longrightarrow>
  corres dc (invs and st_tcb_at active thread and valid_cap cap and ex_nonz_cap_to thread)
            (invs' and tcb_at' thread and valid_cap' cap')
            (receive_signal thread cap isBlocking) (receiveSignal thread cap' isBlocking)" apply (simp add: receive_signal_def receiveSignal_def) apply (case_tac cap, simp_all add: isEndpointCap_def) apply (rename_tac word1 word2 rights) apply (rule corres_guard_imp) apply (rule_tac R="\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and
                            ntfn_at word1 and ex_nonz_cap_to thread and
                            valid_ntfn rv and
                            obj_at (\<lambda>k. k = Notification rv) word1" and
                            R'="\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and
                            valid_ntfn' rv'"
                         in corres_split[OF getNotification_corres]) apply clarsimp apply (case_tac "ntfn_obj rv")
        \<comment> \<open>IdleNtfn\<close> apply (simp add: ntfn_relation_def) apply (rule corres_guard_imp) apply (case_tac isBlocking; simp) apply (rule corres_split[OF setThreadState_corres]) apply simp apply (rule setNotification_corres) apply (simp add: ntfn_relation_def) apply wp+ apply (rule corres_guard_imp, rule doNBRecvFailedTransfer_corres, simp+)
       \<comment> \<open>WaitingNtfn\<close> apply (simp add: ntfn_relation_def) apply (rule corres_guard_imp) apply (case_tac isBlocking; simp) apply (rule corres_split[OF setThreadState_corres]) apply simp apply (rule setNotification_corres) apply (simp add: ntfn_relation_def) apply wp+ apply (rule corres_guard_imp) apply (rule doNBRecvFailedTransfer_corres, simp+)
      \<comment> \<open>ActiveNtfn\<close> apply (simp add: ntfn_relation_def) apply (rule corres_guard_imp) apply (simp add: badgeRegister_def badge_register_def) apply (rule corres_split[OF asUser_setRegister_corres]) apply (rule setNotification_corres) apply (simp add: ntfn_relation_def) apply wp+ apply (fastforce simp: invs_def valid_state_def valid_pspace_def
                       elim!: st_tcb_weakenE) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) apply wp+ apply (clarsimp simp add: ntfn_at_def2 valid_cap_def st_tcb_at_tcb_at) apply (clarsimp simp add: valid_cap'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ntfn_cap cap; cap_relation cap cap'\<rbrakk> \<Longrightarrow> corres dc (invs and st_tcb_at active thread and valid_cap cap and ex_nonz_cap_to thread) (invs' and tcb_at' thread and valid_cap' cap') (receive_signal thread cap isBlocking) (receiveSignal thread cap' isBlocking) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_ntfn_cap cap; cap_relation cap cap'\<rbrakk> \<Longrightarrow> corres dc (invs and st_tcb_at active thread and valid_cap cap and ex_nonz_cap_to thread) (invs' and tcb_at' thread and valid_cap' cap') (do ntfnptr <- case cap of cap.NotificationCap ntfnptr badge rights \<Rightarrow> return ntfnptr | _ \<Rightarrow> fail;
ntfn <- get_notification ntfnptr;
case ntfn_obj ntfn of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification ntfnptr);
set_notification ntfnptr $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification ntfnptr);
set_notification ntfnptr $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification ntfnptr $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn
od
od) (do ntfn <- getNotification (capNtfnPtr cap');
case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread
od) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. \<lbrakk>cap' = capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43); cap = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> corres dc (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap x41 x42 x43) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap x41 x42 (AllowWrite \<in> x43) (AllowRead \<in> x43))) (do ntfn <- get_notification x41;
case ntfn_obj ntfn of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification x41 $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn
od
od) (do ntfn <- getNotification x41;
case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread
od) proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> corres dc (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) (do ntfn <- get_notification word1;
case ntfn_obj ntfn of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn
od
od) (do ntfn <- getNotification word1;
case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread
od) proof (prove)
goal (3 subgoals):
 1. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> corres dc (?Q3 word1 word2 rights) (?Q'3 word1 word2 rights) (do ntfn <- get_notification word1;
case ntfn_obj ntfn of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj ntfn Structures_A.ntfn.IdleNtfn
od
od) (do ntfn <- getNotification word1;
case ntfnObj ntfn of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) ntfn
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) ntfn
od | False \<Rightarrow> doNBRecvFailedTransfer thread
od)
 2. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> ?Q3 word1 word2 rights s
 3. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> ?Q'3 word1 word2 rights s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr cap')) thread;
setNotification (capNtfnPtr cap') $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 4. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 4. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 3. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread) (case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 3. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn\<rbrakk> \<Longrightarrow> corres dc (?Q14 word1 word2 rights rv rv') (?Q'14 word1 word2 rights rv rv') (case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread) (case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> ?Q14 word1 word2 rights rv rv' s
 3. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> ?Q'14 word1 word2 rights rv rv' s
 4. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> corres dc (?Q14 word1 word2 rights rv rv') (?Q'14 word1 word2 rights rv rv') (do y <- set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn [thread]))
od) (do y <- setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread;
setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv')
od)
 2. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (?Q14 word1 word2 rights rv rv') (?Q'14 word1 word2 rights rv rv') (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 3. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> ?Q14 word1 word2 rights rv rv' s
 4. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> ?Q'14 word1 word2 rights rv rv' s
 5. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 6. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 8. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 10. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (13 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> thread_state_relation (Structures_A.thread_state.BlockedOnNotification word1) (Structures_H.thread_state.BlockedOnNotification word1)
 2. \<And>word1 word2 rights rv rv' y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R25 word1 word2 rights rv rv' y) (?R'25 word1 word2 rights rv rv' ya) (set_notification word1 (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn [thread]))) (setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'))
 3. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 word1 word2 rights rv rv'\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>?R25 word1 word2 rights rv rv'\<rbrace>
 4. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 word1 word2 rights rv rv'\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>?R'25 word1 word2 rights rv rv'\<rbrace>
 5. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q25 word1 word2 rights rv rv') (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 6. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q25 word1 word2 rights rv rv') s
 7. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') s
 8. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 9. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 10. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word1 word2 rights rv rv' y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R25 word1 word2 rights rv rv' y) (?R'25 word1 word2 rights rv rv' ya) (set_notification word1 (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn [thread]))) (setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'))
 2. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 word1 word2 rights rv rv'\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>?R25 word1 word2 rights rv rv'\<rbrace>
 3. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 word1 word2 rights rv rv'\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>?R'25 word1 word2 rights rv rv'\<rbrace>
 4. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q25 word1 word2 rights rv rv') (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q25 word1 word2 rights rv rv') s
 6. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') s
 7. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 8. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 9. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 10. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>word1 word2 rights rv rv' y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking; dc y ya\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn [thread])) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv')
 2. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 word1 word2 rights rv rv'\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>\<lambda>y. ntfn_at word1\<rbrace>
 3. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 word1 word2 rights rv rv'\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>\<lambda>ya. ntfn_at' word1\<rbrace>
 4. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q25 word1 word2 rights rv rv') (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q25 word1 word2 rights rv rv') s
 6. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') s
 7. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 8. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 9. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 10. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q25 word1 word2 rights rv rv'\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>\<lambda>y. ntfn_at word1\<rbrace>
 2. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'25 word1 word2 rights rv rv'\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>\<lambda>ya. ntfn_at' word1\<rbrace>
 3. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q25 word1 word2 rights rv rv') (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 4. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q25 word1 word2 rights rv rv') s
 5. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'25 word1 word2 rights rv rv') s
 6. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 7. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 8. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 9. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 10. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights rv rv'. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ntfn_at word1) (tcb_at' thread and ntfn_at' word1) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ntfn_at word1) s
 3. \<And>word1 word2 rights rv rv' s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.IdleNtfn \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.IdleNtfn; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ntfn_at' word1) s
 4. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread) (case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (x2 @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2\<rbrakk> \<Longrightarrow> corres dc (?Q46 word1 word2 rights rv rv' x2) (?Q'46 word1 word2 rights rv rv' x2) (case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread) (case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (x2 @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> ?Q46 word1 word2 rights rv rv' x2 s
 3. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> ?Q'46 word1 word2 rights rv rv' x2 s
 4. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> corres dc (?Q46 word1 word2 rights rv rv' x2) (?Q'46 word1 word2 rights rv rv' x2) (do y <- set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn (x2 @ [thread])))
od) (do y <- setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread;
setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (x2 @ [thread])) rv')
od)
 2. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (?Q46 word1 word2 rights rv rv' x2) (?Q'46 word1 word2 rights rv rv' x2) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 3. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> ?Q46 word1 word2 rights rv rv' x2 s
 4. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> ?Q'46 word1 word2 rights rv rv' x2 s
 5. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (12 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> thread_state_relation (Structures_A.thread_state.BlockedOnNotification word1) (Structures_H.thread_state.BlockedOnNotification word1)
 2. \<And>word1 word2 rights rv rv' x2 y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R57 word1 word2 rights rv rv' x2 y) (?R'57 word1 word2 rights rv rv' x2 ya) (set_notification word1 (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn (x2 @ [thread])))) (setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (x2 @ [thread])) rv'))
 3. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 word1 word2 rights rv rv' x2\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>?R57 word1 word2 rights rv rv' x2\<rbrace>
 4. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 word1 word2 rights rv rv' x2\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>?R'57 word1 word2 rights rv rv' x2\<rbrace>
 5. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 6. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) s
 7. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) s
 8. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 9. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 10. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>word1 word2 rights rv rv' x2 y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R57 word1 word2 rights rv rv' x2 y) (?R'57 word1 word2 rights rv rv' x2 ya) (set_notification word1 (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn (x2 @ [thread])))) (setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (x2 @ [thread])) rv'))
 2. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 word1 word2 rights rv rv' x2\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>?R57 word1 word2 rights rv rv' x2\<rbrace>
 3. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 word1 word2 rights rv rv' x2\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>?R'57 word1 word2 rights rv rv' x2\<rbrace>
 4. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) s
 6. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) s
 7. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 8. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 9. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 10. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>word1 word2 rights rv rv' x2 y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking; dc y ya\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj rv (Structures_A.ntfn.WaitingNtfn (x2 @ [thread]))) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (x2 @ [thread])) rv')
 2. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 word1 word2 rights rv rv' x2\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>\<lambda>y. ntfn_at word1\<rbrace>
 3. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 word1 word2 rights rv rv' x2\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>\<lambda>ya. ntfn_at' word1\<rbrace>
 4. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) s
 6. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) s
 7. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 8. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 9. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 10. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q57 word1 word2 rights rv rv' x2\<rbrace> set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1) \<lbrace>\<lambda>y. ntfn_at word1\<rbrace>
 2. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; isBlocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'57 word1 word2 rights rv rv' x2\<rbrace> setThreadState (Structures_H.thread_state.BlockedOnNotification word1) thread \<lbrace>\<lambda>ya. ntfn_at' word1\<rbrace>
 3. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 4. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q57 word1 word2 rights rv rv' x2) s
 5. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'57 word1 word2 rights rv rv' x2) s
 6. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 8. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 10. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (tcb_at thread and ntfn_at word1) (tcb_at' thread and ntfn_at' word1) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ntfn_at word1) s
 3. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ntfn_at' word1) s
 4. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 rights rv rv' x2. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking\<rbrakk> \<Longrightarrow> corres dc (?Q73 word1 word2 rights rv rv' x2) (?Q'73 word1 word2 rights rv rv' x2) (do_nbrecv_failed_transfer thread) (doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking; (tcb_at thread and ntfn_at word1) s\<rbrakk> \<Longrightarrow> ?Q73 word1 word2 rights rv rv' x2 s
 3. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; \<not> isBlocking; (tcb_at' thread and ntfn_at' word1) s\<rbrakk> \<Longrightarrow> ?Q'73 word1 word2 rights rv rv' x2 s
 4. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ntfn_at word1) s
 5. \<And>word1 word2 rights rv rv' x2 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.WaitingNtfn x2 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.WaitingNtfn x2; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ntfn_at' word1) s
 6. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (case ntfn_obj rv of Structures_A.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do set_thread_state thread (Structures_A.thread_state.BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ Structures_A.ntfn.WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | Structures_A.ntfn.ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv Structures_A.ntfn.IdleNtfn
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 8. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 10. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfn_relation rv rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (case ntfnObj rv' of Structures_H.ntfn.IdleNtfn \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn [thread]) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread | Structures_H.ntfn.ActiveNtfn badge \<Rightarrow> do asUser thread $ setRegister Notification_H.badgeRegister badge;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'
od | Structures_H.ntfn.WaitingNtfn queue \<Rightarrow> case isBlocking of True \<Rightarrow> do setThreadState (Structures_H.thread_state.BlockedOnNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights)))) thread;
setNotification (capNtfnPtr (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) $ ntfnObj_update (\<lambda>_. Structures_H.ntfn.WaitingNtfn (queue @ [thread])) rv'
od | False \<Rightarrow> doNBRecvFailedTransfer thread)
 2. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 4. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (do y <- asUser thread (setRegister Notification_H.badgeRegister x3);
setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv')
od)
 2. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 4. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?Q78 word1 word2 rights rv rv' x3) (?Q'78 word1 word2 rights rv rv' x3) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (do y <- asUser thread (setRegister Notification_H.badgeRegister x3);
setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv')
od)
 2. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> ?Q78 word1 word2 rights rv rv' x3 s
 3. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> ?Q'78 word1 word2 rights rv rv' x3 s
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> corres dc (?Q78 word1 word2 rights rv rv' x3) (?Q'78 word1 word2 rights rv rv' x3) (do y <- as_user thread (setRegister ARM.badgeRegister x3);
set_notification word1 (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)
od) (do y <- asUser thread (setRegister ARM.badgeRegister x3);
setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv')
od)
 2. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> ?Q78 word1 word2 rights rv rv' x3 s
 3. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> ?Q'78 word1 word2 rights rv rv' x3 s
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights rv rv' x3 y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R82 word1 word2 rights rv rv' x3 y) (?R'82 word1 word2 rights rv rv' x3 ya) (set_notification word1 (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn)) (setNotification word1 (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv'))
 2. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q82 word1 word2 rights rv rv' x3\<rbrace> as_user thread (setRegister ARM.badgeRegister x3) \<lbrace>?R82 word1 word2 rights rv rv' x3\<rbrace>
 3. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q'82 word1 word2 rights rv rv' x3\<rbrace> asUser thread (setRegister ARM.badgeRegister x3) \<lbrace>?R'82 word1 word2 rights rv rv' x3\<rbrace>
 4. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q82 word1 word2 rights rv rv' x3) s
 5. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'82 word1 word2 rights rv rv' x3) s
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights rv rv' x3 y ya. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; dc y ya\<rbrakk> \<Longrightarrow> ntfn_relation (ntfn_set_obj rv Structures_A.ntfn.IdleNtfn) (ntfnObj_update (\<lambda>_. Structures_H.ntfn.IdleNtfn) rv')
 2. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q82 word1 word2 rights rv rv' x3\<rbrace> as_user thread (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>y. ntfn_at word1\<rbrace>
 3. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q'82 word1 word2 rights rv rv' x3\<rbrace> asUser thread (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>ya. ntfn_at' word1\<rbrace>
 4. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q82 word1 word2 rights rv rv' x3) s
 5. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'82 word1 word2 rights rv rv' x3) s
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 7. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 9. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q82 word1 word2 rights rv rv' x3\<rbrace> as_user thread (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>y. ntfn_at word1\<rbrace>
 2. \<And>word1 word2 rights rv rv' x3. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3\<rbrakk> \<Longrightarrow> \<lbrace>?Q'82 word1 word2 rights rv rv' x3\<rbrace> asUser thread (setRegister ARM.badgeRegister x3) \<lbrace>\<lambda>ya. ntfn_at' word1\<rbrace>
 3. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ?Q82 word1 word2 rights rv rv' x3) s
 4. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ?Q'82 word1 word2 rights rv rv' x3) s
 5. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 6. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 7. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 8. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1) s\<rbrakk> \<Longrightarrow> (tcb_at thread and ntfn_at word1) s
 2. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ntfn_at' word1) s
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 4. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 6. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights rv rv' x3 s. \<lbrakk>cap = cap.NotificationCap word1 word2 rights; ntfnObj rv' = Structures_H.ntfn.ActiveNtfn x3 \<and> ntfn_bound_tcb rv = ntfnBoundTCB rv'; cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); ntfn_obj rv = Structures_A.ntfn.ActiveNtfn x3; (invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv') s\<rbrakk> \<Longrightarrow> (tcb_at' thread and ntfn_at' word1) s
 2. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 3. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 4. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 5. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 word1 word2 rights\<rbrace> get_notification word1 \<lbrace>\<lambda>rv. invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread and valid_ntfn rv and obj_at (\<lambda>k. k = Notification rv) word1\<rbrace>
 2. \<And>word1 word2 rights. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 word1 word2 rights\<rbrace> getNotification word1 \<lbrace>\<lambda>rv'. invs' and tcb_at' thread and ntfn_at' word1 and valid_ntfn' rv'\<rbrace>
 3. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and ?Q7 word1 word2 rights) s
 4. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and ?Q'7 word1 word2 rights) s proof (prove)
goal (2 subgoals):
 1. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs and st_tcb_at active thread and valid_cap (cap.NotificationCap word1 word2 rights) and ex_nonz_cap_to thread) s\<rbrakk> \<Longrightarrow> (ntfn_at word1 and (\<lambda>s. (invs and tcb_at thread and st_tcb_at active thread and ntfn_at word1 and ex_nonz_cap_to thread) s \<and> (valid_objs and ntfn_at word1) s \<and> obj_at (\<lambda>ko. partial_inv Notification ko \<noteq> None) word1 s)) s
 2. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and (\<lambda>s. (invs' and tcb_at' thread and ntfn_at' word1) s \<and> (invs' and ntfn_at' word1) s)) s proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 rights s. \<lbrakk>cap' = capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights); cap = cap.NotificationCap word1 word2 rights; (invs' and tcb_at' thread and valid_cap' (capability.NotificationCap word1 word2 (AllowWrite \<in> rights) (AllowRead \<in> rights))) s\<rbrakk> \<Longrightarrow> (ntfn_at' word1 and (\<lambda>s. (invs' and tcb_at' thread and ntfn_at' word1) s \<and> (invs' and ntfn_at' word1) s)) s proof (prove)
goal:
No subgoals!