theory Scheduler_IF

lemma 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 e: "\<And>P. f \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace>"
  assumes s: "\<And>P. f \<lbrace>\<lambda>s. P (scheduler_action s)\<rbrace>"
  assumes w: "\<And>P. f \<lbrace>\<lambda>s. P (work_units_completed s)\<rbrace>"
  assumes i: "\<And>P. f \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace>"
  assumes x: "f \<lbrace>arch_scheduler_affects_equiv st\<rbrace>"
  shows "f \<lbrace>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: 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 e s w i x hoare_vcg_imp_lift) apply fastforce done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. 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>scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. 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> cur_thread st = cur_thread s' \<and> scheduler_action st = scheduler_action s' \<and> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s' \<and> idle_thread st = idle_thread s' \<and> (cur_thread st \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s' \<and> scheduler_action st = scheduler_action s' \<and> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s' \<and> idle_thread st = idle_thread s' \<and> (cur_thread st \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s' \<and> scheduler_action st = scheduler_action s' \<and> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s' \<and> idle_thread st = idle_thread s' \<and> (cur_thread st \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s' \<and> scheduler_action st = scheduler_action s' \<and> work_units_completed st = work_units_completed s' \<and> scheduler_globals_frame_equiv st s' \<and> idle_thread st = idle_thread s' \<and> (cur_thread st \<noteq> idle_thread s' \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (cur_thread st \<noteq> idle_thread s \<longrightarrow> arch_scheduler_affects_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> cur_thread st = cur_thread s \<and> scheduler_action st = scheduler_action s \<and> work_units_completed st = work_units_completed s \<and> scheduler_globals_frame_equiv st s \<and> idle_thread st = idle_thread s \<and> (\<not> cur_thread st \<noteq> idle_thread s \<or> arch_scheduler_affects_equiv st s)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>scheduler_affects_equiv aag l st\<rbrace> f \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>

goal:
No subgoals!