theory Ipc_DR

lemma recv_signal_corres:
  "cap = transform_cap cap' \<Longrightarrow>
  dcorres dc \<top> (invs and not_idle_thread thread and st_tcb_at active thread and valid_etcbs)
             (recv_signal thread cap)
             (receive_signal thread cap' is_blocking)" apply (clarsimp simp:receive_signal_def invs_def recv_signal_def corres_free_fail split:cap.splits) apply (rename_tac word1 word2 rights) apply (rule dcorres_expand_pfx) apply (rule_tac Q' = "\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r" in corres_symb_exec_r) apply (rule dcorres_expand_pfx) apply (clarsimp simp:obj_at_def is_ntfn_def) apply (case_tac "ntfn_obj rv"; simp) apply (clarsimp simp: ntfn_waiting_set_lift valid_state_def valid_ntfn_abstract_def
                             none_is_waiting_ntfn_def ) apply (case_tac is_blocking; simp) apply (rule corres_guard_imp) apply (rule corres_alternate1) apply (rule corres_dummy_return_l) apply (rule corres_split[OF set_thread_state_block_on_notification_corres]) apply  (rule corres_dummy_set_notification,simp) apply (wp|simp)+ apply (clarsimp simp:st_tcb_at_def tcb_at_def obj_at_def get_tcb_rev) apply (simp add: do_nbrecv_failed_transfer_def) apply (rule corres_guard_imp) apply (rule corres_alternate2) apply (rule corrupt_tcb_intent_as_user_corres) apply simp apply simp 
      (* WaitingNtfn *)
       apply (clarsimp simp: ntfn_waiting_set_lift valid_state_def valid_ntfn_abstract_def
                            none_is_waiting_ntfn_def) apply (case_tac is_blocking; simp) apply (rule corres_guard_imp) apply (rule corres_alternate1) apply (rule corres_dummy_return_l) apply (rule corres_split[OF set_thread_state_block_on_notification_corres]) apply  (rule corres_dummy_set_notification,simp) apply (wp|simp)+ apply (clarsimp simp:st_tcb_at_def tcb_at_def obj_at_def get_tcb_rev) apply (simp add: do_nbrecv_failed_transfer_def) apply (rule corres_guard_imp) apply (rule corres_alternate2) apply (rule corrupt_tcb_intent_as_user_corres) apply simp apply simp 
     (* Active NTFN *)
      apply (clarsimp simp: ntfn_waiting_set_lift valid_state_def valid_ntfn_abstract_def
                           none_is_waiting_ntfn_def) apply (rule corres_alternate2) apply (rule corres_guard_imp ) apply (rule corres_dummy_return_l) apply (rule corres_split[OF set_register_corres corres_dummy_set_notification]) apply (wp |clarsimp)+ apply (rule_tac Q="\<lambda>r. ko_at (kernel_object.Notification r) word1 and valid_state" in hoare_strengthen_post) apply (wp get_simple_ko_ko_at | clarsimp)+ apply (rule valid_objs_valid_ntfn_simp) apply (clarsimp simp:valid_objs_valid_ntfn_simp valid_state_def valid_pspace_def) apply (simp add:obj_at_def) apply (clarsimp|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. cap = transform_cap cap' \<Longrightarrow> dcorres dc (\<lambda>_. True) (invs and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) (recv_signal thread cap) (receive_signal thread cap' is_blocking) proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43. \<lbrakk>cap = cdl_cap.NotificationCap x41 x42 x43; cap' = cap.NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) (block_thread_on_ipc thread (PendingNtfnRecvCap x41) \<sqinter> corrupt_tcb_intent thread) (do ntfn <- get_notification x41;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification x41);
set_notification x41 $ ntfn_set_obj ntfn $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification x41 $ ntfn_set_obj ntfn IdleNtfn
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 rights. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do ntfn <- get_notification word1;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj ntfn IdleNtfn
od
od) proof (prove)
goal (1 subgoal):
 1. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do ntfn <- get_notification word1;
case ntfn_obj ntfn of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj ntfn $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj ntfn IdleNtfn
od
od) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) s) ((=) s' and ko_at (kernel_object.Notification rv) word1 and valid_ntfn rv) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case ntfn_obj rv of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv IdleNtfn
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s s' rv sa s'a. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; sa = transform s'a; s = sa; ((=) s' and ko_at (kernel_object.Notification rv) word1 and valid_ntfn rv) s'a\<rbrakk> \<Longrightarrow> dcorres dc ((=) sa) ((=) s'a) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case ntfn_obj rv of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv IdleNtfn
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case ntfn_obj rv of IdleNtfn \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | WaitingNtfn queue \<Rightarrow> case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (queue @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread | ActiveNtfn badge \<Rightarrow> do as_user thread $ setRegister badge_register badge;
set_notification word1 $ ntfn_set_obj rv IdleNtfn
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn [thread]
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn [thread]))
od)
 2. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 4. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 6. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q69 word1 word2 rights s' rv) (?Q'69 word1 word2 rights s' rv) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn [thread]))
od)
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q69 word1 word2 rights s' rv s
 3. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'69 word1 word2 rights s' rv s
 4. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 6. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 8. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q69 word1 word2 rights s' rv) (?Q'69 word1 word2 rights s' rv) (block_thread_on_ipc thread (PendingNtfnRecvCap word1)) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn [thread]))
od)
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q69 word1 word2 rights s' rv s
 3. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'69 word1 word2 rights s' rv s
 4. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 6. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 8. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q69 word1 word2 rights s' rv) (?Q'69 word1 word2 rights s' rv) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) >>= return) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn [thread]))
od)
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q69 word1 word2 rights s' rv s
 3. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'69 word1 word2 rights s' rv s
 4. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 6. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 8. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (11 subgoals):
 1. \<And>word1 word2 rights s' rv x y. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R77 word1 word2 rights s' rv x) (?R'77 word1 word2 rights s' rv y) (return x) (set_notification word1 (ntfn_set_obj rv (WaitingNtfn [thread])))
 2. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q77 word1 word2 rights s' rv\<rbrace> block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<lbrace>?R77 word1 word2 rights s' rv\<rbrace>
 3. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 word1 word2 rights s' rv\<rbrace> set_thread_state thread (BlockedOnNotification word1) \<lbrace>?R'77 word1 word2 rights s' rv\<rbrace>
 4. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q77 word1 word2 rights s' rv) s
 5. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and tcb_at thread and valid_etcbs and ?Q'77 word1 word2 rights s' rv) s
 6. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 7. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 8. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 9. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 10. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'77 word1 word2 rights s' rv\<rbrace> set_thread_state thread (BlockedOnNotification word1) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q77 word1 word2 rights s' rv) s
 3. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and tcb_at thread and valid_etcbs and ?Q'77 word1 word2 rights s' rv) s
 4. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 6. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 8. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 9. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s word1 = Some (kernel_object.Notification rv); valid_ntfn rv s; cur_tcb s; not_idle_thread thread s; st_tcb_at active thread s; valid_etcbs s; ntfn_obj rv = IdleNtfn; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; is_blocking; s' = s\<rbrakk> \<Longrightarrow> tcb_at thread s
 2. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 4. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 6. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (as_user thread (setRegister badge_register 0))
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q94 word1 word2 rights s' rv) (?Q'94 word1 word2 rights s' rv) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (as_user thread (setRegister badge_register 0))
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q94 word1 word2 rights s' rv s
 3. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'94 word1 word2 rights s' rv s
 4. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 7. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights s' rv. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q94 word1 word2 rights s' rv) (?Q'94 word1 word2 rights s' rv) (corrupt_tcb_intent thread) (as_user thread (setRegister badge_register 0))
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q94 word1 word2 rights s' rv s
 3. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'94 word1 word2 rights s' rv s
 4. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 7. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread thread and valid_etcbs) s
 3. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 4. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 6. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = IdleNtfn; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread thread and valid_etcbs) s
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (case is_blocking of True \<Rightarrow> do set_thread_state thread (BlockedOnNotification word1);
set_notification word1 $ ntfn_set_obj rv $ WaitingNtfn (x2 @ [thread])
od | False \<Rightarrow> do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn (x2 @ [thread])))
od)
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q134 word1 word2 rights s' rv x2) (?Q'134 word1 word2 rights s' rv x2) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn (x2 @ [thread])))
od)
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q134 word1 word2 rights s' rv x2 s
 3. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'134 word1 word2 rights s' rv x2 s
 4. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 7. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q134 word1 word2 rights s' rv x2) (?Q'134 word1 word2 rights s' rv x2) (block_thread_on_ipc thread (PendingNtfnRecvCap word1)) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn (x2 @ [thread])))
od)
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q134 word1 word2 rights s' rv x2 s
 3. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'134 word1 word2 rights s' rv x2 s
 4. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 7. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q134 word1 word2 rights s' rv x2) (?Q'134 word1 word2 rights s' rv x2) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) >>= return) (do y <- set_thread_state thread (BlockedOnNotification word1);
set_notification word1 (ntfn_set_obj rv (WaitingNtfn (x2 @ [thread])))
od)
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q134 word1 word2 rights s' rv x2 s
 3. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'134 word1 word2 rights s' rv x2 s
 4. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 7. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (10 subgoals):
 1. \<And>word1 word2 rights s' rv x2 x y. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; dc x y\<rbrakk> \<Longrightarrow> dcorres dc (?R142 word1 word2 rights s' rv x2 x) (?R'142 word1 word2 rights s' rv x2 y) (return x) (set_notification word1 (ntfn_set_obj rv (WaitingNtfn (x2 @ [thread]))))
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q142 word1 word2 rights s' rv x2\<rbrace> block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<lbrace>?R142 word1 word2 rights s' rv x2\<rbrace>
 3. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'142 word1 word2 rights s' rv x2\<rbrace> set_thread_state thread (BlockedOnNotification word1) \<lbrace>?R'142 word1 word2 rights s' rv x2\<rbrace>
 4. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q142 word1 word2 rights s' rv x2) s
 5. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and tcb_at thread and valid_etcbs and ?Q'142 word1 word2 rights s' rv x2) s
 6. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 7. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 9. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 10. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (8 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking\<rbrakk> \<Longrightarrow> \<lbrace>?Q'142 word1 word2 rights s' rv x2\<rbrace> set_thread_state thread (BlockedOnNotification word1) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q142 word1 word2 rights s' rv x2) s
 3. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; is_blocking; s' = s\<rbrakk> \<Longrightarrow> (not_idle_thread thread and tcb_at thread and valid_etcbs and ?Q'142 word1 word2 rights s' rv x2) s
 4. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 5. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 7. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 8. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s word1 = Some (kernel_object.Notification rv); valid_ntfn rv s; cur_tcb s; not_idle_thread thread s; st_tcb_at active thread s; valid_etcbs s; ntfn_obj rv = WaitingNtfn x2; valid_pspace s; valid_mdb s; valid_ioc s; valid_idle s; only_idle s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; is_blocking; s' = s\<rbrakk> \<Longrightarrow> tcb_at thread s
 2. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do_nbrecv_failed_transfer thread)
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (as_user thread (setRegister badge_register 0))
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q159 word1 word2 rights s' rv x2) (?Q'159 word1 word2 rights s' rv x2) (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (as_user thread (setRegister badge_register 0))
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q159 word1 word2 rights s' rv x2 s
 3. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'159 word1 word2 rights s' rv x2 s
 4. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 6. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights s' rv x2. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking\<rbrakk> \<Longrightarrow> dcorres dc (?Q159 word1 word2 rights s' rv x2) (?Q'159 word1 word2 rights s' rv x2) (corrupt_tcb_intent thread) (as_user thread (setRegister badge_register 0))
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> ?Q159 word1 word2 rights s' rv x2 s
 3. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> ?Q'159 word1 word2 rights s' rv x2 s
 4. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 6. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; transform s' = s\<rbrakk> \<Longrightarrow> True
 2. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread thread and valid_etcbs) s
 3. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv x2 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = WaitingNtfn x2; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; \<not> is_blocking; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread thread and valid_etcbs) s
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (block_thread_on_ipc thread (PendingNtfnRecvCap word1) \<sqinter> corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> dcorres dc ((=) (transform s')) ((=) s') (corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 2. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q194 word1 word2 rights s' rv x3) (?Q'194 word1 word2 rights s' rv x3) (corrupt_tcb_intent thread) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 2. \<And>word1 word2 rights s' rv x3 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q194 word1 word2 rights s' rv x3 s
 3. \<And>word1 word2 rights s' rv x3 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'194 word1 word2 rights s' rv x3 s
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (6 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> dcorres dc (?Q194 word1 word2 rights s' rv x3) (?Q'194 word1 word2 rights s' rv x3) (corrupt_tcb_intent thread >>= return) (do y <- as_user thread (setRegister badge_register x3);
set_notification word1 (ntfn_set_obj rv IdleNtfn)
od)
 2. \<And>word1 word2 rights s' rv x3 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q194 word1 word2 rights s' rv x3 s
 3. \<And>word1 word2 rights s' rv x3 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'194 word1 word2 rights s' rv x3 s
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 5. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 6. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (7 subgoals):
 1. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q200 word1 word2 rights s' rv x3\<rbrace> corrupt_tcb_intent thread \<lbrace>\<lambda>x _. True\<rbrace>
 2. \<And>word1 word2 rights s' rv x3. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q'200 word1 word2 rights s' rv x3\<rbrace> as_user thread (setRegister badge_register x3) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>word1 word2 rights s' rv x3 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; transform s' = s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and ?Q200 word1 word2 rights s' rv x3) s
 4. \<And>word1 word2 rights s' rv x3 s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; kheap s' word1 = Some (kernel_object.Notification rv); valid_ntfn rv s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ntfn_obj rv = ActiveNtfn x3; valid_pspace s'; valid_mdb s'; valid_ioc s'; valid_idle s'; only_idle s'; if_unsafe_then_cap s'; valid_reply_caps s'; valid_reply_masters s'; valid_global_refs s'; valid_arch_state s'; valid_irq_node s'; valid_irq_handlers s'; valid_irq_states s'; valid_machine_state s'; valid_vspace_objs s'; valid_arch_caps s'; valid_global_objs s'; valid_kernel_mappings s'; equal_kernel_mappings s'; valid_asid_map s'; valid_global_vspace_mappings s'; pspace_in_kernel_window s'; cap_refs_in_kernel_window s'; pspace_respects_device_region s'; cap_refs_respects_device_region s'; s' = s\<rbrakk> \<Longrightarrow> (valid_idle and not_idle_thread thread and valid_etcbs and ?Q'200 word1 word2 rights s' rv x3) s
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'\<rbrakk> \<Longrightarrow> \<lbrace>(=) s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) s' and ko_at (kernel_object.Notification r) word1 and valid_ntfn r\<rbrace>
 6. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 7. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'219 word1 word2 rights (transform s') s'\<rbrace> get_notification word1 \<lbrace>\<lambda>rv s. ko_at (kernel_object.Notification rv) word1 s \<and> valid_ntfn rv s\<rbrace>
 2. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> ?P'219 word1 word2 rights s s' sa
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'\<rbrakk> \<Longrightarrow> \<lbrace>?P'219 word1 word2 rights (transform s') s'\<rbrace> get_notification word1 \<lbrace>\<lambda>r. ko_at (kernel_object.Notification r) word1 and valid_state\<rbrace>
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; (ko_at (kernel_object.Notification rv) word1 and valid_state) s\<rbrakk> \<Longrightarrow> ko_at (kernel_object.Notification rv) word1 s \<and> valid_ntfn rv s
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> ?P'219 word1 word2 rights s s' sa
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ko_at (kernel_object.Notification rv) word1 s; valid_state s\<rbrakk> \<Longrightarrow> valid_ntfn rv s
 2. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> True \<and> valid_state sa
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (5 subgoals):
 1. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ko_at (kernel_object.Notification rv) word1 s; valid_state s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ko_at (kernel_object.Notification rv) word1 s; valid_state s\<rbrakk> \<Longrightarrow> kheap s (?epptr242 word1 word2 rights s' rv s) = Some (kernel_object.Notification rv)
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> True \<and> valid_state sa
 4. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 5. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (4 subgoals):
 1. \<And>word1 word2 rights s' rv s. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; valid_state s'; cur_tcb s'; not_idle_thread thread s'; st_tcb_at active thread s'; valid_etcbs s'; ko_at (kernel_object.Notification rv) word1 s; valid_state s\<rbrakk> \<Longrightarrow> kheap s (?epptr242 word1 word2 rights s' rv s) = Some (kernel_object.Notification rv)
 2. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> True \<and> valid_state sa
 3. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 4. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal (3 subgoals):
 1. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> s' = sa \<and> True \<and> valid_state sa
 2. \<And>word1 word2 rights s s' sa. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; s' = sa\<rbrakk> \<Longrightarrow> \<lbrace>(=) sa\<rbrace> get_notification word1 \<lbrace>\<lambda>r. (=) sa\<rbrace>
 3. \<And>word1 word2 rights s s'. \<lbrakk>cap = cdl_cap.NotificationCap word1 word2 rights; cap' = cap.NotificationCap word1 word2 rights; s = transform s'; True; (valid_state and cur_tcb and not_idle_thread thread and st_tcb_at active thread and valid_etcbs) s'; False\<rbrakk> \<Longrightarrow> no_fail ((=) s') (get_notification word1) proof (prove)
goal:
No subgoals!