theory Schedule_DR

lemma schedule_choose_new_thread_helper:
            "\<lbrakk> ready_queues s (cur_domain s) prio \<noteq> [];
               t = hd (ready_queues s (cur_domain s) prio);
               valid_sched_except_blocked s;
               invs s;
               scheduler_action s = choose_new_thread
             \<rbrakk>
             \<Longrightarrow> (\<exists>y. cdl_objects (transform s) t = Some y) \<and> t \<in> active_tcbs_in_domain (cur_domain s) (transform s)" apply (clarsimp simp: valid_sched_def valid_sched_action_def is_activatable_def invs_def
                        valid_state_def pred_tcb_at_def obj_at_def DetSchedInvs_AI.valid_queues_def
                        max_non_empty_queue_def only_idle_def) apply (erule_tac x="cur_domain s" in allE) apply (erule_tac x="prio" in allE) apply clarsimp apply (erule_tac x="hd (ready_queues s (cur_domain s) prio)" in ballE) apply (clarsimp simp: valid_idle_def pred_tcb_at_def) apply (drule_tac s="idle_thread s" in sym) apply (auto simp: transform_def transform_current_thread_def all_active_tcbs_def transform_objects_def active_tcbs_in_domain_def etcb_at_def
                       is_etcb_at_def
                        map_add_def restrict_map_def option_map_def transform_object_def transform_tcb_def valid_idle_def st_tcb_def2 get_tcb_def
                        transform_cnode_contents_def infer_tcb_pending_op_def transform_cap_def domIff st_tcb_at_kh_def obj_at_def only_idle_def tcb_pending_op_slot_def tcb_boundntfn_slot_def
                  split: option.splits if_split Structures_A.kernel_object.splits Structures_A.thread_state.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); valid_sched_except_blocked s; invs s; scheduler_action s = choose_new_thread\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) t = Some y) \<and> t \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues s d p); valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>p. (\<forall>t\<in>set (ready_queues s (cur_domain s) p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = cur_domain s) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues s (cur_domain s) p)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; (\<forall>t\<in>set (ready_queues s (cur_domain s) prio). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = prio \<and> tcb_domain t = cur_domain s) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))) \<and> distinct (ready_queues s (cur_domain s) prio)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; \<forall>t\<in>set (ready_queues s (cur_domain s) prio). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = prio \<and> tcb_domain t = cur_domain s) t s \<and> (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb))); distinct (ready_queues s (cur_domain s) prio)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; distinct (ready_queues s (cur_domain s) prio); is_etcb_at (hd (ready_queues s (cur_domain s) prio)) s \<and> etcb_at (\<lambda>t. tcb_priority t = prio \<and> tcb_domain t = cur_domain s) (hd (ready_queues s (cur_domain s) prio)) s \<and> (\<exists>ko. kheap s (hd (ready_queues s (cur_domain s) prio)) = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> runnable (tcb_state tcb)))\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s)
 2. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; distinct (ready_queues s (cur_domain s) prio); hd (ready_queues s (cur_domain s) prio) \<notin> set (ready_queues s (cur_domain s) prio)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread_ptr; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; distinct (ready_queues s (cur_domain s) prio); obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb) \<and> tcb_bound_notification tcb = None \<and> valid_arch_idle (tcb_iarch tcb)) idle_thread_ptr s; idle_thread s = idle_thread_ptr; is_etcb_at (hd (ready_queues s (cur_domain s) prio)) s; etcb_at (\<lambda>t. tcb_priority t = prio \<and> tcb_domain t = cur_domain s) (hd (ready_queues s (cur_domain s) prio)) s; kheap s (hd (ready_queues s (cur_domain s) prio)) = Some (TCB tcb); runnable (tcb_state tcb)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s)
 2. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; distinct (ready_queues s (cur_domain s) prio); hd (ready_queues s (cur_domain s) prio) \<notin> set (ready_queues s (cur_domain s) prio)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread_ptr; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; distinct (ready_queues s (cur_domain s) prio); obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb) \<and> tcb_bound_notification tcb = None \<and> valid_arch_idle (tcb_iarch tcb)) idle_thread_ptr s; is_etcb_at (hd (ready_queues s (cur_domain s) prio)) s; etcb_at (\<lambda>t. tcb_priority t = prio \<and> tcb_domain t = cur_domain s) (hd (ready_queues s (cur_domain s) prio)) s; kheap s (hd (ready_queues s (cur_domain s) prio)) = Some (TCB tcb); runnable (tcb_state tcb); idle_thread_ptr = idle_thread s\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s)
 2. \<lbrakk>ready_queues s (cur_domain s) prio \<noteq> []; t = hd (ready_queues s (cur_domain s) prio); scheduler_action s = choose_new_thread; valid_etcbs s; valid_pspace s; valid_mdb s; ct_not_in_q_2 (ready_queues s) choose_new_thread (cur_thread s); valid_idle_etcb s; valid_ioc s; valid_idle s; \<forall>t. (\<exists>ko. kheap s t = Some ko \<and> (\<exists>tcb. ko = TCB tcb \<and> idle (tcb_state tcb))) \<longrightarrow> t = idle_thread s; if_unsafe_then_cap s; valid_reply_caps s; valid_reply_masters s; valid_global_refs s; valid_arch_state s; valid_irq_node s; valid_irq_handlers s; valid_irq_states s; valid_machine_state s; valid_vspace_objs s; valid_arch_caps s; valid_global_objs s; valid_kernel_mappings s; equal_kernel_mappings s; valid_asid_map s; valid_global_vspace_mappings s; pspace_in_kernel_window s; cap_refs_in_kernel_window s; pspace_respects_device_region s; cap_refs_respects_device_region s; cur_tcb s; distinct (ready_queues s (cur_domain s) prio); hd (ready_queues s (cur_domain s) prio) \<notin> set (ready_queues s (cur_domain s) prio)\<rbrakk> \<Longrightarrow> (\<exists>y. cdl_objects (transform s) (hd (ready_queues s (cur_domain s) prio)) = Some y) \<and> hd (ready_queues s (cur_domain s) prio) \<in> active_tcbs_in_domain (cur_domain s) (transform s) proof (prove)
goal:
No subgoals!