theory IpcCancel_R

lemma cancelBadgedSends_invs[wp]:
  notes if_cong[cong del]
  shows
  "\<lbrace>invs'\<rbrace> cancelBadgedSends epptr badge \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: cancelBadgedSends_def) apply (rule hoare_seq_ext [OF _ get_ep_sp']) apply (case_tac ep, simp_all) apply ((wp | simp)+)[2] apply (subst bind_assoc [where g="\<lambda>_. rescheduleRequired",
                           symmetric])+ apply (rule hoare_seq_ext
                [OF rescheduleRequired_all_invs_but_ct_not_inQ]) apply (simp add: list_case_return cong: list.case_cong) apply (rule hoare_pre, wp valid_irq_node_lift irqs_masked_lift) apply simp apply (rule hoare_strengthen_post,
           rule cancelBadgedSends_filterM_helper[where epptr=epptr]) apply (clarsimp simp: ep_redux_simps3 fun_upd_def[symmetric]) apply (clarsimp simp add: valid_ep'_def split: list.split) apply blast apply (wp valid_irq_node_lift irqs_masked_lift | wp (once) sch_act_sane_lift)+ apply (clarsimp simp: invs'_def valid_state'_def
                        valid_ep'_def fun_upd_def[symmetric]
                        obj_at'_weakenE[OF _ TrueI]) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: valid_obj'_def valid_ep'_def projectKOs) apply (frule if_live_then_nonz_capD', simp add: obj_at'_real_def) apply (clarsimp simp: projectKOs) apply (frule(1) sym_refs_ko_atD') apply (clarsimp simp add: fun_upd_idem
                            st_tcb_at_refs_of_rev') apply (drule (1) bspec, drule st_tcb_at_state_refs_ofD', clarsimp) apply (fastforce simp: set_eq_subset tcb_bound_refs'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> cancelBadgedSends epptr badge \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs'\<rbrace> do ep <- getEndpoint epptr;
case ep of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return ()
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep. \<lbrace>invs' and ko_at' ep epptr\<rbrace> case ep of Structures_H.endpoint.SendEP queue \<Rightarrow> do setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- swp filterM queue (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t;
return False
od else return True
od);
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
setEndpoint epptr ep';
rescheduleRequired
od | _ \<Rightarrow> return () \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep x1. ep = Structures_H.endpoint.RecvEP x1 \<Longrightarrow> \<lbrace>invs' and ko_at' (Structures_H.endpoint.RecvEP x1) epptr\<rbrace> return () \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<lbrace>invs' and ko_at' Structures_H.endpoint.IdleEP epptr\<rbrace> return () \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr\<rbrace> do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3;
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
y <- setEndpoint epptr ep';
rescheduleRequired
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr\<rbrace> do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3;
ep' <- case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue';
y <- setEndpoint epptr ep';
rescheduleRequired
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr\<rbrace> do _ <- do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3;
(case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue') >>= setEndpoint epptr
od;
rescheduleRequired
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr\<rbrace> do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3;
(case queue' of [] \<Rightarrow> return Structures_H.endpoint.IdleEP | a # list \<Rightarrow> return $ Structures_H.endpoint.SendEP queue') >>= setEndpoint epptr
od \<lbrace>\<lambda>_ s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> untyped_ranges_zero' s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr\<rbrace> do y <- setEndpoint epptr Structures_H.endpoint.IdleEP;
queue' <- filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3;
setEndpoint epptr (case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list))
od \<lbrace>\<lambda>_ s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>uu_\<in>set (ksDomSchedule s). dschDomain uu_ \<le> maxDomain \<and> 0 < dschLength uu_) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>ep x3 y. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B22 ep x3 y\<rbrace> filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3 \<lbrace>\<lambda>queue' s. valid_pspace' s \<and> valid_ep' (case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' (case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)))) \<and> (if_live_then_nonz_cap' s \<and> ((case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s)) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>uu_\<in>set (ksDomSchedule s). dschDomain uu_ \<le> maxDomain \<and> 0 < dschLength uu_) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s\<rbrace>
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?Q18 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B22 ep x3\<rbrace>
 3. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> ?Q18 ep x3 s proof (prove)
goal (3 subgoals):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?B22 (Structures_H.endpoint.SendEP x3) x3 ()\<rbrace> filterM (\<lambda>t. do st <- getThreadState t;
if blockingIPCBadge st = badge then do y <- setThreadState Structures_H.thread_state.Restart t;
y <- tcbSchedEnqueue t;
return False
od else return True
od) x3 \<lbrace>\<lambda>queue' s. valid_pspace' s \<and> valid_ep' (case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (\<lambda>a. if a = epptr then ep_q_refs_of' (case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) else state_refs_of' s a) \<and> if_live_then_nonz_cap' s \<and> ((case queue' of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>uu_\<in>set (ksDomSchedule s). dschDomain uu_ \<le> maxDomain \<and> 0 < dschLength uu_) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s\<rbrace>
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?Q18 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>?B22 ep x3\<rbrace>
 3. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> ?Q18 ep x3 s proof (prove)
goal (3 subgoals):
 1. \<And>ep x3 rv s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> ex_nonz_cap_to' epptr s \<and> ep_at' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set rv \<times> {EPSend})) \<and> distinct rv \<and> distinct x3 \<and> set rv \<subseteq> set x3 \<and> (\<forall>x\<in>set x3. tcb_at' x s)\<rbrakk> \<Longrightarrow> valid_pspace' s \<and> valid_ep' (case rv of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (\<lambda>a. if a = epptr then ep_q_refs_of' (case rv of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) else state_refs_of' s a) \<and> if_live_then_nonz_cap' s \<and> ((case rv of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>uu_\<in>set (ksDomSchedule s). dschDomain uu_ \<le> maxDomain \<and> 0 < dschLength uu_) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?Q18 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a b. valid_pspace' b \<and> sch_act_wf (ksSchedulerAction b) b \<and> Invariants_H.valid_queues b \<and> if_live_then_nonz_cap' b \<and> if_unsafe_then_cap' b \<and> valid_idle' b \<and> valid_global_refs' b \<and> valid_arch_state' b \<and> valid_irq_node' (irq_node' b) b \<and> valid_irq_handlers' b \<and> valid_irq_states' b \<and> irqs_masked' b \<and> valid_machine_state' b \<and> cur_tcb' b \<and> valid_queues' b \<and> ct_idle_or_in_cur_domain' b \<and> valid_pde_mappings' b \<and> pspace_domain_valid b \<and> ksCurDomain b \<le> maxDomain \<and> ksDomSchedule b \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule b). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule b = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx b < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' b \<and> ex_nonz_cap_to' epptr b \<and> ep_at' epptr b \<and> sym_refs ((state_refs_of' b)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. state_refs_of' b y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' b y. snd r = TCBBound}) \<and> distinct x3\<rbrace>
 3. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> ?Q18 ep x3 s proof (prove)
goal (3 subgoals):
 1. \<And>x3 rv s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; valid_machine_state' s; cur_tcb' s; valid_queues' s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs ((state_refs_of' s)(epptr := set rv \<times> {EPSend})); distinct rv; distinct x3; set rv \<subseteq> set x3; \<forall>x\<in>set x3. tcb_at' x s\<rbrakk> \<Longrightarrow> valid_ep' (case rv of [] \<Rightarrow> Structures_H.endpoint.IdleEP | a # list \<Rightarrow> Structures_H.endpoint.SendEP (a # list)) s
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?Q18 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a b. valid_pspace' b \<and> sch_act_wf (ksSchedulerAction b) b \<and> Invariants_H.valid_queues b \<and> if_live_then_nonz_cap' b \<and> if_unsafe_then_cap' b \<and> valid_idle' b \<and> valid_global_refs' b \<and> valid_arch_state' b \<and> valid_irq_node' (irq_node' b) b \<and> valid_irq_handlers' b \<and> valid_irq_states' b \<and> irqs_masked' b \<and> valid_machine_state' b \<and> cur_tcb' b \<and> valid_queues' b \<and> ct_idle_or_in_cur_domain' b \<and> valid_pde_mappings' b \<and> pspace_domain_valid b \<and> ksCurDomain b \<le> maxDomain \<and> ksDomSchedule b \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule b). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule b = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx b < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' b \<and> ex_nonz_cap_to' epptr b \<and> ep_at' epptr b \<and> sym_refs ((state_refs_of' b)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. state_refs_of' b y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' b y. snd r = TCBBound}) \<and> distinct x3\<rbrace>
 3. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> ?Q18 ep x3 s proof (prove)
goal (3 subgoals):
 1. \<And>x3 s x21 x22 t. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; valid_machine_state' s; cur_tcb' s; valid_queues' s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs ((state_refs_of' s)(epptr := insert (x21, EPSend) (set x22 \<times> {EPSend}))); distinct x3; \<forall>x\<in>set x3. tcb_at' x s; t \<in> set x22; x21 \<notin> set x22; distinct x22; x21 \<in> set x3; set x22 \<subseteq> set x3\<rbrakk> \<Longrightarrow> tcb_at' t s
 2. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?Q18 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a b. valid_pspace' b \<and> sch_act_wf (ksSchedulerAction b) b \<and> Invariants_H.valid_queues b \<and> if_live_then_nonz_cap' b \<and> if_unsafe_then_cap' b \<and> valid_idle' b \<and> valid_global_refs' b \<and> valid_arch_state' b \<and> valid_irq_node' (irq_node' b) b \<and> valid_irq_handlers' b \<and> valid_irq_states' b \<and> irqs_masked' b \<and> valid_machine_state' b \<and> cur_tcb' b \<and> valid_queues' b \<and> ct_idle_or_in_cur_domain' b \<and> valid_pde_mappings' b \<and> pspace_domain_valid b \<and> ksCurDomain b \<le> maxDomain \<and> ksDomSchedule b \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule b). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule b = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx b < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' b \<and> ex_nonz_cap_to' epptr b \<and> ep_at' epptr b \<and> sym_refs ((state_refs_of' b)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. state_refs_of' b y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' b y. snd r = TCBBound}) \<and> distinct x3\<rbrace>
 3. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> ?Q18 ep x3 s proof (prove)
goal (2 subgoals):
 1. \<And>ep x3. ep = Structures_H.endpoint.SendEP x3 \<Longrightarrow> \<lbrace>?Q18 ep x3\<rbrace> setEndpoint epptr Structures_H.endpoint.IdleEP \<lbrace>\<lambda>a b. valid_pspace' b \<and> sch_act_wf (ksSchedulerAction b) b \<and> Invariants_H.valid_queues b \<and> if_live_then_nonz_cap' b \<and> if_unsafe_then_cap' b \<and> valid_idle' b \<and> valid_global_refs' b \<and> valid_arch_state' b \<and> valid_irq_node' (irq_node' b) b \<and> valid_irq_handlers' b \<and> valid_irq_states' b \<and> irqs_masked' b \<and> valid_machine_state' b \<and> cur_tcb' b \<and> valid_queues' b \<and> ct_idle_or_in_cur_domain' b \<and> valid_pde_mappings' b \<and> pspace_domain_valid b \<and> ksCurDomain b \<le> maxDomain \<and> ksDomSchedule b \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule b). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule b = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx b < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' b \<and> ex_nonz_cap_to' epptr b \<and> ep_at' epptr b \<and> sym_refs ((state_refs_of' b)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. state_refs_of' b y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' b y. snd r = TCBBound}) \<and> distinct x3\<rbrace>
 2. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> ?Q18 ep x3 s proof (prove)
goal (1 subgoal):
 1. \<And>ep x3 s. \<lbrakk>ep = Structures_H.endpoint.SendEP x3; (invs' and ko_at' (Structures_H.endpoint.SendEP x3) epptr) s\<rbrakk> \<Longrightarrow> (valid_pspace' and valid_ep' Structures_H.endpoint.IdleEP) s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> (if_live_then_nonz_cap' s \<and> (Structures_H.endpoint.IdleEP \<noteq> Structures_H.endpoint.IdleEP \<longrightarrow> ex_nonz_cap_to' epptr s)) \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> irqs_masked' s \<and> valid_machine_state' s \<and> cur_tcb' s \<and> valid_queues' s \<and> ct_idle_or_in_cur_domain' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> ksDomSchedule s \<noteq> [] \<and> (\<forall>x\<in>set (ksDomSchedule s). dschDomain x \<le> maxDomain \<and> 0 < dschLength x) \<and> ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)) \<and> untyped_ranges_zero' s \<and> ex_nonz_cap_to' epptr s \<and> ep_at' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := ep_q_refs_of' Structures_H.endpoint.IdleEP, epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. ((state_refs_of' s)(epptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) y = insert (epptr, TCBBlockedSend) {r \<in> ((state_refs_of' s)(epptr := ep_q_refs_of' Structures_H.endpoint.IdleEP)) y. snd r = TCBBound}) \<and> distinct x3 proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound})) \<and> distinct x3 proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; \<exists>k. k = Structures_H.endpoint.SendEP x3 \<and> ((\<forall>ko. projectKO_opt ko = Some k \<longrightarrow> injectKO k = ko) \<longrightarrow> valid_obj' (injectKO k) s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound})) \<and> distinct x3 proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound})) proof (prove)
goal (2 subgoals):
 1. \<And>x3 s obj. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; projectKO_opt obj = Some (Structures_H.endpoint.SendEP x3); ksPSpace s epptr = Some obj; is_aligned epptr (objBitsKO obj)\<rbrakk> \<Longrightarrow> live' obj
 2. \<And>x3 s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; ex_nonz_cap_to' epptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound})) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; ex_nonz_cap_to' epptr s\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound})) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; ex_nonz_cap_to' epptr s; state_refs_of' s epptr = refs_of' (injectKO (Structures_H.endpoint.SendEP x3)) \<and> (\<forall>(x, tp)\<in>refs_of' (injectKO (Structures_H.endpoint.SendEP x3)). ko_wp_at' (\<lambda>ko. (epptr, symreftype tp) \<in> refs_of' ko) x s)\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' epptr s \<and> sym_refs ((state_refs_of' s)(epptr := set x3 \<times> {EPSend})) \<and> (\<forall>y\<in>set x3. y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound})) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s y. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; ex_nonz_cap_to' epptr s; y \<in> set x3; state_refs_of' s epptr = set x3 \<times> {EPSend}; \<forall>x\<in>set x3. st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s\<rbrakk> \<Longrightarrow> y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) proof (prove)
goal (1 subgoal):
 1. \<And>x3 s y ntfnptr. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; ko_at' (Structures_H.endpoint.SendEP x3) epptr s; x3 \<noteq> []; \<forall>t\<in>set x3. tcb_at' t s; distinct x3; ex_nonz_cap_to' epptr s; y \<in> set x3; state_refs_of' s epptr = set x3 \<times> {EPSend}; obj_at' (tcb_ntfn_is_bound' ntfnptr) y s; state_refs_of' s y = insert (epptr, TCBBlockedSend) (tcb_bound_refs' ntfnptr)\<rbrakk> \<Longrightarrow> y \<noteq> epptr \<and> (y \<noteq> epptr \<longrightarrow> insert (epptr, TCBBlockedSend) (tcb_bound_refs' ntfnptr) = insert (epptr, TCBBlockedSend) {r. (r = (epptr, TCBBlockedSend) \<or> r \<in> tcb_bound_refs' ntfnptr) \<and> snd r = TCBBound}) proof (prove)
goal:
No subgoals!