theory Tcb_C

lemma setPriority_ccorres:
  "ccorres dc xfdc
      (\<lambda>s. tcb_at' t s \<and> Invariants_H.valid_queues s \<and>  ksCurDomain s \<le> maxDomain \<and>
           valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (priority \<le> maxPriority))
      (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \<inter> {s. prio_' s = ucast priority})
      [] (setPriority t priority) (Call setPriority_'proc)" apply (cinit lift: tptr_' prio_') apply (ctac(no_vcg) add: tcbSchedDequeue_ccorres) apply (rule ccorres_move_c_guard_tcb) apply (rule ccorres_split_nothrow_novcg_dc) apply (rule threadSet_ccorres_lemma2[where P=\<top>]) apply vcg apply clarsimp apply (erule(1) rf_sr_tcb_update_no_queue2,
              (simp add: typ_heap_simps')+, simp_all?)[1] apply (rule ball_tcb_cte_casesI, simp+) apply (simp add: ctcb_relation_def) apply (ctac(no_vcg) add: isRunnable_ccorres) apply (simp add: when_def to_bool_def del: Collect_const) apply (rule ccorres_cond2[where R=\<top>], simp add: Collect_const_mem) apply (rule ccorres_pre_getCurThread) apply (rule_tac R = "\<lambda>s. rv = ksCurThread s" in ccorres_cond2) apply (clarsimp simp: rf_sr_ksCurThread) apply (ctac add: rescheduleRequired_ccorres) apply (ctac add: possibleSwitchTo_ccorres) apply (rule ccorres_return_Skip') apply (wp isRunnable_wp) apply (wpsimp wp: hoare_drop_imps threadSet_valid_queues threadSet_valid_objs'
                       weak_sch_act_wf_lift_linear threadSet_pred_tcb_at_state
                       threadSet_tcbDomain_triv
                 simp: st_tcb_at'_def o_def split: if_splits) apply (simp add: guard_is_UNIV_def) apply (rule hoare_strengthen_post[
                 where Q="\<lambda>rv s.
                          obj_at' (\<lambda>_. True) t s \<and>
                          priority \<le> maxPriority \<and>
                          Invariants_H.valid_queues s \<and>
                          ksCurDomain s \<le> maxDomain \<and>
                          valid_objs' s \<and>
                          valid_queues' s \<and>
                          weak_sch_act_wf (ksSchedulerAction s) s \<and>
                          (\<forall>d p. \<not> t \<in> set (ksReadyQueues s (d, p)))"]) apply (wp weak_sch_act_wf_lift_linear tcbSchedDequeue_valid_queues tcbSchedDequeue_nonq) apply (clarsimp simp: valid_tcb'_tcbPriority_update) apply clarsimp apply (frule (1) valid_objs'_maxDomain[where t=t]) apply (frule (1) valid_objs'_maxPriority[where t=t]) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (\<lambda>s. tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority) (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr t\<rbrace> \<inter> \<lbrace>\<acute>prio = UCAST(8 \<rightarrow> 32) priority\<rbrace>) [] (setPriority t priority) (Call setPriority_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q306 prio tptr) (?Q'306 prio tptr) [SKIP] (do y <- tcbSchedDequeue t;
y <- threadSet (tcbPriority_update (\<lambda>_. priority)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (CALL tcbSchedDequeue_'proc(tptr);;
(Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbPriority_C''])) prio)));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)))
 2. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q306 prio tptr s \<and> s' \<in> ?Q'306 prio tptr proof (prove)
goal (3 subgoals):
 1. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q314 prio tptr rv) (?Q'314 prio tptr rv xfdca) [SKIP] (do y <- threadSet (tcbPriority_update (\<lambda>_. priority)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tptr} (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbPriority_C''])) prio)));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI))
 2. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>?Q314 prio tptr\<rbrace>
 3. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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'314 prio tptr rv (xfdc t)} proof (prove)
goal (3 subgoals):
 1. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?A337 prio tptr rv) (?C'336 prio tptr rv xfdca) [SKIP] (do y <- threadSet (tcbPriority_update (\<lambda>_. priority)) t;
runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbPriority_C''])) prio));;
(\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI))
 2. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. ?A337 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 3. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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> ?C'336 prio tptr rv (xfdc t) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?P341 prio tptr rv) (?C'336 prio tptr rv xfdca) [] (threadSet (tcbPriority_update (\<lambda>_. priority)) t) (\<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbPriority_C''])) prio)))
 2. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. ?P341 prio tptr rv and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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> ?C'336 prio tptr rv (xfdc t) \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>prio tptr rv xfdc s tcb. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q347 prio tptr rv xfdc s tcb) \<acute>globals :== t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbPriority_C''])) prio)) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> injectKOS (tcbPriority_update (\<lambda>_. priority) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>prio tptr rv xfdc s s' tcb tcb'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; (s, s') \<in> rf_sr; True; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q347 prio tptr rv xfdc s tcb
 3. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 4. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 5. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 6. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>prio tptr rv xfdc s s' tcb tcb'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; (s, s') \<in> rf_sr; True; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'; True; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> injectKOS (tcbPriority_update (\<lambda>_. priority) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tptr\<rightarrow>[''tcbPriority_C''])) prio))) sa) \<in> rf_sr}
 2. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>(s, s') \<in> rf_sr; ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(t \<mapsto> KOTCB (tcbPriority_update (\<lambda>_. priority) tcb))\<rparr>, globals_update (t_hrs_'_update (hrs_mem_update (heap_update (PTR(32 word) &(tcb_ptr_to_ctcb_ptr t\<rightarrow>[''tcbPriority_C''])) (UCAST(8 \<rightarrow> 32) priority)))) s') \<in> rf_sr
 2. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbPriority_update (\<lambda>_. priority) tcb) = getF tcb
 2. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbPriority_update (\<lambda>_. priority) tcb) (tcbPriority_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) priority) tcb')
 3. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 4. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 5. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 6. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ko_at' tcb t s; cslift s' (tcb_ptr_to_ctcb_ptr t) = Some tcb'; ctcb_relation tcb tcb'\<rbrakk> \<Longrightarrow> ctcb_relation (tcbPriority_update (\<lambda>_. priority) tcb) (tcbPriority_C_update (\<lambda>_. UCAST(8 \<rightarrow> 32) priority) tcb')
 2. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>prio tptr rv xfdca y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q340 prio tptr rv xfdca y) (?Q'340 prio tptr rv xfdca y rv') [SKIP] (do runnable <- isRunnable t;
when runnable (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)
od) (\<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
IF \<acute>ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 2. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>?Q340 prio tptr rv xfdc\<rbrace>
 3. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (?Q'340 prio tptr rv xfdca)
 4. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 5. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>prio tptr rv xfdca y rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca; dc y rv'; rva = to_bool ret__unsigned_long\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q379 prio tptr rv xfdca y rv' rva) (?Q'379 prio tptr rv xfdca y rv' rva ret__unsigned_long) [SKIP] (when rva (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od)) (IF ret__unsigned_long \<noteq> 0 THEN
  IF tptr = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tptr)
FI
FI)
 2. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>?Q379 prio tptr rv xfdc y rv'\<rbrace>
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'379 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t)})
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q379 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Q'379 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (if ret__unsigned_long \<noteq> 0 then do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od else return ()) (IF ret__unsigned_long \<noteq> 0 THEN
  IF tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tcb_ptr_to_ctcb_ptr t)
FI
FI)
 2. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>?Q379 prio tptr rv xfdc y rv'\<rbrace>
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> ?Q'379 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t)})
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt480 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rt476 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (do curThread <- getCurThread;
if t = curThread then rescheduleRequired else possibleSwitchTo t
od) (IF tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tcb_ptr_to_ctcb_ptr t)
FI)
 2. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf478 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf474 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (return ()) SKIP
 3. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> ?Pt480 prio tptr rv xfdc y rv' a s) and (\<lambda>s. \<not> a \<longrightarrow> ?Pf478 prio tptr rv xfdc y rv' a s)\<rbrace>
 4. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 5. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rt476 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t)) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf474 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 6. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>prio tptr xfdca rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (\<lambda>a. ?P487 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) a rv) (?P'488 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long rv) [SKIP] (if t = rv then rescheduleRequired else possibleSwitchTo t) (IF tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread THEN
  CALL rescheduleRequired_'proc()
ELSE
  CALL possibleSwitchTo_'proc(tcb_ptr_to_ctcb_ptr t)
FI)
 2. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf478 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf474 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (return ()) SKIP
 3. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P487 prio tptr rv xfdc y rv' a s rva)) and (\<lambda>s. \<not> a \<longrightarrow> ?Pf478 prio tptr rv xfdc y rv' a s)\<rbrace>
 4. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 5. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rvb. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rvb \<longrightarrow> s \<in> ?P'488 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t) rvb}) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf474 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 6. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (9 subgoals):
 1. \<And>prio tptr xfdc rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> rv = ksCurThread s \<longrightarrow> (t = rv) = (s' \<in> \<lbrace>tcb_ptr_to_ctcb_ptr t = \<acute>ksCurThread\<rbrace>)
 2. \<And>prio tptr xfdca rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt504 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) rv) (?Rt500 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long rv) [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 3. \<And>prio tptr xfdca rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) rv) (?Rf498 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long rv) [SKIP] (possibleSwitchTo t) (CALL possibleSwitchTo_'proc(tcb_ptr_to_ctcb_ptr t))
 4. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf478 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf474 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (return ()) SKIP
 5. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ((\<lambda>s. rva = ksCurThread s) and (\<lambda>s. t = rva \<longrightarrow> ?Pt504 prio tptr rv xfdc y rv' a rva s) and (\<lambda>s. t \<noteq> rva \<longrightarrow> ?Pf502 prio tptr rv xfdc y rv' a rva s)) s)) and (\<lambda>s. \<not> a \<longrightarrow> ?Pf478 prio tptr rv xfdc y rv' a s)\<rbrace>
 6. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 7. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rvb. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rvb \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rt500 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t) rvb) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rf498 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t) rvb)}}) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf474 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 8. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 9. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>prio tptr xfdca rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt504 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) rv) (?Rt500 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long rv) [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 2. \<And>prio tptr xfdca rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) rv) (?Rf498 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long rv) [SKIP] (possibleSwitchTo t) (CALL possibleSwitchTo_'proc(tcb_ptr_to_ctcb_ptr t))
 3. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf478 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf474 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (return ()) SKIP
 4. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ((\<lambda>s. rva = ksCurThread s) and (\<lambda>s. t = rva \<longrightarrow> ?Pt504 prio tptr rv xfdc y rv' a rva s) and (\<lambda>s. t \<noteq> rva \<longrightarrow> ?Pf502 prio tptr rv xfdc y rv' a rva s)) s)) and (\<lambda>s. \<not> a \<longrightarrow> ?Pf478 prio tptr rv xfdc y rv' a s)\<rbrace>
 5. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 6. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rvb. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rvb \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rt500 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t) rvb) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rf498 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t) rvb)}}) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf474 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 7. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 8. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>prio tptr xfdca rv' rva ret__unsigned_long rv. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf502 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) rv) (?Rf498 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long rv) [SKIP] (possibleSwitchTo t) (CALL possibleSwitchTo_'proc(tcb_ptr_to_ctcb_ptr t))
 2. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf478 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf474 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (return ()) SKIP
 3. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ((\<lambda>s. rva = ksCurThread s) and (\<lambda>s. t = rva \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. t \<noteq> rva \<longrightarrow> ?Pf502 prio tptr rv xfdc y rv' a rva s)) s)) and (\<lambda>s. \<not> a \<longrightarrow> ?Pf478 prio tptr rv xfdc y rv' a s)\<rbrace>
 4. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 5. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rvb. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rvb \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> ?Rf498 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t) rvb)}}) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf474 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 6. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 7. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>prio tptr xfdca rv' rva ret__unsigned_long. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; rva = (ret__unsigned_long \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pf478 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0)) (?Rf474 (UCAST(8 \<rightarrow> 32) priority) (tcb_ptr_to_ctcb_ptr t) () xfdca () rv' (ret__unsigned_long \<noteq> 0) ret__unsigned_long) [SKIP] (return ()) SKIP
 2. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. t = rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. t \<noteq> rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s)) s)) and (\<lambda>s. \<not> a \<longrightarrow> ?Pf478 prio tptr rv xfdc y rv' a s)\<rbrace>
 3. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 4. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rva. rva = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. target_'_update (\<lambda>_. tptr) s \<in> \<lbrace>\<acute>target = tptr\<rbrace> \<inter> UNIV})}}) \<and> (s \<notin> \<lbrace>rva\<rbrace> \<longrightarrow> s \<in> ?Rf474 prio tptr rv xfdca y rv' rva (ret__unsigned_long_' t))}})
 5. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 6. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>prio tptr rv xfdc y rv'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc; dc y rv'\<rbrakk> \<Longrightarrow> \<lbrace>?R381 prio tptr rv xfdc y\<rbrace> isRunnable t \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. a \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. t = rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. t \<noteq> rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s)) s)) and (\<lambda>s. \<not> a \<longrightarrow> True)\<rbrace>
 2. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and ?R381 prio tptr rv xfdc y\<rbrace>
 3. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. target_'_update (\<lambda>_. tptr) s \<in> \<lbrace>\<acute>target = tptr\<rbrace> \<inter> UNIV})}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. dc y (xfdc s)})}})
 4. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 5. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>prio tptr rv xfdc. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdc\<rbrakk> \<Longrightarrow> \<lbrace>?R342 prio tptr rv\<rbrace> threadSet (tcbPriority_update (\<lambda>_. priority)) t \<lbrace>\<lambda>y. tcb_at' t and (\<lambda>a. ((\<lambda>_. True) and (\<lambda>s. st_tcb_at' runnable' t a \<longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ((\<lambda>s. rv = ksCurThread s) and (\<lambda>s. t = rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. t \<noteq> rv \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and st_tcb_at' runnable' t and (\<lambda>s. ksCurDomain s \<le> maxDomain) and valid_objs') s)) s)) and (\<lambda>s. \<not> st_tcb_at' runnable' t a \<longrightarrow> True)) a)\<rbrace>
 2. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. target_'_update (\<lambda>_. tptr) s \<in> \<lbrace>\<acute>target = tptr\<rbrace> \<inter> UNIV})}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. dc y (xfdc s)})}})
 3. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and ?R342 prio tptr rv and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 4. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>prio tptr rv xfdca. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; dc rv xfdca\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>y rv'. {s. thread_'_update (\<lambda>_. tptr) s \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr t\<rbrace>} \<inter> {s'. \<forall>t rv. rv = to_bool (ret__unsigned_long_' t) \<longrightarrow> s'\<lparr>globals := globals t, ret__unsigned_long_' := ret__unsigned_long_' t\<rparr> \<in> {s. (s \<in> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. (s \<in> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>tptr = \<acute>ksCurThread\<rbrace> \<longrightarrow> s \<in> {s. target_'_update (\<lambda>_. tptr) s \<in> \<lbrace>\<acute>target = tptr\<rbrace> \<inter> UNIV})}}) \<and> (s \<notin> \<lbrace>rv\<rbrace> \<longrightarrow> s \<in> UNIV \<inter> {s. dc y (xfdc s)})}})
 2. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and (\<lambda>s. obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> ((Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> ksCurDomain s \<le> maxDomain \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 3. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv. tcb_at' t and (\<lambda>_. True) and (\<lambda>s. obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> ((Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> ksCurDomain s \<le> maxDomain \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)\<rbrace>
 2. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (3 subgoals):
 1. \<And>prio tptr. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t\<rbrakk> \<Longrightarrow> \<lbrace>?R314 prio tptr\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>rv s. obj_at' (\<lambda>_. True) t s \<and> priority \<le> maxPriority \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_objs' s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>prio tptr rv s. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; obj_at' (\<lambda>_. True) t s \<and> priority \<le> maxPriority \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_objs' s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and (\<lambda>s. obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> ((Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> ksCurDomain s \<le> maxDomain \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s
 3. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and ?R314 prio tptr) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (2 subgoals):
 1. \<And>prio tptr rv s. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; tcb_at' t s \<and> priority \<le> maxPriority \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_objs' s \<and> valid_queues' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. t \<notin> set (ksReadyQueues s (d, p)))\<rbrakk> \<Longrightarrow> (tcb_at' t and (\<lambda>_. True) and (\<lambda>s. obj_at' (\<lambda>obj. if t = t then True else True) t s \<and> ((Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbPriority_update (\<lambda>_. priority) tcb) \<and> runnable' (tcbState (tcbPriority_update (\<lambda>_. priority) tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> ksCurDomain s \<le> maxDomain \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbPriority_update (\<lambda>_. priority) tcb) s)) s) and tcb_at' (ctcb_ptr_to_tcb_ptr tptr)) s
 2. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and (\<lambda>s. tcb_at' t s \<and> priority \<le> maxPriority \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<and> ksCurDomain s \<le> maxDomain \<and> valid_objs' s \<and> (valid_queues' and tcb_at' t) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (Invariants_H.valid_queues and tcb_at' t and K (t = t)) s)) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>prio tptr s s'. \<lbrakk>prio = UCAST(8 \<rightarrow> 32) priority; tptr = tcb_ptr_to_ctcb_ptr t; (s, s') \<in> rf_sr; tcb_at' t s \<and> Invariants_H.valid_queues s \<and> ksCurDomain s \<le> maxDomain \<and> valid_queues' s \<and> valid_objs' s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> priority \<le> maxPriority; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (Invariants_H.valid_queues and valid_queues' and tcb_at' t and valid_objs' and (\<lambda>s. tcb_at' t s \<and> priority \<le> maxPriority \<and> (Invariants_H.valid_queues and obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t and obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t) s \<and> ksCurDomain s \<le> maxDomain \<and> valid_objs' s \<and> (valid_queues' and tcb_at' t) s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<and> (Invariants_H.valid_queues and tcb_at' t and K (t = t)) s)) s \<and> s' \<in> {s. tcb_'_update (\<lambda>_. tptr) 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 \<inter> \<lbrace>True\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' t s; Invariants_H.valid_queues s; ksCurDomain s \<le> maxDomain; valid_queues' s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s; priority \<le> maxPriority\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' t s; Invariants_H.valid_queues s; ksCurDomain s \<le> maxDomain; valid_queues' s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s; priority \<le> maxPriority; obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' t s; Invariants_H.valid_queues s; ksCurDomain s \<le> maxDomain; valid_queues' s; valid_objs' s; weak_sch_act_wf (ksSchedulerAction s) s; priority \<le> maxPriority; obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s; obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s \<and> obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s proof (prove)
goal:
No subgoals!