theory Scheduler_IF

lemma tcb_sched_action_unobservable:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows
  "\<lbrace>pas_refined aag and scheduler_affects_equiv aag l st
                    and (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l)\<rbrace>
   tcb_sched_action f t
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: tcb_sched_action_def) apply wp apply (clarsimp simp: etcb_at_def scheduler_affects_equiv_def split: option.splits) apply (clarsimp simp: states_equiv_for_def equiv_for_def equiv_asids_def) apply (rule ext) apply clarsimp apply (frule(1) tcb_domain_wellformed) apply (metis domains_distinct[THEN pas_domains_distinct_inj]) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l)\<rbrace> tcb_sched_action f t \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l)\<rbrace> do d <- ethread_get tcb_domain t;
prio <- ethread_get tcb_priority t;
queue <- get_tcb_queue d prio;
set_tcb_queue d prio (f t queue)
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l)) s \<Longrightarrow> etcb_at (\<lambda>ta. etcb_at (\<lambda>tb. scheduler_affects_equiv aag l st (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain ta \<and> p = tcb_priority tb then f t (ready_queues s (tcb_domain ta) (tcb_priority tb)) else ready_queues s t' p) s)) t s) t s proof (prove)
goal (1 subgoal):
 1. \<And>s x2. \<lbrakk>pas_refined aag s; 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); pasObjectAbs aag t \<notin> reads_scheduler aag l; ekheap s t = Some x2\<rbrakk> \<Longrightarrow> 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 (ready_queues_update (\<lambda>_ t' p. if t' = tcb_domain x2 \<and> p = tcb_priority x2 then f t (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s t' p) s) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x la. \<lbrakk>pas_refined aag 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); pasObjectAbs aag t \<notin> reads_scheduler aag l; ekheap s t = Some x2; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> kheap st x = kheap s x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state s) x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> device_state (machine_state st) x = device_state (machine_state s) x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt st (a, b) = cdt s (a, b)); \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> ekheap st x = ekheap s x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt_list st (a, b) = cdt_list s (a, b)); \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. is_original_cap st (a, b) = is_original_cap s (a, b)); \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_states st x = interrupt_states s x; \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) \<longrightarrow> ready_queues st x = ready_queues s x; \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> equiv_asid asid st s; la \<in> pasDomainAbs aag x; la \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ready_queues s x = (\<lambda>p. if x = tcb_domain x2 \<and> p = tcb_priority x2 then f t (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s x p) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 x la p. \<lbrakk>pas_refined aag 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); pasObjectAbs aag t \<notin> reads_scheduler aag l; ekheap s t = Some x2; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> kheap st x = kheap s x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state s) x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> device_state (machine_state st) x = device_state (machine_state s) x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt st (a, b) = cdt s (a, b)); \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> ekheap st x = ekheap s x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt_list st (a, b) = cdt_list s (a, b)); \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. is_original_cap st (a, b) = is_original_cap s (a, b)); \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_states st x = interrupt_states s x; \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) \<longrightarrow> ready_queues st x = ready_queues s x; \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> equiv_asid asid st s; la \<in> pasDomainAbs aag x; la \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ready_queues s x p = (if x = tcb_domain x2 \<and> p = tcb_priority x2 then f t (ready_queues s (tcb_domain x2) (tcb_priority x2)) else ready_queues s x p) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 la. \<lbrakk>pas_refined aag 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); pasObjectAbs aag t \<notin> reads_scheduler aag l; ekheap s t = Some x2; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> kheap st x = kheap s x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state s) x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> device_state (machine_state st) x = device_state (machine_state s) x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt st (a, b) = cdt s (a, b)); \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> ekheap st x = ekheap s x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt_list st (a, b) = cdt_list s (a, b)); \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. is_original_cap st (a, b) = is_original_cap s (a, b)); \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_states st x = interrupt_states s x; \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) \<longrightarrow> ready_queues st x = ready_queues s x; \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> equiv_asid asid st s; la \<in> pasDomainAbs aag (tcb_domain x2); la \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ready_queues s (tcb_domain x2) (tcb_priority x2) = f t (ready_queues s (tcb_domain x2) (tcb_priority x2)) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 la. \<lbrakk>pas_refined aag 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); pasObjectAbs aag t \<notin> reads_scheduler aag l; ekheap s t = Some x2; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> kheap st x = kheap s x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> underlying_memory (machine_state st) x = underlying_memory (machine_state s) x; \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> device_state (machine_state st) x = device_state (machine_state s) x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt st (a, b) = cdt s (a, b)); \<forall>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<longrightarrow> ekheap st x = ekheap s x; \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. cdt_list st (a, b) = cdt_list s (a, b)); \<forall>a. pasObjectAbs aag a \<in> reads_scheduler aag l \<longrightarrow> (\<forall>b. is_original_cap st (a, b) = is_original_cap s (a, b)); \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_states st x = interrupt_states s x; \<forall>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<forall>x. (\<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l) \<longrightarrow> ready_queues st x = ready_queues s x; \<forall>asid. asid \<noteq> 0 \<and> pasASIDAbs aag asid \<in> reads_scheduler aag l \<longrightarrow> equiv_asid asid st s; la \<in> pasDomainAbs aag (tcb_domain x2); la \<in> reads_scheduler aag l; pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain x2)\<rbrakk> \<Longrightarrow> ready_queues s (tcb_domain x2) (tcb_priority x2) = f t (ready_queues s (tcb_domain x2) (tcb_priority x2)) proof (prove)
goal:
No subgoals!