theory Syscall_R

lemma doReply_invs[wp]:
  "\<lbrace>tcb_at' t and tcb_at' t' and
    cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = ReplyCap t False grant) slot and
    invs' and sch_act_simple\<rbrace>
     doReplyTransfer t' t slot grant
   \<lbrace>\<lambda>rv. invs'\<rbrace>" apply (simp add: doReplyTransfer_def liftM_def) apply (rule hoare_seq_ext [OF _ gts_sp']) apply (rule hoare_seq_ext [OF _ assert_sp]) apply (rule hoare_seq_ext [OF _ getCTE_sp]) apply (wp, wpc) apply (wp) apply (wp (once) sts_invs_minor'') apply (simp) apply (wp (once) sts_st_tcb') apply (wp)[1] apply (rule_tac Q="\<lambda>rv s. invs' s
                                   \<and> t \<noteq> ksIdleThread s
                                   \<and> st_tcb_at' awaiting_reply' t s"
                 in hoare_post_imp) apply (clarsimp) apply (frule_tac t=t in invs'_not_runnable_not_queued) apply (erule pred_tcb'_weakenE, case_tac st, clarsimp+) apply (rule conjI, erule pred_tcb'_weakenE, case_tac st, clarsimp+) apply (rule conjI, rule impI, erule pred_tcb'_weakenE, case_tac st) apply (clarsimp | drule(1) obj_at_conj')+ apply (clarsimp simp: invs'_def valid_state'_def ct_in_state'_def) apply (drule(1) pred_tcb_at_conj') apply (subgoal_tac "st_tcb_at' (\<lambda>_. False) (ksCurThread s) s") apply (clarsimp) apply (erule_tac P="\<lambda>st. awaiting_reply' st \<and> activatable' st"
                  in pred_tcb'_weakenE) apply (case_tac st, clarsimp+) apply (wp cteDeleteOne_reply_pred_tcb_at)+ apply (clarsimp) apply (rule_tac Q="\<lambda>_. (\<lambda>s. t \<noteq> ksIdleThread s)
                          and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot"
                in hoare_strengthen_post [rotated]) apply (fastforce simp: cte_wp_at'_def) apply (wp) apply (rule hoare_strengthen_post [OF doIPCTransfer_non_null_cte_wp_at']) apply (erule conjE) apply assumption apply (erule cte_wp_at_weakenE') apply (fastforce) apply (wp sts_invs_minor'' sts_st_tcb' hoare_weak_lift_imp) apply (rule_tac Q="\<lambda>rv s. invs' s \<and> sch_act_simple s
                                   \<and> st_tcb_at' awaiting_reply' t s
                                   \<and> t \<noteq> ksIdleThread s"
                         in hoare_post_imp) apply (clarsimp) apply (frule_tac t=t in invs'_not_runnable_not_queued) apply (erule pred_tcb'_weakenE, case_tac st, clarsimp+) apply (rule conjI, erule pred_tcb'_weakenE, case_tac st, clarsimp+) apply (rule conjI, rule impI, erule pred_tcb'_weakenE, case_tac st) apply (clarsimp | drule(1) obj_at_conj')+ apply (clarsimp simp: invs'_def valid_state'_def ct_in_state'_def) apply (drule(1) pred_tcb_at_conj') apply (subgoal_tac "st_tcb_at' (\<lambda>_. False) (ksCurThread s) s") apply (clarsimp) apply (erule_tac P="\<lambda>st. awaiting_reply' st \<and> activatable' st"
                      in pred_tcb'_weakenE) apply (case_tac st, clarsimp+) apply (wp threadSet_invs_trivial threadSet_st_tcb_at2 hoare_weak_lift_imp
                    | clarsimp simp add: inQ_def)+ apply (rule_tac Q="\<lambda>_. invs' and tcb_at' t
                                 and sch_act_simple and st_tcb_at' awaiting_reply' t"
                   in hoare_strengthen_post [rotated]) apply (clarsimp) apply (rule conjI) apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) apply (rule conjI) apply clarsimp apply (clarsimp simp: obj_at'_def idle_tcb'_def pred_tcb_at'_def) apply clarsimp apply (rule conjI) apply (clarsimp simp: invs'_def valid_state'_def valid_idle'_def) apply (erule pred_tcb'_weakenE, clarsimp) apply (rule conjI) apply (clarsimp simp : invs'_def valid_state'_def valid_idle'_def pred_tcb_at'_def
                                    obj_at'_def idle_tcb'_def) apply (rule conjI) apply clarsimp apply (frule invs'_not_runnable_not_queued) apply (erule pred_tcb'_weakenE, clarsimp) apply (frule (1) not_tcbQueued_not_ksQ) apply simp apply clarsimp apply (wp cteDeleteOne_reply_pred_tcb_at hoare_drop_imp hoare_allI)+ apply (clarsimp simp add: isReply_awaiting_reply' cte_wp_at_ctes_of) apply (auto dest!: st_tcb_idle'[rotated] simp:isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple\<rbrace> doReplyTransfer t' t slot grant \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple\<rbrace> do state <- getThreadState t;
y <- assert (isReply state);
x <- getCTE slot;
y <- assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
parentCap <- getSlotCap (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault t >>= case_option (do y <- doIPCTransfer t' None 0 grant t;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running t;
possibleSwitchTo t
od) (\<lambda>f. do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply f t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state. \<lbrace>st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)\<rbrace> do y <- assert (isReply state);
x <- getCTE slot;
y <- assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
parentCap <- getSlotCap (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault t >>= case_option (do y <- doIPCTransfer t' None 0 grant t;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running t;
possibleSwitchTo t
od) (\<lambda>f. do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply f t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state y. \<lbrace>\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state\<rbrace> do x <- getCTE slot;
y <- assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
parentCap <- getSlotCap (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault t >>= case_option (do y <- doIPCTransfer t' None 0 grant t;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running t;
possibleSwitchTo t
od) (\<lambda>f. do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply f t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>state y x. \<lbrace>cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)\<rbrace> do y <- assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer);
parentCap <- getSlotCap (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap parentCap \<and> capReplyMaster parentCap);
threadGet tcbFault t >>= case_option (do y <- doIPCTransfer t' None 0 grant t;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running t;
possibleSwitchTo t
od) (\<lambda>f. do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply f t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od)
od \<lbrace>\<lambda>rv. invs'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> do y <- doIPCTransfer t' None 0 grant t;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running t;
possibleSwitchTo t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>state y x ya parentCap yb xa yc yd. xa = None \<Longrightarrow> \<lbrace>?B36 state y x ya parentCap yb xa yc yd\<rbrace> setThreadState Structures_H.thread_state.Running t \<lbrace>\<lambda>ye s. invs' s \<and> st_tcb_at' runnable' t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>?B36 state y x ya parentCap yb xa yc\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>state y x ya parentCap yb xa yc yd. xa = None \<Longrightarrow> \<lbrace>?P'43 state y x ya parentCap yb xa yc yd\<rbrace> setThreadState Structures_H.thread_state.Running t \<lbrace>\<lambda>rv s. st_tcb_at' runnable' t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>yd s. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) and (\<lambda>s. runnable' Structures_H.thread_state.Running \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_not t s) and invs') s \<and> ?P'43 state y x ya parentCap yb xa yc yd s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>state x parentCap. \<lbrace>?P'43 state () x () parentCap () None () ()\<rbrace> setThreadState Structures_H.thread_state.Running t \<lbrace>\<lambda>rv s. st_tcb_at' runnable' t s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>yd s. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) and (\<lambda>s. runnable' Structures_H.thread_state.Running \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_not t s) and invs') s \<and> ?P'43 state y x ya parentCap yb xa yc yd s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>state x parentCap. \<lbrace>?P'48 state () x () parentCap () None () ()\<rbrace> setThreadState Structures_H.thread_state.Running t \<lbrace>\<lambda>rv s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t\<rbrace>
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>yd s. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) and (\<lambda>s. runnable' Structures_H.thread_state.Running \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_not t s) and invs') s \<and> (if t = t then K (runnable' Structures_H.thread_state.Running) else st_tcb_at' runnable' t) s \<and> ?P'48 state y x ya parentCap yb xa yc yd s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (8 subgoals):
 1. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>yd s. (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) and (\<lambda>s. runnable' Structures_H.thread_state.Running \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_not t s) and invs') s \<and> (if t = t then K (runnable' Structures_H.thread_state.Running) else st_tcb_at' runnable' t) s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 5. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 6. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 7. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 8. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>state y x ya parentCap yb xa yc rv s. \<lbrakk>xa = None; invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Running \<and> (Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Running \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Running) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Running) and (\<lambda>s. runnable' Structures_H.thread_state.Running \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Running \<longrightarrow> sch_act_not t s) and invs') s \<and> (if t = t then K (runnable' Structures_H.thread_state.Running) else st_tcb_at' runnable' t) s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<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) t s \<and> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> runnable') t s
 2. \<And>s. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' t s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<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) t s \<and> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 3. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 4. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 7. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 8. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 9. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 10. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' t s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<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) t s \<and> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' t s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (17 subgoals):
 1. \<And>s st x11 x12. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.BlockedOnReceive x11 x12\<rbrakk> \<Longrightarrow> runnable' st
 2. \<And>s st. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; awaiting_reply' st\<rbrakk> \<Longrightarrow> runnable' st
 3. \<And>s st x3. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> runnable' st
 4. \<And>s st. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> runnable' st
 5. \<And>s st. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> runnable' st
 6. \<And>s st. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; idle' st\<rbrakk> \<Longrightarrow> runnable' st
 7. \<And>s st x71 x72 x73 x74 x75. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> runnable' st
 8. \<And>s st. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> runnable' st
 9. \<And>s. \<lbrakk>invs' s; t \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' t s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t
 10. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
A total of 17 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>invs' s; ksCurThread s \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' (ksCurThread s) s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>ksCurThread s \<noteq> ksIdleThread s; st_tcb_at' awaiting_reply' (ksCurThread s) s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (10 subgoals):
 1. \<And>s. \<lbrakk>ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s; st_tcb_at' (\<lambda>_. False) (ksCurThread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>_. False) (ksCurThread s) s
 3. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 4. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 6. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 7. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 8. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 9. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 10. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s. \<lbrakk>ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>_. False) (ksCurThread s) s
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (9 subgoals):
 1. \<And>s st. \<lbrakk>ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; awaiting_reply' st \<and> activatable' st\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa yc. xa = None \<Longrightarrow> \<lbrace>?B35 state y x ya parentCap yb xa yc\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 3. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 5. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 6. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 7. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 8. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 9. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (8 subgoals):
 1. \<And>state x parentCap. \<lbrace>?B35 state () x () parentCap () None ()\<rbrace> cteDeleteOne slot \<lbrace>\<lambda>rv s. invs' s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s\<rbrace>
 2. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?R31 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>?B35 state y x ya parentCap yb xa\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> ?R31 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 5. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 6. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 7. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 8. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya parentCap yb xa. xa = None \<Longrightarrow> \<lbrace>?P'145 state y x ya parentCap yb xa\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>\<lambda>rv s. \<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> ?P'145 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (7 subgoals):
 1. \<And>state x parentCap. \<lbrace>?P'145 state () x () parentCap () None\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>\<lambda>rv s. \<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> ?P'145 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (8 subgoals):
 1. \<And>state x parentCap rv s. ((\<lambda>s. t \<noteq> ksIdleThread s) and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot) s \<Longrightarrow> \<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s
 2. \<And>state x parentCap. \<lbrace>?P'145 state () x () parentCap () None\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>\<lambda>_. (\<lambda>s. t \<noteq> ksIdleThread s) and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> ?P'145 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 5. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 6. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 7. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 8. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (7 subgoals):
 1. \<And>state x parentCap. \<lbrace>?P'145 state () x () parentCap () None\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>\<lambda>_. (\<lambda>s. t \<noteq> ksIdleThread s) and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> ?P'145 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (7 subgoals):
 1. \<And>state x parentCap. \<lbrace>?P'161 state () x () parentCap () (ds_id None)\<rbrace> doIPCTransfer t' None 0 grant t \<lbrace>\<lambda>rv. cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> ?P'161 state y x ya parentCap yb xa s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (8 subgoals):
 1. \<And>state x parentCap cap. ?P166 state x parentCap cap \<Longrightarrow> \<not> isUntypedCap cap
 2. \<And>state x parentCap rv s. cte_wp_at' (\<lambda>cte. ?P166 state x parentCap (cteCap cte) \<and> cteCap cte \<noteq> capability.NullCap) (?ptr169 state () x () parentCap () (ds_id None)) s \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot s
 3. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. ?P170 state y x ya parentCap yb xa cte \<and> cteCap cte \<noteq> capability.NullCap) (?ptr169 state y x ya parentCap yb xa) s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 5. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 6. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 7. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 8. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s
flex-flex pairs:
\<lambda>state x parentCap. ?P170 state () x () parentCap () (ds_id None) \<equiv>\<^sup>? \<lambda>state x parentCap cte. ?P166 state x parentCap (cteCap cte) proof (prove)
goal (8 subgoals):
 1. \<And>state x parentCap cap. \<lbrakk>?P173 state x parentCap cap; ?Q173 state x parentCap cap\<rbrakk> \<Longrightarrow> \<not> isUntypedCap cap
 2. \<And>state x parentCap rv s. cte_wp_at' (\<lambda>cte. (?P173 state x parentCap (cteCap cte) \<and> ?Q173 state x parentCap (cteCap cte)) \<and> cteCap cte \<noteq> capability.NullCap) (?ptr169 state () x () parentCap () (ds_id None)) s \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot s
 3. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 4. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (?P175 state y x ya parentCap yb xa cte \<and> ?Q174 state y x ya parentCap yb xa cte) \<and> cteCap cte \<noteq> capability.NullCap) (?ptr169 state y x ya parentCap yb xa) s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 5. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 6. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 7. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 8. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s
flex-flex pairs:
\<lambda>state x parentCap. ?P175 state () x () parentCap () (ds_id None) \<equiv>\<^sup>? \<lambda>state x parentCap cte. ?P173 state x parentCap (cteCap cte)
\<lambda>state x parentCap. ?Q174 state () x () parentCap () (ds_id None) \<equiv>\<^sup>? \<lambda>state x parentCap cte. ?Q173 state x parentCap (cteCap cte) proof (prove)
goal (7 subgoals):
 1. \<And>state x parentCap rv s. cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> ?Q173 state x parentCap (cteCap cte)) \<and> cteCap cte \<noteq> capability.NullCap) (?ptr169 state () x () parentCap () (ds_id None)) s \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot s
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> ?Q174 state y x ya parentCap yb xa cte) \<and> cteCap cte \<noteq> capability.NullCap) (?ptr169 state y x ya parentCap yb xa) s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s
flex-flex pairs:
\<lambda>state x parentCap. ?Q174 state () x () parentCap () (ds_id None) \<equiv>\<^sup>? \<lambda>state x parentCap cte. ?Q173 state x parentCap (cteCap cte) proof (prove)
goal (7 subgoals):
 1. \<And>state x parentCap rv s c. (\<not> isUntypedCap (cteCap c) \<and> ?Q173 state x parentCap (cteCap c)) \<and> cteCap c \<noteq> capability.NullCap \<Longrightarrow> \<exists>grant. cteCap c = capability.ReplyCap t False grant
 2. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 3. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> ?Q174 state y x ya parentCap yb xa cte) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 4. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 5. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 6. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 7. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s
flex-flex pairs:
\<lambda>state x parentCap. ?Q174 state () x () parentCap () (ds_id None) \<equiv>\<^sup>? \<lambda>state x parentCap cte. ?Q173 state x parentCap (cteCap cte) proof (prove)
goal (6 subgoals):
 1. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> do y <- cteDeleteOne slot;
tag <- getMessageInfo t';
sendBuffer <- lookupIPCBuffer False t';
mrs <- getMRs t' sendBuffer tag;
restart <- handleFaultReply x2 t (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) t;
if restart then do y <- setThreadState Structures_H.thread_state.Restart t;
possibleSwitchTo t
od else setThreadState Structures_H.thread_state.Inactive t
od \<lbrace>\<lambda>rv. invs'\<rbrace>
 2. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 3. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 4. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 5. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 6. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (12 subgoals):
 1. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. 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)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (\<not> runnable' Structures_H.thread_state.Restart \<longrightarrow> sch_act_not t s) \<and> invs' s \<and> (if t = t then K (runnable' Structures_H.thread_state.Restart) else st_tcb_at' runnable' t) s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart rv s. \<lbrakk>xa = Some x2; invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> 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)) t s \<and> (t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Restart) \<and> ((\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Restart) \<and> (runnable' Structures_H.thread_state.Restart \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (\<not> runnable' Structures_H.thread_state.Restart \<longrightarrow> sch_act_not t s) \<and> invs' s \<and> (if t = t then K (runnable' Structures_H.thread_state.Restart) else st_tcb_at' runnable' t) s \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; t \<noteq> ksIdleThread s\<rbrakk> \<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) t s \<and> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; t \<noteq> ksIdleThread s\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> runnable') t s
 2. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<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) t s \<and> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 9. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 10. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<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) t s \<and> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> (obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) \<and> (ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t)
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (21 subgoals):
 1. \<And>s st x11 x12. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.BlockedOnReceive x11 x12\<rbrakk> \<Longrightarrow> runnable' st
 2. \<And>s st. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; awaiting_reply' st\<rbrakk> \<Longrightarrow> runnable' st
 3. \<And>s st x3. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.BlockedOnNotification x3\<rbrakk> \<Longrightarrow> runnable' st
 4. \<And>s st. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.Running\<rbrakk> \<Longrightarrow> runnable' st
 5. \<And>s st. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> runnable' st
 6. \<And>s st. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; idle' st\<rbrakk> \<Longrightarrow> runnable' st
 7. \<And>s st x71 x72 x73 x74 x75. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.BlockedOnSend x71 x72 x73 x74 x75\<rbrakk> \<Longrightarrow> runnable' st
 8. \<And>s st. \<lbrakk>invs' s; sch_act_simple s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s; obj_at' tcbQueued t s; awaiting_reply' st; st = Structures_H.thread_state.Restart\<rbrakk> \<Longrightarrow> runnable' st
 9. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; t \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> t
 10. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
A total of 21 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>invs' s; sch_act_simple s; st_tcb_at' awaiting_reply' (ksCurThread s) s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; st_tcb_at' awaiting_reply' (ksCurThread s) s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s; st_tcb_at' (\<lambda>_. False) (ksCurThread s) s\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>sch_act_simple s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>_. False) (ksCurThread s) s
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 9. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 10. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s. \<lbrakk>sch_act_simple s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; st_tcb_at' (\<lambda>a. awaiting_reply' a \<and> activatable' a) (ksCurThread s) s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>_. False) (ksCurThread s) s
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>s st. \<lbrakk>sch_act_simple s; ksCurThread s \<noteq> ksIdleThread s; obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s; ksSchedulerAction s = ResumeCurrentThread; t = ksCurThread s; valid_pspace' s; st_tcb_at' activatable' (ksCurThread s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; awaiting_reply' st \<and> activatable' st\<rbrakk> \<Longrightarrow> False
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>state x parentCap x2 tag sendBuffer mrs restart. \<lbrace>?P'203 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. invs' s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart. xa = Some x2 \<Longrightarrow> \<lbrace>?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart\<rbrace> threadSet (tcbFault_update (\<lambda>_. None)) t \<lbrace>\<lambda>rv s. \<not> restart \<longrightarrow> (st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = tcb_st_refs_of' Structures_H.thread_state.Inactive \<and> (Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.Inactive \<and> Structures_H.thread_state.Inactive \<noteq> Structures_H.thread_state.IdleThreadState \<longrightarrow> st' \<noteq> Structures_H.thread_state.Inactive \<and> st' \<noteq> Structures_H.thread_state.IdleThreadState)) t and (\<lambda>s. t = ksIdleThread s \<longrightarrow> idle' Structures_H.thread_state.Inactive) and (\<lambda>s. (\<exists>p. t \<in> set (ksReadyQueues s p)) \<longrightarrow> runnable' Structures_H.thread_state.Inactive) and (\<lambda>s. runnable' Structures_H.thread_state.Inactive \<and> obj_at' tcbQueued t s \<longrightarrow> st_tcb_at' runnable' t s) and (\<lambda>s. \<not> runnable' Structures_H.thread_state.Inactive \<longrightarrow> sch_act_not t s) and invs') s\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer mrs. xa = Some x2 \<Longrightarrow> \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> ?P'203 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s) \<and> ?P'202 state y x ya parentCap yb xa x2 yc tag sendBuffer mrs restart s\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>restart s. (restart \<longrightarrow> invs' s \<and> tcb_at' t s \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))) \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s) \<and> (\<not> restart \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not t s \<and> invs' s \<and> tcb_at' t s \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))))\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 6. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 7. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 8. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 9. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 10. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (11 subgoals):
 1. \<And>state x parentCap x2 tag sendBuffer mrs rv s. (invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t) s \<Longrightarrow> (rv \<longrightarrow> invs' s \<and> tcb_at' t s \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))) \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s) \<and> (\<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> sch_act_not t s \<and> invs' s \<and> tcb_at' t s \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> (rv \<longrightarrow> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))) \<and> t \<noteq> ksIdleThread s) \<and> (\<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> rv \<longrightarrow> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))) \<and> t \<noteq> ksIdleThread s
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> \<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv\<rbrakk> \<Longrightarrow> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))) \<and> t \<noteq> idle_thread_ptr
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> \<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv s. \<lbrakk>tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 2. \<And>rv s. \<lbrakk>tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread_ptr
 3. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> \<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 4. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s; rv\<rbrakk> \<Longrightarrow> t \<noteq> idle_thread_ptr
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> \<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s\<rbrakk> \<Longrightarrow> \<not> rv \<longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s \<and> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; obj_at' idle_tcb' idle_thread_ptr s; idle_thread_ptr = ksIdleThread s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; valid_machine_state' s; irqs_masked' s; valid_queues' s; ct_not_inQ s; ct_idle_or_in_cur_domain' s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; cur_tcb' s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st'. tcb_st_refs_of' st' = {}) t s
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> t \<noteq> ksIdleThread s \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> t \<noteq> ksIdleThread s
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b))) \<and> (\<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>a b. t \<notin> set (ksReadyQueues s (a, b))
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s a b. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv; t \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> False
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>rv s a b. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv; t \<in> set (ksReadyQueues s (a, b))\<rbrakk> \<Longrightarrow> st_tcb_at' (Not \<circ> runnable') (?t512 rv s a b) s
 2. \<And>rv s a b. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv; t \<in> set (ksReadyQueues s (a, b)); obj_at' (Not \<circ> tcbQueued) (?t512 rv s a b) s\<rbrakk> \<Longrightarrow> False
 3. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 4. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 8. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 9. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 10. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
A total of 13 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s a b. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv; t \<in> set (ksReadyQueues s (a, b)); obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> False
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>rv s a b. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv; t \<in> set (ksReadyQueues s (a, b)); obj_at' (Not \<circ> tcbQueued) t s; \<forall>d p. t \<notin> set (ksReadyQueues s (d, p))\<rbrakk> \<Longrightarrow> False
 2. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 3. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 7. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 8. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 9. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 10. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>rv s. \<lbrakk>invs' s; tcb_at' t s; sch_act_simple s; st_tcb_at' awaiting_reply' t s; \<not> rv\<rbrakk> \<Longrightarrow> \<forall>d p. (\<exists>tcb. tcbQueued tcb \<and> tcbPriority tcb = p \<and> tcbDomain tcb = d \<and> (tcbQueued tcb \<longrightarrow> tcbDomain tcb \<noteq> d)) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
 2. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 6. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 7. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 8. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 9. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 10. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>state x parentCap x2 tag sendBuffer mrs. \<lbrace>?B188 state () x () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 t (msgLabel tag) mrs \<lbrace>\<lambda>_. invs' and tcb_at' t and sch_act_simple and st_tcb_at' awaiting_reply' t\<rbrace>
 2. \<And>state y x ya parentCap yb xa x2 yc tag sendBuffer. xa = Some x2 \<Longrightarrow> \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace> getMRs t' sendBuffer tag \<lbrace>?B188 state y x ya parentCap yb xa x2 yc tag sendBuffer\<rbrace>
 3. \<And>state y x ya parentCap yb xa x2 yc tag. xa = Some x2 \<Longrightarrow> \<lbrace>?B186 state y x ya parentCap yb xa x2 yc tag\<rbrace> lookupIPCBuffer False t' \<lbrace>?B187 state y x ya parentCap yb xa x2 yc tag\<rbrace>
 4. \<And>state y x ya parentCap yb xa x2 yc. xa = Some x2 \<Longrightarrow> \<lbrace>?B185 state y x ya parentCap yb xa x2 yc\<rbrace> getMessageInfo t' \<lbrace>?B186 state y x ya parentCap yb xa x2 yc\<rbrace>
 5. \<And>state y x ya parentCap yb xa x2. xa = Some x2 \<Longrightarrow> \<lbrace>?R32 state y x ya parentCap yb xa x2\<rbrace> cteDeleteOne slot \<lbrace>?B185 state y x ya parentCap yb xa x2\<rbrace>
 6. \<And>state y x ya parentCap yb. \<lbrace>?B21 state y x ya parentCap yb\<rbrace> threadGet tcbFault t \<lbrace>\<lambda>xa s. (xa = None \<longrightarrow> (invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> (\<forall>xb. xa = Some xb \<longrightarrow> ?R32 state y x ya parentCap yb xa xb s)\<rbrace>
 7. \<And>state y x ya parentCap. \<lbrace>?B20 state y x ya parentCap\<rbrace> assert (isReplyCap parentCap \<and> capReplyMaster parentCap) \<lbrace>?B21 state y x ya parentCap\<rbrace>
 8. \<And>state y x ya. \<lbrace>?B19 state y x ya\<rbrace> getSlotCap (mdbPrev (cteMDBNode x)) \<lbrace>?B20 state y x ya\<rbrace>
 9. \<And>state y x. \<lbrace>?Q18 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer) \<lbrace>?B19 state y x\<rbrace>
 10. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> ?Q18 state y x s proof (prove)
goal (1 subgoal):
 1. \<And>state y x s. (cte_wp_at' (\<lambda>c. c = x) slot and (\<lambda>s. (st_tcb_at' (\<lambda>st. st = state) t and (tcb_at' t and tcb_at' t' and cte_wp_at' (\<lambda>cte. \<exists>grant. cteCap cte = capability.ReplyCap t False grant) slot and invs' and sch_act_simple)) s \<and> isReply state)) s \<Longrightarrow> mdbPrev (cteMDBNode x) \<noteq> nullPointer \<and> mdbNext (cteMDBNode x) = nullPointer \<longrightarrow> ((invs' and tcb_at' t' and tcb_at' t) s \<and> t \<noteq> ksIdleThread s \<and> st_tcb_at' awaiting_reply' t s \<and> t \<noteq> ksIdleThread s \<and> cte_wp_at' (\<lambda>cte. (\<not> isUntypedCap (cteCap cte) \<and> (\<exists>grant. cteCap cte = capability.ReplyCap t False grant)) \<and> cteCap cte \<noteq> capability.NullCap) slot s) \<and> invs' s \<and> tcb_at' t s \<and> tcb_at' t s \<and> sch_act_simple s \<and> st_tcb_at' awaiting_reply' t s \<and> (\<exists>t' r. cte_wp_at' (\<lambda>cte. cteCap cte = capability.ReplyCap t' False r) slot s) proof (prove)
goal (1 subgoal):
 1. \<And>x s grant. \<lbrakk>st_tcb_at' awaiting_reply' (ksIdleThread s) s; tcb_at' (ksIdleThread s) s; tcb_at' t' s; invs' s; sch_act_simple s; ctes_of s slot = Some x; cteCap x = capability.ReplyCap (ksIdleThread s) False grant; mdbPrev (cteMDBNode x) \<noteq> nullPointer; mdbNext (cteMDBNode x) = nullPointer; t = ksIdleThread s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!