theory Schedule_R

lemma switchToThread_corres:
  "corres dc (valid_arch_state and valid_objs and valid_asid_map
                and valid_vspace_objs and pspace_aligned and pspace_distinct
                and valid_vs_lookup and valid_global_objs
                and unique_table_refs o caps_of_state
                and st_tcb_at runnable t and valid_etcbs)
             (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues
                and st_tcb_at' runnable' t and cur_tcb')
             (switch_to_thread t) (switchToThread t)"
  (is "corres _ ?PA ?PH _ _") proof - have mainpart: "corres dc (?PA) (?PH)
     (do y \<leftarrow> arch_switch_to_thread t;
         y \<leftarrow> (tcb_sched_action tcb_sched_dequeue t);
         modify (cur_thread_update (\<lambda>_. t))
      od)
     (do y \<leftarrow> Arch.switchToThread t;
         y \<leftarrow> tcbSchedDequeue t;
         setCurThread t
      od)" apply (rule corres_guard_imp) apply (rule corres_split[OF arch_switchToThread_corres]) apply (rule corres_split[OF tcbSchedDequeue_corres setCurThread_corres]) apply (wp|clarsimp simp: tcb_at_is_etcb_at st_tcb_at_tcb_at)+ done show ?thesis apply - apply (simp add: switch_to_thread_def Thread_H.switchToThread_def) apply (rule corres_symb_exec_l [where Q = "\<lambda> s rv. (?PA and (=) rv) s",
                                    OF corres_symb_exec_l [OF mainpart]]) apply (auto intro: no_fail_pre [OF no_fail_assert]
                      no_fail_pre [OF no_fail_get]
                dest: st_tcb_at_tcb_at [THEN get_tcb_at] |
           simp add: assert_def | wp)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (switch_to_thread t) (global.switchToThread t) proof (state)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (switch_to_thread t) (global.switchToThread t) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (do y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) (do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) (do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od)
 2. \<And>s. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) s \<Longrightarrow> ?Q s
 3. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> corres dc (?R4 y) (?R'4 ya) (do y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) (do y <- tcbSchedDequeue t;
setCurThread t
od)
 2. \<lbrace>?Q4\<rbrace> arch_switch_to_thread t \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> Arch.switchToThread t \<lbrace>?R'4\<rbrace>
 4. \<And>s. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) s \<Longrightarrow> (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and ?Q4) s
 5. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> (valid_arch_state' and valid_pspace' and st_tcb_at' runnable' t and ?Q'4) s proof (prove)
goal (6 subgoals):
 1. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q15 y\<rbrace> tcb_sched_action tcb_sched_dequeue t \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>y ya. dc y ya \<Longrightarrow> \<lbrace>?Q'17 ya\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<lbrace>?Q4\<rbrace> arch_switch_to_thread t \<lbrace>\<lambda>y. is_etcb_at t and ?Q15 y\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>ya. tcb_at' t and Invariants_H.valid_queues and ?Q'17 ya\<rbrace>
 5. \<And>s. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) s \<Longrightarrow> (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and ?Q4) s
 6. \<And>s. (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') s \<Longrightarrow> (valid_arch_state' and valid_pspace' and st_tcb_at' runnable' t and ?Q'4) s proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (do y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) (do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od)

goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (switch_to_thread t) (global.switchToThread t) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (switch_to_thread t) (global.switchToThread t) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (switch_to_thread t) (global.switchToThread t) proof (prove)
goal (1 subgoal):
 1. corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (do state <- get;
y <- assert (\<exists>y. get_tcb t state = Some y);
y <- arch_switch_to_thread t;
y <- tcb_sched_action tcb_sched_dequeue t;
modify (cur_thread_update (\<lambda>_. t))
od) (do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od) proof (prove)
goal (6 subgoals):
 1. \<And>y s. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs and (=) s) y \<Longrightarrow> \<lbrace>(=) s\<rbrace> assert (\<exists>ya. get_tcb t y = Some ya) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>y. \<lbrace>\<lambda>ya. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs and (=) ya) y\<rbrace> assert (\<exists>ya. get_tcb t y = Some ya) \<lbrace>\<lambda>y. valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs\<rbrace>
 3. \<And>y. True \<Longrightarrow> no_fail (\<lambda>ya. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs and (=) ya) y) (assert (\<exists>ya. get_tcb t y = Some ya))
 4. \<And>s. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) s \<Longrightarrow> \<lbrace>(=) s\<rbrace> get \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs\<rbrace> get \<lbrace>\<lambda>s y. (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs and (=) y) s\<rbrace>
 6. True \<Longrightarrow> no_fail (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) get proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (valid_arch_state and valid_objs and valid_asid_map and valid_vspace_objs and pspace_aligned and pspace_distinct and valid_vs_lookup and valid_global_objs and unique_table_refs \<circ> caps_of_state and st_tcb_at runnable t and valid_etcbs) (valid_arch_state' and valid_pspace' and Invariants_H.valid_queues and st_tcb_at' runnable' t and cur_tcb') (switch_to_thread t) (global.switchToThread t)

goal:
No subgoals!