theory IpcCancel_C

lemma rescheduleRequired_ccorres_valid_queues'_simple:
  "ccorresG rf_sr \<Gamma> dc xfdc (valid_queues' and sch_act_simple) UNIV [] rescheduleRequired (Call rescheduleRequired_'proc)" apply cinit apply (rule ccorres_symb_exec_l) apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) apply (simp add: scheduler_action_case_switch_to_if
                      cong: if_weak_cong split del: if_split) apply (rule_tac R="\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s"
                     in ccorres_cond) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                  cscheduler_action_relation_def) apply (clarsimp simp: weak_sch_act_wf_def tcb_at_1 tcb_at_not_NULL
                           split: scheduler_action.split_asm dest!: st_tcb_strg'[rule_format]) apply (ctac add: tcbSchedEnqueue_ccorres) apply (rule ccorres_return_Skip) apply ceqv apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: setSchedulerAction_def simpler_modify_def) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                              cscheduler_action_relation_def
                              carch_state_relation_def cmachine_state_relation_def
                              ) apply wp apply (simp add: guard_is_UNIV_def) apply wp+ apply (simp add: getSchedulerAction_def) apply (clarsimp simp: weak_sch_act_wf_def rf_sr_def cstate_relation_def
                        Let_def cscheduler_action_relation_def) by (auto simp: tcb_at_not_NULL tcb_at_1
                    tcb_at_not_NULL[THEN not_sym] tcb_at_1[THEN not_sym]
                 split: scheduler_action.split_asm)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_queues' and sch_act_simple) UNIV [] rescheduleRequired (Call rescheduleRequired_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q9 ?Q'9 [SKIP] (do action <- getSchedulerAction;
y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI;;
\<acute>ksSchedulerAction :== tcb_Ptr 1)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> ?Q'9 proof (prove)
goal (5 subgoals):
 1. \<And>action. ccorres dc xfdc (?Q15 action) (?Q'15 action) [SKIP] (do y <- case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ();
setSchedulerAction ChooseNewThread
od) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI;;
\<acute>ksSchedulerAction :== tcb_Ptr 1)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>?Q15\<rbrace>
 4. empty_fail getSchedulerAction
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q15 rv s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (9 subgoals):
 1. \<And>action. ccorres dc xfdc (?P20 action) (?Q'15 action) [] (case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return ()) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI)
 2. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 3. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 4. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 5. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 6. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. ?P20 action and ?R20 action\<rbrace>
 8. empty_fail getSchedulerAction
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P20 rv and ?R20 rv) s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (9 subgoals):
 1. \<And>action. ccorres dc xfdc (?P20 action) (?Q'15 action) [] (if \<exists>t. action = SwitchToThread t then tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t) else return ()) (IF \<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1 THEN
  CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction)
FI)
 2. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 3. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 4. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 5. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 6. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. ?P20 action and ?R20 action\<rbrace>
 8. empty_fail getSchedulerAction
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (?P20 rv and ?R20 rv) s \<longrightarrow> s' \<in> ?Q'15 rv} proof (prove)
goal (11 subgoals):
 1. \<And>action. \<forall>s s'. (s, s') \<in> rf_sr \<and> action = ksSchedulerAction s \<and> sch_act_simple s \<longrightarrow> (\<exists>t. action = SwitchToThread t) = (s' \<in> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>)
 2. \<And>action. ccorres dc xfdc (?Pt27 action) (?Rt27 action) [] (tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t)) (CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction))
 3. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 4. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 5. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 6. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 7. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 8. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> ?Pt27 action s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 10. empty_fail getSchedulerAction
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>s s'. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread s); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); case ksSchedulerAction s of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s') = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr p'; carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); cte_array_relation s (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages s, gsCNodes s); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted s; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx s); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain s); ksDomainTime_' (globals s') = ksDomainTime s; sch_act_simple s; ksSchedulerAction_' (globals s') \<noteq> tcb_Ptr 1\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals s') = NULL
 2. \<And>action. ccorres dc xfdc (?Pt27 action) (?Rt27 action) [] (tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t)) (CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction))
 3. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 4. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 5. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 6. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 7. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 8. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> ?Pt27 action s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 10. empty_fail getSchedulerAction
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>action. ccorres dc xfdc (?Pt27 action) (?Rt27 action) [] (tcbSchedEnqueue (case action of SwitchToThread t \<Rightarrow> t)) (CALL tcbSchedEnqueue_'proc(\<acute>ksSchedulerAction))
 2. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 3. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 4. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 5. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 6. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 7. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> ?Pt27 action s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 9. empty_fail getSchedulerAction
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> ?Pt27 rv s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> ?Pf27 rv s) and ?R20 rv) s \<longrightarrow> s' \<in> ?Rt27 rv \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> ?Rf27 rv \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (9 subgoals):
 1. \<And>action. ccorres dc xfdc (?Pf27 action) (?Rf27 action) [] (return ()) SKIP
 2. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 3. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 4. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 5. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 6. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> ?Pf27 action s) and ?R20 action\<rbrace>
 8. empty_fail getSchedulerAction
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> ?Pf27 rv s) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> ?Rf27 rv \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (8 subgoals):
 1. \<And>action rv' t t'. ceqv \<Gamma> xfdc rv' t t' (\<acute>ksSchedulerAction :== tcb_Ptr 1) (?d'20 action rv')
 2. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (?d'20 action rv')
 3. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 4. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 5. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 7. empty_fail getSchedulerAction
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>action y rv'. dc y rv' \<Longrightarrow> ccorres dc xfdc (?Q20 action y) (?Q'20 action y rv') [SKIP] (setSchedulerAction ChooseNewThread) (\<acute>ksSchedulerAction :== tcb_Ptr 1)
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>?Q20 action\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (?Q'20 action)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>action y rv'. dc y rv' \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ksSchedulerAction :== tcb_Ptr 1 {s. \<exists>(rv, \<sigma>')\<in>fst (setSchedulerAction ChooseNewThread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>action y rv' \<sigma>. dc y rv' \<Longrightarrow> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (setSchedulerAction ChooseNewThread \<sigma>). (\<sigma>', globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) s) \<in> rf_sr \<and> dc rv (xfdc (globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) s))}
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (7 subgoals):
 1. \<And>\<sigma> x. (\<sigma>, x) \<in> rf_sr \<Longrightarrow> (\<sigma>\<lparr>ksSchedulerAction := ChooseNewThread\<rparr>, globals_update (ksSchedulerAction_'_update (\<lambda>_. tcb_Ptr 1)) x) \<in> rf_sr
 2. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 4. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 6. empty_fail getSchedulerAction
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (6 subgoals):
 1. \<And>action. \<lbrace>?R20 action\<rbrace> case action of SwitchToThread target \<Rightarrow> tcbSchedEnqueue target | _ \<Rightarrow> return () \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 3. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and ?R20 action\<rbrace>
 5. empty_fail getSchedulerAction
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and ?R20 rv) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (5 subgoals):
 1. \<And>action. guard_is_UNIV dc xfdc (\<lambda>y rv'. UNIV)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)\<rbrace>
 4. empty_fail getSchedulerAction
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<lbrace>?Q9\<rbrace> getSchedulerAction \<lbrace>\<lambda>action. (\<lambda>s. action = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. action = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case action of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. action = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)\<rbrace>
 3. empty_fail getSchedulerAction
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q9 s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (valid_queues' and sch_act_simple) s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>sa. ksSchedulerAction s = ksSchedulerAction sa \<and> sch_act_simple sa) and (\<lambda>sa. (\<exists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) and valid_objs') sa) and (\<lambda>sa. (\<nexists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ((\<lambda>s. rv = ksSchedulerAction s \<and> sch_act_simple s) and (\<lambda>s. (\<exists>t. rv = SwitchToThread t) \<longrightarrow> (Invariants_H.valid_queues and tcb_at' (case rv of SwitchToThread t \<Rightarrow> t) and valid_objs') s) and (\<lambda>s. (\<nexists>t. rv = SwitchToThread t) \<longrightarrow> True) and (\<lambda>_. True)) s \<longrightarrow> s' \<in> {s. tcb_'_update (\<lambda>_. ksSchedulerAction_' (globals s)) s \<in> UNIV \<inter> \<lbrace>\<acute>tcb = tcb_ptr_to_ctcb_ptr (case rv of SwitchToThread t \<Rightarrow> t)\<rbrace>} \<inter> \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace> \<union> UNIV \<inter> - \<lbrace>\<acute>ksSchedulerAction \<noteq> NULL \<and> \<acute>ksSchedulerAction \<noteq> tcb_Ptr 1\<rbrace>} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; valid_queues' s \<and> sch_act_simple s\<rbrakk> \<Longrightarrow> \<forall>s. (s, s') \<in> rf_sr \<and> sch_act_simple s \<and> ((\<exists>t. ksSchedulerAction s = SwitchToThread t) \<longrightarrow> Invariants_H.valid_queues s \<and> tcb_at' (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) s \<and> valid_objs' s) \<longrightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr (case ksSchedulerAction s of SwitchToThread t \<Rightarrow> t) \<and> ksSchedulerAction_' (globals s') \<noteq> NULL \<and> ksSchedulerAction_' (globals s') \<noteq> tcb_Ptr 1 \<or> ksSchedulerAction_' (globals s') = NULL \<or> ksSchedulerAction_' (globals s') = tcb_Ptr 1 proof (prove)
goal (1 subgoal):
 1. \<And>s s' sa. \<lbrakk>cpspace_relation (ksPSpace s) (underlying_memory (ksMachineState s)) (t_hrs_' (globals s')); valid_queues' s; sch_act_simple s; cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues s); zero_ranges_are_zero (gsUntypedZeroRanges s) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap s); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap s); ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread sa); ksIdleThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksIdleThread sa); cinterrupt_relation (ksInterruptState s) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); case ksSchedulerAction s of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s') = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr p'; carch_state_relation (ksArchState s) (globals s'); cmachine_state_relation (ksMachineState s) (globals s'); tcb_cte_array_relation s (globals s'); apsnd fst (ghost'state_' (globals s')) = (gsUserPages sa, gsCNodes sa); ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize s); ksWorkUnitsCompleted_' (globals s') = ksWorkUnitsCompleted sa; s' \<Turnstile>\<^sub>c intStateIRQNode_array_Ptr; {symbol_table ''intStateIRQNode''..+256 * size_of TYPE(cte_C)} \<subseteq> kernel_data_refs; s' \<Turnstile>\<^sub>c armKSGlobalPD_Ptr; {symbol_table ''armKSGlobalPD''..+16384} \<subseteq> kernel_data_refs; htd_safe domain (hrs_htd (t_hrs_' (globals s'))); - domain \<subseteq> kernel_data_refs; globals_list_distinct (- kernel_data_refs) symbol_table kernel_all_global_addresses.global_data_list; cdom_schedule_relation (kernel_state.ksDomSchedule s) kernel_all_global_addresses.ksDomSchedule; ksDomScheduleIdx_' (globals s') = word_of_nat (ksDomScheduleIdx sa); ksCurDomain_' (globals s') = UCAST(8 \<rightarrow> 32) (ksCurDomain sa); ksDomainTime_' (globals s') = ksDomainTime sa; cpspace_relation (ksPSpace sa) (underlying_memory (ksMachineState sa)) (t_hrs_' (globals s')); cready_queues_relation (cslift s') (ksReadyQueues_' (globals s')) (ksReadyQueues sa); zero_ranges_are_zero (gsUntypedZeroRanges sa) (t_hrs_' (globals s')); cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' (globals s')) (ksReadyQueuesL1Bitmap sa); cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' (globals s')) (ksReadyQueuesL2Bitmap sa); ksCurThread s = ksCurThread sa; ksIdleThread s = ksIdleThread sa; cinterrupt_relation (ksInterruptState sa) intStateIRQNode_array_Ptr (intStateIRQTable_' (globals s')); case ksSchedulerAction sa of ResumeCurrentThread \<Rightarrow> ksSchedulerAction_' (globals s') = NULL | ChooseNewThread \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_Ptr 1 | SwitchToThread p' \<Rightarrow> ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr p'; carch_state_relation (ksArchState sa) (globals s'); cmachine_state_relation (ksMachineState sa) (globals s'); cte_array_relation sa (globals s'); tcb_cte_array_relation sa (globals s'); gsUserPages s = gsUserPages sa; gsCNodes s = gsCNodes sa; ghost_size_rel (ghost'state_' (globals s')) (gsMaxObjectSize sa); ksWorkUnitsCompleted s = ksWorkUnitsCompleted sa; cdom_schedule_relation (kernel_state.ksDomSchedule sa) kernel_all_global_addresses.ksDomSchedule; word_of_nat (ksDomScheduleIdx s) = word_of_nat (ksDomScheduleIdx sa); ksCurDomain s = ksCurDomain sa; ksDomainTime s = ksDomainTime sa; sch_act_simple sa; ksSchedulerAction_' (globals s') = tcb_ptr_to_ctcb_ptr (case ksSchedulerAction sa of SwitchToThread t \<Rightarrow> t) \<longrightarrow> tcb_ptr_to_ctcb_ptr (case ksSchedulerAction sa of SwitchToThread t \<Rightarrow> t) = NULL; ksSchedulerAction_' (globals s') \<noteq> tcb_Ptr 1\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals s') = NULL