theory Schedule_C

lemma activateThread_ccorres:
  "ccorres dc xfdc
           (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s)
                   and valid_queues and valid_objs')
           UNIV []
           activateThread
           (Call activateThread_'proc)" apply (cinit) apply (rule ccorres_pre_getCurThread) apply (ctac add: get_tsType_ccorres2 [where f="\<lambda>s. ksCurThread_' (globals s)"]) apply (rule_tac P="activatable' rv" in ccorres_gen_asm) apply (wpc) apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) apply simp apply (rule ccorres_cond_true) apply (rule ccorres_return_Skip) apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) apply (simp add: "StrictC'_thread_state_defs" del: Collect_const) apply (rule ccorres_cond_false) apply (rule ccorres_cond_false) apply (rule ccorres_cond_true) apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: activateIdleThread_def return_def) apply (rule_tac P=\<top> and P'=UNIV in ccorres_inst, simp) apply (simp add: "StrictC'_thread_state_defs" del: Collect_const) apply (rule ccorres_cond_false) apply (rule ccorres_cond_true) apply (rule ccorres_rhs_assoc)+ apply csymbr apply (ctac) apply (ctac add: setNextPC_ccorres) apply ctac apply (wp | simp add: valid_tcb_state'_def)+ apply vcg apply wp apply vcg apply (wp gts_wp') apply vcg apply (clarsimp simp: ct_in_state'_def) apply (rule conjI, clarsimp) apply (clarsimp simp: st_tcb_at'_def) apply (rule conjI, clarsimp simp: obj_at'_def) apply clarsimp apply (drule (1) obj_at_cslift_tcb) apply (subgoal_tac "ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)") prefer 2 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (clarsimp simp: typ_heap_simps ThreadState_Running_def mask_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') UNIV [] activateThread (Call activateThread_'proc) proof (prove)
goal (2 subgoals):
 1. ccorres dc xfdc ?Q191 ?Q'191 [SKIP] (do thread <- getCurThread;
state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)} (\<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q191 s \<and> s' \<in> ?Q'191 proof (prove)
goal (2 subgoals):
 1. \<And>thread. ccorres dc xfdc (?P197 thread) (?P'197 thread) [SKIP] (do state <- getThreadState thread;
case state of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show state
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)} (\<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))));;
IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF \<acute>ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> ?P197 rv s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> ?P'197 rv} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv ret__unsigned. ret__unsigned = thread_state_to_tsType rv \<Longrightarrow> ccorres dc xfdc (?Q202 thread rv) (?Q'202 thread rv ret__unsigned) [SKIP] (case rv of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>?Q202 thread\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> ?Q'202 thread rv (ret__unsigned_' s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?G382 thread rv) (?Q'202 thread rv ret__unsigned) [SKIP] (case rv of Structures_H.thread_state.Running \<Rightarrow> return () | Structures_H.thread_state.IdleThreadState \<Rightarrow> activateIdleThread thread | Structures_H.thread_state.Restart \<Rightarrow> do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. ?G382 thread rv and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> ?Q'202 thread rv (ret__unsigned_' s)}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (11 subgoals):
 1. \<And>thread rv ret__unsigned x11 x12. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnReceive x11 x12\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R410 thread rv x11 x12) (?R''408 thread rv ret__unsigned x11 x12) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; awaiting_reply' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R411 thread rv) (?R''405 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned x3. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R412 thread rv x3) (?R''404 thread rv ret__unsigned x3) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R413 thread rv) (?R''402 thread rv ret__unsigned) [SKIP] (return ()) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 6. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 7. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 8. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 9. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> ?R410 thread rv x xa s) \<and> (awaiting_reply' rv \<longrightarrow> ?R411 thread rv s) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R412 thread rv x s) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> ?R413 thread rv s) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 10. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> sa \<in> ?R''408 thread rv (ret__unsigned_' s) x xa}}} \<inter> ({sa. awaiting_reply' rv \<longrightarrow> sa \<in> ?R''405 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> sa \<in> ?R''404 thread rv (ret__unsigned_' s) x}} \<inter> ({sa. rv = Structures_H.thread_state.Running \<longrightarrow> sa \<in> ?R''402 thread rv (ret__unsigned_' s)} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; awaiting_reply' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R411 thread rv) (?R''405 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned x3. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R412 thread rv x3) (?R''404 thread rv ret__unsigned x3) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R413 thread rv) (?R''402 thread rv ret__unsigned) [SKIP] (return ()) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 6. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 7. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 8. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> ?R411 thread rv s) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R412 thread rv x s) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> ?R413 thread rv s) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 9. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({sa. awaiting_reply' rv \<longrightarrow> sa \<in> ?R''405 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> sa \<in> ?R''404 thread rv (ret__unsigned_' s) x}} \<inter> ({sa. rv = Structures_H.thread_state.Running \<longrightarrow> sa \<in> ?R''402 thread rv (ret__unsigned_' s)} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 10. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (9 subgoals):
 1. \<And>thread rv ret__unsigned x3. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R412 thread rv x3) (?R''404 thread rv ret__unsigned x3) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R413 thread rv) (?R''402 thread rv ret__unsigned) [SKIP] (return ()) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 6. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 7. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> ?R412 thread rv x s) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> ?R413 thread rv s) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 8. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({sa. \<forall>x. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> sa \<in> ?R''404 thread rv (ret__unsigned_' s) x}} \<inter> ({sa. rv = Structures_H.thread_state.Running \<longrightarrow> sa \<in> ?R''402 thread rv (ret__unsigned_' s)} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 9. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (8 subgoals):
 1. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R413 thread rv) (?R''402 thread rv ret__unsigned) [SKIP] (return ()) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 6. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> ?R413 thread rv s) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 7. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. rv = Structures_H.thread_state.Running \<longrightarrow> sa \<in> ?R''402 thread rv (ret__unsigned_' s)} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (8 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R413 thread Structures_H.thread_state.Running) (?R''402 thread Structures_H.thread_state.Running (SCAST(32 signed \<rightarrow> 32) ThreadState_Running)) [SKIP] (return ()) (Cond UNIV SKIP (Cond (if ThreadState_Running = ThreadState_Restart then UNIV else {}) (lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)) (Cond (if ThreadState_Running = ThreadState_IdleThreadState then UNIV else {}) (CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)) (Guard DontReach {} SKIP))))
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 6. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> ?R413 thread rv s) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 7. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. rv = Structures_H.thread_state.Running \<longrightarrow> sa \<in> ?R''402 thread rv (ret__unsigned_' s)} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (8 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R413 thread Structures_H.thread_state.Running) (?R'436 thread Structures_H.thread_state.Running (SCAST(32 signed \<rightarrow> 32) ThreadState_Running)) [SKIP] (return ()) SKIP
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 6. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> ?R413 thread rv s) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 7. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({sa. rv = Structures_H.thread_state.Running \<longrightarrow> sa \<in> ?R'436 thread rv (ret__unsigned_' s) \<inter> UNIV} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (7 subgoals):
 1. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R414 thread rv) (?R''401 thread rv ret__unsigned) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 5. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> ?R414 thread rv s) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 6. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({sa. rv = Structures_H.thread_state.Inactive \<longrightarrow> sa \<in> ?R''401 thread rv (ret__unsigned_' s)} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; idle' rv\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R415 thread rv) (?R''400 thread rv ret__unsigned) [SKIP] (activateIdleThread thread) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R415 thread Structures_H.thread_state.IdleThreadState) (?R''400 thread Structures_H.thread_state.IdleThreadState 7) [SKIP] (activateIdleThread thread) (IF False THEN
  SKIP
ELSE
  IF False THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1)
ELSE
  IF True THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R''400 thread rv (ret__unsigned_' s)} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R415 thread Structures_H.thread_state.IdleThreadState) (?R'442 thread Structures_H.thread_state.IdleThreadState 7) [SKIP] (activateIdleThread thread) (IF False THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1)
ELSE
  IF True THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R'442 thread rv (ret__unsigned_' s) \<inter> - \<lbrace>False\<rbrace>} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R415 thread Structures_H.thread_state.IdleThreadState) (?R'445 thread Structures_H.thread_state.IdleThreadState 7) [SKIP] (activateIdleThread thread) (IF True THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI)
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R'445 thread rv (ret__unsigned_' s) \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R415 thread Structures_H.thread_state.IdleThreadState) (?R'448 thread Structures_H.thread_state.IdleThreadState 7) [SKIP] (activateIdleThread thread) (CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread))
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> ?R415 thread rv s) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({sa. idle' rv \<longrightarrow> sa \<in> ?R'448 thread rv (ret__unsigned_' s) \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread) {s. \<exists>(rv, \<sigma>')\<in>fst (activateIdleThread thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread \<sigma>. {s. True \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst (activateIdleThread thread \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> dc rv (xfdc s)}
 2. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (5 subgoals):
 1. \<And>thread rv ret__unsigned x71 x72 x73 x74 x75. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R416 thread rv x71 x72 x73 x74 x75) (?R''399 thread rv ret__unsigned x71 x72 x73 x74 x75) [SKIP] (haskell_fail $ [] @ show rv) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 3. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> ?R416 thread rv x xa xb xc xd s) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 4. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({sa. \<forall>x. sa \<in> {sa. \<forall>xa. sa \<in> {sa. \<forall>xb. sa \<in> {sa. \<forall>xc. sa \<in> {sa. \<forall>xd. sa \<in> {sa. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> sa \<in> ?R''399 thread rv (ret__unsigned_' s) x xa xb xc xd}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread rv ret__unsigned. \<lbrakk>ret__unsigned = thread_state_to_tsType rv; activatable' rv; rv = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?R417 thread rv) (?R''393 thread rv ret__unsigned) [SKIP] (do pc <- asUser thread $ getRestartPC;
asUser thread $ setNextPC pc;
setThreadState Structures_H.thread_state.Running thread
od) (IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Running THEN
  SKIP
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,SCAST(32 signed \<rightarrow> 32) ThreadState_Running)
ELSE
  IF ret__unsigned = SCAST(32 signed \<rightarrow> 32) ThreadState_IdleThreadState THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R417 thread Structures_H.thread_state.Restart) (?R''393 thread Structures_H.thread_state.Restart 2) [SKIP] (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od) (IF False THEN
  SKIP
ELSE
  IF True THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1)
ELSE
  IF False THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI
FI)
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R''393 thread rv (ret__unsigned_' s)}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R417 thread Structures_H.thread_state.Restart) (?R'500 thread Structures_H.thread_state.Restart 2) [SKIP] (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od) (IF True THEN
  lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1)
ELSE
  IF False THEN
  CALL Arch_activateIdleThread_'proc(\<acute>ksCurThread)
ELSE
  Guard DontReach {} SKIP
FI
FI)
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R'500 thread rv (ret__unsigned_' s) \<inter> - \<lbrace>False\<rbrace>}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R417 thread Structures_H.thread_state.Restart) (?R'503 thread Structures_H.thread_state.Restart 2) [SKIP] (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od) (lvar_nondet_init pc_' pc_'_update;;
\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1))
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R'503 thread rv (ret__unsigned_' s) \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R417 thread Structures_H.thread_state.Restart) (?R'503 thread Structures_H.thread_state.Restart 2) [SKIP] (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od) (lvar_nondet_init pc_' pc_'_update;;
(\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
(CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1))))
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> ?R'503 thread rv (ret__unsigned_' s) \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread. ccorres dc xfdc (?R417 thread Structures_H.thread_state.Restart) (?G'513 thread Structures_H.thread_state.Restart 2) [SKIP] (do pc <- asUser thread getRestartPC;
y <- asUser thread (setNextPC pc);
setThreadState Structures_H.thread_state.Running thread
od) (\<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread);;
(CALL setNextPC_'proc(\<acute>ksCurThread,\<acute>pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1)))
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ?R417 thread rv s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> ?G'513 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread rv pc. rv = pc \<Longrightarrow> ccorres dc xfdc (?Q524 thread rv) (?Q'524 thread rv pc) [SKIP] (do y <- asUser thread (setNextPC rv);
setThreadState Structures_H.thread_state.Running thread
od) (CALL setNextPC_'proc(\<acute>ksCurThread,pc);;
CALL setThreadState_'proc(\<acute>ksCurThread,1))
 2. \<And>thread. \<lbrace>?R532 thread Structures_H.thread_state.Restart\<rbrace> asUser thread getRestartPC \<lbrace>?Q524 thread\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'527 thread Structures_H.thread_state.Restart 2) \<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread) {s. \<forall>rv. rv = pc_' s \<longrightarrow> s \<in> ?Q'524 thread rv (pc_' s)}
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and ?R532 thread rv) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'527 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (8 subgoals):
 1. \<And>thread rv pc rva xfdca. \<lbrakk>rv = pc; dc rva xfdca\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q599 thread rv pc rva) (?Q'599 thread rv pc rva xfdca) [SKIP] (setThreadState Structures_H.thread_state.Running thread) (CALL setThreadState_'proc(\<acute>ksCurThread,1))
 2. \<And>thread rv pc. rv = pc \<Longrightarrow> \<lbrace>?R601 thread rv\<rbrace> asUser thread (setNextPC rv) \<lbrace>?Q599 thread rv pc\<rbrace>
 3. \<And>thread rv pc. rv = pc \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'599 thread rv pc) CALL setNextPC_'proc(\<acute>ksCurThread,pc) {s. \<forall>rva. dc rva (xfdc s) \<longrightarrow> s \<in> ?Q'599 thread rv pc rva (xfdc s)}
 4. \<And>thread. \<lbrace>?R532 thread Structures_H.thread_state.Restart\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R601 thread a\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'527 thread Structures_H.thread_state.Restart 2) \<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread) {s. \<forall>rv. rv = pc_' s \<longrightarrow> s \<in> {sa. v_'_update (\<lambda>_. pc_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals sa)) sa) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = rv\<rbrace>} \<inter> ?R'599 thread rv (pc_' s)}
 6. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and ?R532 thread rv) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 7. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'527 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 8. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (7 subgoals):
 1. \<And>thread rv pc. rv = pc \<Longrightarrow> \<lbrace>?R601 thread rv\<rbrace> asUser thread (setNextPC rv) \<lbrace>\<lambda>rva s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> valid_tcb_state' Structures_H.thread_state.Running s \<and> (ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' Structures_H.thread_state.Running) \<and> (\<forall>p. thread \<in> set (ksReadyQueues s p) \<longrightarrow> runnable' Structures_H.thread_state.Running) \<and> sch_act_wf (ksSchedulerAction s) s\<rbrace>
 2. \<And>thread rv pc. rv = pc \<Longrightarrow> \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'599 thread rv pc) CALL setNextPC_'proc(\<acute>ksCurThread,pc) {s. \<forall>rv. dc rv (xfdc s) \<longrightarrow> s \<in> {s. ts_'_update (\<lambda>_. 1) (tptr_'_update (\<lambda>_. ksCurThread_' (globals s)) s) \<in> \<lbrace>\<forall>cl fl. cthread_state_relation_lifted Structures_H.thread_state.Running (cl\<lparr>tsType_CL := \<acute>ts && mask 4\<rparr>, fl)\<rbrace> \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>}}
 3. \<And>thread. \<lbrace>?R532 thread Structures_H.thread_state.Restart\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>_. True) and ?R601 thread a\<rbrace>
 4. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'527 thread Structures_H.thread_state.Restart 2) \<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread) {s. \<forall>rv. rv = pc_' s \<longrightarrow> s \<in> {sa. v_'_update (\<lambda>_. pc_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals sa)) sa) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = rv\<rbrace>} \<inter> ?R'599 thread rv (pc_' s)}
 5. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and ?R532 thread rv) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 6. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'527 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 7. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (6 subgoals):
 1. \<And>thread rv. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'599 thread rv rv) CALL setNextPC_'proc(\<acute>ksCurThread,rv) \<lbrace>1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> \<acute>ksCurThread = tcb_ptr_to_ctcb_ptr thread\<rbrace>
 2. \<And>thread. \<lbrace>?R532 thread Structures_H.thread_state.Restart\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'527 thread Structures_H.thread_state.Restart 2) \<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread) {s. \<forall>rv. rv = pc_' s \<longrightarrow> s \<in> {sa. v_'_update (\<lambda>_. pc_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals sa)) sa) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = rv\<rbrace>} \<inter> ?R'599 thread rv (pc_' s)}
 4. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and ?R532 thread rv) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 5. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'527 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 6. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (5 subgoals):
 1. \<And>thread. \<lbrace>?R532 thread Structures_H.thread_state.Restart\<rbrace> asUser thread getRestartPC \<lbrace>\<lambda>a. (\<lambda>_. True) and (\<lambda>s. tcb_at' thread s \<and> Invariants_H.valid_queues s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s)\<rbrace>
 2. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'527 thread Structures_H.thread_state.Restart 2) \<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread) {s. \<forall>rv. rv = pc_' s \<longrightarrow> s \<in> {sa. v_'_update (\<lambda>_. pc_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals sa)) sa) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = rv\<rbrace>} \<inter> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread}}
 3. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and ?R532 thread rv) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 4. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'527 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 5. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (4 subgoals):
 1. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'527 thread Structures_H.thread_state.Restart 2) \<acute>pc :== CALL getRestartPC_'proc(\<acute>ksCurThread) {s. \<forall>rv. rv = pc_' s \<longrightarrow> s \<in> {sa. v_'_update (\<lambda>_. pc_' s) (thread_'_update (\<lambda>_. ksCurThread_' (globals sa)) sa) \<in> UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>v = rv\<rbrace>} \<inter> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread}}
 2. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> sch_act_wf (ksSchedulerAction a) a)) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 3. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {sa. rv = Structures_H.thread_state.Restart \<longrightarrow> sa \<in> {sa. \<forall>v. pc_'_update (\<lambda>_. v) sa \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> ?R'527 thread rv (ret__unsigned_' s)} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 4. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (3 subgoals):
 1. \<And>thread. \<lbrace>?R202 thread\<rbrace> getThreadState thread \<lbrace>\<lambda>rv. (\<lambda>s. (\<forall>x xa. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' rv \<longrightarrow> True) \<and> (\<forall>x. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' rv \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (rv = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> tcb_at' thread a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> sch_act_wf (ksSchedulerAction a) a)) s)) and (\<lambda>_. activatable' rv)\<rbrace>
 2. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {s. rv = Structures_H.thread_state.Restart \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread)}} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 3. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and ?R202 rv) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (2 subgoals):
 1. \<And>thread. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> (?R'202 thread) \<acute>ret__unsigned :== CALL thread_state_get_tsType_'proc(h_val (hrs_mem \<acute>t_hrs) (PTR(thread_state_C) &(\<acute>ksCurThread\<rightarrow>[''tcbState_C'']))) {s. \<forall>rv. ret__unsigned_' s = thread_state_to_tsType rv \<longrightarrow> s \<in> {s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. rv = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> s \<in> UNIV}}} \<inter> ({s. awaiting_reply' rv \<longrightarrow> s \<in> UNIV} \<inter> ({s. \<forall>x. s \<in> {s. rv = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> s \<in> UNIV}} \<inter> ({s. rv = Structures_H.thread_state.Running \<longrightarrow> s \<in> UNIV \<inter> UNIV} \<inter> ({s. rv = Structures_H.thread_state.Inactive \<longrightarrow> s \<in> UNIV} \<inter> ({s. idle' rv \<longrightarrow> s \<in> UNIV \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace> \<inter> - \<lbrace>False\<rbrace>} \<inter> ({s. \<forall>x. s \<in> {s. \<forall>xa. s \<in> {s. \<forall>xb. s \<in> {s. \<forall>xc. s \<in> {s. \<forall>xd. s \<in> {s. rv = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> s \<in> UNIV}}}}}} \<inter> {s. rv = Structures_H.thread_state.Restart \<longrightarrow> s \<in> {s. \<forall>v. pc_'_update (\<lambda>_. v) s \<in> {s. thread_'_update (\<lambda>_. ksCurThread_' (globals s)) s \<in> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace>} \<inter> {s. SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr thread)}} \<inter> \<lbrace>True\<rbrace> \<inter> - \<lbrace>False\<rbrace>}))))))}
 2. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and (\<lambda>s. \<forall>st. st_tcb_at' ((=) st) rv s \<longrightarrow> ((\<lambda>s. (\<forall>x xa. st = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' st \<longrightarrow> True) \<and> (\<forall>x. st = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (st = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (st = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' st \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. st = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (st = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> tcb_at' rv a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> sch_act_wf (ksSchedulerAction a) a)) s)) and (\<lambda>_. activatable' st)) s)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> ?R'202 rv \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; (ct_in_state' activatable' and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (\<forall>rv. ksCurThread s = rv \<longrightarrow> (tcb_at' rv and (\<lambda>s. \<forall>st. st_tcb_at' ((=) st) rv s \<longrightarrow> ((\<lambda>s. (\<forall>x xa. st = Structures_H.thread_state.BlockedOnReceive x xa \<longrightarrow> True) \<and> (awaiting_reply' st \<longrightarrow> True) \<and> (\<forall>x. st = Structures_H.thread_state.BlockedOnNotification x \<longrightarrow> True) \<and> (st = Structures_H.thread_state.Running \<longrightarrow> True) \<and> (st = Structures_H.thread_state.Inactive \<longrightarrow> True) \<and> (idle' st \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd. st = Structures_H.thread_state.BlockedOnSend x xa xb xc xd \<longrightarrow> True) \<and> (st = Structures_H.thread_state.Restart \<longrightarrow> ((\<lambda>a. True) and (\<lambda>a. True \<and> tcb_at' rv a \<and> Invariants_H.valid_queues a \<and> valid_objs' a \<and> sch_act_wf (ksSchedulerAction a) a)) s)) and (\<lambda>_. activatable' st)) s)) s) \<and> s' \<in> {s. \<forall>rv. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> s \<in> {s. thread_state_'_update (\<lambda>_. h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C'']))) s \<in> UNIV \<inter> \<lbrace>\<acute>ksCurThread = tcb_ptr_to_ctcb_ptr rv\<rbrace> \<inter> {s. cslift s (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])) = Some (thread_state_' s)}} \<inter> {s. \<forall>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])))) \<longrightarrow> (\<forall>rva. tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s))) (PTR(thread_state_C) &(ksCurThread_' (globals s)\<rightarrow>[''tcbState_C''])))) = thread_state_to_tsType rva \<longrightarrow> rva = Structures_H.thread_state.Restart \<longrightarrow> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> s \<Turnstile>\<^sub>c ksCurThread_' (globals s) \<longrightarrow> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv \<and> (SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < SCAST(32 signed \<rightarrow> 32) 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rv)))} \<inter> {s. s \<Turnstile>\<^sub>c ksCurThread_' (globals s)}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; st_tcb_at' activatable' (ksCurThread s) s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> (\<forall>st. st_tcb_at' ((=) st) (ksCurThread s) s \<longrightarrow> (st = Structures_H.thread_state.Restart \<longrightarrow> tcb_at' (ksCurThread s) s) \<and> activatable' st) \<and> (\<forall>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; st_tcb_at' activatable' (ksCurThread s) s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s\<rbrakk> \<Longrightarrow> (\<forall>st. st_tcb_at' ((=) st) (ksCurThread s) s \<longrightarrow> (st = Structures_H.thread_state.Restart \<longrightarrow> tcb_at' (ksCurThread s) s) \<and> activatable' st) \<and> (\<forall>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s\<rbrakk> \<Longrightarrow> (\<forall>st. obj_at' ((=) st \<circ> tcbState) (ksCurThread s) s \<longrightarrow> (st = Structures_H.thread_state.Restart \<longrightarrow> tcb_at' (ksCurThread s) s) \<and> activatable' st) \<and> (\<forall>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv) proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s\<rbrakk> \<Longrightarrow> \<forall>rv. ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv \<longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; obj_at' (activatable' \<circ> tcbState) (ksCurThread s) s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv\<rbrakk> \<Longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> (activatable' \<circ> tcbState) ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv proof (prove)
goal (2 subgoals):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> (activatable' \<circ> tcbState) ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rbrakk> \<Longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv
 2. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> (activatable' \<circ> tcbState) ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s) proof (prove)
goal (2 subgoals):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> (activatable' \<circ> tcbState) ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)
 2. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> (activatable' \<circ> tcbState) ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rbrakk> \<Longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv proof (prove)
goal (1 subgoal):
 1. \<And>s s' rv. \<lbrakk>(s, s') \<in> rf_sr; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr rv; \<exists>ko ko'. ko_at' ko (ksCurThread s) s \<and> (activatable' \<circ> tcbState) ko \<and> cslift s' (tcb_ptr_to_ctcb_ptr (ksCurThread s)) = Some ko' \<and> ctcb_relation ko ko'; ksCurThread_' (globals s') = tcb_ptr_to_ctcb_ptr (ksCurThread s)\<rbrakk> \<Longrightarrow> cslift s' (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])) = Some (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))) \<and> ((\<exists>t. ret__unsigned_' t = tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C'']))))) \<longrightarrow> tsType_CL (thread_state_lift (h_val (hrs_mem (t_hrs_' (globals s'))) (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr rv\<rightarrow>[''tcbState_C''])))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.FaultIP < 0x14 \<longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv \<longrightarrow> SCAST(32 signed \<rightarrow> 32) Kernel_C.NextIP < 0x14 \<longrightarrow> 1 && mask 4 = SCAST(32 signed \<rightarrow> 32) ThreadState_Running) \<and> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr rv proof (prove)
goal:
No subgoals!