theory Scheduler_IF

lemma ethread_set_unobservable[wp]:
   "\<lbrace>(\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace>
    ethread_set f t
    \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: ethread_set_def set_eobject_def) apply wp apply (clarsimp simp: get_etcb_def scheduler_affects_equiv_def) apply (elim states_equiv_forE equiv_forE) apply (clarsimp simp: equiv_for_def states_equiv_for_def equiv_asids_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> ethread_set f t \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> do tcb <- gets_the (get_etcb t);
es <- get;
put (ekheap_update (\<lambda>_. (ekheap es)(t \<mapsto> f tcb)) es)
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st) s \<Longrightarrow> get_etcb t s \<noteq> None \<longrightarrow> scheduler_affects_equiv aag l st (ekheap_update (\<lambda>_. (ekheap s)(t \<mapsto> f (the (get_etcb t s)))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag t \<notin> 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); ekheap s t = Some y\<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 (ekheap_update (\<lambda>_ a. if a = t then Some (f (the (ekheap s t))) else ekheap s a) s) proof (prove)
goal (1 subgoal):
 1. \<And>s y. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; (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); ekheap s t = Some y; equiv_machine_state (\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) (machine_state st) (machine_state s); equiv_asids (\<lambda>x. pasASIDAbs aag x \<in> reads_scheduler aag l) st s; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> kheap st x = kheap s x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> cdt st x = cdt s x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> cdt_list st x = cdt_list s x; \<And>x. pasObjectAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> ekheap st x = ekheap s x; \<And>x. ((\<lambda>x. pasObjectAbs aag x \<in> reads_scheduler aag l) \<circ> fst) x \<Longrightarrow> is_original_cap st x = is_original_cap s x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_states st x = interrupt_states s x; \<And>x. pasIRQAbs aag x \<in> reads_scheduler aag l \<Longrightarrow> interrupt_irq_node st x = interrupt_irq_node s x; \<And>x. \<exists>la\<in>pasDomainAbs aag x. la \<in> reads_scheduler aag l \<Longrightarrow> ready_queues st x = ready_queues s x\<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 (ekheap_update (\<lambda>_ a. if a = t then Some (f (the (ekheap s t))) else ekheap s a) s) proof (prove)
goal:
No subgoals!