theory IpcCancel_R

lemma cancel_all_invs'_helper:
  "\<lbrace>all_invs_but_sym_refs_ct_not_inQ' and (\<lambda>s. \<forall>x \<in> set q. tcb_at' x s)
         and (\<lambda>s. sym_refs (\<lambda>x. if x \<in> set q then {r \<in> state_refs_of' s x. snd r = TCBBound}
                                else state_refs_of' s x)
                \<and>  (\<forall>x \<in> set q. ex_nonz_cap_to' x s))\<rbrace>
     mapM_x (\<lambda>t. do
                   y \<leftarrow> setThreadState Structures_H.thread_state.Restart t;
                   tcbSchedEnqueue t
                 od) q
   \<lbrace>\<lambda>rv. all_invs_but_ct_not_inQ'\<rbrace>" apply (rule mapM_x_inv_wp2) apply clarsimp apply (rule hoare_pre) apply (wp valid_irq_node_lift valid_irq_handlers_lift'' irqs_masked_lift
             hoare_vcg_const_Ball_lift untyped_ranges_zero_lift
             sts_valid_queues sts_st_tcb' setThreadState_not_st
        | simp add: cteCaps_of_def o_def)+ apply (unfold fun_upd_apply Invariants_H.tcb_st_refs_of'_simps) apply clarsimp apply (intro conjI) apply (clarsimp simp: valid_tcb_state'_def global'_no_ex_cap
                 elim!: rsubst[where P=sym_refs]
                 dest!: set_mono_suffix
                intro!: ext
       | (drule (1) bspec, clarsimp simp: valid_pspace'_def valid_tcb'_def elim!: valid_objs_valid_tcbE))+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s) and (\<lambda>s. sym_refs (\<lambda>x. if x \<in> set q then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set q. ex_nonz_cap_to' x s))\<rbrace> mapM_x (\<lambda>t. do y <- setThreadState Structures_H.thread_state.Restart t;
tcbSchedEnqueue t
od) q \<lbrace>\<lambda>rv 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 (2 subgoals):
 1. \<And>s. \<lbrakk>((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s; sym_refs (\<lambda>x. if x \<in> set [] then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set []. ex_nonz_cap_to' x s)\<rbrakk> \<Longrightarrow> 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
 2. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>\<lambda>s. ((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s \<and> sym_refs (\<lambda>x. if x \<in> set (a # as) then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set (a # as). ex_nonz_cap_to' x s)\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart a;
tcbSchedEnqueue a
od \<lbrace>\<lambda>r s. ((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s \<and> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set as. ex_nonz_cap_to' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>\<lambda>s. ((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s \<and> sym_refs (\<lambda>x. if x \<in> set (a # as) then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set (a # as). ex_nonz_cap_to' x s)\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart a;
tcbSchedEnqueue a
od \<lbrace>\<lambda>r s. ((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s \<and> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set as. ex_nonz_cap_to' x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a as. suffix (a # as) q \<Longrightarrow> \<lbrace>?Q55 a as\<rbrace> do y <- setThreadState Structures_H.thread_state.Restart a;
tcbSchedEnqueue a
od \<lbrace>\<lambda>r s. ((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s \<and> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set as. ex_nonz_cap_to' x s)\<rbrace>
 2. \<And>a as s. \<lbrakk>suffix (a # as) q; ((\<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 (\<lambda>s. \<forall>x\<in>set q. tcb_at' x s)) s \<and> sym_refs (\<lambda>x. if x \<in> set (a # as) then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> (\<forall>x\<in>set (a # as). ex_nonz_cap_to' x s)\<rbrakk> \<Longrightarrow> ?Q55 a as s proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s) \<and> (\<forall>x\<in>set q. tcb_at' x s) \<and> sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> ex_nonz_cap_to' a s \<and> (\<forall>x\<in>set as. ex_nonz_cap_to' x s)\<rbrakk> \<Longrightarrow> tcb_at' a s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> valid_objs' s \<and> a \<noteq> ksIdleThread s \<and> ksDomSchedule (newKernelState undefined) \<noteq> [] \<and> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> ((state_refs_of' s)(a := tcb_st_refs_of' Structures_H.thread_state.Restart \<union> {r \<in> state_refs_of' s a. snd r = TCBBound})) x. snd r = TCBBound} else ((state_refs_of' s)(a := tcb_st_refs_of' Structures_H.thread_state.Restart \<union> {r \<in> state_refs_of' s a. snd r = TCBBound})) x) proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<and> ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)) \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s) \<and> (\<forall>x\<in>set q. tcb_at' x s) \<and> sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x) \<and> ex_nonz_cap_to' a s \<and> (\<forall>x\<in>set as. ex_nonz_cap_to' x s)\<rbrakk> \<Longrightarrow> tcb_at' a s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> valid_objs' s \<and> a \<noteq> ksIdleThread s \<and> ksDomSchedule (newKernelState undefined) \<noteq> [] \<and> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> if x = a then {} \<union> {r \<in> state_refs_of' s a. snd r = TCBBound} else state_refs_of' s x. snd r = TCBBound} else if x = a then {} \<union> {r \<in> state_refs_of' s a. snd r = TCBBound} else state_refs_of' s x) proof (prove)
goal (1 subgoal):
 1. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s); \<forall>x\<in>set q. tcb_at' x s; sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x); ex_nonz_cap_to' a s; \<forall>x\<in>set as. ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> tcb_at' a s \<and> valid_tcb_state' Structures_H.thread_state.Restart s \<and> valid_objs' s \<and> a \<noteq> ksIdleThread s \<and> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> if x = a then {} \<union> {r \<in> state_refs_of' s a. snd r = TCBBound} else state_refs_of' s x. snd r = TCBBound} else if x = a then {} \<union> {r \<in> state_refs_of' s a. snd r = TCBBound} else state_refs_of' s x) proof (prove)
goal (5 subgoals):
 1. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s); \<forall>x\<in>set q. tcb_at' x s; sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x); ex_nonz_cap_to' a s; \<forall>x\<in>set as. ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> tcb_at' a s
 2. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s); \<forall>x\<in>set q. tcb_at' x s; sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x); ex_nonz_cap_to' a s; \<forall>x\<in>set as. ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> valid_tcb_state' Structures_H.thread_state.Restart s
 3. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s); \<forall>x\<in>set q. tcb_at' x s; sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x); ex_nonz_cap_to' a s; \<forall>x\<in>set as. ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> valid_objs' s
 4. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s); \<forall>x\<in>set q. tcb_at' x s; sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x); ex_nonz_cap_to' a s; \<forall>x\<in>set as. ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> a \<noteq> ksIdleThread s
 5. \<And>a as s. \<lbrakk>suffix (a # as) q; 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 (newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (newKernelState undefined)); untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s); \<forall>x\<in>set q. tcb_at' x s; sym_refs (\<lambda>x. if x = a \<or> x \<in> set as then {r \<in> state_refs_of' s x. snd r = TCBBound} else state_refs_of' s x); ex_nonz_cap_to' a s; \<forall>x\<in>set as. ex_nonz_cap_to' x s\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>x. if x \<in> set as then {r \<in> if x = a then {} \<union> {r \<in> state_refs_of' s a. snd r = TCBBound} else state_refs_of' s x. snd r = TCBBound} else if x = a then {} \<union> {r \<in> state_refs_of' s a. snd r = TCBBound} else state_refs_of' s x) proof (prove)
goal:
No subgoals!