theory Orphanage

lemma handleInvocation_no_orphans [wp]:
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and>
         ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<rbrace>
   handleInvocation isCall isBlocking
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" unfolding handleInvocation_def apply (rule hoare_pre) apply (wp syscall_valid' setThreadState_isRestart_no_orphans | wpc | clarsimp)+ apply (rule_tac Q="\<lambda>state s. no_orphans s \<and> invs' s \<and>
                             (state = Structures_H.thread_state.Restart \<longrightarrow>
                              st_tcb_at' isRestart thread s)"
                       in hoare_post_imp) apply (wp | clarsimp)+ apply (wp setThreadState_current_no_orphans sts_invs_minor'
                  ct_in_state'_set setThreadState_st_tcb
                  hoare_vcg_all_lift
                | simp add: split_def split del: if_split)+ apply (wps setThreadState_ct') apply (wp sts_ksQ
                   setThreadState_current_no_orphans sts_invs_minor'
                   ct_in_state'_set setThreadState_st_tcb
                 | simp add: split_def split del: if_split)+ apply (clarsimp simp: if_apply_def2) apply (frule(1) ct_not_ksQ) by (auto simp: ct_in_state'_def pred_tcb_at'_def obj_at'_def invs'_def
                    cur_tcb'_def valid_state'_def valid_idle'_def)

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> handleInvocation isCall isBlocking \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread\<rbrace> doE thread <- withoutPreemption getCurThread;
info <- withoutPreemption $ getMessageInfo thread;
ptr <- withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister;
Syscall_H.syscall (doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE) (\<lambda>fault. when isBlocking $ handleFault thread fault) (\<lambda>(slot, cap, extracaps, buffer). doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE) (\<lambda>err. when isCall $ replyFromKernel thread $ msgFromSyscallError err) (\<lambda>oper. doE withoutPreemption $ setThreadState Structures_H.thread_state.Restart thread;
reply <- global.performInvocation isBlocking isCall oper;
withoutPreemption $ do state <- getThreadState thread;
case state of Structures_H.thread_state.Restart \<Rightarrow> do when isCall $ replyFromKernel thread (0, reply);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> return ()
od
odE)
odE \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> doE thread <- withoutPreemption getCurThread;
info <- withoutPreemption $ getMessageInfo thread;
ptr <- withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister;
Syscall_H.syscall (doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE) (\<lambda>fault. when isBlocking $ handleFault thread fault) (\<lambda>(slot, cap, extracaps, buffer). doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE) (\<lambda>err. when isCall $ replyFromKernel thread $ msgFromSyscallError err) (\<lambda>oper. doE withoutPreemption $ setThreadState Structures_H.thread_state.Restart thread;
reply <- global.performInvocation isBlocking isCall oper;
withoutPreemption $ do state <- getThreadState thread;
case state of Structures_H.thread_state.Restart \<Rightarrow> do when isCall $ replyFromKernel thread (0, reply);
setThreadState Structures_H.thread_state.Running thread
od | _ \<Rightarrow> return ()
od
odE)
odE \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>thread info ptr rv reply. \<lbrace>?P'19 thread info ptr rv () reply\<rbrace> getThreadState thread \<lbrace>\<lambda>x s. ((\<exists>xa xb. x = Structures_H.thread_state.BlockedOnReceive xa xb) \<longrightarrow> no_orphans s) \<and> (awaiting_reply' x \<longrightarrow> no_orphans s) \<and> ((\<exists>xa. x = Structures_H.thread_state.BlockedOnNotification xa) \<longrightarrow> no_orphans s) \<and> (x = Structures_H.thread_state.Running \<longrightarrow> no_orphans s) \<and> (x = Structures_H.thread_state.Inactive \<longrightarrow> no_orphans s) \<and> (idle' x \<longrightarrow> no_orphans s) \<and> ((\<exists>xa xb xc xd xe. x = Structures_H.thread_state.BlockedOnSend xa xb xc xd xe) \<longrightarrow> no_orphans s) \<and> (x = Structures_H.thread_state.Restart \<longrightarrow> no_orphans s \<and> st_tcb_at' isRestart thread s \<and> valid_queues' s)\<rbrace>
 2. \<And>thread info ptr rv x. \<lbrace>?B16 thread info ptr rv x\<rbrace> global.performInvocation isBlocking isCall rv \<lbrace>\<lambda>reply s. True \<and> ?P'19 thread info ptr rv x reply s\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_err8 thread info ptr rv\<rbrace> withoutPreemption $ setThreadState Structures_H.thread_state.Restart thread \<lbrace>?B16 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_flt8 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err8 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if isCall then no_orphans else no_orphans\<rbrace>
 5. \<And>thread info ptr. \<lbrace>?B7 thread info ptr\<rbrace> doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt8 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if isBlocking then \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s else no_orphans\<rbrace>
 6. \<And>thread info. \<lbrace>?B6 thread info\<rbrace> withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister \<lbrace>?B7 thread info\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>thread. \<lbrace>?B5 thread\<rbrace> withoutPreemption $ getMessageInfo thread \<lbrace>?B6 thread\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. \<lbrace>?Q\<rbrace> withoutPreemption getCurThread \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 9. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (10 subgoals):
 1. \<And>thread info ptr rv reply rva s. no_orphans s \<and> invs' s \<and> (rva = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' isRestart thread s) \<Longrightarrow> ((\<exists>x xa. rva = Structures_H.thread_state.BlockedOnReceive x xa) \<longrightarrow> no_orphans s) \<and> (awaiting_reply' rva \<longrightarrow> no_orphans s) \<and> ((\<exists>x. rva = Structures_H.thread_state.BlockedOnNotification x) \<longrightarrow> no_orphans s) \<and> (rva = Structures_H.thread_state.Running \<longrightarrow> no_orphans s) \<and> (rva = Structures_H.thread_state.Inactive \<longrightarrow> no_orphans s) \<and> (idle' rva \<longrightarrow> no_orphans s) \<and> ((\<exists>x xa xb xc xd. rva = Structures_H.thread_state.BlockedOnSend x xa xb xc xd) \<longrightarrow> no_orphans s) \<and> (rva = Structures_H.thread_state.Restart \<longrightarrow> no_orphans s \<and> st_tcb_at' isRestart thread s \<and> valid_queues' s)
 2. \<And>thread info ptr rv reply. \<lbrace>?P'19 thread info ptr rv () reply\<rbrace> getThreadState thread \<lbrace>\<lambda>state s. no_orphans s \<and> invs' s \<and> (state = Structures_H.thread_state.Restart \<longrightarrow> st_tcb_at' isRestart thread s)\<rbrace>
 3. \<And>thread info ptr rv x. \<lbrace>?B16 thread info ptr rv x\<rbrace> global.performInvocation isBlocking isCall rv \<lbrace>\<lambda>reply s. True \<and> ?P'19 thread info ptr rv x reply s\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>thread info ptr rv. \<lbrace>?P_no_err8 thread info ptr rv\<rbrace> withoutPreemption $ setThreadState Structures_H.thread_state.Restart thread \<lbrace>?B16 thread info ptr rv\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>thread info ptr rv. \<lbrace>?P_no_flt8 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE \<lbrace>?P_no_err8 thread info ptr\<rbrace>, \<lbrace>\<lambda>err. if isCall then no_orphans else no_orphans\<rbrace>
 6. \<And>thread info ptr. \<lbrace>?B7 thread info ptr\<rbrace> doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt8 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if isBlocking then \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s else no_orphans\<rbrace>
 7. \<And>thread info. \<lbrace>?B6 thread info\<rbrace> withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister \<lbrace>?B7 thread info\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. \<And>thread. \<lbrace>?B5 thread\<rbrace> withoutPreemption $ getMessageInfo thread \<lbrace>?B6 thread\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 9. \<lbrace>?Q\<rbrace> withoutPreemption getCurThread \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 10. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>thread info ptr rv. \<lbrace>?P'139 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>x s. no_orphans s \<and> invs' s \<and> valid_invocation' rv s \<and> ct_active' s \<and> sch_act_simple s \<and> no_orphans s \<and> invs' s \<and> valid_invocation' rv s \<and> ct_active' s \<and> sch_act_simple s \<and> invs' s \<and> sch_act_simple s \<and> (\<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))) \<and> ct_active' s \<and> valid_invocation' rv s \<and> invs' s \<and> st_tcb_at' active' thread s \<and> valid_invocation' rv s \<and> ct_active' s\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P_no_flt8 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE \<lbrace>\<lambda>rv s. True \<and> ?P'139 thread info ptr rv s\<rbrace>, \<lbrace>\<lambda>err. if isCall then no_orphans else no_orphans\<rbrace>
 3. \<And>thread info ptr. \<lbrace>?B7 thread info ptr\<rbrace> doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt8 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if isBlocking then \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s else no_orphans\<rbrace>
 4. \<And>thread info. \<lbrace>?B6 thread info\<rbrace> withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister \<lbrace>?B7 thread info\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>thread. \<lbrace>?B5 thread\<rbrace> withoutPreemption $ getMessageInfo thread \<lbrace>?B6 thread\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<lbrace>?Q\<rbrace> withoutPreemption getCurThread \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv a b. \<lbrace>?P186 thread info ptr rv a b\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rv s. ksCurThread s \<notin> set (ksReadyQueues s (a, b))\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P'184 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rva s. ct_active' s \<and> valid_invocation' rv s \<and> invs' s \<and> st_tcb_at' active' thread s \<and> valid_invocation' rv s \<and> ct_active' s\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt8 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE \<lbrace>\<lambda>rv s. True \<and> (no_orphans s \<and> ksCurThread s = thread \<and> valid_queues' s) \<and> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') s \<and> valid_invocation' rv s \<and> (tcb_at' thread s \<and> active' Structures_H.thread_state.Restart \<and> thread = ksCurThread s) \<and> sch_act_simple s \<and> (no_orphans s \<and> ksCurThread s = thread \<and> valid_queues' s) \<and> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') s \<and> valid_invocation' rv s \<and> (tcb_at' thread s \<and> active' Structures_H.thread_state.Restart \<and> thread = ksCurThread s) \<and> sch_act_simple s \<and> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') s \<and> sch_act_simple s \<and> (\<forall>x xa. ?P186 thread info ptr rv x xa s) \<and> ?P'184 thread info ptr rv s\<rbrace>, \<lbrace>\<lambda>err. if isCall then no_orphans else no_orphans\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B7 thread info ptr\<rbrace> doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt8 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if isBlocking then \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s else no_orphans\<rbrace>
 5. \<And>thread info. \<lbrace>?B6 thread info\<rbrace> withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister \<lbrace>?B7 thread info\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>thread. \<lbrace>?B5 thread\<rbrace> withoutPreemption $ getMessageInfo thread \<lbrace>?B6 thread\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<lbrace>?Q\<rbrace> withoutPreemption getCurThread \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>thread info ptr rv a b prev_s. \<lbrace>?P188 thread info ptr rv a b prev_s\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rva s'. ksCurThread prev_s \<notin> set (ksReadyQueues s' (a, b))\<rbrace>
 2. \<And>thread info ptr rv. \<lbrace>?P'184 thread info ptr rv\<rbrace> setThreadState Structures_H.thread_state.Restart thread \<lbrace>\<lambda>rva s. ct_active' s \<and> valid_invocation' rv s \<and> invs' s \<and> st_tcb_at' active' thread s \<and> valid_invocation' rv s \<and> ct_active' s\<rbrace>
 3. \<And>thread info ptr rv. \<lbrace>?P_no_flt8 thread info ptr rv\<rbrace> case rv of (slot, cap, extracaps, buffer) \<Rightarrow> doE args <- withoutFailure $ getMRs thread buffer info;
global.decodeInvocation (msgLabel info) args ptr slot cap extracaps
odE \<lbrace>\<lambda>rv s. True \<and> (no_orphans s \<and> ksCurThread s = thread \<and> valid_queues' s) \<and> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') s \<and> valid_invocation' rv s \<and> (tcb_at' thread s \<and> active' Structures_H.thread_state.Restart \<and> thread = ksCurThread s) \<and> sch_act_simple s \<and> (no_orphans s \<and> ksCurThread s = thread \<and> valid_queues' s) \<and> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') s \<and> valid_invocation' rv s \<and> (tcb_at' thread s \<and> active' Structures_H.thread_state.Restart \<and> thread = ksCurThread s) \<and> sch_act_simple s \<and> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Restart \<and> (Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Restart \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) thread and (\<lambda>s. thread = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) and (\<lambda>s. (\<exists>p. thread \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) and (\<lambda>s. runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued thread s \<longrightarrow> st_tcb_at' runnable' thread s) and sch_act_simple and invs') s \<and> sch_act_simple s \<and> (\<forall>x xa. ?P188 thread info ptr rv x xa s s) \<and> ?P'184 thread info ptr rv s\<rbrace>, \<lbrace>\<lambda>err. if isCall then no_orphans else no_orphans\<rbrace>
 4. \<And>thread info ptr. \<lbrace>?B7 thread info ptr\<rbrace> doE (cap, slot) <- capFaultOnFailure ptr False $ lookupCapAndSlot thread ptr;
buffer <- withoutFailure $ lookupIPCBuffer False thread;
extracaps <- lookupExtraCaps thread buffer info;
returnOk (slot, cap, extracaps, buffer)
odE \<lbrace>?P_no_flt8 thread info ptr\<rbrace>, \<lbrace>\<lambda>ft. if isBlocking then \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s else no_orphans\<rbrace>
 5. \<And>thread info. \<lbrace>?B6 thread info\<rbrace> withoutPreemption $ asUser thread $ liftM CPtr $ getRegister Thread_H.capRegister \<lbrace>?B7 thread info\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>thread. \<lbrace>?B5 thread\<rbrace> withoutPreemption $ getMessageInfo thread \<lbrace>?B6 thread\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<lbrace>?Q\<rbrace> withoutPreemption getCurThread \<lbrace>?B5\<rbrace>, \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 8. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<and> vs_valid_duplicates' (ksPSpace s) \<and> ct_active' s \<and> ksSchedulerAction s = ResumeCurrentThread \<Longrightarrow> (if isBlocking then \<lambda>s. no_orphans s \<and> valid_queues' s \<and> valid_objs' s \<and> sch_act_wf (ksSchedulerAction s) s else no_orphans) s \<and> valid_queues' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s \<and> valid_queues' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> (\<forall>x xa. ksCurThread s \<notin> set (ksReadyQueues s (x, xa))) \<and> tcb_at' (ksCurThread s) s \<and> valid_objs' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; vs_valid_duplicates' (ksPSpace s); ct_active' s; ksSchedulerAction s = ResumeCurrentThread\<rbrakk> \<Longrightarrow> (isBlocking \<longrightarrow> valid_queues' s \<and> valid_objs' s \<and> ct_in_state' activatable' s) \<and> valid_queues' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s \<and> valid_queues' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> (\<forall>x xa. ksCurThread s \<notin> set (ksReadyQueues s (x, xa))) \<and> tcb_at' (ksCurThread s) s \<and> valid_objs' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; vs_valid_duplicates' (ksPSpace s); ct_active' s; ksSchedulerAction s = ResumeCurrentThread; \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)\<rbrakk> \<Longrightarrow> (isBlocking \<longrightarrow> valid_queues' s \<and> valid_objs' s \<and> ct_in_state' activatable' s) \<and> valid_queues' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s \<and> valid_queues' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> (\<forall>x xa. ksCurThread s \<notin> set (ksReadyQueues s (x, xa))) \<and> tcb_at' (ksCurThread s) s \<and> valid_objs' 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> (obj_at' tcbQueued (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s) \<and> valid_objs' s \<and> tcb_at' (ksCurThread s) s