theory ArchScheduler_IF

lemma ev_asahi_to_asahi_ex_dmo_clearExMonitor:
  "equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l)
               (asahi_ex_scheduler_affects_equiv aag l) \<top> (do_machine_op clearExMonitor)" apply (simp add: clearExMonitor_def) apply (wp dmo_ev) apply (rule ev_modify) apply clarsimp apply (rule conjI) apply (clarsimp simp: scheduler_equiv_def domain_fields_equiv_def globals_equiv_scheduler_def
                         silc_dom_equiv_def equiv_for_def) apply (clarsimp simp: midstrength_scheduler_affects_equiv_def asahi_scheduler_affects_equiv_def
                        asahi_ex_scheduler_affects_equiv_def states_equiv_for_def equiv_for_def
                        arch_scheduler_affects_equiv_def equiv_asids_def equiv_asid_def
                        scheduler_globals_frame_equiv_def
              simp del: split_paired_All) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) (asahi_ex_scheduler_affects_equiv aag l) (\<lambda>_. True) (do_machine_op clearExMonitor) proof (prove)
goal (1 subgoal):
 1. equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) (asahi_ex_scheduler_affects_equiv aag l) (\<lambda>_. True) (do_machine_op (modify (exclusive_state_update (\<lambda>_. default_exclusive_state)))) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. equiv_valid (\<lambda>ms ms'. scheduler_equiv aag (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (\<lambda>ms ms'. midstrength_scheduler_affects_equiv aag l (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (\<lambda>ms ms'. asahi_ex_scheduler_affects_equiv aag l (s\<lparr>machine_state := ms\<rparr>) (s'\<lparr>machine_state := ms'\<rparr>)) (K (True \<and> True)) (modify (exclusive_state_update (\<lambda>_. default_exclusive_state))) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>K (True \<and> True) sa; K (True \<and> True) t; midstrength_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) \<and> asahi_ex_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>midstrength_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) \<and> asahi_ex_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>s s' sa t. \<lbrakk>midstrength_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> scheduler_equiv aag (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>)
 2. \<And>s s' sa t. \<lbrakk>midstrength_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa t. \<lbrakk>midstrength_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>); scheduler_equiv aag (s\<lparr>machine_state := sa\<rparr>) (s'\<lparr>machine_state := t\<rparr>)\<rbrakk> \<Longrightarrow> asahi_ex_scheduler_affects_equiv aag l (s\<lparr>machine_state := sa\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) (s'\<lparr>machine_state := t\<lparr>exclusive_state := default_exclusive_state\<rparr>\<rparr>) proof (prove)
goal:
No subgoals!