theory Ipc_R

lemma setupCallerCap_ifunsafe[wp]:
  "\<lbrace>if_unsafe_then_cap' and valid_objs' and
    ex_nonz_cap_to' rcvr and tcb_at' rcvr\<rbrace>
   setupCallerCap sender rcvr grant
   \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace>" unfolding setupCallerCap_def getThreadCallerSlot_def
            getThreadReplySlot_def locateSlot_conv apply (wp getSlotCap_cte_wp_at
       | simp add: unique_master_reply_cap' | strengthen eq_imp_strg
       | wp (once) hoare_drop_imp[where f="getCTE rs" for rs])+ apply (rule_tac Q="\<lambda>rv. valid_objs' and tcb_at' rcvr and ex_nonz_cap_to' rcvr"
                in hoare_post_imp) apply (clarsimp simp: ex_nonz_tcb_cte_caps' tcbCallerSlot_def
                          objBits_def objBitsKO_def dom_def cte_level_bits_def) apply (wp sts_valid_objs' | simp)+ apply (clarsimp simp: valid_tcb_state'_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and valid_objs' and ex_nonz_cap_to' rcvr and tcb_at' rcvr\<rbrace> setupCallerCap sender rcvr grant \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>if_unsafe_then_cap' and valid_objs' and ex_nonz_cap_to' rcvr and tcb_at' rcvr\<rbrace> do setThreadState Structures_H.thread_state.BlockedOnReply sender;
replySlot <- return (sender + 2 ^ cte_level_bits * tcbReplySlot);
masterCTE <- getCTE replySlot;
masterCap <- return (cteCap masterCTE);
haskell_assert (isReplyCap masterCap \<and> capReplyMaster masterCap \<and> capTCBPtr masterCap = sender) [];
haskell_assert (mdbNext (cteMDBNode masterCTE) = nullPointer) [];
callerSlot <- return (rcvr + 2 ^ cte_level_bits * tcbCallerSlot);
callerCap <- getSlotCap callerSlot;
haskell_assert (isNullCap callerCap) [];
cteInsert (capability.ReplyCap sender False grant) replySlot callerSlot
od \<lbrace>\<lambda>rv. if_unsafe_then_cap'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'66\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>rv. ex_cte_cap_wp_to' (\<lambda>_. True) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot)\<rbrace>
 2. \<And>s. (if_unsafe_then_cap' and valid_objs' and ex_nonz_cap_to' rcvr and tcb_at' rcvr) s \<Longrightarrow> if_unsafe_then_cap' s \<and> ?P'66 s proof (prove)
goal (3 subgoals):
 1. \<And>rv s. (valid_objs' and tcb_at' rcvr and ex_nonz_cap_to' rcvr) s \<Longrightarrow> ex_cte_cap_wp_to' (\<lambda>_. True) (rcvr + 2 ^ cte_level_bits * tcbCallerSlot) s
 2. \<lbrace>?P'66\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>rv. valid_objs' and tcb_at' rcvr and ex_nonz_cap_to' rcvr\<rbrace>
 3. \<And>s. (if_unsafe_then_cap' and valid_objs' and ex_nonz_cap_to' rcvr and tcb_at' rcvr) s \<Longrightarrow> if_unsafe_then_cap' s \<and> ?P'66 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?P'66\<rbrace> setThreadState Structures_H.thread_state.BlockedOnReply sender \<lbrace>\<lambda>rv. valid_objs' and tcb_at' rcvr and ex_nonz_cap_to' rcvr\<rbrace>
 2. \<And>s. (if_unsafe_then_cap' and valid_objs' and ex_nonz_cap_to' rcvr and tcb_at' rcvr) s \<Longrightarrow> if_unsafe_then_cap' s \<and> ?P'66 s proof (prove)
goal (1 subgoal):
 1. \<And>s. if_unsafe_then_cap' s \<and> valid_objs' s \<and> ex_nonz_cap_to' rcvr s \<and> tcb_at' rcvr s \<Longrightarrow> valid_tcb_state' Structures_H.thread_state.BlockedOnReply s proof (prove)
goal:
No subgoals!