kings-crown/FVELER_Isabelle huggingface dataset:
theory Scheduler_IF

lemma context_update_cur_thread_snippit_cur_domain:
  "reads_respects_scheduler aag l
     (\<lambda>s. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and>
          (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s)
     (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc)))" apply wp apply (clarsimp simp: cur_thread_idle silc_inv_not_cur_thread del: notI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. reads_scheduler_cur_domain aag l s \<and> invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc))) proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<and> silc_inv aag st s \<and> (ct_idle s \<longrightarrow> uc = idle_context s) \<and> guarded_pas_domain aag s \<Longrightarrow> (invs and K (pasObjectAbs aag (cur_thread s) \<noteq> SilcLabel) and (\<lambda>sa. cur_thread s = idle_thread sa \<longrightarrow> uc = idle_context sa) and guarded_pas_domain aag) s proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma arch_globals_equiv_from_scheduler[Scheduler_IF_assms]:
  "\<lbrakk> arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s');
     cur_thread s' \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv s s' \<rbrakk>
     \<Longrightarrow> arch_globals_equiv (cur_thread s') (idle_thread s) (kheap s) (kheap s')
                            (arch_state s) (arch_state s') (machine_state s) (machine_state s')" by (clarsimp simp: arch_globals_equiv_scheduler_def arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s'); cur_thread s' \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_equiv s s'\<rbrakk> \<Longrightarrow> arch_globals_equiv (cur_thread s') (idle_thread s) (kheap s) (kheap s') (arch_state s) (arch_state s') (machine_state s) (machine_state s')
theory ArchScheduler_IF

lemma arch_globals_equiv_scheduler_refl[Scheduler_IF_assms]:
  "arch_globals_equiv_scheduler (kheap s) (kheap s) (arch_state s) (arch_state s)" by (simp add: idle_equiv_refl arch_globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv_scheduler (kheap s) (kheap s) (arch_state s) (arch_state s)
theory ArchScheduler_IF

lemma arch_globals_equiv_scheduler_sym[Scheduler_IF_assms]:
  "arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s')
   \<Longrightarrow> arch_globals_equiv_scheduler (kheap s') (kheap s) (arch_state s') (arch_state s)" by (auto simp: arch_globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s') \<Longrightarrow> arch_globals_equiv_scheduler (kheap s') (kheap s) (arch_state s') (arch_state s)
theory ArchScheduler_IF

lemma arch_globals_equiv_scheduler_trans[Scheduler_IF_assms]:
  "\<lbrakk> arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s');
     arch_globals_equiv_scheduler (kheap s') (kheap s'') (arch_state s') (arch_state s'') \<rbrakk>
     \<Longrightarrow> arch_globals_equiv_scheduler (kheap s) (kheap s'') (arch_state s) (arch_state s'')" by (clarsimp simp: arch_globals_equiv_scheduler_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_globals_equiv_scheduler (kheap s) (kheap s') (arch_state s) (arch_state s'); arch_globals_equiv_scheduler (kheap s') (kheap s'') (arch_state s') (arch_state s'')\<rbrakk> \<Longrightarrow> arch_globals_equiv_scheduler (kheap s) (kheap s'') (arch_state s) (arch_state s'')
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_trans[Scheduler_IF_assms, elim]:
  "\<lbrakk> arch_scheduler_affects_equiv s s'; arch_scheduler_affects_equiv s' s'' \<rbrakk>
     \<Longrightarrow> arch_scheduler_affects_equiv s s''" by (simp add: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>arch_scheduler_affects_equiv s s'; arch_scheduler_affects_equiv s' s''\<rbrakk> \<Longrightarrow> arch_scheduler_affects_equiv s s''
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_sym[Scheduler_IF_assms, elim]:
  "arch_scheduler_affects_equiv s s' \<Longrightarrow> arch_scheduler_affects_equiv s' s" by (simp add: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_scheduler_affects_equiv s s' \<Longrightarrow> arch_scheduler_affects_equiv s' s
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_sa_update[Scheduler_IF_assms, simp]:
  "arch_scheduler_affects_equiv (scheduler_action_update f s) s' =
   arch_scheduler_affects_equiv s s'"
  "arch_scheduler_affects_equiv s (scheduler_action_update f s') =
   arch_scheduler_affects_equiv s s'" by (auto simp: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_scheduler_affects_equiv (scheduler_action_update f s) s' = arch_scheduler_affects_equiv s s' &&& arch_scheduler_affects_equiv s (scheduler_action_update f s') = arch_scheduler_affects_equiv s s'
theory ArchScheduler_IF

lemma equiv_asid_cur_thread_update[Scheduler_IF_assms, simp]:
  "equiv_asid asid (cur_thread_update f s) s' = equiv_asid asid s s'"
  "equiv_asid asid s (cur_thread_update f s') = equiv_asid asid s s'" by (auto simp: equiv_asid_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_asid asid (cur_thread_update f s) s' = equiv_asid asid s s' &&& equiv_asid asid s (cur_thread_update f s') = equiv_asid asid s s'
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_cur_thread_update[Scheduler_IF_assms, simp]:
  "arch_scheduler_affects_equiv (cur_thread_update f s) s' = arch_scheduler_affects_equiv s s'"
  "arch_scheduler_affects_equiv s (cur_thread_update f s') = arch_scheduler_affects_equiv s s'" by (auto simp: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_scheduler_affects_equiv (cur_thread_update f s) s' = arch_scheduler_affects_equiv s s' &&& arch_scheduler_affects_equiv s (cur_thread_update f s') = arch_scheduler_affects_equiv s s'
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_domain_time_update[Scheduler_IF_assms, simp]:
  "arch_scheduler_affects_equiv (domain_time_update f s) s' = arch_scheduler_affects_equiv s s'"
  "arch_scheduler_affects_equiv s (domain_time_update f s') = arch_scheduler_affects_equiv s s'" by (auto simp: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_scheduler_affects_equiv (domain_time_update f s) s' = arch_scheduler_affects_equiv s s' &&& arch_scheduler_affects_equiv s (domain_time_update f s') = arch_scheduler_affects_equiv s s'
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_ekheap_update[Scheduler_IF_assms, simp]:
  "arch_scheduler_affects_equiv (ekheap_update f s) s' = arch_scheduler_affects_equiv s s'"
  "arch_scheduler_affects_equiv s (ekheap_update f s') = arch_scheduler_affects_equiv s s'" by (auto simp: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_scheduler_affects_equiv (ekheap_update f s) s' = arch_scheduler_affects_equiv s s' &&& arch_scheduler_affects_equiv s (ekheap_update f s') = arch_scheduler_affects_equiv s s'
theory ArchScheduler_IF

lemma arch_scheduler_affects_equiv_update[Scheduler_IF_assms]:
  "arch_scheduler_affects_equiv st s
   \<Longrightarrow> arch_scheduler_affects_equiv st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB y')\<rparr>)" by (clarsimp simp: arch_scheduler_affects_equiv_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. arch_scheduler_affects_equiv st s \<Longrightarrow> arch_scheduler_affects_equiv st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB y')\<rparr>)
theory ArchScheduler_IF

lemma equiv_asid_equiv_update[Scheduler_IF_assms]:
  "\<lbrakk> get_tcb x s = Some y; equiv_asid asid st s \<rbrakk>
     \<Longrightarrow> equiv_asid asid st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB y')\<rparr>)" by (clarsimp simp: equiv_asid_def obj_at_def get_tcb_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_tcb x s = Some y; equiv_asid asid st s\<rbrakk> \<Longrightarrow> equiv_asid asid st (s\<lparr>kheap := (kheap s)(x \<mapsto> TCB y')\<rparr>)
theory ArchScheduler_IF

lemma clearExMonitor_globals_equiv_scheduler[wp]:
  "do_machine_op clearExMonitor \<lbrace>globals_equiv_scheduler sta\<rbrace>" unfolding clearExMonitor_def including no_pre apply (wp dmo_no_mem_globals_equiv_scheduler) apply simp apply (simp add: simpler_modify_def valid_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler sta\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler sta\<rbrace> do_machine_op (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>globals_equiv_scheduler sta\<rbrace> do_machine_op (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>P s. P (underlying_memory s) \<Longrightarrow> P (underlying_memory (s\<lparr>exclusive_state := default_exclusive_state\<rparr>))
 2. \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> modify (exclusive_state_update (\<lambda>_. default_exclusive_state)) \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> modify (exclusive_state_update (\<lambda>_. default_exclusive_state)) \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma arch_switch_to_thread_globals_equiv_scheduler[Scheduler_IF_assms]:
  "\<lbrace>invs and globals_equiv_scheduler sta\<rbrace>
   arch_switch_to_thread thread
   \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>" unfolding arch_switch_to_thread_def storeWord_def by (wpsimp wp: clearExMonitor_globals_equiv_scheduler dmo_wp modify_wp thread_get_wp'
      | wp (once) globals_equiv_scheduler_inv'[where P="\<top>"])+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> arch_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 set_vm_root thread;
do_machine_op $ clearExMonitor
od \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
theory ArchScheduler_IF

lemma dmo_mol_exclusive_state[wp]:
  "do_machine_op (machine_op_lift mop) \<lbrace>\<lambda>s. P (exclusive_state (machine_state s))\<rbrace>" by (wp mol_exclusive_state dmo_wp
      | simp add: split_def dmo_bind_valid writeTTBR0_def isb_def dsb_def)+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (exclusive_state (machine_state s))\<rbrace> do_machine_op (machine_op_lift mop) \<lbrace>\<lambda>_ s. P (exclusive_state (machine_state s))\<rbrace>
theory ArchScheduler_IF

lemma set_vm_root_arch_scheduler_affects_equiv[wp]:
  "set_vm_root tcb \<lbrace>arch_scheduler_affects_equiv st\<rbrace>" unfolding arch_scheduler_affects_equiv_def by wpsimp

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>arch_scheduler_affects_equiv st\<rbrace> set_vm_root tcb \<lbrace>\<lambda>_. arch_scheduler_affects_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. exclusive_state (machine_state st) = exclusive_state (machine_state s')\<rbrace> set_vm_root tcb \<lbrace>\<lambda>_ s'. exclusive_state (machine_state st) = exclusive_state (machine_state s')\<rbrace>
theory ArchScheduler_IF

lemma store_cur_thread_fragment_midstrength_reads_respects:
  "equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
               (scheduler_affects_equiv aag l) invs
               (do y \<leftarrow> do_machine_op clearExMonitor;
                   x \<leftarrow> modify (cur_thread_update (\<lambda>_. t));
                   set_scheduler_action resume_cur_thread
                od)" apply (rule equiv_valid_guard_imp) apply (rule bind_ev_general[OF ev_asahi_ex_to_full_fragement]) apply (rule ev_asahi_to_asahi_ex_dmo_clearExMonitor) apply wp apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l invs (do y <- do_machine_op clearExMonitor;
x <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od) proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q (do y <- do_machine_op clearExMonitor;
x <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 2. \<And>s. invs s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) (asahi_ex_scheduler_affects_equiv aag l) ?P'3 (do_machine_op clearExMonitor)
 2. \<lbrace>?P''3\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s. invs s \<Longrightarrow> ?P'3 s \<and> ?P''3 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P''3\<rbrace> do_machine_op clearExMonitor \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>s. invs s \<Longrightarrow> True \<and> ?P''3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> True \<and> True proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma arch_switch_to_thread_globals_equiv_scheduler':
  "\<lbrace>invs and globals_equiv_scheduler sta\<rbrace>
   set_vm_root t
   \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>" by (rule globals_equiv_scheduler_inv', wpsimp)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> set_vm_root t \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
theory ArchScheduler_IF

lemma arch_switch_to_idle_thread_globals_equiv_scheduler[Scheduler_IF_assms, wp]:
  "\<lbrace>invs and globals_equiv_scheduler sta\<rbrace>
   arch_switch_to_idle_thread
   \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>" unfolding arch_switch_to_idle_thread_def storeWord_def by (wp dmo_wp modify_wp thread_get_wp' arch_switch_to_thread_globals_equiv_scheduler')

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> arch_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> gets idle_thread >>= set_vm_root \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
theory ArchScheduler_IF

lemma arch_switch_to_idle_thread_unobservable[Scheduler_IF_assms]:
  "\<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 st = cur_domain s) and invs\<rbrace>
   arch_switch_to_idle_thread
   \<lbrace>\<lambda>_ s. scheduler_affects_equiv aag l st s\<rbrace>" apply (simp add: arch_switch_to_idle_thread_def) apply wp apply (clarsimp simp add: scheduler_equiv_def domain_fields_equiv_def invs_def valid_state_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 st = cur_domain s) and invs\<rbrace> arch_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 st = cur_domain s) and invs\<rbrace> gets idle_thread >>= set_vm_root \<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 st = cur_domain s) and invs) s \<Longrightarrow> scheduler_affects_equiv aag l st s proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma clearExMonitor_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)\<rbrace>
   do_machine_op clearExMonitor
   \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>" apply (simp add: clearExMonitor_def) apply (rule hoare_pre) apply (wp dmo_wp modify_wp) apply (auto simp: states_equiv_for_def scheduler_affects_equiv_def equiv_for_def equiv_asids_def
                    equiv_asid_def scheduler_globals_frame_equiv_def silc_dom_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)\<rbrace> do_machine_op clearExMonitor \<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)\<rbrace> do_machine_op (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do_machine_op (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<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)) s \<Longrightarrow> ?Q s 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)) s \<Longrightarrow> scheduler_affects_equiv aag l st (s\<lparr>machine_state := machine_state s\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma arch_switch_to_thread_unobservable[Scheduler_IF_assms]:
  "\<lbrace>(\<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\<rbrace>
   arch_switch_to_thread t
   \<lbrace>\<lambda>_ s. scheduler_affects_equiv aag l st s\<rbrace>" apply (simp add: arch_switch_to_thread_def) apply (wp set_vm_root_scheduler_affects_equiv clearExMonitor_unobservable | simp)+ done

(* 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 st = cur_domain s) and invs\<rbrace> arch_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 scheduler_affects_equiv aag l st and (\<lambda>s. cur_domain st = cur_domain s) and invs\<rbrace> do y <- set_vm_root t;
do_machine_op clearExMonitor
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma next_domain_midstrength_equiv_scheduler[Scheduler_IF_assms]:
  "equiv_valid (scheduler_equiv aag) (weak_scheduler_affects_equiv aag l)
               (midstrength_scheduler_affects_equiv aag l) \<top> next_domain" apply (simp add: next_domain_def) apply (rule ev_modify) apply (clarsimp simp: equiv_for_def equiv_asid_def equiv_asids_def Let_def scheduler_equiv_def
                        globals_equiv_scheduler_def silc_dom_equiv_def domain_fields_equiv_def
                        weak_scheduler_affects_equiv_def midstrength_scheduler_affects_equiv_def
                        states_equiv_for_def idle_equiv_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (weak_scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (\<lambda>_. True) next_domain proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (weak_scheduler_affects_equiv aag l) (midstrength_scheduler_affects_equiv aag l) (\<lambda>_. True) (modify (\<lambda>s. let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s)) proof (prove)
goal (1 subgoal):
 1. \<And>s t. \<lbrakk>True; True; weak_scheduler_affects_equiv aag l s t; scheduler_equiv aag s t\<rbrakk> \<Longrightarrow> scheduler_equiv aag (let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s) (let domain_index' = Suc (domain_index t) mod length (domain_list t); next_dom = domain_list t ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) t) \<and> midstrength_scheduler_affects_equiv aag l (let domain_index' = Suc (domain_index s) mod length (domain_list s); next_dom = domain_list s ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) s) (let domain_index' = Suc (domain_index t) mod length (domain_list t); next_dom = domain_list t ! domain_index' in trans_state (\<lambda>e. e\<lparr>domain_index_internal := domain_index', cur_domain_internal := fst next_dom, domain_time_internal := snd next_dom, work_units_completed_internal := 0\<rparr>) t) proof (prove)
goal:
No subgoals!
theory ArchScheduler_IF

lemma resetTimer_exclusive_state[wp]:
  "resetTimer \<lbrace>\<lambda>s. P (exclusive_state s)\<rbrace>" by (wpsimp simp: resetTimer_def wp: mol_exclusive_state)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (exclusive_state s)\<rbrace> resetTimer \<lbrace>\<lambda>_ s. P (exclusive_state s)\<rbrace>
theory ArchScheduler_IF

lemma resetTimer_irq_state[wp]:
  "resetTimer \<lbrace>\<lambda>s. P (irq_state s)\<rbrace>" apply (simp add: resetTimer_def machine_op_lift_def machine_rest_lift_def) apply (wp | wpc| simp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state s)\<rbrace> resetTimer \<lbrace>\<lambda>_ s. P (irq_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (irq_state s)\<rbrace> do mr <- gets machine_state_rest;
(r, mr') <- select_f (ignore_failure resetTimer_impl mr);
modify (machine_state_rest_update (\<lambda>_. mr'))
od \<lbrace>\<lambda>_ s. P (irq_state s)\<rbrace> proof (prove)
goal:
No subgoals!