theory IpcCancel_R

lemma cancelBadgedSends_filterM_helper':
  notes if_cong[cong del]
  shows
  "\<forall>ys.
   \<lbrace>\<lambda>s. all_invs_but_sym_refs_ct_not_inQ' s
           \<and> ex_nonz_cap_to' epptr s \<and> ep_at' epptr s
           \<and> sym_refs ((state_refs_of' s) (epptr := set (xs @ ys) \<times> {EPSend}))
           \<and> (\<forall>y \<in> set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)}
                                       \<union> {r \<in> state_refs_of' s y. snd r = TCBBound})
           \<and> distinct (xs @ ys)\<rbrace>
      filterM (\<lambda>t. do st \<leftarrow> getThreadState t;
                      if blockingIPCBadge st = badge then
                        do y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                           y \<leftarrow> tcbSchedEnqueue t;
                           return False
                        od
                      else return True
                   od) xs
   \<lbrace>\<lambda>rv s. all_invs_but_sym_refs_ct_not_inQ' s
           \<and> ex_nonz_cap_to' epptr s \<and> ep_at' epptr s
           \<and> sym_refs ((state_refs_of' s) (epptr := (set rv \<union> set ys) \<times> {EPSend}))
           \<and> (\<forall>y \<in> set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)}
                                   \<union> {r \<in> state_refs_of' s y. snd r = TCBBound})
           \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x \<in> set xs. tcb_at' x s)\<rbrace>" apply (rule_tac xs=xs in rev_induct) apply clarsimp apply wp apply clarsimp apply (clarsimp simp: filterM_append bind_assoc simp del: set_append distinct_append) apply (drule spec, erule hoare_seq_ext[rotated]) apply (rule hoare_seq_ext [OF _ gts_inv']) apply (rule hoare_pre) apply (wp valid_irq_node_lift hoare_vcg_const_Ball_lift sts_sch_act'
             sch_act_wf_lift valid_irq_handlers_lift'' cur_tcb_lift irqs_masked_lift
             sts_st_tcb' sts_valid_queues setThreadState_not_st
             tcbSchedEnqueue_not_st
             untyped_ranges_zero_lift
        | clarsimp simp: cteCaps_of_def o_def)+ apply (frule insert_eqD, frule state_refs_of'_elemD) apply (clarsimp simp: valid_tcb_state'_def st_tcb_at_refs_of_rev') apply (frule pred_tcb_at') apply (rule conjI[rotated], blast) apply clarsimp apply (intro conjI) apply (clarsimp simp: valid_pspace'_def valid_tcb'_def elim!: valid_objs_valid_tcbE dest!: st_tcb_ex_cap'') apply (fastforce dest!: st_tcb_ex_cap'') apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply (erule delta_sym_refs) apply (fastforce elim!: obj_atE'
                      simp: state_refs_of'_def projectKOs tcb_bound_refs'_def
                            subsetD symreftype_inverse'
                     split: if_split_asm)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 (xs @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ ys)\<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) xs \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 ([] @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ([] @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ([] @ ys)\<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) [] \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct ([] @ ys) \<and> set rv \<subseteq> set [] \<and> (\<forall>x\<in>set []. tcb_at' x s)\<rbrace>
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 (xs @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ ys)\<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) xs \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ((xs @ [x]) @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ((xs @ [x]) @ ys)\<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) (xs @ [x]) \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ys. \<lbrace>\<lambda>s. 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 (\<lambda>a. if a = epptr then set ys \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ys\<rbrace> return [] \<lbrace>\<lambda>rv s. 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 (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct ys \<and> rv = []\<rbrace>
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 (xs @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ ys)\<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) xs \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ((xs @ [x]) @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ((xs @ [x]) @ ys)\<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) (xs @ [x]) \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>ys s. 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 (\<lambda>a. if a = epptr then set ys \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ys \<Longrightarrow> 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 (\<lambda>a. if a = epptr then (set [] \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct [] \<and> distinct ys \<and> [] = []
 2. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 (xs @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ ys)\<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) xs \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ((xs @ [x]) @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ((xs @ [x]) @ ys)\<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) (xs @ [x]) \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs. \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 (xs @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ ys)\<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) xs \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> \<Longrightarrow> \<forall>ys. \<lbrace>\<lambda>s. (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> valid_dom_schedule' s \<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 ((xs @ [x]) @ ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ((xs @ [x]) @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct ((xs @ [x]) @ ys)\<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) (xs @ [x]) \<lbrace>\<lambda>rv s. (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> valid_dom_schedule' s \<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 \<union> set ys) \<times> {EPSend})) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} \<union> {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct ((xs @ [x]) @ ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys. \<forall>ys. \<lbrace>\<lambda>s. 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 (\<lambda>a. if a = epptr then set (xs @ ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set (xs @ ys). state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ ys)\<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) xs \<lbrace>\<lambda>rv s. 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 (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ ys) \<and> set rv \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> \<Longrightarrow> \<lbrace>\<lambda>s. 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 (\<lambda>a. if a = epptr then set (xs @ x # ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set (xs @ x # ys). state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct (xs @ x # ys)\<rbrace> do xs' <- 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) xs;
xa <- getThreadState x;
b <- if blockingIPCBadge xa = badge then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True;
return (xs' @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. 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 (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa. \<lbrace>\<lambda>s. 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 (\<lambda>a. if a = epptr then (set xa \<union> set (x # ys)) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set (x # ys). state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct xa \<and> distinct (xs @ x # ys) \<and> set xa \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> do xb <- getThreadState x;
b <- if blockingIPCBadge xb = badge then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True;
return (xa @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. 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 (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb. \<lbrace>\<lambda>s. 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 (\<lambda>a. if a = epptr then (set xa \<union> set (x # ys)) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set (x # ys). state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct xa \<and> distinct (xs @ x # ys) \<and> set xa \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s)\<rbrace> do b <- if blockingIPCBadge xb = badge then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True;
return (xa @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. 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 (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x xs ys xa xb. \<lbrace>?Q69 x xs ys xa xb\<rbrace> do b <- if blockingIPCBadge xb = badge then do y <- setThreadState Structures_H.thread_state.Restart x;
y <- tcbSchedEnqueue x;
return False
od else return True;
return (xa @ (if b then [x] else []))
od \<lbrace>\<lambda>rv s. 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 (\<lambda>a. if a = epptr then (set rv \<union> set ys) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct rv \<and> distinct (xs @ x # ys) \<and> set rv \<subseteq> set (xs @ [x]) \<and> (\<forall>x\<in>set (xs @ [x]). tcb_at' x s)\<rbrace>
 2. \<And>x xs ys xa xb s. 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 (\<lambda>a. if a = epptr then (set xa \<union> set (x # ys)) \<times> {EPSend} else state_refs_of' s a) \<and> (\<forall>y\<in>set (x # ys). state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}) \<and> distinct xa \<and> distinct (xs @ x # ys) \<and> set xa \<subseteq> set xs \<and> (\<forall>x\<in>set xs. tcb_at' x s) \<Longrightarrow> ?Q69 x xs ys xa xb s proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s\<rbrakk> \<Longrightarrow> (blockingIPCBadge xb = badge \<longrightarrow> tcb_at' x s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> x \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a) \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) \<and> (blockingIPCBadge xb \<noteq> badge \<longrightarrow> x \<notin> set xa \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; ko_wp_at' (\<lambda>obj. (epptr, TCBBlockedSend) \<in> refs_of' obj) x s\<rbrakk> \<Longrightarrow> (blockingIPCBadge xb = badge \<longrightarrow> tcb_at' x s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> x \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a) \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) \<and> (blockingIPCBadge xb \<noteq> badge \<longrightarrow> x \<notin> set xa \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; 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> (blockingIPCBadge xb = badge \<longrightarrow> tcb_at' x s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> x \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a) \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) \<and> (blockingIPCBadge xb \<noteq> badge \<longrightarrow> x \<notin> set xa \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s\<rbrakk> \<Longrightarrow> (blockingIPCBadge xb = badge \<longrightarrow> tcb_at' x s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> x \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a) \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) \<and> (blockingIPCBadge xb \<noteq> badge \<longrightarrow> x \<notin> set xa \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s) proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s\<rbrakk> \<Longrightarrow> blockingIPCBadge xb = badge \<longrightarrow> tcb_at' x s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> x \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a) \<and> set xa \<subseteq> insert x (set xs) \<and> tcb_at' x s proof (prove)
goal (1 subgoal):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> x \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a) \<and> set xa \<subseteq> insert x (set xs) proof (prove)
goal (5 subgoals):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> valid_objs' s
 2. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' x s
 3. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> x \<noteq> ksIdleThread s
 4. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a)
 5. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> set xa \<subseteq> insert x (set xs) proof (prove)
goal (4 subgoals):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> ex_nonz_cap_to' x s
 2. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> x \<noteq> ksIdleThread s
 3. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a)
 4. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> set xa \<subseteq> insert x (set xs) proof (prove)
goal (3 subgoals):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> x \<noteq> ksIdleThread s
 2. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a)
 3. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> set xa \<subseteq> insert x (set xs) proof (prove)
goal (2 subgoals):
 1. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = epptr then (set xa \<union> set ys) \<times> {EPSend} else if a = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s a)
 2. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> set xa \<subseteq> insert x (set xs) proof (prove)
goal (3 subgoals):
 1. \<And>x xs ys xa xb s xc y tp. \<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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb; (y, tp) \<in> (if xc = epptr then (set xa \<union> set ys) \<times> {EPSend} else if xc = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s xc); (y, tp) \<notin> (if xc = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s xc)\<rbrakk> \<Longrightarrow> (xc, symreftype tp) \<in> (if y = epptr then (set xa \<union> set ys) \<times> {EPSend} else if y = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s y)
 2. \<And>x xs ys xa xb s xc y tp. \<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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb; (y, tp) \<in> (if xc = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s xc); (y, tp) \<notin> (if xc = epptr then (set xa \<union> set ys) \<times> {EPSend} else if xc = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s xc)\<rbrakk> \<Longrightarrow> (xc, symreftype tp) \<notin> (if y = epptr then (set xa \<union> set ys) \<times> {EPSend} else if y = x then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s y)
 3. \<And>x xs ys xa xb 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_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); ex_nonz_cap_to' epptr s; ep_at' epptr s; sym_refs (\<lambda>a. if a = epptr then insert (x, EPSend) ((set xa \<union> set ys) \<times> {EPSend}) else state_refs_of' s a); state_refs_of' s x = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s x. snd r = TCBBound}; \<forall>y\<in>set ys. state_refs_of' s y = insert (epptr, TCBBlockedSend) {r \<in> state_refs_of' s y. snd r = TCBBound}; distinct xa; distinct xs; x \<notin> set ys; distinct ys; x \<notin> set xs; set xs \<inter> set ys = {}; set xa \<subseteq> set xs; \<forall>x\<in>set xs. tcb_at' x s; (epptr, TCBBlockedSend) \<in> state_refs_of' s x; st_tcb_at' (\<lambda>ts. \<exists>a b c d. ts = Structures_H.thread_state.BlockedOnSend epptr a b c d) x s; tcb_at' x s; badge = blockingIPCBadge xb\<rbrakk> \<Longrightarrow> set xa \<subseteq> insert x (set xs) proof (prove)
goal:
No subgoals!