theory Scheduler_IF

lemma asahi_scheduler_affects_equiv_unobservable:
  assumes a: "\<And>P Q R S st. f \<lbrace>states_equiv_for P Q R S st\<rbrace>"
  assumes c: "\<And>P. f \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>"
  assumes w: "\<And>P. f \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace>"
  shows "f \<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace>" proof - have d: "\<lbrace>scheduler_globals_frame_equiv st\<rbrace> f \<lbrace>\<lambda>_. scheduler_globals_frame_equiv st\<rbrace>" apply (simp add: globals_frame_equiv_as_states_equiv[abs_def]) apply (clarsimp simp add: valid_def) apply (frule use_valid[OF _ a]) apply assumption apply (simp add: states_equiv_for_def equiv_for_def equiv_asids_def) done show ?thesis apply (simp add: asahi_scheduler_affects_equiv_def[abs_def]) apply (rule hoare_pre) apply (wps c) apply (wp hoare_weak_lift_imp a silc_dom_equiv_states_equiv_lift d w) apply clarsimp done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. asahi_scheduler_affects_equiv aag l st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. asahi_scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_globals_frame_equiv st\<rbrace> f \<lbrace>\<lambda>_. scheduler_globals_frame_equiv st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s\<rbrace> f \<lbrace>\<lambda>_ s. states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (b\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) b proof (prove)
goal (2 subgoals):
 1. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s; (a, b) \<in> fst (f s)\<rbrakk> \<Longrightarrow> states_equiv_for (?P9 s a b) (?Q9 s a b) (?R9 s a b) (?S9 s a b) (?st9 s a b) s
 2. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s; (a, b) \<in> fst (f s); states_equiv_for (?P9 s a b) (?Q9 s a b) (?R9 s a b) (?S9 s a b) (?st9 s a b) b\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (b\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) b proof (prove)
goal (1 subgoal):
 1. \<And>s a b. \<lbrakk>states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) s; (a, b) \<in> fst (f s); states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (s\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) b\<rbrakk> \<Longrightarrow> states_equiv_for (\<lambda>x. False) (\<lambda>_. False) (\<lambda>_. False) (\<lambda>_. False) (b\<lparr>machine_state := machine_state st, arch_state := arch_state st\<rparr>) b proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>scheduler_globals_frame_equiv st\<rbrace> f \<lbrace>\<lambda>_. scheduler_globals_frame_equiv st\<rbrace>

goal (1 subgoal):
 1. \<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. asahi_scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. asahi_scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s'. 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' \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s')\<rbrace> f \<lbrace>\<lambda>_ s'. 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' \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q3\<rbrace> f \<lbrace>\<lambda>_ s'. 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' \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s') \<longrightarrow> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s')\<rbrace>
 2. \<And>s. 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 \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s) \<Longrightarrow> ?Q3 s proof (prove)
goal (2 subgoals):
 1. \<And>prev_s. \<lbrace>?P6 prev_s\<rbrace> f \<lbrace>\<lambda>rv s'. 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' \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l prev_s) \<longrightarrow> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s')\<rbrace>
 2. \<And>s. 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 \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s) \<Longrightarrow> ?P6 s s proof (prove)
goal (1 subgoal):
 1. \<And>s. 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 \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st 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) st s \<and> ((pasDomainAbs aag (cur_domain st) \<inter> reads_scheduler aag l = {} \<longrightarrow> reads_scheduler_cur_domain aag l s) \<longrightarrow> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>asahi_scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. asahi_scheduler_affects_equiv aag l st\<rbrace>

goal:
No subgoals!