theory Syscall_R

lemma threadSet_all_invs_but_sch_extra:
  shows      "\<lbrace> tcb_at' t and (\<lambda>s. (\<forall>p. t \<notin> set (ksReadyQueues s p))) and
                all_invs_but_sch_extra and sch_act_simple and
                K (ds \<le> maxDomain) \<rbrace>
                threadSet (tcbDomain_update (\<lambda>_. ds)) t
              \<lbrace>\<lambda>rv. all_invs_but_sch_extra \<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_pre) apply (wp threadSet_valid_pspace'T_P[where P = False and Q = \<top> and Q' = \<top>]) apply (simp add:tcb_cte_cases_def)+ apply (wp
     threadSet_valid_pspace'T_P
     threadSet_state_refs_of'T_P[where f'=id and P'=False and Q=\<top> and g'=id and Q'=\<top>]
     threadSet_idle'T
     threadSet_global_refsT
     threadSet_cur
     irqs_masked_lift
     valid_irq_node_lift
     valid_irq_handlers_lift''
     threadSet_ctes_ofT
     threadSet_not_inQ
     threadSet_valid_queues'_no_state
     threadSet_valid_queues
     threadSet_valid_dom_schedule'
     threadSet_iflive'T
     threadSet_ifunsafe'T
     untyped_ranges_zero_lift
     | simp add:tcb_cte_cases_def cteCaps_of_def o_def)+ apply (wp hoare_vcg_all_lift hoare_vcg_imp_lift threadSet_pred_tcb_no_state | simp)+ apply (clarsimp simp:sch_act_simple_def o_def cteCaps_of_def) apply (intro conjI) apply fastforce+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple and K (ds \<le> maxDomain)\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) t \<lbrace>\<lambda>rv s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. ds \<le> maxDomain \<Longrightarrow> \<lbrace>tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) t \<lbrace>\<lambda>rv s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. ds \<le> maxDomain \<Longrightarrow> \<lbrace>?Q2\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) t \<lbrace>\<lambda>rv s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace>
 2. \<And>s. \<lbrakk>ds \<le> maxDomain; (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> ?Q2 s proof (prove)
goal (9 subgoals):
 1. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. \<forall>(getF, setF)\<in>ran tcb_cte_cases. getF (tcbDomain_update (\<lambda>_. ds) tcb) = getF tcb
 2. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. (False \<longrightarrow> True) \<longrightarrow> (\<forall>s. valid_tcb_state' (tcbState tcb) s \<longrightarrow> valid_tcb_state' (tcbState (tcbDomain_update (\<lambda>_. ds) tcb)) s)
 3. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. (False \<longrightarrow> True) \<longrightarrow> (\<forall>s. valid_bound_ntfn' (tcbBoundNotification tcb) s \<longrightarrow> valid_bound_ntfn' (tcbBoundNotification (tcbDomain_update (\<lambda>_. ds) tcb)) s)
 4. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. is_aligned (tcbIPCBuffer tcb) msg_align_bits \<longrightarrow> is_aligned (tcbIPCBuffer (tcbDomain_update (\<lambda>_. ds) tcb)) msg_align_bits
 5. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. tcbDomain tcb \<le> maxDomain \<longrightarrow> tcbDomain (tcbDomain_update (\<lambda>_. ds) tcb) \<le> maxDomain
 6. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. tcbPriority tcb \<le> maxPriority \<longrightarrow> tcbPriority (tcbDomain_update (\<lambda>_. ds) tcb) \<le> maxPriority
 7. ds \<le> maxDomain \<Longrightarrow> \<forall>tcb. tcbMCP tcb \<le> maxPriority \<longrightarrow> tcbMCP (tcbDomain_update (\<lambda>_. ds) tcb) \<le> maxPriority
 8. ds \<le> maxDomain \<Longrightarrow> \<lbrace>?P'6\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) t \<lbrace>\<lambda>rv s. 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace>
 9. \<And>s. \<lbrakk>ds \<le> maxDomain; (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> (valid_pspace' and (\<lambda>s. False \<longrightarrow> st_tcb_at' (\<lambda>_. True) t s \<and> bound_tcb_at' (\<lambda>_. True) t s)) s \<and> ?P'6 s proof (prove)
goal (2 subgoals):
 1. ds \<le> maxDomain \<Longrightarrow> \<lbrace>?P'6\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) t \<lbrace>\<lambda>rv s. 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> untyped_ranges_zero' s \<and> valid_queues' 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> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)\<rbrace>
 2. \<And>s. \<lbrakk>ds \<le> maxDomain; (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> (valid_pspace' and (\<lambda>s. False \<longrightarrow> st_tcb_at' (\<lambda>_. True) t s \<and> bound_tcb_at' (\<lambda>_. True) t s)) s \<and> ?P'6 s proof (prove)
goal (2 subgoals):
 1. ds \<le> maxDomain \<Longrightarrow> \<lbrace>?P'126\<rbrace> threadSet (tcbDomain_update (\<lambda>_. ds)) t \<lbrace>\<lambda>rv s. \<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s\<rbrace>
 2. \<And>s. \<lbrakk>ds \<le> maxDomain; (tcb_at' t and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p)) and (\<lambda>s. valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' s \<and> valid_pde_mappings' s \<and> pspace_domain_valid s \<and> ksCurDomain s \<le> maxDomain \<and> valid_dom_schedule' s \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s)) and sch_act_simple) s\<rbrakk> \<Longrightarrow> (valid_pspace' and (\<lambda>s. False \<longrightarrow> st_tcb_at' (\<lambda>_. True) t s \<and> bound_tcb_at' (\<lambda>_. True) t s)) s \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbDomain_update (\<lambda>_. ds) tcb) \<and> runnable' (tcbState (tcbDomain_update (\<lambda>_. ds) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbDomain_update (\<lambda>_. ds) tcb) \<and> runnable' (tcbState (tcbDomain_update (\<lambda>_. ds) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> (sym_refs ((state_refs_of' s)(t := id {r \<in> state_refs_of' s t. snd r \<noteq> TCBBound} \<union> id {r \<in> state_refs_of' s t. snd r = TCBBound})) \<and> (False \<longrightarrow> st_tcb_at' (\<lambda>_. True) t s \<and> bound_tcb_at' (\<lambda>_. True) t s)) \<and> (if_live_then_nonz_cap' s \<and> ((\<exists>tcb. \<not> tcbBoundNotification tcb \<noteq> None \<and> tcbBoundNotification (tcbDomain_update (\<lambda>_. ds) tcb) \<noteq> None \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState (tcbDomain_update (\<lambda>_. ds) tcb) \<noteq> Structures_H.thread_state.Inactive \<and> tcbState (tcbDomain_update (\<lambda>_. ds) tcb) \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued (tcbDomain_update (\<lambda>_. ds) tcb) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s)) \<and> if_unsafe_then_cap' s \<and> (valid_idle' s \<and> (t = ksIdleThread s \<longrightarrow> (\<forall>tcb. ko_at' tcb t s \<and> idle_tcb' tcb \<longrightarrow> idle_tcb' (tcbDomain_update (\<lambda>_. ds) tcb)))) \<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> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s) \<and> (valid_queues' and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))) 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> ?P'126 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ds \<le> maxDomain; tcb_at' t s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> valid_pspace' 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> untyped_ranges_zero' s \<and> valid_queues' 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> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> ((\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. tcbBoundNotification tcb = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcb \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued tcb \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> untyped_ranges_zero_inv (\<lambda>a. map_option cteCap (ctes_of s a)) (gsUntypedZeroRanges s) \<and> ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> [] proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>ds \<le> maxDomain; tcb_at' t s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); valid_pspace' 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; irqs_masked' s; valid_machine_state' s; cur_tcb' s; untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); valid_queues' 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)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> ((\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. tcbBoundNotification tcb = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcb \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) \<and> ((\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued tcb \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>ds \<le> maxDomain; tcb_at' t s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); valid_pspace' 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; irqs_masked' s; valid_machine_state' s; cur_tcb' s; untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); valid_queues' 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)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> (\<exists>tcb. tcbBoundNotification tcb = None \<and> (\<exists>y. tcbBoundNotification tcb = Some y) \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s
 2. \<And>s. \<lbrakk>ds \<le> maxDomain; tcb_at' t s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); valid_pspace' 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; irqs_masked' s; valid_machine_state' s; cur_tcb' s; untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); valid_queues' 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)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> (\<exists>tcb. (tcbState tcb = Structures_H.thread_state.Inactive \<or> idle' (tcbState tcb)) \<and> tcbState tcb \<noteq> Structures_H.thread_state.Inactive \<and> tcbState tcb \<noteq> Structures_H.thread_state.IdleThreadState \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s
 3. \<And>s. \<lbrakk>ds \<le> maxDomain; tcb_at' t s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); valid_pspace' 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; irqs_masked' s; valid_machine_state' s; cur_tcb' s; untyped_ranges_zero_inv (\<lambda>x. map_option cteCap (ctes_of s x)) (gsUntypedZeroRanges s); valid_queues' 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)); ksSchedulerAction s = ResumeCurrentThread \<or> ksSchedulerAction s = ChooseNewThread\<rbrakk> \<Longrightarrow> (\<exists>tcb. \<not> tcbQueued tcb \<and> tcbQueued tcb \<and> ko_at' tcb t s) \<longrightarrow> ex_nonz_cap_to' t s proof (prove)
goal:
No subgoals!