kings-crown/FVELER_Isabelle huggingface dataset:
theory Scheduler_IF

lemma reschedule_required_scheduler_affects_equiv_unobservable[wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "\<lbrace>pas_refined aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)
                          and valid_queues and valid_etcbs and valid_sched_action
                          and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace>
         reschedule_required
         \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: reschedule_required_def) apply (wp set_scheduler_action_unobservable tcb_sched_action_unobservable | wpc | simp)+ apply (fastforce dest!: switch_to_cur_domain' cur_thread_cur_domain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and valid_queues and valid_etcbs and valid_sched_action and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> reschedule_required \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>pas_refined aag and (\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and valid_queues and valid_etcbs and valid_sched_action and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do action <- gets scheduler_action;
y <- case action of switch_thread t \<Rightarrow> tcb_sched_action tcb_sched_enqueue t | _ \<Rightarrow> return ();
set_scheduler_action choose_new_thread
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pas_refined aag s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> valid_queues s \<and> valid_etcbs s \<and> valid_sched_action s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<Longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> cur_domain st = cur_domain s) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> cur_domain st = cur_domain s) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma timer_tick_reads_respects_scheduler:
  assumes domains_distinct: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l
           (invs and guarded_pas_domain aag and pas_refined aag and valid_sched) timer_tick" apply (rule reads_respects_scheduler_cases') apply (rule timer_tick_reads_respects_scheduler_cur_domain[OF domains_distinct]) apply simp apply (rule timer_tick_reads_respects_scheduler_unobservable[OF domains_distinct]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and guarded_pas_domain aag and pas_refined aag and valid_sched) timer_tick proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' timer_tick
 2. \<And>s. \<lbrakk>(invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P' s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' timer_tick
 4. \<And>s. \<lbrakk>(invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>(invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> (reads_scheduler_cur_domain aag l and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' timer_tick
 3. \<And>s. \<lbrakk>(invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' timer_tick
 2. \<And>s. \<lbrakk>(invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>(invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<not> reads_scheduler_cur_domain aag l s) and invs and guarded_pas_domain aag and pas_refined aag and valid_sched) s proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma gets_ev':
  "equiv_valid_inv I A (P and K(\<forall>s t. P s \<longrightarrow> P t \<longrightarrow> I s t \<and> A s t \<longrightarrow> f s = f t)) (gets f)" by (clarsimp simp: equiv_valid_def2 equiv_valid_2_def gets_def get_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv I A (P and K (\<forall>s t. P s \<longrightarrow> P t \<longrightarrow> I s t \<and> A s t \<longrightarrow> f s = f t)) (gets f)
theory Scheduler_IF

lemma equiv_valid_2_bind_right:
  "\<lbrakk> \<And>rv. equiv_valid_2 D A A R T' (Q rv) g' (g rv);
     \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>;
     \<And>st. \<lbrace>D st and A st and S'\<rbrace> f \<lbrace>\<lambda>r. D st\<rbrace>;
     \<And>st. \<lbrace>A st and D st and S''\<rbrace> f \<lbrace>\<lambda>r. A st\<rbrace>;
     \<And>s. T s \<Longrightarrow> P s \<and> S s \<and> S' s \<and> S'' s;
     \<And>s. T' s \<Longrightarrow> P s\<rbrakk>
     \<Longrightarrow> equiv_valid_2 D A A R T' T g' (f >>= g) " apply atomize apply (clarsimp simp: equiv_valid_2_def equiv_valid_def2 valid_def bind_def) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<And>rv. equiv_valid_2 D A A R T' (Q rv) g' (g rv); \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>; \<And>st. \<lbrace>D st and A st and S'\<rbrace> f \<lbrace>\<lambda>r. D st\<rbrace>; \<And>st. \<lbrace>A st and D st and S''\<rbrace> f \<lbrace>\<lambda>r. A st\<rbrace>; \<And>s. T s \<Longrightarrow> P s \<and> S s \<and> S' s \<and> S'' s; \<And>s. T' s \<Longrightarrow> P s\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A R T' T g' (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>rv. equiv_valid_2 D A A R T' (Q rv) g' (g rv); \<lbrace>S\<rbrace> f \<lbrace>Q\<rbrace>; \<forall>st. \<lbrace>D st and A st and S'\<rbrace> f \<lbrace>\<lambda>r. D st\<rbrace>; \<forall>st. \<lbrace>A st and D st and S''\<rbrace> f \<lbrace>\<lambda>r. A st\<rbrace>; \<forall>s. T s \<longrightarrow> P s \<and> S s \<and> S' s \<and> S'' s; \<forall>s. T' s \<longrightarrow> P s\<rbrakk> \<Longrightarrow> equiv_valid_2 D A A R T' T g' (f >>= g) proof (prove)
goal (1 subgoal):
 1. \<And>s t a b aa ba ab bb. \<lbrakk>\<forall>rv s t. T' s \<and> Q rv t \<and> D s t \<and> A s t \<longrightarrow> (\<forall>x\<in>fst (g' s). case x of (rva, s') \<Rightarrow> \<forall>x\<in>fst (g rv t). case x of (rvb, t') \<Rightarrow> R rva rvb \<and> D s' t' \<and> A s' t'); \<forall>s. S s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (x, xa) \<Rightarrow> Q x xa); \<forall>st s. D st s \<and> A st s \<and> S' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, x) \<Rightarrow> D st x); \<forall>st s. A st s \<and> D st s \<and> S'' s \<longrightarrow> (\<forall>x\<in>fst (f s). case x of (r, x) \<Rightarrow> A st x); \<forall>s. T s \<longrightarrow> P s \<and> S s \<and> S' s \<and> S'' s; \<forall>s. T' s \<longrightarrow> P s; (a, b) \<in> fst (g' s); (aa, ba) \<in> fst (f t); (ab, bb) \<in> fst (g aa ba); T' s; T t; D s t; A s t\<rbrakk> \<Longrightarrow> R a ab \<and> D b bb \<and> A b bb proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma dmo_if_distr:
  "do_machine_op (if A then f else g) = (if A then (do_machine_op f) else (do_machine_op g))" by simp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (if A then f else g) = (if A then do_machine_op f else do_machine_op g)
theory Scheduler_IF

lemma dmo_gets_distr:
  "do_machine_op (gets f) = gets (\<lambda>s. f (machine_state s))" by (clarsimp simp: do_machine_op_def bind_assoc gets_def get_def
                     simpler_modify_def select_f_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (gets f) = gets (\<lambda>s. f (machine_state s))
theory Scheduler_IF

lemma dmo_modify_distr:
  "do_machine_op (modify f) = modify (machine_state_update f)" by (fastforce simp: do_machine_op_def bind_assoc gets_def get_def
                      simpler_modify_def select_f_def bind_def return_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. do_machine_op (modify f) = modify (machine_state_update f)
theory Scheduler_IF

lemma get_irq_state_reads_respects_scheduler_trivial:
  "reads_respects_scheduler aag l (domain_sep_inv False st) (get_irq_state irq)" apply (simp add: get_irq_state_def) apply (rule equiv_valid_guard_imp) apply (rule_tac P="domain_sep_inv False st" in  gets_ev') apply clarsimp apply (clarsimp simp: domain_sep_inv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (domain_sep_inv False st) (get_irq_state irq) proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (domain_sep_inv False st) (gets (\<lambda>s. interrupt_states s irq)) proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?Q (gets (\<lambda>s. interrupt_states s irq))
 2. \<And>s. domain_sep_inv False st s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. domain_sep_inv False st s \<Longrightarrow> (domain_sep_inv False st and K (\<forall>s t. domain_sep_inv False st s \<longrightarrow> domain_sep_inv False st t \<longrightarrow> scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> interrupt_states s irq = interrupt_states t irq)) s proof (prove)
goal (1 subgoal):
 1. \<And>s sa t. \<lbrakk>domain_sep_inv False st s; domain_sep_inv False st sa; domain_sep_inv False st t; scheduler_equiv aag sa t; scheduler_affects_equiv aag l sa t\<rbrakk> \<Longrightarrow> interrupt_states sa irq = interrupt_states t irq proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma reads_respects_only_scheduler:
  "reads_respects_scheduler aag SilcLabel P f \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) \<top>\<top> P f" by (fastforce simp: equiv_valid_def2 equiv_valid_2_def scheduler_affects_equiv_def
                      reads_scheduler_def states_equiv_for_def equiv_for_def scheduler_equiv_def
                      equiv_asids_def globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag SilcLabel) P f \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (\<lambda>_ _. True) P f
theory Scheduler_IF

lemma get_tcb_scheduler_equiv:
  "\<lbrakk> pasObjectAbs aag rv \<in> reads_scheduler aag l; scheduler_affects_equiv aag l s t \<rbrakk>
     \<Longrightarrow> get_tcb rv s = get_tcb rv t" by (clarsimp simp: get_tcb_def scheduler_affects_equiv_def states_equiv_for_def equiv_for_def
              split: option.splits kernel_object.splits)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pasObjectAbs aag rv \<in> reads_scheduler aag l; scheduler_affects_equiv aag l s t\<rbrakk> \<Longrightarrow> get_tcb rv s = get_tcb rv t
theory Scheduler_IF

lemma as_user_reads_respects_scheduler:
  "reads_respects_scheduler aag l (K (pasObjectAbs aag rv \<in> reads_scheduler aag l) and
                                   (\<lambda>s. rv \<noteq> idle_thread s) and K (det f))
                            (as_user rv f)" apply (rule gen_asm_ev) apply (simp add: as_user_def) apply (wp select_f_ev | wpc | simp)+ apply (clarsimp simp: get_tcb_scheduler_equiv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (K (pasObjectAbs aag rv \<in> reads_scheduler aag l) and (\<lambda>s. rv \<noteq> idle_thread s) and K (det f)) (as_user rv f) proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (K (pasObjectAbs aag rv \<in> reads_scheduler aag l) and (\<lambda>s. rv \<noteq> idle_thread s)) (as_user rv f) proof (prove)
goal (1 subgoal):
 1. det f \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ((\<lambda>y. pasObjectAbs aag rv \<in> reads_scheduler aag l) and (\<lambda>s. rv \<noteq> idle_thread s)) (do tcb <- gets_the (get_tcb rv);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object rv (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>det f; pasObjectAbs aag rv \<in> reads_scheduler aag l \<and> rv \<noteq> idle_thread s\<rbrakk> \<Longrightarrow> \<forall>s t. scheduler_equiv aag s t \<and> scheduler_affects_equiv aag l s t \<longrightarrow> get_tcb rv s = get_tcb rv t proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma idle_equiv_identical_kheap_updates:
  "\<lbrakk> identical_kheap_updates s t kh kh'; idle_equiv s t \<rbrakk>
     \<Longrightarrow> idle_equiv (s\<lparr>kheap := kh\<rparr>) (t\<lparr>kheap := kh'\<rparr>)" apply (clarsimp simp: identical_kheap_updates_def idle_equiv_def tcb_at_def2) apply (drule_tac x="idle_thread t" in spec) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>identical_kheap_updates s t kh kh'; idle_equiv s t\<rbrakk> \<Longrightarrow> idle_equiv (s\<lparr>kheap := kh\<rparr>) (t\<lparr>kheap := kh'\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x. kh x \<noteq> kh' x \<longrightarrow> kheap s x = kh x \<and> kheap t x = kh' x; idle_thread s = idle_thread t; \<forall>tcb. kheap s (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap t (idle_thread t) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); (\<exists>tcb. kheap s (idle_thread t) = Some (TCB tcb)) = (\<exists>tcb. kheap t (idle_thread t) = Some (TCB tcb))\<rbrakk> \<Longrightarrow> (\<forall>tcb. kh (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kh' (idle_thread t) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<exists>tcb. kh (idle_thread t) = Some (TCB tcb)) = (\<exists>tcb. kh' (idle_thread t) = Some (TCB tcb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idle_thread s = idle_thread t; \<forall>tcb. kheap s (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kheap t (idle_thread t) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb')); (\<exists>tcb. kheap s (idle_thread t) = Some (TCB tcb)) = (\<exists>tcb. kheap t (idle_thread t) = Some (TCB tcb)); kh (idle_thread t) \<noteq> kh' (idle_thread t) \<longrightarrow> kheap s (idle_thread t) = kh (idle_thread t) \<and> kheap t (idle_thread t) = kh' (idle_thread t)\<rbrakk> \<Longrightarrow> (\<forall>tcb. kh (idle_thread t) = Some (TCB tcb) \<longrightarrow> (\<forall>tcb'. kh' (idle_thread t) = Some (TCB tcb') \<longrightarrow> arch_tcb_context_get (tcb_arch tcb) = arch_tcb_context_get (tcb_arch tcb'))) \<and> (\<exists>tcb. kh (idle_thread t) = Some (TCB tcb)) = (\<exists>tcb. kh' (idle_thread t) = Some (TCB tcb)) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma restart_not_idle:
  "\<lbrakk> valid_idle s; st_tcb_at ((=) Restart) t s \<rbrakk>
     \<Longrightarrow> t \<noteq> idle_thread s" by (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; st_tcb_at ((=) Restart) t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s
theory Scheduler_IF

lemma as_user_silc_dom_equiv[wp]:
  "\<lbrace>K (pasObjectAbs aag x \<noteq> SilcLabel) and silc_dom_equiv aag st\<rbrace>
   as_user x f
   \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace>" apply (simp add: as_user_def) apply (wp dxo_wp_weak set_object_wp | wpc | simp)+ apply (clarsimp simp: silc_dom_equiv_def equiv_for_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (pasObjectAbs aag x \<noteq> SilcLabel) and silc_dom_equiv aag st\<rbrace> as_user x f \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. pasObjectAbs aag x \<noteq> SilcLabel) and silc_dom_equiv aag st\<rbrace> do tcb <- gets_the (get_tcb x);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object x (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. pasObjectAbs aag x \<noteq> SilcLabel \<and> silc_dom_equiv aag st s \<Longrightarrow> (\<exists>y. get_tcb x s = Some y) \<longrightarrow> (\<forall>xa\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb x s))))). \<forall>xb xc. xa = (xb, xc) \<longrightarrow> silc_dom_equiv aag st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_arch := arch_tcb_context_set xc (tcb_arch (the (get_tcb x s)))\<rparr>))\<rparr>)) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma set_scheduler_action_wp[wp]:
  "\<lbrace>\<lambda>s. P () (s\<lparr>scheduler_action := a\<rparr>)\<rbrace> set_scheduler_action a \<lbrace>P\<rbrace>" by (simp add: set_scheduler_action_def | wp)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P () (scheduler_action_update (\<lambda>_. a) s)\<rbrace> set_scheduler_action a \<lbrace>P\<rbrace>
theory Scheduler_IF

lemma scheduler_affects_equiv_update:
  "\<lbrakk> get_tcb x s = Some y; pasObjectAbs aag x \<notin> reads_scheduler aag l;
     scheduler_affects_equiv aag l st s \<rbrakk>
     \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB y')\<rparr>)" by (clarsimp simp: scheduler_affects_equiv_def equiv_for_def equiv_asids_def
                     states_equiv_for_def scheduler_globals_frame_equiv_def
                     arch_scheduler_affects_equiv_update equiv_asid_equiv_update)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb x s = Some y; pasObjectAbs aag x \<notin> reads_scheduler aag l; scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB y')\<rparr>)
theory Scheduler_IF

lemma as_user_scheduler_affects_equiv[wp]:
  "\<lbrace>K (pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace>
   as_user x f
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: as_user_def) apply (wp gts_wp set_object_wp | wpc)+ apply (intro impI conjI allI) apply (fastforce intro!: scheduler_affects_equiv_update) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>K (pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> as_user x f \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st\<rbrace> do tcb <- gets_the (get_tcb x);
(a, uc') <- select_f (f (arch_tcb_context_get (tcb_arch tcb)));
y <- set_object x (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set uc' (tcb_arch tcb)\<rparr>));
return a
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st) s \<Longrightarrow> get_tcb x s \<noteq> None \<longrightarrow> (\<forall>xa\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb x s))))). \<forall>xb xc. xa = (xb, xc) \<longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_arch := arch_tcb_context_set xc (tcb_arch (the (get_tcb x s)))\<rparr>))\<rparr>)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>((\<lambda>y. pasObjectAbs aag x \<notin> reads_scheduler aag l) and scheduler_affects_equiv aag l st) s; get_tcb x s \<noteq> None\<rbrakk> \<Longrightarrow> \<forall>xa\<in>fst (f (arch_tcb_context_get (tcb_arch (the (get_tcb x s))))). \<forall>xb xc. xa = (xb, xc) \<longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB (the (get_tcb x s)\<lparr>tcb_arch := arch_tcb_context_set xc (tcb_arch (the (get_tcb x s)))\<rparr>))\<rparr>) proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma SilcLabel_affects_scheduler_equiv:
  "scheduler_equiv aag s t \<Longrightarrow> scheduler_affects_equiv aag SilcLabel s t" by (simp add: scheduler_affects_equiv_def reads_scheduler_def states_equiv_for_def
                equiv_for_def scheduler_equiv_def equiv_asids_def globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. scheduler_equiv aag s t \<Longrightarrow> scheduler_affects_equiv aag SilcLabel s t
theory Scheduler_IF

lemma st_tcb_at_not_idle_thread:
  "\<lbrakk> invs s; st_tcb_at ((=) t_st) t s; t_st \<noteq> IdleThreadState \<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s" apply (frule st_tcb_at_tcb_at) apply (fastforce dest: st_tcb_at_idle_thread) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at ((=) t_st) t s; t_st \<noteq> IdleThreadState\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; st_tcb_at ((=) t_st) t s; t_st \<noteq> IdleThreadState; tcb_at t s\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread s proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma bind_return_ign:
  "\<lbrace>P\<rbrace> (f >>= (\<lambda>_. return x)) \<lbrace>\<lambda>_. Q\<rbrace>
   \<Longrightarrow> \<lbrace>P\<rbrace> (f >>= (\<lambda>_. return y)) \<lbrace>\<lambda>_. Q\<rbrace>" apply (fastforce simp: valid_def bind_def return_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>P\<rbrace> do _ <- f;
return x
od \<lbrace>\<lambda>_. Q\<rbrace> \<Longrightarrow> \<lbrace>P\<rbrace> do _ <- f;
return y
od \<lbrace>\<lambda>_. Q\<rbrace> proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma op_eq_unit_dc:
  "((=) :: unit \<Rightarrow> unit \<Rightarrow> bool) = (dc)" apply (rule ext)+ apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (=) = dc proof (prove)
goal (1 subgoal):
 1. \<And>x xa. (x = xa) = dc x xa proof (prove)
goal:
No subgoals!
theory Scheduler_IF

lemma cur_thread_idle':
  "\<lbrakk> valid_idle s; only_idle s \<rbrakk> \<Longrightarrow> ct_idle s = (cur_thread s = idle_thread s)" apply (rule iffI) apply (clarsimp simp: only_idle_def ct_in_state_def ) apply (clarsimp simp: valid_idle_def ct_in_state_def pred_tcb_at_def obj_at_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; only_idle s\<rbrakk> \<Longrightarrow> ct_idle s = (cur_thread s = idle_thread s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_idle s; only_idle s; ct_idle s\<rbrakk> \<Longrightarrow> cur_thread s = idle_thread s
 2. \<lbrakk>valid_idle s; only_idle s; cur_thread s = idle_thread s\<rbrakk> \<Longrightarrow> ct_idle s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_idle s; only_idle s; cur_thread s = idle_thread s\<rbrakk> \<Longrightarrow> ct_idle s proof (prove)
goal:
No subgoals!