kings-crown/FVELER_Isabelle huggingface dataset:
theory Scheduler_IF

lemma midstrength_scheduler_affects_equiv_sym[elim]:
  "midstrength_scheduler_affects_equiv aag l s s'
   \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s' s" apply (simp add: midstrength_scheduler_affects_equiv_def) apply (fastforce intro: states_equiv_for_sym) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_scheduler_affects_equiv aag l s s' \<Longrightarrow> midstrength_scheduler_affects_equiv aag l s' s proof (prove)
goal (1 subgoal):
 1. 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 s' \<and> ((pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> work_units_completed s = work_units_completed s') \<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) s' s \<and> ((pasDomainAbs aag (cur_domain s') \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed s' = work_units_completed s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma ethread_get_oblivious_cur_thread:
  "oblivious (cur_thread_update f) (ethread_get a b)" by (wpsimp wp: oblivious_bind simp: ethread_get_def gets_the_def get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious (cur_thread_update f) (ethread_get a b)
theory Scheduler_IF

lemma ethread_get_oblivious_schact:
  "oblivious (scheduler_action_update f) (ethread_get a b)" by (wpsimp wp: oblivious_bind simp: ethread_get_def gets_the_def get_etcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious (scheduler_action_update f) (ethread_get a b)
theory Scheduler_IF

lemma tcb_action_oblivious_cur_thread:
  "oblivious (cur_thread_update a) (tcb_sched_action f t)" apply (simp add: tcb_sched_action_def) apply (wp oblivious_bind ethread_get_oblivious_cur_thread
          | clarsimp simp: get_tcb_queue_def set_tcb_queue_def)+ apply (fastforce intro: state.equality det_ext.equality) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious (cur_thread_update a) (tcb_sched_action f t) proof (prove)
goal (1 subgoal):
 1. oblivious (cur_thread_update a) (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) proof (prove)
goal (1 subgoal):
 1. \<And>rv rva rvb s. cur_thread_update a (ready_queues_update (\<lambda>_ d' p. if d' = rv \<and> p = rva then f t rvb else ready_queues (cur_thread_update a s) d' p) s) = cur_thread_update a (ready_queues_update (\<lambda>_ d' p. if d' = rv \<and> p = rva then f t rvb else ready_queues s d' p) s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma tcb_action_oblivious_schact:
  "oblivious (scheduler_action_update a) (tcb_sched_action f t)" apply (simp add: tcb_sched_action_def) apply (wp oblivious_bind ethread_get_oblivious_schact
          | clarsimp simp: get_tcb_queue_def set_tcb_queue_def)+ apply (fastforce intro: state.equality det_ext.equality) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. oblivious (scheduler_action_update a) (tcb_sched_action f t) proof (prove)
goal (1 subgoal):
 1. oblivious (scheduler_action_update a) (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) proof (prove)
goal (1 subgoal):
 1. \<And>rv rva rvb s. trans_state (\<lambda>e. scheduler_action_internal_update a e\<lparr>ready_queues_internal := \<lambda>d' p. if d' = rv \<and> p = rva then f t rvb else ready_queues (scheduler_action_update a s) d' p\<rparr>) s = trans_state (\<lambda>e. scheduler_action_internal_update a (e\<lparr>ready_queues_internal := \<lambda>d' p. if d' = rv \<and> p = rva then f t rvb else ready_queues s d' p\<rparr>)) s proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma equiv_valid_get_assert:
  "equiv_valid I A B P f
   \<Longrightarrow> equiv_valid I A B P (get >>= (\<lambda> s. assert (g s) >>= (\<lambda>y. f)))" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def bind_def
                      get_def assert_def return_def fail_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P f \<Longrightarrow> equiv_valid I A B P (do s <- get;
y <- assert (g s);
f
od)
theory Scheduler_IF

lemma ev_irrelevant_bind:
  assumes inv: "\<And>P. f \<lbrace>P\<rbrace>"
  assumes ev: "equiv_valid I A B P g"
  shows "equiv_valid I A B P (do y \<leftarrow> f; g od)" proof - have a: "\<And>a b s. (a,b) \<in> fst (f s) \<Longrightarrow> b = s" apply (erule use_valid[OF _ inv]) apply simp done show ?thesis apply (insert ev) apply (clarsimp simp add: equiv_valid_def2 equiv_valid_2_def
                              bind_def) apply (drule a)+ apply clarsimp apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P (do y <- f;
g
od) proof (state)
goal (1 subgoal):
 1. equiv_valid I A B P (do y <- f;
g
od) proof (prove)
goal (1 subgoal):
 1. \<And>a b s. (a, b) \<in> fst (f s) \<Longrightarrow> b = s proof (prove)
goal (1 subgoal):
 1. \<And>a b s. s = s proof (prove)
goal:
No subgoals! proof (state)
this:
(?a, ?b) \<in> fst (f ?s) \<Longrightarrow> ?b = ?s

goal (1 subgoal):
 1. equiv_valid I A B P (do y <- f;
g
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P (do y <- f;
g
od) proof (prove)
goal (1 subgoal):
 1. equiv_valid I A B P g \<Longrightarrow> equiv_valid I A B P (do y <- f;
g
od) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba ab bb ac bc. \<lbrakk>\<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> B s' t'); (a, b) \<in> fst (f s); (aa, ba) \<in> fst (g b); (ab, bb) \<in> fst (f t); (ac, bc) \<in> fst (g bb); P s; P t; I s t; A s t\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> B ba bc proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba ab bb ac bc. \<lbrakk>\<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> B s' t'); (aa, ba) \<in> fst (g b); (ac, bc) \<in> fst (g bb); P s; P t; I s t; A s t; b = s; bb = t\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> B ba bc proof (prove)
goal (1 subgoal):
 1. \<And>s t aa ba ac bc. \<lbrakk>\<forall>s t. P s \<and> P t \<and> I s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (g s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g t). case x of (rvb, t') \<Rightarrow> rva = rvb \<and> I s' t' \<and> B s' t'); (aa, ba) \<in> fst (g s); (ac, bc) \<in> fst (g t); P s; P t; I s t; A s t\<rbrakk> \<Longrightarrow> aa = ac \<and> I ba bc \<and> B ba bc proof (prove)
goal:
No subgoals! proof (state)
this:
equiv_valid I A B P (do y <- f;
g
od)

goal:
No subgoals!
theory Scheduler_IF

lemma globals_equiv_scheduler[wp]:
  "I (globals_equiv_scheduler st)" by (rule lift_inv, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler st\<rbrace> f \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>
theory Scheduler_IF

lemma switch_to_thread_globals_equiv_scheduler[wp]:
  "\<lbrace>invs and globals_equiv_scheduler sta\<rbrace>
   switch_to_thread thread
   \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>" apply (simp add: switch_to_thread_def) apply (wp dxo_wp_weak arch_switch_to_thread_globals_equiv_scheduler | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> switch_to_thread thread \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb thread state = Some y);
y <- arch_switch_to_thread thread;
y <- tcb_sched_action tcb_sched_dequeue thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma guarded_switch_to_thread_midstrength_reads_respects_scheduler[wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "midstrength_reads_respects_scheduler aag l
           (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)))
           (guarded_switch_to t >>= (\<lambda>_. set_scheduler_action resume_cur_thread))" apply (simp add: guarded_switch_to_def bind_assoc) apply (subst bind_assoc[symmetric]) apply (rule ev_irrelevant_bind) apply (wp gts_wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do _ <- guarded_switch_to t;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do x <- get_thread_state t;
x <- assert (runnable x);
_ <- switch_to_thread t;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do x <- do x <- get_thread_state t;
assert (runnable x)
od;
_ <- switch_to_thread t;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (2 subgoals):
 1. \<And>P. \<lbrace>P\<rbrace> do x <- get_thread_state t;
assert (runnable x)
od \<lbrace>\<lambda>_. P\<rbrace>
 2. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do _ <- switch_to_thread t;
set_scheduler_action resume_cur_thread
od) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma switch_to_idle_thread_globals_equiv_scheduler[wp]:
  "\<lbrace>invs and globals_equiv_scheduler sta\<rbrace>
   switch_to_idle_thread
   \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>" apply (simp add: switch_to_idle_thread_def) apply (wp | simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> switch_to_idle_thread \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma gets_read_queue_ev_from_weak_sae:
  "(\<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t)
   \<Longrightarrow> equiv_valid_inv R B
         (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (\<lambda>s. f (ready_queues s d)))" apply (rule equiv_valid_guard_imp) apply wp apply (force simp: weak_scheduler_affects_equiv_def states_equiv_for_def equiv_for_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t \<Longrightarrow> equiv_valid_inv R B (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (\<lambda>s. f (ready_queues s d))) proof (prove)
goal (2 subgoals):
 1. \<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t \<Longrightarrow> equiv_valid_inv R B ?Q (gets (\<lambda>s. f (ready_queues s d)))
 2. \<And>s. \<lbrakk>\<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t; pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}\<rbrakk> \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>s t. B s t \<longrightarrow> weak_scheduler_affects_equiv aag l s t; pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}\<rbrakk> \<Longrightarrow> \<forall>s t. R s t \<and> B s t \<longrightarrow> f (ready_queues s d) = f (ready_queues t d) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma gets_ready_queue_midstrength_equiv_scheduler[wp]:
  "equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
     (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {})
     (gets (\<lambda>s. f (ready_queues s d)))" by (rule gets_read_queue_ev_from_weak_sae, auto)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (\<lambda>s. f (ready_queues s d)))
theory Scheduler_IF

lemma tcb_with_domain_at:
  "\<lbrakk> valid_queues s; x \<in> set (ready_queues s d p) \<rbrakk>
     \<Longrightarrow> \<exists>t. ekheap s x = Some t \<and> (tcb_domain t) = d" by (fastforce simp: valid_queues_def is_etcb_at_def etcb_at_def split: option.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_queues s; x \<in> set (ready_queues s d p)\<rbrakk> \<Longrightarrow> \<exists>t. ekheap s x = Some t \<and> tcb_domain t = d
theory Scheduler_IF

lemma if_ev_bind:
  "\<lbrakk> b \<Longrightarrow> equiv_valid I A B P (f >>= s); \<not> b \<Longrightarrow> equiv_valid I A B Q (g >>= s) \<rbrakk>
     \<Longrightarrow> equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ((if b then f else g) >>= s)" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>b \<Longrightarrow> equiv_valid I A B P (f >>= s); \<not> b \<Longrightarrow> equiv_valid I A B Q (g >>= s)\<rbrakk> \<Longrightarrow> equiv_valid I A B (\<lambda>s. (b \<longrightarrow> P s) \<and> (\<not> b \<longrightarrow> Q s)) ((if b then f else g) >>= s)
theory Scheduler_IF

lemma equiv_valid_cases':
  "\<lbrakk> \<And>s t. A s t \<Longrightarrow> I s t \<Longrightarrow> P s = P t;
     equiv_valid I A B (R and P) f; equiv_valid I A B ((\<lambda>s. \<not>P s) and R) f \<rbrakk>
     \<Longrightarrow> equiv_valid I A B R f" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>s t. \<lbrakk>A s t; I s t\<rbrakk> \<Longrightarrow> P s = P t; equiv_valid I A B (R and P) f; equiv_valid I A B ((\<lambda>s. \<not> P s) and R) f\<rbrakk> \<Longrightarrow> equiv_valid I A B R f
theory Scheduler_IF

lemma ev_weaken_pre_relation:
  "\<lbrakk> equiv_valid I A B P f; \<And>s t. A' s t \<Longrightarrow> A s t \<rbrakk>
     \<Longrightarrow> equiv_valid I A' B P f" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>equiv_valid I A B P f; \<And>s t. A' s t \<Longrightarrow> A s t\<rbrakk> \<Longrightarrow> equiv_valid I A' B P f
theory Scheduler_IF

lemma gets_cur_domain_reads_respects_scheduler[wp]:
  "equiv_valid (scheduler_equiv aag) A A \<top> (gets cur_domain)" apply (rule equiv_valid_guard_imp) apply wp apply (simp add: scheduler_equiv_def states_equiv_for_def equiv_for_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) A (\<lambda>_. True) (gets cur_domain) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) A ?Q (gets cur_domain)
 2. \<And>s. True \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. True \<Longrightarrow> \<forall>s t. scheduler_equiv aag s t \<and> A s t \<longrightarrow> cur_domain s = cur_domain t proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma gets_read_queue_reads_respects_scheduler[wp]:
  "weak_reads_respects_scheduler aag l
     (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (\<lambda>s. f (ready_queues s d)))" by (rule gets_read_queue_ev_from_weak_sae, simp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. weak_reads_respects_scheduler aag l (\<lambda>s. pasDomainAbs aag d \<inter> reads_scheduler aag l \<noteq> {}) (gets (\<lambda>s. f (ready_queues s d)))
theory Scheduler_IF

lemma cur_thread_update_unobservable:
  "\<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and scheduler_affects_equiv aag l st
                                               and (\<lambda>s. cur_domain s = cur_domain st)\<rbrace>
   modify (cur_thread_update (\<lambda>_. thread))
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" by (wpsimp simp: scheduler_affects_equiv_def scheduler_equiv_def domain_fields_equiv_def)

(* 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 (\<lambda>s. cur_domain s = cur_domain st)\<rbrace> modify (cur_thread_update (\<lambda>_. thread)) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
theory Scheduler_IF

lemma weak_scheduler_affects_equiv[intro]:
  "scheduler_affects_equiv aag l st s \<Longrightarrow> weak_scheduler_affects_equiv aag l st s" by (simp add: scheduler_affects_equiv_def weak_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_affects_equiv aag l st s \<Longrightarrow> weak_scheduler_affects_equiv aag l st s
theory Scheduler_IF

lemma midstrength_scheduler_affects_equiv[intro]:
  "scheduler_affects_equiv aag l st s \<Longrightarrow> midstrength_scheduler_affects_equiv aag l st s" by (simp add: scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_affects_equiv aag l st s \<Longrightarrow> midstrength_scheduler_affects_equiv aag l st s
theory Scheduler_IF

lemma get_cur_thread_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l
     (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l \<noteq> {})
     (gets cur_thread)" by (clarsimp simp: scheduler_equiv_def scheduler_affects_equiv_def domain_fields_equiv_def
                     gets_def get_def bind_def return_def equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (reads_scheduler_cur_domain aag l) (gets cur_thread)
theory Scheduler_IF

lemma get_scheduler_action_reads_respects_scheduler[wp]:
  "reads_respects_scheduler aag l
     (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l \<noteq> {})
     (gets scheduler_action)" by (clarsimp simp: scheduler_equiv_def scheduler_affects_equiv_def domain_fields_equiv_def
                     gets_def get_def bind_def return_def equiv_valid_def2 equiv_valid_2_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (reads_scheduler_cur_domain aag l) (gets scheduler_action)
theory Scheduler_IF

lemma switch_to_idle_thread_unobservable:
  "\<lbrace>(\<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\<rbrace>
   switch_to_idle_thread
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: switch_to_idle_thread_def) apply (wp cur_thread_update_unobservable arch_switch_to_idle_thread_unobservable) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
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 (\<lambda>s. cur_domain s = cur_domain st) and invs\<rbrace> switch_to_idle_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 (\<lambda>s. cur_domain s = cur_domain st) and invs\<rbrace> do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
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 (\<lambda>s. cur_domain s = cur_domain st) and invs) s \<Longrightarrow> \<not> reads_scheduler_cur_domain aag l s \<and> ((\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s) and invs) s \<and> cur_domain s = cur_domain st proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma switch_to_thread_unobservable:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "\<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and
          (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and
          scheduler_affects_equiv aag l st and scheduler_equiv aag st and invs and pas_refined aag\<rbrace>
         switch_to_thread t
         \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: switch_to_thread_def) apply (wp cur_thread_update_unobservable arch_switch_to_idle_thread_unobservable
            tcb_sched_action_unobservable arch_switch_to_thread_unobservable) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and scheduler_equiv aag st and invs and pas_refined aag\<rbrace> switch_to_thread t \<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 (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and scheduler_equiv aag st and invs and pas_refined aag\<rbrace> do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
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 (\<lambda>s. pasObjectAbs aag t \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st and scheduler_equiv aag st and invs and pas_refined aag) s \<Longrightarrow> (\<exists>y. get_tcb t s = Some y) \<longrightarrow> \<not> reads_scheduler_cur_domain aag l s \<and> pas_refined aag s \<and> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s) and invs) s \<and> pasObjectAbs aag t \<notin> reads_scheduler aag l \<and> cur_domain s = cur_domain st proof (prove)
goal:
No subgoals!