theory Scheduler_IF

lemma choose_thread_unobservable:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
    "\<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and scheduler_affects_equiv aag l st and
      invs and valid_queues and pas_refined aag and scheduler_equiv aag st\<rbrace>
     choose_thread
     \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: choose_thread_def) apply (wp switch_to_idle_thread_unobservable guarded_switch_to_lift
            switch_to_thread_unobservable) apply (simp add: scheduler_affects_equiv_def
                   scheduler_equiv_def domain_fields_equiv_def) apply (intro impI conjI) apply (elim conjE exE) apply (erule any_valid_thread) apply (frule(1) tcb_with_domain_at) apply clarsimp apply (frule(1) tcb_domain_wellformed) apply (force simp: disjoint_iff_not_equal) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and scheduler_affects_equiv aag l st and invs and valid_queues and pas_refined aag and scheduler_equiv aag st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_affects_equiv aag l st and invs and valid_queues and pas_refined aag and scheduler_equiv aag st\<rbrace> do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_affects_equiv aag l st and invs and valid_queues and pas_refined aag and scheduler_equiv aag st) s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain s = cur_domain st) and invs) s) \<and> (\<not> (\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>sa. pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and scheduler_equiv aag st and invs and pas_refined aag) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st s)) \<and> invs s \<and> valid_queues s \<and> pas_refined aag s \<and> cur_domain st = cur_domain s \<and> domain_time st = domain_time s \<and> domain_index st = domain_index s \<and> domain_list st = domain_list s \<and> idle_thread st = idle_thread s \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<and> equiv_irq_state (machine_state st) (machine_state s) \<Longrightarrow> (\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st s)) \<and> invs s \<and> valid_queues s \<and> pas_refined aag s \<and> cur_domain st = cur_domain s \<and> domain_time st = domain_time s \<and> domain_index st = domain_index s \<and> domain_list st = domain_list s \<and> idle_thread st = idle_thread s \<and> globals_equiv_scheduler st s \<and> silc_dom_equiv aag st s \<and> equiv_irq_state (machine_state st) (machine_state s); \<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s prio. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st s); invs s; valid_queues s; pas_refined aag s; cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; idle_thread st = idle_thread s; globals_equiv_scheduler st s; silc_dom_equiv aag st s; equiv_irq_state (machine_state st) (machine_state s); ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s prio x prioa. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st s); invs s; valid_queues s; pas_refined aag s; cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; idle_thread st = idle_thread s; globals_equiv_scheduler st s; silc_dom_equiv aag st s; equiv_irq_state (machine_state st) (machine_state s); x \<in> set (ready_queues s (cur_domain s) prioa)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s prio x prioa. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s; (pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv st s); invs s; valid_queues s; pas_refined aag s; cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; idle_thread st = idle_thread s; globals_equiv_scheduler st s; silc_dom_equiv aag st s; equiv_irq_state (machine_state st) (machine_state s); x \<in> set (ready_queues s (cur_domain s) prioa); \<exists>t. ekheap s x = Some t \<and> tcb_domain t = cur_domain s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l proof (prove)
goal (1 subgoal):
 1. \<And>s x prioa t. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s; invs s; valid_queues s; pas_refined aag s; cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; idle_thread st = idle_thread s; globals_equiv_scheduler st s; silc_dom_equiv aag st s; equiv_irq_state (machine_state st) (machine_state s); x \<in> set (ready_queues s (cur_domain s) prioa); ekheap s x = Some t; tcb_domain t = cur_domain s; pasObjectAbs aag x \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s x prioa t. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; states_equiv_for (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasIRQAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) (\<lambda>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) st s; invs s; valid_queues s; pas_refined aag s; cur_domain st = cur_domain s; domain_time st = domain_time s; domain_index st = domain_index s; domain_list st = domain_list s; idle_thread st = idle_thread s; globals_equiv_scheduler st s; silc_dom_equiv aag st s; equiv_irq_state (machine_state st) (machine_state s); x \<in> set (ready_queues s (cur_domain s) prioa); ekheap s x = Some t; tcb_domain t = cur_domain s; pasObjectAbs aag x \<in> reads_scheduler aag l; pasObjectAbs aag x \<in> pasDomainAbs aag (tcb_domain t)\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!