theory Orphanage

lemma doReplyTransfer_no_orphans[wp]:
  "\<lbrace>no_orphans and invs' and tcb_at' sender and tcb_at' receiver\<rbrace>
   doReplyTransfer sender receiver slot grant
   \<lbrace>\<lambda>rv. no_orphans\<rbrace>" unfolding doReplyTransfer_def apply (wp sts_st_tcb' setThreadState_not_active_no_orphans threadSet_no_orphans
            threadSet_valid_queues' threadSet_weak_sch_act_wf
         | wpc | clarsimp simp: is_active_thread_state_def isRunning_def isRestart_def
         | wp (once) hoare_drop_imps
         | strengthen sch_act_wf_weak invs_valid_queues')+ apply (rule_tac Q="\<lambda>rv. invs' and no_orphans" in hoare_post_imp) apply (fastforce simp: inQ_def) apply (wp hoare_drop_imps | clarsimp)+ apply (clarsimp simp:invs'_def valid_state'_def valid_pspace'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans and invs' and tcb_at' sender and tcb_at' receiver\<rbrace> doReplyTransfer sender receiver slot grant \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>no_orphans and invs' and tcb_at' sender and tcb_at' receiver\<rbrace> do state <- getThreadState receiver;
haskell_assert (isReply state) [];
mdbNode <- liftM cteMDBNode $ getCTE slot;
haskell_assert (mdbPrev mdbNode \<noteq> nullPointer \<and> mdbNext mdbNode = nullPointer) [];
parentCap <- getSlotCap (mdbPrev mdbNode);
haskell_assert (isReplyCap parentCap \<and> capReplyMaster parentCap) [];
fault <- threadGet tcbFault receiver;
case fault of None \<Rightarrow> do doIPCTransfer sender Nothing 0 grant receiver;
cteDeleteOne slot;
setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od | Some f \<Rightarrow> do cteDeleteOne slot;
tag <- getMessageInfo sender;
sendBuffer <- lookupIPCBuffer False sender;
mrs <- getMRs sender sendBuffer tag;
restart <- handleFaultReply f receiver (msgLabel tag) mrs;
threadSet (tcbFault_update (\<lambda>_. Nothing)) receiver;
if restart then do setThreadState Structures_H.thread_state.Restart receiver;
possibleSwitchTo receiver
od else setThreadState Structures_H.thread_state.Inactive receiver
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (13 subgoals):
 1. \<And>state mdbNode parentCap x2 tag sendBuffer mrs. \<lbrace>?P'146 state () mdbNode () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 receiver (msgLabel tag) mrs \<lbrace>\<lambda>r s. (\<forall>ko qdom prio. ko_at' ko receiver s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. None) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> receiver \<in> set (ksReadyQueues s (qdom, prio))) \<and> invs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> no_orphans s \<and> (\<forall>ko qdom prio. ko_at' ko receiver s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. None) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> receiver \<in> set (ksReadyQueues s (qdom, prio))) \<and> invs' s\<rbrace>
 2. \<And>state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer. fault = Some x2 \<Longrightarrow> \<lbrace>?B92 state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer\<rbrace> getMRs sender sendBuffer tag \<lbrace>\<lambda>mrs s. no_orphans s \<and> ?P'146 state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer mrs s\<rbrace>
 3. \<And>state x mdbNode xa parentCap xb fault x2 xc tag. fault = Some x2 \<Longrightarrow> \<lbrace>?B91 state x mdbNode xa parentCap xb fault x2 xc tag\<rbrace> lookupIPCBuffer False sender \<lbrace>?B92 state x mdbNode xa parentCap xb fault x2 xc tag\<rbrace>
 4. \<And>state x mdbNode xa parentCap xb fault x2 xc. fault = Some x2 \<Longrightarrow> \<lbrace>?B89 state x mdbNode xa parentCap xb fault x2 xc\<rbrace> getMessageInfo sender \<lbrace>?B91 state x mdbNode xa parentCap xb fault x2 xc\<rbrace>
 5. \<And>state x mdbNode xa parentCap xb fault x2. fault = Some x2 \<Longrightarrow> \<lbrace>?R20 state x mdbNode xa parentCap xb fault x2\<rbrace> cteDeleteOne slot \<lbrace>?B89 state x mdbNode xa parentCap xb fault x2\<rbrace>
 6. \<And>state x mdbNode xa parentCap xb. \<lbrace>?B8 state x mdbNode xa parentCap xb\<rbrace> threadGet tcbFault receiver \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> (valid_objs' and valid_mdb') s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (invs' and tcb_at' sender and tcb_at' receiver) s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>xc. fault = Some xc \<longrightarrow> ?R20 state x mdbNode xa parentCap xb fault xc s)\<rbrace>
 7. \<And>state x mdbNode xa parentCap. \<lbrace>?B7 state x mdbNode xa parentCap\<rbrace> haskell_assert (isReplyCap parentCap \<and> capReplyMaster parentCap) [] \<lbrace>?B8 state x mdbNode xa parentCap\<rbrace>
 8. \<And>state x mdbNode xa. \<lbrace>?B5 state x mdbNode xa\<rbrace> getSlotCap (mdbPrev mdbNode) \<lbrace>?B7 state x mdbNode xa\<rbrace>
 9. \<And>state x mdbNode. \<lbrace>?B4 state x mdbNode\<rbrace> haskell_assert (mdbPrev mdbNode \<noteq> nullPointer \<and> mdbNext mdbNode = nullPointer) [] \<lbrace>?B5 state x mdbNode\<rbrace>
 10. \<And>state x. \<lbrace>?B2 state x\<rbrace> liftM cteMDBNode $ getCTE slot \<lbrace>?B4 state x\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>state mdbNode parentCap x2 tag sendBuffer mrs rv s. (invs' and no_orphans) s \<Longrightarrow> (\<forall>ko qdom prio. ko_at' ko receiver s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. None) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> receiver \<in> set (ksReadyQueues s (qdom, prio))) \<and> invs' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> no_orphans s \<and> (\<forall>ko qdom prio. ko_at' ko receiver s \<and> inQ qdom prio (tcbFault_update (\<lambda>_. None) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> receiver \<in> set (ksReadyQueues s (qdom, prio))) \<and> invs' s
 2. \<And>state mdbNode parentCap x2 tag sendBuffer mrs. \<lbrace>?P'146 state () mdbNode () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 receiver (msgLabel tag) mrs \<lbrace>\<lambda>rv. invs' and no_orphans\<rbrace>
 3. \<And>state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer. fault = Some x2 \<Longrightarrow> \<lbrace>?B92 state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer\<rbrace> getMRs sender sendBuffer tag \<lbrace>\<lambda>mrs s. no_orphans s \<and> ?P'146 state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer mrs s\<rbrace>
 4. \<And>state x mdbNode xa parentCap xb fault x2 xc tag. fault = Some x2 \<Longrightarrow> \<lbrace>?B91 state x mdbNode xa parentCap xb fault x2 xc tag\<rbrace> lookupIPCBuffer False sender \<lbrace>?B92 state x mdbNode xa parentCap xb fault x2 xc tag\<rbrace>
 5. \<And>state x mdbNode xa parentCap xb fault x2 xc. fault = Some x2 \<Longrightarrow> \<lbrace>?B89 state x mdbNode xa parentCap xb fault x2 xc\<rbrace> getMessageInfo sender \<lbrace>?B91 state x mdbNode xa parentCap xb fault x2 xc\<rbrace>
 6. \<And>state x mdbNode xa parentCap xb fault x2. fault = Some x2 \<Longrightarrow> \<lbrace>?R20 state x mdbNode xa parentCap xb fault x2\<rbrace> cteDeleteOne slot \<lbrace>?B89 state x mdbNode xa parentCap xb fault x2\<rbrace>
 7. \<And>state x mdbNode xa parentCap xb. \<lbrace>?B8 state x mdbNode xa parentCap xb\<rbrace> threadGet tcbFault receiver \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> (valid_objs' and valid_mdb') s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (invs' and tcb_at' sender and tcb_at' receiver) s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>xc. fault = Some xc \<longrightarrow> ?R20 state x mdbNode xa parentCap xb fault xc s)\<rbrace>
 8. \<And>state x mdbNode xa parentCap. \<lbrace>?B7 state x mdbNode xa parentCap\<rbrace> haskell_assert (isReplyCap parentCap \<and> capReplyMaster parentCap) [] \<lbrace>?B8 state x mdbNode xa parentCap\<rbrace>
 9. \<And>state x mdbNode xa. \<lbrace>?B5 state x mdbNode xa\<rbrace> getSlotCap (mdbPrev mdbNode) \<lbrace>?B7 state x mdbNode xa\<rbrace>
 10. \<And>state x mdbNode. \<lbrace>?B4 state x mdbNode\<rbrace> haskell_assert (mdbPrev mdbNode \<noteq> nullPointer \<and> mdbNext mdbNode = nullPointer) [] \<lbrace>?B5 state x mdbNode\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>state mdbNode parentCap x2 tag sendBuffer mrs. \<lbrace>?P'146 state () mdbNode () parentCap () (Some x2) x2 () tag sendBuffer mrs\<rbrace> handleFaultReply x2 receiver (msgLabel tag) mrs \<lbrace>\<lambda>rv. invs' and no_orphans\<rbrace>
 2. \<And>state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer. fault = Some x2 \<Longrightarrow> \<lbrace>?B92 state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer\<rbrace> getMRs sender sendBuffer tag \<lbrace>\<lambda>mrs s. no_orphans s \<and> ?P'146 state x mdbNode xa parentCap xb fault x2 xc tag sendBuffer mrs s\<rbrace>
 3. \<And>state x mdbNode xa parentCap xb fault x2 xc tag. fault = Some x2 \<Longrightarrow> \<lbrace>?B91 state x mdbNode xa parentCap xb fault x2 xc tag\<rbrace> lookupIPCBuffer False sender \<lbrace>?B92 state x mdbNode xa parentCap xb fault x2 xc tag\<rbrace>
 4. \<And>state x mdbNode xa parentCap xb fault x2 xc. fault = Some x2 \<Longrightarrow> \<lbrace>?B89 state x mdbNode xa parentCap xb fault x2 xc\<rbrace> getMessageInfo sender \<lbrace>?B91 state x mdbNode xa parentCap xb fault x2 xc\<rbrace>
 5. \<And>state x mdbNode xa parentCap xb fault x2. fault = Some x2 \<Longrightarrow> \<lbrace>?R20 state x mdbNode xa parentCap xb fault x2\<rbrace> cteDeleteOne slot \<lbrace>?B89 state x mdbNode xa parentCap xb fault x2\<rbrace>
 6. \<And>state x mdbNode xa parentCap xb. \<lbrace>?B8 state x mdbNode xa parentCap xb\<rbrace> threadGet tcbFault receiver \<lbrace>\<lambda>fault s. (fault = None \<longrightarrow> no_orphans s \<and> valid_queues' s \<and> (valid_objs' and valid_mdb') s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> (invs' and tcb_at' sender and tcb_at' receiver) s \<and> sch_act_wf (ksSchedulerAction s) s) \<and> (\<forall>xc. fault = Some xc \<longrightarrow> ?R20 state x mdbNode xa parentCap xb fault xc s)\<rbrace>
 7. \<And>state x mdbNode xa parentCap. \<lbrace>?B7 state x mdbNode xa parentCap\<rbrace> haskell_assert (isReplyCap parentCap \<and> capReplyMaster parentCap) [] \<lbrace>?B8 state x mdbNode xa parentCap\<rbrace>
 8. \<And>state x mdbNode xa. \<lbrace>?B5 state x mdbNode xa\<rbrace> getSlotCap (mdbPrev mdbNode) \<lbrace>?B7 state x mdbNode xa\<rbrace>
 9. \<And>state x mdbNode. \<lbrace>?B4 state x mdbNode\<rbrace> haskell_assert (mdbPrev mdbNode \<noteq> nullPointer \<and> mdbNext mdbNode = nullPointer) [] \<lbrace>?B5 state x mdbNode\<rbrace>
 10. \<And>state x. \<lbrace>?B2 state x\<rbrace> liftM cteMDBNode $ getCTE slot \<lbrace>?B4 state x\<rbrace>
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; tcb_at' sender s; tcb_at' receiver s\<rbrakk> \<Longrightarrow> valid_queues' s \<and> valid_objs' s \<and> valid_mdb' s \<and> valid_queues' s \<and> sch_act_wf (ksSchedulerAction s) s \<and> valid_queues' s \<and> valid_objs' s \<and> valid_queues' s \<and> valid_objs' s proof (prove)
goal:
No subgoals!