theory Ipc_DR

lemma receive_blocked_waiting_syncs:
  "\<lbrakk>valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn);
    ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; receive_blocked (tcb_state aa)\<rbrakk>
   \<Longrightarrow> get_waiting_sync_bound_ntfn_threads ntfnptr (transform s) = {a}" apply (clarsimp simp: get_waiting_sync_bound_ntfn_threads_def) apply (frule get_notification_pick, simp) apply (clarsimp simp: valid_ntfn_abstract_def ntfn_bound_set_def get_tcb_def
                 split: Structures_A.kernel_object.splits option.splits) apply (rule set_eqI) apply clarsimp apply (rule iffI) apply (clarsimp) apply (rule_tac x=aa in exI) apply (clarsimp simp: valid_state_def valid_pspace_def) apply (frule (3) ntfn_bound_tcb_at[where P="\<lambda>a. a = Some ntfnptr"], simp) apply (clarsimp simp: pred_tcb_at_def obj_at_def) apply (clarsimp simp: transform_def transform_objects_def restrict_map_def map_add_def
                  split: option.splits) apply (subst (asm) handy_if_lemma)+ apply clarsimp apply (case_tac "x \<noteq> idle_thread s") apply (clarsimp simp: transform_object_def
                   split: Structures_A.kernel_object.splits ARM_A.arch_kernel_obj.splits
                          option.splits nat.splits) apply (frule_tac ptr=x in valid_etcbs_tcb_etcb, simp+) apply (clarsimp simp add: transform_tcb_def tcb_pending_op_slot_def
                              tcb_boundntfn_slot_def infer_tcb_bound_notification_def
                       split: option.splits) apply (frule_tac tcb="x2a" in  bound_tcb_fold, simp) apply (frule (3) bound_tcb_bound_notification_at) apply clarsimp apply clarsimp apply clarsimp apply (frule_tac tcb=t in bound_tcb_fold, simp) apply (clarsimp simp: valid_state_def valid_pspace_def) apply (frule (3) bound_tcb_bound_notification_at) apply clarsimp apply (drule get_tcb_rev) apply (frule (1) valid_etcbs_get_tcb_get_etcb, clarsimp) apply (clarsimp simp: transform_def) apply (frule (1) transform_objects_tcb) apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) apply (clarsimp simp: transform_tcb_def tcb_pending_op_slot_def tcb_boundntfn_slot_def
                        infer_tcb_pending_op_def infer_tcb_bound_notification_def receive_blocked_def
                 split: Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; receive_blocked (tcb_state aa)\<rbrakk> \<Longrightarrow> get_waiting_sync_bound_ntfn_threads ntfnptr (transform s) = {a} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; receive_blocked (tcb_state aa)\<rbrakk> \<Longrightarrow> {x. \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)} = {a} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; receive_blocked (tcb_state aa); valid_ntfn_abstract ntfn ntfnptr s\<rbrakk> \<Longrightarrow> {x. \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)} = {a} proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa)\<rbrakk> \<Longrightarrow> {x. \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr} proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa)\<rbrakk> \<Longrightarrow> (x \<in> {x. \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)}) = (x \<in> {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa)\<rbrakk> \<Longrightarrow> (\<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)) = (\<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr)\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); cdl_objects (transform s) x = Some (Tcb ab); cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)\<rbrakk> \<Longrightarrow> \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); cdl_objects (transform s) x = Some (Tcb ab); cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa) \<and> tcb_bound_notification aa = Some ntfnptr
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); cdl_objects (transform s) x = Some (Tcb ab); cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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> kheap s x = Some (TCB aa) \<and> tcb_bound_notification aa = Some ntfnptr
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); cdl_objects (transform s) x = Some (Tcb ab); cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; bound_tcb_at (\<lambda>a. a = Some ntfnptr) a s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa) \<and> tcb_bound_notification aa = Some ntfnptr
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); cdl_objects (transform s) x = Some (Tcb ab); cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = None; (if x \<noteq> idle_thread s then Some cdl_object.Untyped else None) = Some (Tcb ab)\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ab ep_id can_grant. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = None; x \<noteq> idle_thread s \<and> cdl_object.Untyped = Tcb ab\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (4 subgoals):
 1. \<And>x ab ep_id can_grant x2a. \<lbrakk>x \<noteq> idle_thread s; cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB x2a); ekheap s x = None; undefined = Tcb ab\<rbrakk> \<Longrightarrow> x2a = aa
 2. \<And>x ab ep_id can_grant x2a x2b. \<lbrakk>x \<noteq> idle_thread s; cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB x2a); ekheap s x = Some x2b; transform_tcb (machine_state s) x x2a x2b = Tcb ab\<rbrakk> \<Longrightarrow> x2a = aa
 3. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 4. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ab ep_id can_grant x2a x2b. \<lbrakk>x \<noteq> idle_thread s; cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB x2a); ekheap s x = Some x2b; transform_tcb (machine_state s) x x2a x2b = Tcb ab\<rbrakk> \<Longrightarrow> x2a = aa
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ep_id can_grant x2a x2b. \<lbrakk>x \<noteq> idle_thread s; infer_tcb_pending_op x (tcb_state x2a) = PendingSyncRecvCap ep_id False can_grant; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB x2a); ekheap s x = Some x2b; tcb_bound_notification x2a = Some ntfnptr\<rbrakk> \<Longrightarrow> x2a = aa
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ep_id can_grant x2a x2b. \<lbrakk>x \<noteq> idle_thread s; infer_tcb_pending_op x (tcb_state x2a) = PendingSyncRecvCap ep_id False can_grant; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB x2a); ekheap s x = Some x2b; tcb_bound_notification x2a = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s\<rbrakk> \<Longrightarrow> x2a = aa
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (3 subgoals):
 1. \<And>x ep_id can_grant x2a x2b. \<lbrakk>x \<noteq> idle_thread s; infer_tcb_pending_op x (tcb_state x2a) = PendingSyncRecvCap ep_id False can_grant; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB x2a); ekheap s x = Some x2b; tcb_bound_notification x2a = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> x2a = aa
 2. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 3. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>x ab ep_id can_grant x2. \<lbrakk>cdl_tcb_caps ab tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr); cdl_tcb_caps ab tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant); valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; tcb_bound_notification aa = Some ntfnptr; receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); (if x \<noteq> idle_thread s then kheap s x else None) = Some x2; transform_object (machine_state s) x (if x \<noteq> idle_thread s then ekheap s x else None) x2 = Tcb ab; \<not> x \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> kheap s x = Some (TCB aa)
 2. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); \<exists>t. kheap s x = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB t); tcb_bound_notification t = Some ntfnptr\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>receive_blocked (tcb_state aa); valid_state s; valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB t); tcb_bound_notification t = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB t); tcb_bound_notification t = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>x t. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); ntfn_bound_tcb ntfn = Some a; {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); kheap s x = Some (TCB t); tcb_bound_notification t = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) x s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some x\<rbrakk> \<Longrightarrow> \<exists>a. cdl_objects (transform s) x = Some (Tcb a) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps a tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps a tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; kheap s a = Some (TCB aa); tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a\<rbrakk> \<Longrightarrow> \<exists>aa. cdl_objects (transform s) a = Some (Tcb aa) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps aa tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps aa tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa\<rbrakk> \<Longrightarrow> \<exists>aa. cdl_objects (transform s) a = Some (Tcb aa) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps aa tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps aa tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; get_etcb a s = Some etcb\<rbrakk> \<Longrightarrow> \<exists>aa. cdl_objects (transform s) a = Some (Tcb aa) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps aa tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps aa tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; get_etcb a s = Some etcb\<rbrakk> \<Longrightarrow> \<exists>aa. transform_objects s a = Some (Tcb aa) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps aa tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps aa tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (2 subgoals):
 1. \<And>etcb. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; get_etcb a s = Some etcb\<rbrakk> \<Longrightarrow> a \<noteq> idle_thread s
 2. \<And>etcb. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; get_etcb a s = Some etcb; transform_objects s a = Some (transform_tcb (machine_state s) a aa etcb)\<rbrakk> \<Longrightarrow> \<exists>aa. transform_objects s a = Some (Tcb aa) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps aa tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps aa tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal (1 subgoal):
 1. \<And>etcb. \<lbrakk>receive_blocked (tcb_state aa); valid_etcbs s; kheap s ntfnptr = Some (kernel_object.Notification ntfn); {a} = {tcb. \<exists>t. kheap s tcb = Some (TCB t) \<and> tcb_bound_notification t = Some ntfnptr}; case ntfn_obj ntfn of WaitingNtfn queue \<Rightarrow> queue \<noteq> [] \<and> set queue = ntfn_waiting_set ntfnptr s \<and> (\<forall>p'. kheap s ntfnptr = kheap s p' \<longrightarrow> ntfnptr = p') | _ \<Rightarrow> none_is_waiting_ntfn ntfnptr s; tcb_bound_notification aa = Some ntfnptr; bound_tcb_at (\<lambda>ntfn. ntfn = Some ntfnptr) a s; valid_objs s; pspace_aligned s; pspace_distinct s; if_live_then_nonz_cap s; zombies_final s; sym_refs (state_refs_of s); sym_refs (state_hyp_refs_of 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; ntfn_bound_tcb ntfn = Some a; get_tcb a s = Some aa; get_etcb a s = Some etcb; transform_objects s a = Some (transform_tcb (machine_state s) a aa etcb)\<rbrakk> \<Longrightarrow> \<exists>aa. transform_objects s a = Some (Tcb aa) \<and> (\<exists>ep_id can_grant. cdl_tcb_caps aa tcb_pending_op_slot = Some (PendingSyncRecvCap ep_id False can_grant)) \<and> cdl_tcb_caps aa tcb_boundntfn_slot = Some (BoundNotificationCap ntfnptr) proof (prove)
goal:
No subgoals!