theory Syscall_R

lemma hw_invs'[wp]:
  "\<lbrace>invs' and ct_in_state' simple' and sch_act_sane
          and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s)
          and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s)
          and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace>
   handleRecv isBlocking \<lbrace>\<lambda>r. invs'\<rbrace>" apply (simp add: handleRecv_def cong: if_cong) apply (rule hoare_pre) apply ((wp getNotification_wp | wpc | simp)+)[1] apply (clarsimp simp: ct_in_state'_def) apply ((wp deleteCallerCap_nonz_cap hoare_vcg_all_lift
                           deleteCallerCap_ksQ_ct'
                           hoare_lift_Pf2[OF deleteCallerCap_simple
                           deleteCallerCap_ct']
                      | wpc | simp)+)[1] apply simp apply (wp deleteCallerCap_nonz_cap hoare_vcg_all_lift
                         deleteCallerCap_ksQ_ct'
                         hoare_lift_Pf2[OF deleteCallerCap_simple
                         deleteCallerCap_ct']
                    | wpc | simp add: ct_in_state'_def whenE_def split del: if_split)+ apply (rule validE_validE_R) apply (rule_tac Q="\<lambda>rv s. invs' s
                             \<and> sch_act_sane s
                             \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))
                             \<and> thread = ksCurThread s
                             \<and> ct_in_state' simple' s
                             \<and> ex_nonz_cap_to' thread s
                             \<and> thread \<noteq> ksIdleThread s
                            \<and> (\<forall>x \<in> zobj_refs' rv. ex_nonz_cap_to' x s)"
              and E="\<lambda>_ _. True"
           in hoare_post_impErr[rotated]) apply (clarsimp simp: isCap_simps ct_in_state'_def pred_tcb_at' invs_valid_objs'
                              sch_act_sane_not obj_at'_def projectKOs pred_tcb_at'_def) apply (assumption) apply (wp)+ apply (clarsimp) apply (auto elim: st_tcb_ex_cap'' pred_tcb'_weakenE
             dest!: st_tcb_at_idle_thread'
              simp: ct_in_state'_def sch_act_sane_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p))\<rbrace> handleRecv isBlocking \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))\<rbrace> do thread <- getCurThread;
epCPtr <- asUser thread (getRegister Thread_H.capRegister);
capFaultOnFailure epCPtr True (doE epCap <- lookupCap thread epCPtr;
case epCap of capability.NotificationCap ntfnPtr x xa True \<Rightarrow> doE ntfn <- withoutFailure $ getNotification ntfnPtr;
boundTCB <- returnOk $ ntfnBoundTCB ntfn;
if boundTCB = Just thread \<or> boundTCB = Nothing then withoutFailure $ receiveSignal thread epCap isBlocking else throw $ Fault_H.lookup_failure.MissingCapability 0
odE | capability.NotificationCap ntfnPtr x xa False \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap x xa xb True xc xd \<Rightarrow> withoutFailure $ do deleteCallerCap thread;
receiveIPC thread epCap isBlocking
od | capability.EndpointCap x xa xb False xc xd \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0
odE) <catch> handleFault thread
od \<lbrace>\<lambda>r. invs'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do thread <- getCurThread;
epCPtr <- asUser thread (getRegister Thread_H.capRegister);
capFaultOnFailure epCPtr True (doE epCap <- lookupCap thread epCPtr;
case epCap of capability.NotificationCap ntfnPtr x xa True \<Rightarrow> doE ntfn <- withoutFailure $ getNotification ntfnPtr;
boundTCB <- returnOk $ ntfnBoundTCB ntfn;
if boundTCB = Just thread \<or> boundTCB = Nothing then withoutFailure $ receiveSignal thread epCap isBlocking else throw $ Fault_H.lookup_failure.MissingCapability 0
odE | capability.NotificationCap ntfnPtr x xa False \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | capability.EndpointCap x xa xb True xc xd \<Rightarrow> withoutFailure $ do deleteCallerCap thread;
receiveIPC thread epCap isBlocking
od | capability.EndpointCap x xa xb False xc xd \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0 | _ \<Rightarrow> throw $ Fault_H.lookup_failure.MissingCapability 0
odE) <catch> handleFault thread
od \<lbrace>\<lambda>r. invs'\<rbrace>
 2. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (13 subgoals):
 1. \<And>thread epCPtr epCap x51 x52 x53 x54 x55 x56. \<lbrakk>epCap = capability.EndpointCap x51 x52 x53 True x55 x56; x54\<rbrakk> \<Longrightarrow> \<lbrace>?P'452 thread epCPtr (capability.EndpointCap x51 x52 x53 True x55 x56) x51 x52 x53 True x55 x56\<rbrace> deleteCallerCap thread \<lbrace>\<lambda>rv s. ct_in_state' simple' s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x51 s\<rbrace>
 2. \<And>thread epCPtr epCap x51 x52 x53 x54 x55 x56. \<lbrakk>epCap = capability.EndpointCap x51 x52 x53 x54 x55 x56; x54 = False\<rbrakk> \<Longrightarrow> \<lbrace>?R416 thread epCPtr epCap x51 x52 x53 x54 x55 x56\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 3. \<And>thread epCPtr epCap. epCap = capability.DomainCap \<Longrightarrow> \<lbrace>?R50 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 4. \<And>thread epCPtr epCap x71 x72 x73. epCap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>?R49 thread epCPtr epCap x71 x72 x73\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 5. \<And>thread epCPtr epCap x8. epCap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>?R45 thread epCPtr epCap x8\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 6. \<And>thread epCPtr epCap x91 x92 x93. epCap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>?R43 thread epCPtr epCap x91 x92 x93\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 7. \<And>thread epCPtr epCap x101 x102 x103 x104. epCap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>?R39 thread epCPtr epCap x101 x102 x103 x104\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 8. \<And>thread epCPtr epCap x111 x112 x113 x114. epCap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>?R34 thread epCPtr epCap x111 x112 x113 x114\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 9. \<And>thread epCPtr epCap. epCap = capability.IRQControlCap \<Longrightarrow> \<lbrace>?R29 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 10. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. (\<forall>x. epCap = capability.ThreadCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (epCap = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (invs' and sch_act_not thread and st_tcb_at' simple' thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread and (\<lambda>s. \<forall>r\<in>zobj_refs' epCap. ex_nonz_cap_to' r s) and (\<lambda>s. \<exists>ntfnptr. isNotificationCap epCap \<and> capNtfnPtr epCap = ntfnptr \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) ntfnptr s)) s) \<and> (\<not> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True))) \<and> (xc = False \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True)) \<and> (\<forall>x. epCap = capability.IRQHandlerCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc xd xe. epCap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> invs' s \<and> sch_act_not thread s \<and> ?P'452 thread epCPtr epCap x xa xb xc xd xe s) \<and> (xc = False \<longrightarrow> ?R416 thread epCPtr epCap x xa xb xc xd xe s)) \<and> (epCap = capability.DomainCap \<longrightarrow> ?R50 thread epCPtr epCap s) \<and> (\<forall>x xa xb. epCap = capability.Zombie x xa xb \<longrightarrow> ?R49 thread epCPtr epCap x xa xb s) \<and> (\<forall>x. epCap = capability.ArchObjectCap x \<longrightarrow> ?R45 thread epCPtr epCap x s) \<and> (\<forall>x xa xb. epCap = capability.ReplyCap x xa xb \<longrightarrow> ?R43 thread epCPtr epCap x xa xb s) \<and> (\<forall>x xa xb xc. epCap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R39 thread epCPtr epCap x xa xb xc s) \<and> (\<forall>x xa xb xc. epCap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R34 thread epCPtr epCap x xa xb xc s) \<and> (epCap = capability.IRQControlCap \<longrightarrow> ?R29 thread epCPtr epCap s)\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>thread epCPtr x51 x52 x53 x54 x55 x56. x54 \<Longrightarrow> \<lbrace>?P'452 thread epCPtr (capability.EndpointCap x51 x52 x53 True x55 x56) x51 x52 x53 True x55 x56\<rbrace> deleteCallerCap thread \<lbrace>\<lambda>rv s. st_tcb_at' simple' (ksCurThread s) s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x51 s\<rbrace>
 2. \<And>thread epCPtr epCap x51 x52 x53 x54 x55 x56. \<lbrakk>epCap = capability.EndpointCap x51 x52 x53 x54 x55 x56; x54 = False\<rbrakk> \<Longrightarrow> \<lbrace>?R416 thread epCPtr epCap x51 x52 x53 x54 x55 x56\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 3. \<And>thread epCPtr epCap. epCap = capability.DomainCap \<Longrightarrow> \<lbrace>?R50 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 4. \<And>thread epCPtr epCap x71 x72 x73. epCap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>?R49 thread epCPtr epCap x71 x72 x73\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 5. \<And>thread epCPtr epCap x8. epCap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>?R45 thread epCPtr epCap x8\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 6. \<And>thread epCPtr epCap x91 x92 x93. epCap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>?R43 thread epCPtr epCap x91 x92 x93\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 7. \<And>thread epCPtr epCap x101 x102 x103 x104. epCap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>?R39 thread epCPtr epCap x101 x102 x103 x104\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 8. \<And>thread epCPtr epCap x111 x112 x113 x114. epCap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>?R34 thread epCPtr epCap x111 x112 x113 x114\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 9. \<And>thread epCPtr epCap. epCap = capability.IRQControlCap \<Longrightarrow> \<lbrace>?R29 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 10. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. (\<forall>x. epCap = capability.ThreadCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (epCap = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (invs' and sch_act_not thread and st_tcb_at' simple' thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread and (\<lambda>s. \<forall>r\<in>zobj_refs' epCap. ex_nonz_cap_to' r s) and (\<lambda>s. \<exists>ntfnptr. isNotificationCap epCap \<and> capNtfnPtr epCap = ntfnptr \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) ntfnptr s)) s) \<and> (\<not> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True))) \<and> (xc = False \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True)) \<and> (\<forall>x. epCap = capability.IRQHandlerCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc xd xe. epCap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> invs' s \<and> sch_act_not thread s \<and> ?P'452 thread epCPtr epCap x xa xb xc xd xe s) \<and> (xc = False \<longrightarrow> ?R416 thread epCPtr epCap x xa xb xc xd xe s)) \<and> (epCap = capability.DomainCap \<longrightarrow> ?R50 thread epCPtr epCap s) \<and> (\<forall>x xa xb. epCap = capability.Zombie x xa xb \<longrightarrow> ?R49 thread epCPtr epCap x xa xb s) \<and> (\<forall>x. epCap = capability.ArchObjectCap x \<longrightarrow> ?R45 thread epCPtr epCap x s) \<and> (\<forall>x xa xb. epCap = capability.ReplyCap x xa xb \<longrightarrow> ?R43 thread epCPtr epCap x xa xb s) \<and> (\<forall>x xa xb xc. epCap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R39 thread epCPtr epCap x xa xb xc s) \<and> (\<forall>x xa xb xc. epCap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R34 thread epCPtr epCap x xa xb xc s) \<and> (epCap = capability.IRQControlCap \<longrightarrow> ?R29 thread epCPtr epCap s)\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>thread epCPtr epCap x51 x52 x53 x54 x55 x56. \<lbrakk>epCap = capability.EndpointCap x51 x52 x53 x54 x55 x56; x54 = False\<rbrakk> \<Longrightarrow> \<lbrace>?R416 thread epCPtr epCap x51 x52 x53 x54 x55 x56\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 2. \<And>thread epCPtr epCap. epCap = capability.DomainCap \<Longrightarrow> \<lbrace>?R50 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 3. \<And>thread epCPtr epCap x71 x72 x73. epCap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>?R49 thread epCPtr epCap x71 x72 x73\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 4. \<And>thread epCPtr epCap x8. epCap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>?R45 thread epCPtr epCap x8\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 5. \<And>thread epCPtr epCap x91 x92 x93. epCap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>?R43 thread epCPtr epCap x91 x92 x93\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 6. \<And>thread epCPtr epCap x101 x102 x103 x104. epCap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>?R39 thread epCPtr epCap x101 x102 x103 x104\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 7. \<And>thread epCPtr epCap x111 x112 x113 x114. epCap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>?R34 thread epCPtr epCap x111 x112 x113 x114\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 8. \<And>thread epCPtr epCap. epCap = capability.IRQControlCap \<Longrightarrow> \<lbrace>?R29 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 9. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. (\<forall>x. epCap = capability.ThreadCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (epCap = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (invs' and sch_act_not thread and st_tcb_at' simple' thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread and (\<lambda>s. \<forall>r\<in>zobj_refs' epCap. ex_nonz_cap_to' r s) and (\<lambda>s. \<exists>ntfnptr. isNotificationCap epCap \<and> capNtfnPtr epCap = ntfnptr \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) ntfnptr s)) s) \<and> (\<not> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True))) \<and> (xc = False \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True)) \<and> (\<forall>x. epCap = capability.IRQHandlerCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc xd xe. epCap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> st_tcb_at' simple' thread s \<and> (\<forall>x xa. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s (x, xa)) \<and> thread = ksCurThread s)) s) \<and> (ex_nonz_cap_to' thread and tcb_at' thread and valid_objs') s \<and> (ex_nonz_cap_to' x and tcb_at' thread and valid_objs') s) \<and> (xc = False \<longrightarrow> ?R416 thread epCPtr epCap x xa xb xc xd xe s)) \<and> (epCap = capability.DomainCap \<longrightarrow> ?R50 thread epCPtr epCap s) \<and> (\<forall>x xa xb. epCap = capability.Zombie x xa xb \<longrightarrow> ?R49 thread epCPtr epCap x xa xb s) \<and> (\<forall>x. epCap = capability.ArchObjectCap x \<longrightarrow> ?R45 thread epCPtr epCap x s) \<and> (\<forall>x xa xb. epCap = capability.ReplyCap x xa xb \<longrightarrow> ?R43 thread epCPtr epCap x xa xb s) \<and> (\<forall>x xa xb xc. epCap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R39 thread epCPtr epCap x xa xb xc s) \<and> (\<forall>x xa xb xc. epCap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R34 thread epCPtr epCap x xa xb xc s) \<and> (epCap = capability.IRQControlCap \<longrightarrow> ?R29 thread epCPtr epCap s)\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 10. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>thread epCPtr epCap x51 x52 x53 x54 x55 x56. \<lbrakk>epCap = capability.EndpointCap x51 x52 x53 False x55 x56; \<not> x54\<rbrakk> \<Longrightarrow> \<lbrace>?R416 thread epCPtr (capability.EndpointCap x51 x52 x53 False x55 x56) x51 x52 x53 False x55 x56\<rbrace> throwError (Fault_H.lookup_failure.MissingCapability 0) \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 2. \<And>thread epCPtr epCap. epCap = capability.DomainCap \<Longrightarrow> \<lbrace>?R50 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 3. \<And>thread epCPtr epCap x71 x72 x73. epCap = capability.Zombie x71 x72 x73 \<Longrightarrow> \<lbrace>?R49 thread epCPtr epCap x71 x72 x73\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 4. \<And>thread epCPtr epCap x8. epCap = capability.ArchObjectCap x8 \<Longrightarrow> \<lbrace>?R45 thread epCPtr epCap x8\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 5. \<And>thread epCPtr epCap x91 x92 x93. epCap = capability.ReplyCap x91 x92 x93 \<Longrightarrow> \<lbrace>?R43 thread epCPtr epCap x91 x92 x93\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 6. \<And>thread epCPtr epCap x101 x102 x103 x104. epCap = capability.UntypedCap x101 x102 x103 x104 \<Longrightarrow> \<lbrace>?R39 thread epCPtr epCap x101 x102 x103 x104\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 7. \<And>thread epCPtr epCap x111 x112 x113 x114. epCap = capability.CNodeCap x111 x112 x113 x114 \<Longrightarrow> \<lbrace>?R34 thread epCPtr epCap x111 x112 x113 x114\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 8. \<And>thread epCPtr epCap. epCap = capability.IRQControlCap \<Longrightarrow> \<lbrace>?R29 thread epCPtr epCap\<rbrace> throw $ Fault_H.lookup_failure.MissingCapability 0 \<lbrace>\<lambda>r. invs'\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 9. \<And>thread epCPtr. \<lbrace>?B5 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. (\<forall>x. epCap = capability.ThreadCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (epCap = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> (invs' and sch_act_not thread and st_tcb_at' simple' thread and (\<lambda>s. \<forall>p. thread \<notin> set (ksReadyQueues s p)) and ex_nonz_cap_to' thread and (\<lambda>s. \<forall>r\<in>zobj_refs' epCap. ex_nonz_cap_to' r s) and (\<lambda>s. \<exists>ntfnptr. isNotificationCap epCap \<and> capNtfnPtr epCap = ntfnptr \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) ntfnptr s)) s) \<and> (\<not> (ntfnBoundTCB ntfn = Just thread \<or> ntfnBoundTCB ntfn = Nothing) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True))) \<and> (xc = False \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True)) \<and> (\<forall>x. epCap = capability.IRQHandlerCap x \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> True) \<and> (\<forall>x xa xb xc xd xe. epCap = capability.EndpointCap x xa xb xc xd xe \<longrightarrow> (xc = True \<longrightarrow> True \<and> True \<and> True \<and> True \<and> True \<and> True \<and> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> st_tcb_at' simple' thread s \<and> (\<forall>x xa. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ksCurThread s \<notin> set (ksReadyQueues s (x, xa)) \<and> thread = ksCurThread s)) s) \<and> (ex_nonz_cap_to' thread and tcb_at' thread and valid_objs') s \<and> (ex_nonz_cap_to' x and tcb_at' thread and valid_objs') s) \<and> (xc = False \<longrightarrow> ?R416 thread epCPtr epCap x xa xb xc xd xe s)) \<and> (epCap = capability.DomainCap \<longrightarrow> ?R50 thread epCPtr epCap s) \<and> (\<forall>x xa xb. epCap = capability.Zombie x xa xb \<longrightarrow> ?R49 thread epCPtr epCap x xa xb s) \<and> (\<forall>x. epCap = capability.ArchObjectCap x \<longrightarrow> ?R45 thread epCPtr epCap x s) \<and> (\<forall>x xa xb. epCap = capability.ReplyCap x xa xb \<longrightarrow> ?R43 thread epCPtr epCap x xa xb s) \<and> (\<forall>x xa xb xc. epCap = capability.UntypedCap x xa xb xc \<longrightarrow> ?R39 thread epCPtr epCap x xa xb xc s) \<and> (\<forall>x xa xb xc. epCap = capability.CNodeCap x xa xb xc \<longrightarrow> ?R34 thread epCPtr epCap x xa xb xc s) \<and> (epCap = capability.IRQControlCap \<longrightarrow> ?R29 thread epCPtr epCap s)\<rbrace>, \<lbrace>\<lambda>ft s. invs' s \<and> sch_act_not thread s \<and> (\<forall>p. thread \<notin> set (ksReadyQueues s p)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s\<rbrace>
 10. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>?B5 thread\<rbrace>
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?P'1005 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. ((\<exists>x. epCap = capability.ThreadCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (epCap = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc \<longrightarrow> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> (ntfnBoundTCB ntfn = Some thread \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x s \<and> isNotificationCap (capability.NotificationCap x xa xb True) \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) x s) \<and> (ntfnBoundTCB ntfn = None \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x s \<and> isNotificationCap (capability.NotificationCap x xa xb True) \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) x s) \<and> (ntfnBoundTCB ntfn \<noteq> Some thread \<and> (\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s))) \<and> (\<not> xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)) \<and> ((\<exists>x. epCap = capability.IRQHandlerCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (\<forall>x xa xb xc. (\<exists>xd xe. epCap = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> (xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> st_tcb_at' simple' thread s \<and> invs' s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> sch_act_sane s \<and> (\<forall>x xa. ksCurThread s \<notin> set (ksReadyQueues s (x, xa))) \<and> thread = ksCurThread s \<and> ex_nonz_cap_to' thread s \<and> tcb_at' thread s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> tcb_at' thread s \<and> valid_objs' s) \<and> (\<not> xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>x xa. thread \<notin> set (ksReadyQueues s (x, xa))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)) \<and> (epCap = capability.DomainCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb. epCap = capability.Zombie x xa xb) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x. epCap = capability.ArchObjectCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb. epCap = capability.ReplyCap x xa xb) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb xc. epCap = capability.UntypedCap x xa xb xc) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb xc. epCap = capability.CNodeCap x xa xb xc) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (epCap = capability.IRQControlCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)\<rbrace>, -
 2. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. invs' s \<and> sch_act_not thread s \<and> (\<forall>x. thread \<notin> set (ksReadyQueues s x)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> ?P'1005 thread epCPtr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?P'1005 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>epCap s. ((\<exists>x. epCap = capability.ThreadCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (epCap = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (\<forall>x xa xb xc. epCap = capability.NotificationCap x xa xb xc \<longrightarrow> (xc \<longrightarrow> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> (ntfnBoundTCB ntfn = Some thread \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x s \<and> isNotificationCap (capability.NotificationCap x xa xb True) \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) x s) \<and> (ntfnBoundTCB ntfn = None \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x s \<and> isNotificationCap (capability.NotificationCap x xa xb True) \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) x s) \<and> (ntfnBoundTCB ntfn \<noteq> Some thread \<and> (\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s))) \<and> (\<not> xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)) \<and> ((\<exists>x. epCap = capability.IRQHandlerCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (\<forall>x xa xb xc. (\<exists>xd xe. epCap = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> (xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> st_tcb_at' simple' thread s \<and> invs' s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> sch_act_sane s \<and> (\<forall>x xa. ksCurThread s \<notin> set (ksReadyQueues s (x, xa))) \<and> thread = ksCurThread s \<and> ex_nonz_cap_to' thread s \<and> tcb_at' thread s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> tcb_at' thread s \<and> valid_objs' s) \<and> (\<not> xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>x xa. thread \<notin> set (ksReadyQueues s (x, xa))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)) \<and> (epCap = capability.DomainCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb. epCap = capability.Zombie x xa xb) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x. epCap = capability.ArchObjectCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb. epCap = capability.ReplyCap x xa xb) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb xc. epCap = capability.UntypedCap x xa xb xc) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb xc. epCap = capability.CNodeCap x xa xb xc) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (epCap = capability.IRQControlCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. invs' s \<and> sch_act_not thread s \<and> (\<forall>x. thread \<notin> set (ksReadyQueues s x)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> ?P'1005 thread epCPtr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>thread epCPtr rv s. invs' s \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> thread = ksCurThread s \<and> ct_in_state' simple' s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> (\<forall>x\<in>zobj_refs' rv. ex_nonz_cap_to' x s) \<Longrightarrow> ((\<exists>x. rv = capability.ThreadCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (rv = capability.NullCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (\<forall>x xa xb xc. rv = capability.NotificationCap x xa xb xc \<longrightarrow> (xc \<longrightarrow> (\<forall>ntfn. ko_at' ntfn x s \<longrightarrow> (ntfnBoundTCB ntfn = Some thread \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x s \<and> isNotificationCap (capability.NotificationCap x xa xb True) \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) x s) \<and> (ntfnBoundTCB ntfn = None \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> ex_nonz_cap_to' thread s \<and> ex_nonz_cap_to' x s \<and> isNotificationCap (capability.NotificationCap x xa xb True) \<and> obj_at' (\<lambda>ko. ntfnBoundTCB ko = None \<or> ntfnBoundTCB ko = Some thread) x s) \<and> (ntfnBoundTCB ntfn \<noteq> Some thread \<and> (\<exists>y. ntfnBoundTCB ntfn = Some y) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s))) \<and> (\<not> xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)) \<and> ((\<exists>x. rv = capability.IRQHandlerCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (\<forall>x xa xb xc. (\<exists>xd xe. rv = capability.EndpointCap x xa xb xc xd xe) \<longrightarrow> (xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> st_tcb_at' simple' thread s \<and> invs' s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> sch_act_sane s \<and> (\<forall>x xa. ksCurThread s \<notin> set (ksReadyQueues s (x, xa))) \<and> thread = ksCurThread s \<and> ex_nonz_cap_to' thread s \<and> tcb_at' thread s \<and> valid_objs' s \<and> ex_nonz_cap_to' x s \<and> tcb_at' thread s \<and> valid_objs' s) \<and> (\<not> xc \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>x xa. thread \<notin> set (ksReadyQueues s (x, xa))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)) \<and> (rv = capability.DomainCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb. rv = capability.Zombie x xa xb) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x. rv = capability.ArchObjectCap x) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb. rv = capability.ReplyCap x xa xb) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb xc. rv = capability.UntypedCap x xa xb xc) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> ((\<exists>x xa xb xc. rv = capability.CNodeCap x xa xb xc) \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s) \<and> (rv = capability.IRQControlCap \<longrightarrow> invs' s \<and> sch_act_not thread s \<and> (\<forall>a b. thread \<notin> set (ksReadyQueues s (a, b))) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s)
 2. \<And>thread epCPtr e s. True \<Longrightarrow> True
 3. \<And>thread epCPtr. \<lbrace>?P'1005 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> thread = ksCurThread s \<and> ct_in_state' simple' s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> (\<forall>x\<in>zobj_refs' rv. ex_nonz_cap_to' x s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. invs' s \<and> sch_act_not thread s \<and> (\<forall>x. thread \<notin> set (ksReadyQueues s x)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> ?P'1005 thread epCPtr s\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 6. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>thread epCPtr e s. True \<Longrightarrow> True
 2. \<And>thread epCPtr. \<lbrace>?P'1005 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> thread = ksCurThread s \<and> ct_in_state' simple' s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> (\<forall>x\<in>zobj_refs' rv. ex_nonz_cap_to' x s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. invs' s \<and> sch_act_not thread s \<and> (\<forall>x. thread \<notin> set (ksReadyQueues s x)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> ?P'1005 thread epCPtr s\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 5. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>thread epCPtr. \<lbrace>?P'1005 thread epCPtr\<rbrace> lookupCap thread epCPtr \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> thread = ksCurThread s \<and> ct_in_state' simple' s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> (\<forall>x\<in>zobj_refs' rv. ex_nonz_cap_to' x s)\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 2. \<And>thread. \<lbrace>?B4 thread\<rbrace> asUser thread (getRegister Thread_H.capRegister) \<lbrace>\<lambda>epCPtr s. invs' s \<and> sch_act_not thread s \<and> (\<forall>x. thread \<notin> set (ksReadyQueues s x)) \<and> st_tcb_at' simple' thread s \<and> ex_nonz_cap_to' thread s \<and> thread \<noteq> ksIdleThread s \<and> ?P'1005 thread epCPtr s\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B4\<rbrace>
 4. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs' and ct_in_state' simple' and sch_act_sane and (\<lambda>s. ex_nonz_cap_to' (ksCurThread s) s) and (\<lambda>s. ksCurThread s \<noteq> ksIdleThread s) and (\<lambda>s. \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> (invs' and tcb_at' (ksCurThread s)) s \<and> sch_act_not (ksCurThread s) s \<and> (\<forall>x. ksCurThread s \<notin> set (ksReadyQueues s x)) \<and> st_tcb_at' simple' (ksCurThread s) s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> True \<and> (invs' and tcb_at' (ksCurThread s)) s \<and> sch_act_sane s \<and> (\<forall>p. ksCurThread s \<notin> set (ksReadyQueues s p)) \<and> ksCurThread s = ksCurThread s \<and> ct_in_state' simple' s \<and> ex_nonz_cap_to' (ksCurThread s) s \<and> ksCurThread s \<noteq> ksIdleThread s \<and> invs' s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs' s; ct_in_state' simple' s; sch_act_sane s; ex_nonz_cap_to' (ksCurThread s) s; ksCurThread s \<noteq> ksIdleThread s; \<forall>a b. ksCurThread s \<notin> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> tcb_at' (ksCurThread s) s \<and> sch_act_not (ksCurThread s) s \<and> st_tcb_at' simple' (ksCurThread s) s \<and> tcb_at' (ksCurThread s) s proof (prove)
goal:
No subgoals!