theory Fastpath_Equiv

lemma doReplyTransfer_simple:
  "monadic_rewrite True False
     (obj_at' (\<lambda>tcb. tcbFault tcb = None) receiver)
     (doReplyTransfer sender receiver slot grant)
     (do state \<leftarrow> getThreadState receiver;
         assert (isReply state);
         cte \<leftarrow> getCTE slot;
         mdbnode \<leftarrow> return $ cteMDBNode cte;
         assert (mdbPrev mdbnode \<noteq> 0 \<and> mdbNext mdbnode = 0);
         parentCTE \<leftarrow> getCTE (mdbPrev mdbnode);
         assert (isReplyCap (cteCap parentCTE) \<and> capReplyMaster (cteCap parentCTE));
         doIPCTransfer sender Nothing 0 grant receiver;
         cteDeleteOne slot;
         setThreadState Running receiver;
         possibleSwitchTo receiver
         od)" apply (simp add: doReplyTransfer_def liftM_def nullPointer_def getSlotCap_def) apply (rule monadic_rewrite_bind_tail)+ apply (monadic_rewrite_symb_exec_l_known None, simp) apply (rule monadic_rewrite_refl) apply (wpsimp wp: threadGet_const gts_wp' getCTE_wp' simp: o_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (obj_at' (\<lambda>tcb. tcbFault tcb = None) receiver) (doReplyTransfer sender receiver slot grant) (do state <- getThreadState receiver;
assert (isReply state);
cte <- getCTE slot;
mdbnode <- return $ cteMDBNode cte;
assert (mdbPrev mdbnode \<noteq> 0 \<and> mdbNext mdbnode = 0);
parentCTE <- getCTE (mdbPrev mdbnode);
assert (isReplyCap (cteCap parentCTE) \<and> capReplyMaster (cteCap parentCTE));
doIPCTransfer sender Nothing 0 grant receiver;
cteDeleteOne slot;
setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True False (obj_at' (\<lambda>tcb. tcbFault tcb = None) receiver) (do state <- getThreadState receiver;
y <- assert (isReply state);
x <- getCTE slot;
y <- assert (mdbPrev (cteMDBNode x) \<noteq> 0 \<and> mdbNext (cteMDBNode x) = 0);
cte <- getCTE (mdbPrev (cteMDBNode x));
y <- assert (isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte));
threadGet tcbFault receiver >>= case_option (do y <- doIPCTransfer sender None 0 grant receiver;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od) (\<lambda>f. do y <- cteDeleteOne slot;
tag <- getMessageInfo sender;
sendBuffer <- lookupIPCBuffer False sender;
mrs <- getMRs sender sendBuffer tag;
restart <- handleFaultReply f receiver (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) receiver;
if restart then do y <- setThreadState Structures_H.thread_state.Restart receiver;
possibleSwitchTo receiver
od else setThreadState Structures_H.thread_state.Inactive receiver
od)
od) (do state <- getThreadState receiver;
y <- assert (isReply state);
cte <- getCTE slot;
y <- assert (mdbPrev (cteMDBNode cte) \<noteq> 0 \<and> mdbNext (cteMDBNode cte) = 0);
parentCTE <- getCTE (mdbPrev (cteMDBNode cte));
y <- assert (isReplyCap (cteCap parentCTE) \<and> capReplyMaster (cteCap parentCTE));
y <- doIPCTransfer sender None 0 grant receiver;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od) proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya cte yb. monadic_rewrite True False (?Q21 state y x ya cte yb) (threadGet tcbFault receiver >>= case_option (do y <- doIPCTransfer sender None 0 grant receiver;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od) (\<lambda>f. do y <- cteDeleteOne slot;
tag <- getMessageInfo sender;
sendBuffer <- lookupIPCBuffer False sender;
mrs <- getMRs sender sendBuffer tag;
restart <- handleFaultReply f receiver (msgLabel tag) mrs;
y <- threadSet (tcbFault_update (\<lambda>_. None)) receiver;
if restart then do y <- setThreadState Structures_H.thread_state.Restart receiver;
possibleSwitchTo receiver
od else setThreadState Structures_H.thread_state.Inactive receiver
od)) (do y <- doIPCTransfer sender None 0 grant receiver;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od)
 2. \<And>state y x ya cte. \<lbrace>?Q18 state y x ya cte\<rbrace> assert (isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) \<lbrace>?Q21 state y x ya cte\<rbrace>
 3. \<And>state y x ya. \<lbrace>?Q15 state y x ya\<rbrace> getCTE (mdbPrev (cteMDBNode x)) \<lbrace>?Q18 state y x ya\<rbrace>
 4. \<And>state y x. \<lbrace>?Q12 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> 0 \<and> mdbNext (cteMDBNode x) = 0) \<lbrace>?Q15 state y x\<rbrace>
 5. \<And>state y. \<lbrace>?Q9 state y\<rbrace> getCTE slot \<lbrace>?Q12 state y\<rbrace>
 6. \<And>state. \<lbrace>?Q6 state\<rbrace> assert (isReply state) \<lbrace>?Q9 state\<rbrace>
 7. \<lbrace>obj_at' (\<lambda>tcb. tcbFault tcb = None) receiver\<rbrace> getThreadState receiver \<lbrace>?Q6\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>state x cte. monadic_rewrite True False (?Q25 state () x () cte ()) (do y <- doIPCTransfer sender None 0 grant receiver;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od) (do y <- doIPCTransfer sender None 0 grant receiver;
y <- cteDeleteOne slot;
y <- setThreadState Structures_H.thread_state.Running receiver;
possibleSwitchTo receiver
od)
 2. \<And>state y x ya cte yb. \<lbrace>?P25 state y x ya cte yb\<rbrace> threadGet tcbFault receiver \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 3. \<And>state y x ya cte. \<lbrace>?Q18 state y x ya cte\<rbrace> assert (isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) \<lbrace>\<lambda>yb. ?P25 state y x ya cte yb and ?Q25 state y x ya cte yb\<rbrace>
 4. \<And>state y x ya. \<lbrace>?Q15 state y x ya\<rbrace> getCTE (mdbPrev (cteMDBNode x)) \<lbrace>?Q18 state y x ya\<rbrace>
 5. \<And>state y x. \<lbrace>?Q12 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> 0 \<and> mdbNext (cteMDBNode x) = 0) \<lbrace>?Q15 state y x\<rbrace>
 6. \<And>state y. \<lbrace>?Q9 state y\<rbrace> getCTE slot \<lbrace>?Q12 state y\<rbrace>
 7. \<And>state. \<lbrace>?Q6 state\<rbrace> assert (isReply state) \<lbrace>?Q9 state\<rbrace>
 8. \<lbrace>obj_at' (\<lambda>tcb. tcbFault tcb = None) receiver\<rbrace> getThreadState receiver \<lbrace>?Q6\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>state y x ya cte yb. \<lbrace>?P25 state y x ya cte yb\<rbrace> threadGet tcbFault receiver \<lbrace>\<lambda>rv' _. rv' = None\<rbrace>
 2. \<And>state y x ya cte. \<lbrace>?Q18 state y x ya cte\<rbrace> assert (isReplyCap (cteCap cte) \<and> capReplyMaster (cteCap cte)) \<lbrace>\<lambda>yb. ?P25 state y x ya cte yb and (\<lambda>a. True)\<rbrace>
 3. \<And>state y x ya. \<lbrace>?Q15 state y x ya\<rbrace> getCTE (mdbPrev (cteMDBNode x)) \<lbrace>?Q18 state y x ya\<rbrace>
 4. \<And>state y x. \<lbrace>?Q12 state y x\<rbrace> assert (mdbPrev (cteMDBNode x) \<noteq> 0 \<and> mdbNext (cteMDBNode x) = 0) \<lbrace>?Q15 state y x\<rbrace>
 5. \<And>state y. \<lbrace>?Q9 state y\<rbrace> getCTE slot \<lbrace>?Q12 state y\<rbrace>
 6. \<And>state. \<lbrace>?Q6 state\<rbrace> assert (isReply state) \<lbrace>?Q9 state\<rbrace>
 7. \<lbrace>obj_at' (\<lambda>tcb. tcbFault tcb = None) receiver\<rbrace> getThreadState receiver \<lbrace>?Q6\<rbrace> proof (prove)
goal:
No subgoals!