theory IsolatedThreadAction

lemma setupCallerCap_rewrite:
  "monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s))
   (setupCallerCap send rcv canGrant)
   (do setThreadState BlockedOnReply send;
       replySlot \<leftarrow> getThreadReplySlot send;
       callerSlot \<leftarrow> getThreadCallerSlot rcv;
       replySlotCTE \<leftarrow> getCTE replySlot;
       assert (mdbNext (cteMDBNode replySlotCTE) = 0
                 \<and> isReplyCap (cteCap replySlotCTE)
                 \<and> capReplyMaster (cteCap replySlotCTE)
                 \<and> mdbFirstBadged (cteMDBNode replySlotCTE)
                 \<and> mdbRevocable (cteMDBNode replySlotCTE));
       cteInsert (ReplyCap send False canGrant) replySlot callerSlot
    od)" apply (simp add: setupCallerCap_def getThreadCallerSlot_def
                   getThreadReplySlot_def locateSlot_conv
                   getSlotCap_def) apply (rule monadic_rewrite_bind_tail)+ apply (rule monadic_rewrite_assert)+ apply (rule_tac P="mdbFirstBadged (cteMDBNode masterCTE)
                       \<and> mdbRevocable (cteMDBNode masterCTE)"
                in monadic_rewrite_gen_asm) apply (rule monadic_rewrite_trans) apply monadic_rewrite_symb_exec_l apply monadic_rewrite_symb_exec_l_drop apply (rule monadic_rewrite_refl) apply wpsimp+ apply (rule monadic_rewrite_refl) apply (wpsimp wp: getCTE_wp' simp: cte_wp_at_ctes_of)+ apply (fastforce simp: reply_masters_rvk_fb_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) (setupCallerCap send rcv canGrant) (do setThreadState Structures_H.thread_state.BlockedOnReply send;
replySlot <- getThreadReplySlot send;
callerSlot <- getThreadCallerSlot rcv;
replySlotCTE <- getCTE replySlot;
assert (mdbNext (cteMDBNode replySlotCTE) = 0 \<and> isReplyCap (cteCap replySlotCTE) \<and> capReplyMaster (cteCap replySlotCTE) \<and> mdbFirstBadged (cteMDBNode replySlotCTE) \<and> mdbRevocable (cteMDBNode replySlotCTE));
cteInsert (capability.ReplyCap send False canGrant) replySlot callerSlot
od) proof (prove)
goal (1 subgoal):
 1. monadic_rewrite True True (\<lambda>s. reply_masters_rvk_fb (ctes_of s)) (do y <- setThreadState Structures_H.thread_state.BlockedOnReply send;
masterCTE <- getCTE (send + 2 ^ cte_level_bits * tcbReplySlot);
y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
cte <- getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) (do y <- setThreadState Structures_H.thread_state.BlockedOnReply send;
replySlotCTE <- getCTE (send + 2 ^ cte_level_bits * tcbReplySlot);
y <- assert (mdbNext (cteMDBNode replySlotCTE) = 0 \<and> isReplyCap (cteCap replySlotCTE) \<and> capReplyMaster (cteCap replySlotCTE) \<and> mdbFirstBadged (cteMDBNode replySlotCTE) \<and> mdbRevocable (cteMDBNode replySlotCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) proof (prove)
goal (3 subgoals):
 1. \<And>y masterCTE. monadic_rewrite True True (?Q4 y masterCTE) (do y <- assert (isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send);
y <- assert (mdbNext (cteMDBNode masterCTE) = nullPointer);
cte <- getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>?Q4 y\<rbrace>
 3. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?P9 y masterCTE) (do cte <- getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ?P9 y masterCTE s\<rbrace>
 3. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q11 y masterCTE) (do cte <- getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 2. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and ?Q11 y masterCTE) s\<rbrace>
 3. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?P12 y masterCTE) (do cte <- getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot);
y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) (?g12 y masterCTE)
 2. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q12 y masterCTE) (?g12 y masterCTE) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 3. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and (?P12 y masterCTE and ?Q12 y masterCTE)) s\<rbrace>
 4. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y masterCTE cte. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q16 y masterCTE cte) (do y <- assert (cteCap cte = capability.NullCap);
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od) (?g12 y masterCTE)
 2. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> \<lbrace>?P12 y masterCTE\<rbrace> getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q16 y masterCTE\<rbrace>
 3. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q12 y masterCTE) (?g12 y masterCTE) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 4. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and (?P12 y masterCTE and ?Q12 y masterCTE)) s\<rbrace>
 5. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>y masterCTE cte. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q16 y masterCTE cte) (cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)) (?g12 y masterCTE)
 2. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> \<lbrace>?P12 y masterCTE\<rbrace> getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>?Q16 y masterCTE\<rbrace>
 3. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q12 y masterCTE) (?g12 y masterCTE) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 4. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and (?P12 y masterCTE and ?Q12 y masterCTE)) s\<rbrace>
 5. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> \<lbrace>?P12 y masterCTE\<rbrace> getCTE (rcv + 2 ^ cte_level_bits * tcbCallerSlot) \<lbrace>\<lambda>cte _. True\<rbrace>
 2. \<And>y masterCTE. \<lbrakk>isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send; mdbNext (cteMDBNode masterCTE) = nullPointer; mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q12 y masterCTE) (cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)) (do y <- assert (mdbNext (cteMDBNode masterCTE) = 0 \<and> isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE));
cteInsert (capability.ReplyCap send False canGrant) (send + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)
od)
 3. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and (?P12 y masterCTE and ?Q12 y masterCTE)) s\<rbrace>
 4. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>masterCTE. \<lbrakk>mdbNext (cteMDBNode masterCTE) = nullPointer; isReplyCap (cteCap masterCTE); mdbFirstBadged (cteMDBNode masterCTE); mdbRevocable (cteMDBNode masterCTE); capReplyMaster (cteCap masterCTE); send = capTCBPtr (cteCap masterCTE)\<rbrakk> \<Longrightarrow> monadic_rewrite True True (?Q12 () masterCTE) (cteInsert (capability.ReplyCap (capTCBPtr (cteCap masterCTE)) False canGrant) (capTCBPtr (cteCap masterCTE) + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot)) (cteInsert (capability.ReplyCap (capTCBPtr (cteCap masterCTE)) False canGrant) (capTCBPtr (cteCap masterCTE) + 2 ^ cte_level_bits * tcbReplySlot) (rcv + 2 ^ cte_level_bits * tcbCallerSlot))
 2. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and ((\<lambda>_. True) and ?Q12 y masterCTE)) s\<rbrace>
 3. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>y. \<lbrace>?Q1 y\<rbrace> getCTE (send + 2 ^ cte_level_bits * tcbReplySlot) \<lbrace>\<lambda>masterCTE s. isReplyCap (cteCap masterCTE) \<and> capReplyMaster (cteCap masterCTE) \<and> capTCBPtr (cteCap masterCTE) = send \<longrightarrow> mdbNext (cteMDBNode masterCTE) = nullPointer \<longrightarrow> ((\<lambda>_. mdbFirstBadged (cteMDBNode masterCTE) \<and> mdbRevocable (cteMDBNode masterCTE)) and ((\<lambda>_. True) and (\<lambda>a. True))) s\<rbrace>
 2. \<lbrace>\<lambda>s. reply_masters_rvk_fb (ctes_of s)\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply send \<lbrace>?Q1\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>reply_masters_rvk_fb (ctes_of s); ctes_of s (capTCBPtr (cteCap cte) + 2 ^ cte_level_bits * tcbReplySlot) = Some cte; isReplyCap (cteCap cte); capReplyMaster (cteCap cte); send = capTCBPtr (cteCap cte); mdbNext (cteMDBNode cte) = nullPointer\<rbrakk> \<Longrightarrow> mdbFirstBadged (cteMDBNode cte) \<and> mdbRevocable (cteMDBNode cte) proof (prove)
goal:
No subgoals!