theory Schedule_C

lemma switchToThread_ccorres:
  "ccorres dc xfdc
           (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t)
           (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>)
           hs
           (switchToThread t)
           (Call switchToThread_'proc)" apply (cinit lift: thread_') apply (ctac (no_vcg) add: Arch_switchToThread_ccorres) apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg) apply clarsimp apply (rule conseqPre, vcg) apply (clarsimp simp: setCurThread_def simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                           carch_state_relation_def cmachine_state_relation_def) apply wp+ apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>) hs (global.switchToThread t) (Call switchToThread_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q76 thread) (?Q'76 thread) (SKIP # hs) (do y <- Arch.switchToThread t;
y <- tcbSchedDequeue t;
setCurThread t
od) (CALL Arch_switchToThread_'proc(thread);;
(CALL tcbSchedDequeue_'proc(thread);;
\<acute>ksCurThread :== thread))
 2. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q76 thread s \<and> s' \<in> ?Q'76 thread proof (prove)
goal (3 subgoals):
 1. \<And>thread rv xfdca. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q84 thread rv) (?Q'84 thread rv xfdca) (SKIP # hs) (do y <- tcbSchedDequeue t;
setCurThread t
od) (CALL tcbSchedDequeue_'proc(thread);;
\<acute>ksCurThread :== thread)
 2. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>?Q84 thread\<rbrace>
 3. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'84 thread rv (xfdc t)} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv xfdca rva xfdcb. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q107 thread rv xfdca rva) (?Q'107 thread rv xfdca rva xfdcb) (SKIP # hs) (setCurThread t) (\<acute>ksCurThread :== thread)
 2. \<And>thread rv xfdc. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R109 thread rv\<rbrace> tcbSchedDequeue t \<lbrace>?Q107 thread rv xfdc\<rbrace>
 3. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R109 thread rv\<rbrace>
 4. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. dc rva (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> ?Q'107 thread rv (xfdc ta) rva (xfdc t)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv xfdca rva xfdcb. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksCurThread :== thread {s. \<exists>(rv, \<sigma>')\<in>fst (setCurThread t \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>thread rv xfdc. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R109 thread rv\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R109 thread rv\<rbrace>
 4. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. \<Gamma>\<turnstile> {s. (\<sigma>, s) \<in> rf_sr} \<acute>ksCurThread :== tcb_ptr_to_ctcb_ptr t {s. \<exists>x\<in>fst (setCurThread t \<sigma>). case x of (rv, \<sigma>') \<Rightarrow> (\<sigma>', s) \<in> rf_sr}
 2. \<And>thread rv xfdc. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R109 thread rv\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R109 thread rv\<rbrace>
 4. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma>. {s. (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setCurThread t \<sigma>). (\<sigma>', globals_update (ksCurThread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t)) s) \<in> rf_sr}
 2. \<And>thread rv xfdc. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R109 thread rv\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R109 thread rv\<rbrace>
 4. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (4 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (\<sigma>\<lparr>ksCurThread := t\<rparr>, globals_update (ksCurThread_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr t)) x) \<in> rf_sr
 2. \<And>thread rv xfdc. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R109 thread rv\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R109 thread rv\<rbrace>
 4. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (3 subgoals):
 1. \<And>thread rv xfdc. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R109 thread rv\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>thread. thread = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R84 thread\<rbrace> Arch.switchToThread t \<lbrace>\<lambda>rv. Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R109 thread rv\<rbrace>
 3. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and ?R84 thread) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal (1 subgoal):
 1. \<And>thread s s'. \<lbrakk>thread = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t and (\<lambda>s. Invariants_H.valid_queues s \<and> valid_queues' s \<and> tcb_at' t s \<and> valid_objs' s \<and> True)) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>ta rv. dc rv (xfdc ta) \<longrightarrow> s'\<lparr>globals := globals ta\<rparr> \<in> {s. tcb_'_update (\<lambda>_. thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. dc rv (xfdc t) \<longrightarrow> s'\<lparr>globals := globals t\<rparr> \<in> UNIV}} proof (prove)
goal:
No subgoals!