theory Ipc_R

lemma setThreadState_nonqueued_state_update:
  "\<lbrace>\<lambda>s. invs' s \<and> st_tcb_at' simple' t s
               \<and> st \<in> {Inactive, Running, Restart, IdleThreadState}
               \<and> (st \<noteq> Inactive \<longrightarrow> ex_nonz_cap_to' t s)
               \<and> (t = ksIdleThread s \<longrightarrow> idle' st)

               \<and> (\<not> runnable' st \<longrightarrow> sch_act_simple s)
               \<and> (\<not> runnable' st \<longrightarrow> (\<forall>p. t \<notin> set (ksReadyQueues s p)))\<rbrace>
  setThreadState st t \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: invs'_def valid_state'_def) apply (rule hoare_pre, wp valid_irq_node_lift
                            sts_valid_queues
                            setThreadState_ct_not_inQ) apply (clarsimp simp: pred_tcb_at') apply (rule conjI, fastforce simp: valid_tcb_state'_def) apply (drule simple_st_tcb_at_state_refs_ofD') apply (drule bound_tcb_at_state_refs_ofD') apply (rule conjI, fastforce) apply clarsimp apply (erule delta_sym_refs) apply (fastforce split: if_split_asm) apply (fastforce simp: symreftype_inverse' tcb_bound_refs'_def
                  split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. invs' s \<and> st_tcb_at' simple' t s \<and> st \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s) \<and> (t = ksIdleThread s \<longrightarrow> idle' st) \<and> (\<not> runnable' st \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' st \<longrightarrow> (\<forall>p. t \<notin> set (ksReadyQueues s p)))\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. invs'\<rbrace> 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> 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> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ 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> cur_tcb' s \<and> st_tcb_at' simple' t s \<and> (st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st) \<and> (st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s) \<and> (t = ksIdleThread s \<longrightarrow> idle' st) \<and> (\<not> runnable' st \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))))\<rbrace> setThreadState st t \<lbrace>\<lambda>rv. (\<lambda>s. valid_pspace' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> Invariants_H.valid_queues s \<and> sym_refs (state_refs_of' s) \<and> if_live_then_nonz_cap' s \<and> if_unsafe_then_cap' s \<and> valid_idle' s \<and> valid_global_refs' s \<and> valid_arch_state' s \<and> valid_irq_node' (irq_node' s) s \<and> valid_irq_handlers' s \<and> valid_irq_states' s \<and> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ 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 cur_tcb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>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> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ 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> cur_tcb' s \<and> st_tcb_at' simple' t s \<and> (st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st) \<and> (st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s) \<and> (t = ksIdleThread s \<longrightarrow> idle' st) \<and> (\<not> runnable' st \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) \<Longrightarrow> (valid_pspace' and tcb_at' t and valid_tcb_state' st) s \<and> ((\<not> runnable' st \<longrightarrow> sch_act_simple s) \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (Invariants_H.valid_queues s \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' st)) \<and> sym_refs ((state_refs_of' s)(t := tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound})) \<and> (if_live_then_nonz_cap' s \<and> (st \<noteq> Structures_H.thread_state.Inactive \<and> st \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> ex_nonz_cap_to' t s)) \<and> if_unsafe_then_cap' s \<and> (valid_idle' and valid_pspace' and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' st)) 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> valid_machine_state' s \<and> irqs_masked' s \<and> valid_queues' s \<and> ct_not_inQ 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> cur_tcb' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' simple' t s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> valid_tcb_state' st s \<and> ((\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' simple' t s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<Longrightarrow> ((\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); bound_tcb_at' (\<lambda>x. tcb_bound_refs' x = state_refs_of' s t) t s\<rbrakk> \<Longrightarrow> ((\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); \<exists>ts ntfnptr. tcb_bound_refs' ntfnptr = state_refs_of' s t \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr\<rbrakk> \<Longrightarrow> ((\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<longrightarrow> runnable' st) \<and> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); \<exists>ts ntfnptr. tcb_bound_refs' ntfnptr = state_refs_of' s t \<and> obj_at' (tcb_ntfn_is_bound' ntfnptr) t s \<and> state_refs_of' s t = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> state_refs_of' s t. snd r = TCBBound} else state_refs_of' s a) proof (prove)
goal (1 subgoal):
 1. \<And>s ts ntfnptr. \<lbrakk>valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); tcb_bound_refs' ntfnptr = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_bound_refs' ntfnptr\<rbrakk> \<Longrightarrow> sym_refs (\<lambda>a. if a = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s a) proof (prove)
goal (2 subgoals):
 1. \<And>s ts ntfnptr x 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; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); tcb_bound_refs' ntfnptr = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_bound_refs' ntfnptr; (y, tp) \<in> (if x = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s x); (y, tp) \<notin> state_refs_of' s x\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<in> (if y = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s y)
 2. \<And>s ts ntfnptr x 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; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); tcb_bound_refs' ntfnptr = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_bound_refs' ntfnptr; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s y) proof (prove)
goal (1 subgoal):
 1. \<And>s ts ntfnptr x 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; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st = Structures_H.thread_state.Inactive \<or> st = Structures_H.thread_state.Running \<or> st = Structures_H.thread_state.Restart \<or> idle' st; st \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' t s; t = ksIdleThread s \<longrightarrow> idle' st; \<not> runnable' st \<longrightarrow> sch_act_simple s; \<not> runnable' st \<longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))); tcb_bound_refs' ntfnptr = tcb_st_refs_of' ts \<union> tcb_bound_refs' ntfnptr; obj_at' (tcb_ntfn_is_bound' ntfnptr) t s; state_refs_of' s t = tcb_bound_refs' ntfnptr; (y, tp) \<in> state_refs_of' s x; (y, tp) \<notin> (if x = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s x)\<rbrakk> \<Longrightarrow> (x, symreftype tp) \<notin> (if y = t then tcb_st_refs_of' st \<union> {r \<in> tcb_bound_refs' ntfnptr. snd r = TCBBound} else state_refs_of' s y) proof (prove)
goal:
No subgoals!