theory Schedule_R

lemma switchToIdleThread_corres:
  "corres dc invs invs_no_cicd' switch_to_idle_thread switchToIdleThread" apply (simp add: switch_to_idle_thread_def Thread_H.switchToIdleThread_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getIdleThread_corres]) apply (rule corres_split[OF arch_switchToIdleThread_corres]) apply (unfold setCurThread_def) apply (rule corres_trivial, rule corres_modify) apply (simp add: state_relation_def cdt_relation_def) apply (wp+, simp+) apply (simp add: invs_unique_refs invs_valid_vs_lookup invs_valid_objs invs_valid_asid_map
                    invs_arch_state invs_valid_global_objs invs_psp_aligned invs_distinct
                    invs_valid_idle invs_vspace_objs) apply (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc invs all_invs_but_ct_idle_or_in_cur_domain' switch_to_idle_thread global.switchToIdleThread proof (prove)
goal (1 subgoal):
 1. corres dc invs all_invs_but_ct_idle_or_in_cur_domain' (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) (do thread <- getIdleThread;
y <- Arch.switchToIdleThread;
setCurThread thread
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do thread <- gets idle_thread;
y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) (do thread <- getIdleThread;
y <- Arch.switchToIdleThread;
setCurThread thread
od)
 2. \<And>s. invs s \<Longrightarrow> ?Q s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>thread threada. thread = threada \<Longrightarrow> corres dc (?R4 thread) (?R'4 threada) (do y <- arch_switch_to_idle_thread;
modify (cur_thread_update (\<lambda>_. thread))
od) (do y <- Arch.switchToIdleThread;
setCurThread threada
od)
 2. \<lbrace>?Q4\<rbrace> gets idle_thread \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> getIdleThread \<lbrace>?R'4\<rbrace>
 4. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread threada y ya. \<lbrakk>thread = threada; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R8 thread threada y) (?R'8 thread threada ya) (modify (cur_thread_update (\<lambda>_. thread))) (setCurThread threada)
 2. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q9 thread\<rbrace> arch_switch_to_idle_thread \<lbrace>?R8 thread threada\<rbrace>
 3. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q'10 threada\<rbrace> Arch.switchToIdleThread \<lbrace>?R'8 thread threada\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets idle_thread \<lbrace>\<lambda>thread. valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle and ?Q9 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getIdleThread \<lbrace>\<lambda>threada. valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle' and ?Q'10 threada\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread threada y ya. \<lbrakk>thread = threada; dc y ya\<rbrakk> \<Longrightarrow> corres dc (?R8 thread threada y) (?R'8 thread threada ya) (modify (cur_thread_update (\<lambda>_. thread))) (modify (ksCurThread_update (\<lambda>_. threada)))
 2. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q9 thread\<rbrace> arch_switch_to_idle_thread \<lbrace>?R8 thread threada\<rbrace>
 3. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q'10 threada\<rbrace> Arch.switchToIdleThread \<lbrace>?R'8 thread threada\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets idle_thread \<lbrace>\<lambda>thread. valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle and ?Q9 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getIdleThread \<lbrace>\<lambda>threada. valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle' and ?Q'10 threada\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>thread threada y ya s s'. \<lbrakk>thread = threada; dc y ya; True; True; (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (s\<lparr>cur_thread := thread\<rparr>, s'\<lparr>ksCurThread := threada\<rparr>) \<in> state_relation
 2. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q9 thread\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q'10 threada\<rbrace> Arch.switchToIdleThread \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets idle_thread \<lbrace>\<lambda>thread. valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle and ?Q9 thread\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> getIdleThread \<lbrace>\<lambda>threada. valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle' and ?Q'10 threada\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q9 thread\<rbrace> arch_switch_to_idle_thread \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>thread threada. thread = threada \<Longrightarrow> \<lbrace>?Q'10 threada\<rbrace> Arch.switchToIdleThread \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<lbrace>?Q4\<rbrace> gets idle_thread \<lbrace>\<lambda>thread. valid_arch_state and valid_objs and valid_asid_map and unique_table_refs \<circ> caps_of_state and valid_vs_lookup and valid_global_objs and pspace_aligned and pspace_distinct and valid_vspace_objs and valid_idle and ?Q9 thread\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> getIdleThread \<lbrace>\<lambda>threada. valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle' and ?Q'10 threada\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 6. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and ?Q'4) s proof (prove)
goal (2 subgoals):
 1. \<And>s. invs s \<Longrightarrow> valid_arch_state s \<and> valid_objs s \<and> valid_asid_map s \<and> unique_table_refs (caps_of_state s) \<and> valid_vs_lookup s \<and> valid_global_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_vspace_objs s \<and> valid_idle s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle' and (\<lambda>_. True))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>_. True) and (valid_arch_state' and pspace_aligned' and pspace_distinct' and no_0_obj' and valid_idle' and (\<lambda>_. True))) s proof (prove)
goal:
No subgoals!