theory Syscall_R

lemma hinv_invs'[wp]:
  "\<lbrace>invs' and ct_active' and
          (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
          (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace>
     handleInvocation calling blocking
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: handleInvocation_def split_def
                   ts_Restart_case_helper') apply (wp syscall_valid' setThreadState_nonqueued_state_update rfk_invs'
            hoare_vcg_all_lift hoare_weak_lift_imp) apply simp apply (intro conjI impI) apply (wp gts_imp' | simp)+ apply (rule_tac Q'="\<lambda>rv. invs'" in hoare_post_imp_R[rotated]) apply clarsimp apply (subgoal_tac "thread \<noteq> ksIdleThread s", simp_all)[1] apply (fastforce elim!: pred_tcb'_weakenE st_tcb_ex_cap'') apply (clarsimp simp: valid_idle'_def valid_state'_def
                               invs'_def pred_tcb_at'_def obj_at'_def idle_tcb'_def) apply wp+ apply (rule_tac Q="\<lambda>rv'. invs' and valid_invocation' rv
                                and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)
                                and (\<lambda>s. ksCurThread s = thread)
                                and st_tcb_at' active' thread"
                  in hoare_post_imp) apply (clarsimp simp: ct_in_state'_def) apply (frule(1) ct_not_ksQ) apply (clarsimp) apply (wp sts_invs_minor' setThreadState_st_tcb setThreadState_rct | simp)+ apply (clarsimp) apply (frule(1) ct_not_ksQ) apply (fastforce simp add: tcb_at_invs' ct_in_state'_def
                              simple_sane_strg
                              sch_act_simple_def
                       elim!: pred_tcb'_weakenE st_tcb_ex_cap''
                        dest: st_tcb_at_idle_thread')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> handleInvocation calling blocking \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)\<rbrace> doE thread <- liftE getCurThread;
info <- liftE (getMessageInfo thread);
ptr <- liftE (asUser thread (getRegister Thread_H.capRegister));
Syscall_H.syscall (doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE) (\<lambda>fault. when blocking (handleFault thread fault)) (\<lambda>p. doE args <- liftE (getMRs thread (snd (snd (snd p))) info);
global.decodeInvocation (msgLabel info) args ptr (fst p) (fst (snd p)) (fst (snd (snd p)))
odE) (\<lambda>err. when calling (replyFromKernel thread (msgFromSyscallError err))) (\<lambda>oper. doE y <- liftE (setThreadState Structures_H.thread_state.Restart thread);
reply <- global.performInvocation blocking calling oper;
liftE (do state <- getThreadState thread;
if state = Structures_H.thread_state.Restart then do y <- when calling (replyFromKernel thread (0, reply));
setThreadState Structures_H.thread_state.Running thread
od else return ()
od)
odE)
odE \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (9 subgoals):
 1. \<And>thread info ptr rv y reply. \<lbrace>?B15 thread info ptr rv y reply\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Restart \<longrightarrow> (if calling then \<lambda>s. (invs' and tcb_at' thread) s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>x. thread \<notin> set (ksReadyQueues s x))) else (\<lambda>s. invs' s \<and> st_tcb_at' simple' thread s \<and> Structures_H.thread_state.Running \<in> {Structures_H.thread_state.Inactive, Structures_H.thread_state.Running, Structures_H.thread_state.Restart, Structures_H.thread_state.IdleThreadState} \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<longrightarrow> ex_nonz_cap_to' thread s) \<and> (thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_simple s) \<and> (\<not> runnable' Structures_H.thread_state.Running \<longrightarrow> (\<forall>p. thread \<notin> set (ksReadyQueues s p))))) s) \<and> (state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> invs' s)\<rbrace>
 2. \<And>thread info ptr rv y. \<lbrace>?B14 thread info ptr rv y\<rbrace> global.performInvocation blocking calling rv \<lbrace>?B15 thread info ptr rv y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>?B14 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>thread info ptr rv reply. (calling \<longrightarrow> \<lbrace>?B15 thread info ptr rv () reply\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Restart \<longrightarrow> invs' s \<and> tcb_at' thread s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> invs' s)\<rbrace>) \<and> (\<not> calling \<longrightarrow> \<lbrace>?B15 thread info ptr rv () reply\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Restart \<longrightarrow> invs' s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> invs' s)\<rbrace>)
 2. \<And>thread info ptr rv y. \<lbrace>?B14 thread info ptr rv y\<rbrace> global.performInvocation blocking calling rv \<lbrace>?B15 thread info ptr rv y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>?B14 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>thread info ptr rv reply. calling \<Longrightarrow> \<lbrace>?B15 thread info ptr rv () reply\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Restart \<longrightarrow> invs' s \<and> tcb_at' thread s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> invs' s)\<rbrace>
 2. \<And>thread info ptr rv reply. \<not> calling \<Longrightarrow> \<lbrace>?B15 thread info ptr rv () reply\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. (state = Structures_H.thread_state.Restart \<longrightarrow> invs' s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (state \<noteq> Structures_H.thread_state.Restart \<longrightarrow> invs' s)\<rbrace>
 3. \<And>thread info ptr rv y. \<lbrace>?B14 thread info ptr rv y\<rbrace> global.performInvocation blocking calling rv \<lbrace>?B15 thread info ptr rv y\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>?B14 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 6. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 7. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 10. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?P'67 thread info ptr rv ()\<rbrace> global.performInvocation blocking calling rv \<lbrace>\<lambda>a b. (st_tcb_at' (\<lambda>a. a = Structures_H.thread_state.Restart) thread b \<longrightarrow> invs' b \<and> tcb_at' thread b \<and> st_tcb_at' simple' thread b \<and> ex_nonz_cap_to' thread b \<and> thread \<noteq> ksIdleThread b) \<and> (st_tcb_at' (\<lambda>a. a \<noteq> Structures_H.thread_state.Restart) thread b \<longrightarrow> invs' b)\<rbrace>, -
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>\<lambda>y s. (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s \<and> ?P'67 thread info ptr rv y s\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>thread info ptr rv rva s. invs' s \<Longrightarrow> (st_tcb_at' (\<lambda>a. a = Structures_H.thread_state.Restart) thread s \<longrightarrow> invs' s \<and> tcb_at' thread s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (st_tcb_at' (\<lambda>a. a \<noteq> Structures_H.thread_state.Restart) thread s \<longrightarrow> invs' s)
 2. \<And>thread info ptr rv. \<lbrace>?P'67 thread info ptr rv ()\<rbrace> global.performInvocation blocking calling rv \<lbrace>\<lambda>rv. invs'\<rbrace>, -
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>\<lambda>y s. (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s \<and> ?P'67 thread info ptr rv y s\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>thread s. \<lbrakk>invs' s; st_tcb_at' (\<lambda>a. a = Structures_H.thread_state.Restart) thread s\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s
 2. \<And>thread info ptr rv. \<lbrace>?P'67 thread info ptr rv ()\<rbrace> global.performInvocation blocking calling rv \<lbrace>\<lambda>rv. invs'\<rbrace>, -
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>\<lambda>y s. (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s \<and> ?P'67 thread info ptr rv y s\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (10 subgoals):
 1. \<And>thread s. \<lbrakk>invs' s; st_tcb_at' (\<lambda>a. a = Structures_H.thread_state.Restart) thread s; thread \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> tcb_at' thread s \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s
 2. \<And>thread s. \<lbrakk>invs' s; st_tcb_at' (\<lambda>a. a = Structures_H.thread_state.Restart) thread s\<rbrakk> \<Longrightarrow> thread \<noteq> ksIdleThread s
 3. \<And>thread info ptr rv. \<lbrace>?P'67 thread info ptr rv ()\<rbrace> global.performInvocation blocking calling rv \<lbrace>\<lambda>rv. invs'\<rbrace>, -
 4. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>\<lambda>y s. (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s \<and> ?P'67 thread info ptr rv y s\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 6. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 7. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 10. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (9 subgoals):
 1. \<And>thread s. \<lbrakk>invs' s; st_tcb_at' (\<lambda>a. a = Structures_H.thread_state.Restart) thread s\<rbrakk> \<Longrightarrow> thread \<noteq> ksIdleThread s
 2. \<And>thread info ptr rv. \<lbrace>?P'67 thread info ptr rv ()\<rbrace> global.performInvocation blocking calling rv \<lbrace>\<lambda>rv. invs'\<rbrace>, -
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>\<lambda>y s. (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s \<and> ?P'67 thread info ptr rv y s\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 6. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 9. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?P'67 thread info ptr rv ()\<rbrace> global.performInvocation blocking calling rv \<lbrace>\<lambda>rv. invs'\<rbrace>, -
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> liftE (setThreadState Structures_H.thread_state.Restart thread) \<lbrace>\<lambda>y s. (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s \<and> ?P'67 thread info ptr rv y s\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>y s. invs' s \<and> sch_act_simple s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> ct_active' s \<and> valid_invocation' rv s \<and> (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 3. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv rva s. (invs' and valid_invocation' rv and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksCurThread s = thread) and st_tcb_at' active' thread) s \<Longrightarrow> invs' s \<and> sch_act_simple s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> ct_active' s \<and> valid_invocation' rv s \<and> (invs' and sch_act_simple and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) and ct_active' and valid_invocation' rv) s
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rv'. invs' and valid_invocation' rv and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksCurThread s = thread) and st_tcb_at' active' thread\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>rv s a b. \<lbrakk>invs' s; valid_invocation' rv s; ksSchedulerAction s = ResumeCurrentThread; st_tcb_at' active' (ksCurThread s) s; ksCurThread s \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> False
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rv'. invs' and valid_invocation' rv and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksCurThread s = thread) and st_tcb_at' active' thread\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (8 subgoals):
 1. \<And>rv s a b. \<lbrakk>invs' s; valid_invocation' rv s; ksSchedulerAction s = ResumeCurrentThread; st_tcb_at' active' (ksCurThread s) s; ksCurThread s \<in> set (ksReadyQueues s (a, b)); \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> False
 2. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rv'. invs' and valid_invocation' rv and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksCurThread s = thread) and st_tcb_at' active' thread\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 5. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 8. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (7 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?P_no_err9 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rv'. invs' and valid_invocation' rv and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and (\<lambda>s. ksCurThread s = thread) and st_tcb_at' active' thread\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P_no_flt9 thread info ptr rv\<rbrace> doE args <- liftE (getMRs thread (snd (snd (snd rv))) info);
global.decodeInvocation (msgLabel info) args ptr (fst rv) (fst (snd rv)) (fst (snd (snd rv)))
odE \<lbrace>?P_no_err9 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if calling then invs' and tcb_at' thread else invs'\<rbrace>
 3. \<And>thread info ptr. \<lbrace>?B8 thread info ptr\<rbrace> doE p <- capFaultOnFailure ptr False (lookupCapAndSlot thread ptr);
buffer <- liftE (lookupIPCBuffer False thread);
extracaps <- lookupExtraCaps thread buffer info;
returnOk (snd p, fst p, extracaps, buffer)
odE \<lbrace>?P_no_flt9 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if blocking then invs' and sch_act_not thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and st_tcb_at' simple' thread and ex_nonz_cap_to' thread and (\<lambda>s. thread \<noteq> ksIdleThread s) else invs'\<rbrace>
 4. \<And>thread info. \<lbrace>?B7 thread info\<rbrace> liftE (asUser thread (getRegister Thread_H.capRegister)) \<lbrace>?B8 thread info\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>thread. \<lbrace>?B6 thread\<rbrace> liftE (getMessageInfo thread) \<lbrace>?B7 thread\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<lbrace>?Q4\<rbrace> liftE getCurThread \<lbrace>?B6\<rbrace>, \<lbrace>\<lambda>rv. invs'\<rbrace>
 7. \<And>s. (invs' and ct_active' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s \<Longrightarrow> ?Q4 s proof (prove)
goal (1 subgoal):
 1. \<And>s. invs' s \<and> ct_active' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> (calling \<longrightarrow> (blocking \<longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s) \<and> (\<not> blocking \<longrightarrow> tcb_at' (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s)) \<and> (\<not> calling \<longrightarrow> (blocking \<longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s) \<and> (\<not> blocking \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_active' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (calling \<longrightarrow> (blocking \<longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s) \<and> (\<not> blocking \<longrightarrow> tcb_at' (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s)) \<and> (\<not> calling \<longrightarrow> (blocking \<longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s) \<and> (\<not> blocking \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_active' s; vs_valid_duplicates' (ksPSpace s); ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> (calling \<longrightarrow> (blocking \<longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s) \<and> (\<not> blocking \<longrightarrow> tcb_at' (ksCurThread s) s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s)) \<and> (\<not> calling \<longrightarrow> (blocking \<longrightarrow> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s) \<and> (\<not> blocking \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {} \<and> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState) (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s)) proof (prove)
goal:
No subgoals!