theory Syscall_C

lemma handleYield_ccorres:
  "ccorres dc xfdc
       (invs' and ct_active')
       UNIV
       []
       (handleYield)
       (Call handleYield_'proc)" apply cinit apply (rule ccorres_pre_getCurThread) apply (ctac add: tcbSchedDequeue_ccorres) apply (ctac  add: tcbSchedAppend_ccorres) apply (ctac add: rescheduleRequired_ccorres) apply (wp weak_sch_act_wf_lift_linear tcbSchedAppend_valid_objs') apply (vcg exspec= tcbSchedAppend_modifies) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues) apply (vcg exspec= tcbSchedDequeue_modifies) apply (clarsimp simp: tcb_at_invs' invs_valid_objs'
                        valid_objs'_maxPriority valid_objs'_maxDomain) apply (auto simp: obj_at'_def st_tcb_at'_def ct_in_state'_def valid_objs'_maxDomain) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (invs' and ct_active') UNIV [] handleYield (Call handleYield_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (do thread <- getCurThread;
y <- tcbSchedDequeue thread;
y <- tcbSchedAppend thread;
rescheduleRequired
od) (CALL tcbSchedDequeue_'proc(\<acute>ksCurThread);;
(CALL tcbSchedAppend_'proc(\<acute>ksCurThread);;
CALL rescheduleRequired_'proc()))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (2 subgoals):
 1. \<And>thread. ccorres dc xfdc (?P15 thread) (?P'15 thread) [SKIP] (do y <- tcbSchedDequeue thread;
y <- tcbSchedAppend thread;
rescheduleRequired
od) (CALL tcbSchedDequeue_'proc(\<acute>ksCurThread);;
(CALL tcbSchedAppend_'proc(\<acute>ksCurThread);;
CALL rescheduleRequired_'proc()))
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P15 rv s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'15 rv} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv xfdca. dc rv xfdca \<Longrightarrow> ccorres dc xfdc (?Q19 thread rv) (?Q'19 thread rv xfdca) [SKIP] (do y <- tcbSchedAppend thread;
rescheduleRequired
od) (CALL tcbSchedAppend_'proc(\<acute>ksCurThread);;
CALL rescheduleRequired_'proc())
 2. \<And>thread. \<lbrace>?R19 thread\<rbrace> tcbSchedDequeue thread \<lbrace>?Q19 thread\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'19 thread) CALL tcbSchedDequeue_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> ?Q'19 thread rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and ?R19 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> ?R'19 rv} proof (prove)
goal (6 subgoals):
 1. \<And>thread rv xfdca rva xfdcb. \<lbrakk>dc rv xfdca; dc rva xfdcb\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q44 thread rv xfdca rva) (?Q'44 thread rv xfdca rva xfdcb) [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 2. \<And>thread rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R46 thread rv\<rbrace> tcbSchedAppend thread \<lbrace>?Q44 thread rv xfdc\<rbrace>
 3. \<And>thread rv xfdca. dc rv xfdca \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'44 thread rv xfdca) CALL tcbSchedAppend_'proc(\<acute>ksCurThread) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'44 thread rv xfdca rva (xfdc s)}
 4. \<And>thread. \<lbrace>?R19 thread\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>rv. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R46 thread rv\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'19 thread) CALL tcbSchedDequeue_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'44 thread rv (xfdc s)}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and ?R19 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> ?R'19 rv} proof (prove)
goal (5 subgoals):
 1. \<And>thread rv xfdc. dc rv xfdc \<Longrightarrow> \<lbrace>?R46 thread rv\<rbrace> tcbSchedAppend thread \<lbrace>\<lambda>rva. Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs'\<rbrace>
 2. \<And>thread rv xfdca. dc rv xfdca \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'44 thread rv xfdca) CALL tcbSchedAppend_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV}}
 3. \<And>thread. \<lbrace>?R19 thread\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>rv. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and ?R46 thread rv\<rbrace>
 4. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'19 thread) CALL tcbSchedDequeue_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'44 thread rv (xfdc s)}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and ?R19 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> ?R'19 rv} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv xfdca. dc rv xfdca \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'44 thread rv xfdca) CALL tcbSchedAppend_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. s \<in> UNIV}}
 2. \<And>thread. \<lbrace>?R19 thread\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>rv. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues and st_tcb_at' runnable' thread and valid_objs') s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'19 thread) CALL tcbSchedDequeue_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'44 thread rv (xfdc s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and ?R19 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> ?R'19 rv} proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?R19 thread\<rbrace> tcbSchedDequeue thread \<lbrace>\<lambda>rv. Invariants_H.valid_queues and tcb_at' thread and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues and st_tcb_at' runnable' thread and valid_objs') s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s)\<rbrace>
 2. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'19 thread) CALL tcbSchedDequeue_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> \<lbrace>True\<rbrace>}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and ?R19 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> ?R'19 rv} proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'19 thread) CALL tcbSchedDequeue_'proc(\<acute>ksCurThread) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> \<lbrace>True\<rbrace>}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) rv and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) rv) s \<and> tcb_at' rv s \<and> valid_objs' s \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) rv and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) rv) s \<and> st_tcb_at' runnable' rv s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> ?R'19 rv} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (invs' and ct_active') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' rv and valid_objs' and (\<lambda>s. (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) rv and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) rv) s \<and> tcb_at' rv s \<and> valid_objs' s \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) rv and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) rv) s \<and> st_tcb_at' runnable' rv s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> valid_objs' s)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. tcb_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr rv\<rbrace>} \<inter> {s. \<forall>t rva. dc rva (xfdc (s\<lparr>globals := globals s\<lparr>ksReadyQueues_' := ksReadyQueues_' (globals t), ksReadyQueuesL1Bitmap_' := ksReadyQueuesL1Bitmap_' (globals t), ksReadyQueuesL2Bitmap_' := ksReadyQueuesL2Bitmap_' (globals t), t_hrs_' := t_hrs_' (globals t)\<rparr>\<rparr>)) \<longrightarrow> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; invs' s; ct_active' s\<rbrakk> \<Longrightarrow> Invariants_H.valid_queues s \<and> valid_queues' s \<and> Invariants_H.valid_queues s \<and> st_tcb_at' runnable' (ksCurThread s) s \<and> weak_sch_act_wf (ksSchedulerAction s) s proof (prove)
goal:
No subgoals!