theory Schedule_C

lemma Arch_switchToThread_ccorres:
  "ccorres dc xfdc
           (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' t)
           (UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>)
           []
           (Arch.switchToThread t) (Call Arch_switchToThread_'proc)" apply (cinit lift: tcb_') apply (unfold ARM_H.switchToThread_def)[1] apply (ctac (no_vcg) add: setVMRoot_ccorres) apply (simp (no_asm) del: Collect_const) apply (rule_tac A'=UNIV in ccorres_guard_imp2) apply (ctac add: clearExMonitor_ccorres) apply clarsimp apply wp apply clarsimp 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>tcb = tcb_ptr_to_ctcb_ptr t\<rbrace>) [] (Arch.switchToThread t) (Call Arch_switchToThread_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q122 tcb) (?Q'122 tcb) [SKIP] (Arch.switchToThread t) (CALL setVMRoot_'proc(tcb);;
CALL clearExMonitor_'proc())
 2. \<And>tcb s s'. \<lbrakk>tcb = 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> ?Q122 tcb s \<and> s' \<in> ?Q'122 tcb proof (prove)
goal (2 subgoals):
 1. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> ccorres dc xfdc (?Q122 tcb) (?Q'122 tcb) [SKIP] (do setVMRoot t;
doMachineOp $ ARM.clearExMonitor
od) (CALL setVMRoot_'proc(tcb);;
CALL clearExMonitor_'proc())
 2. \<And>tcb s s'. \<lbrakk>tcb = 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> ?Q122 tcb s \<and> s' \<in> ?Q'122 tcb proof (prove)
goal (3 subgoals):
 1. \<And>tcb rv xfdca. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q132 tcb rv) (?Q'132 tcb rv xfdca) [SKIP] (K_bind (doMachineOp $ ARM.clearExMonitor) rv) (CALL clearExMonitor_'proc())
 2. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R132 tcb\<rbrace> setVMRoot t \<lbrace>?Q132 tcb\<rbrace>
 3. \<And>tcb s s'. \<lbrakk>tcb = 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 ?R132 tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) 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'132 tcb rv (xfdc t)} proof (prove)
goal (3 subgoals):
 1. \<And>tcb rv xfdca. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q132 tcb ()) (?Q'132 tcb () xfdca) [SKIP] (doMachineOp ARM.clearExMonitor) (CALL clearExMonitor_'proc())
 2. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R132 tcb\<rbrace> setVMRoot t \<lbrace>?Q132 tcb\<rbrace>
 3. \<And>tcb s s'. \<lbrakk>tcb = 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 ?R132 tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) 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'132 tcb rv (xfdc t)} proof (prove)
goal (4 subgoals):
 1. \<And>tcb rv xfdca. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q153 tcb rv xfdca) (?Q'153 tcb rv xfdca) [SKIP] (doMachineOp ARM.clearExMonitor) (CALL clearExMonitor_'proc())
 2. \<And>tcb rv xfdc s s'. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; (s, s') \<in> rf_sr; ?Q132 tcb () s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q153 tcb rv xfdc s \<and> s' \<in> ?Q'153 tcb rv xfdc
 3. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R132 tcb\<rbrace> setVMRoot t \<lbrace>?Q132 tcb\<rbrace>
 4. \<And>tcb s s'. \<lbrakk>tcb = 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 ?R132 tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) 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>tcb rv xfdc s s'. \<lbrakk>tcb = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; (s, s') \<in> rf_sr; ?Q132 tcb () s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> True \<and> s' \<in> {s. s \<in> UNIV}
 2. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R132 tcb\<rbrace> setVMRoot t \<lbrace>?Q132 tcb\<rbrace>
 3. \<And>tcb s s'. \<lbrakk>tcb = 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 ?R132 tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) 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 (2 subgoals):
 1. \<And>tcb. tcb = tcb_ptr_to_ctcb_ptr t \<Longrightarrow> \<lbrace>?R132 tcb\<rbrace> setVMRoot t \<lbrace>?Q132 tcb\<rbrace>
 2. \<And>tcb s s'. \<lbrakk>tcb = 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 ?R132 tcb) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) 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>tcb s s'. \<lbrakk>tcb = 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. True)) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tcb) 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!