theory Scheduler_IF

lemma ethread_set_reads_respects_scheduler:
  "reads_respects_scheduler aag l (\<lambda>s. pasObjectAbs aag t \<in> reads_scheduler aag l)
                            (ethread_set f t)" apply (clarsimp simp: thread_set_time_slice_def ethread_set_def gets_the_def gets_def get_def
                        bind_def put_def get_etcb_def return_def assert_opt_def set_eobject_def
                        fail_def equiv_valid_def2 equiv_valid_2_def scheduler_equiv_def
                        domain_fields_equiv_def globals_equiv_scheduler_def idle_equiv_def
                 split: option.splits) apply (rule conjI) apply (clarsimp simp: silc_dom_equiv_def reads_scheduler_def equiv_for_def split: if_split_asm) apply (simp add: scheduler_affects_equiv_def) apply clarsimp apply (rule conjI) apply (rule states_equiv_for_identical_ekheap_updates,assumption) apply (elim states_equiv_forE equiv_forE) apply (clarsimp simp: identical_ekheap_updates_def) apply (clarsimp simp: scheduler_globals_frame_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. pasObjectAbs aag t \<in> reads_scheduler aag l) (ethread_set f t) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); scheduler_affects_equiv aag l s ta\<rbrakk> \<Longrightarrow> silc_dom_equiv aag (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta \<and> scheduler_affects_equiv aag l (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap ta)(t \<mapsto> f x2a)) ta) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); scheduler_affects_equiv aag l s ta\<rbrakk> \<Longrightarrow> silc_dom_equiv aag (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta
 2. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); scheduler_affects_equiv aag l s ta\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap ta)(t \<mapsto> f x2a)) ta) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); scheduler_affects_equiv aag l s ta\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap ta)(t \<mapsto> f x2a)) ta) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta \<and> (reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta))\<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) (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap ta)(t \<mapsto> f x2a)) ta) \<and> (reads_scheduler_cur_domain aag l ta \<longrightarrow> scheduler_globals_frame_equiv (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta) proof (prove)
goal (1 subgoal):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<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) (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap ta)(t \<mapsto> f x2a)) ta) \<and> (reads_scheduler_cur_domain aag l ta \<longrightarrow> scheduler_globals_frame_equiv (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta) proof (prove)
goal (2 subgoals):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<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) (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) (ekheap_update (\<lambda>_. (ekheap ta)(t \<mapsto> f x2a)) ta)
 2. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l ta \<longrightarrow> scheduler_globals_frame_equiv (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta proof (prove)
goal (2 subgoals):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<rbrakk> \<Longrightarrow> identical_ekheap_updates s ta ((ekheap s)(t \<mapsto> f x2)) ((ekheap ta)(t \<mapsto> f x2a))
 2. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l ta \<longrightarrow> scheduler_globals_frame_equiv (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta proof (prove)
goal (2 subgoals):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta); equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (machine_state s) (machine_state ta); equiv_asids (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) s ta; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> kheap s x = kheap ta x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> cdt s x = cdt ta x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> cdt_list s x = cdt_list ta x; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> ekheap s x = ekheap ta x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> is_original_cap s x = is_original_cap ta x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_states s x = interrupt_states ta x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_irq_node s x = interrupt_irq_node ta x; \<And>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l \<Longrightarrow> ready_queues s x = ready_queues ta x\<rbrakk> \<Longrightarrow> identical_ekheap_updates s ta ((ekheap s)(t \<mapsto> f x2)) ((ekheap ta)(t \<mapsto> f x2a))
 2. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l ta \<longrightarrow> scheduler_globals_frame_equiv (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta proof (prove)
goal (1 subgoal):
 1. \<And>s x2 ta x2a. \<lbrakk>ekheap s t = Some x2; ekheap ta t = Some x2a; pasObjectAbs aag t \<in> reads_scheduler aag l; cur_domain s = cur_domain ta; domain_time s = domain_time ta; domain_index s = domain_index ta; domain_list s = domain_list ta; arch_globals_equiv_scheduler (kheap s) (kheap ta) (arch_state s) (arch_state ta); idle_thread s = idle_thread ta; \<forall>tcb. kheap s (idle_thread ta) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap ta (idle_thread ta) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); tcb_at (idle_thread ta) s = tcb_at (idle_thread ta) ta; dom (device_state (machine_state s)) = dom (device_state (machine_state ta)); silc_dom_equiv aag s ta; equiv_irq_state (machine_state s) (machine_state ta); 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) s ta; reads_scheduler_cur_domain aag l ta \<longrightarrow> cur_thread s = cur_thread ta \<and> scheduler_action s = scheduler_action ta \<and> work_units_completed s = work_units_completed ta \<and> scheduler_globals_frame_equiv s ta \<and> (cur_thread s \<noteq> idle_thread ta \<longrightarrow> arch_scheduler_affects_equiv s ta)\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l ta \<longrightarrow> scheduler_globals_frame_equiv (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f x2)) s) ta proof (prove)
goal:
No subgoals!