theory KHeap_DR

lemma get_tcb_reply_cap_wp_original_cap:
    "\<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
    \<lbrace>\<lambda>rv s. is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)\<rbrace>" apply (rule hoare_post_imp
     [where Q="\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb
       and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"]) apply (rename_tac rv s) apply clarsimp apply (subgoal_tac "is_master_reply_cap rv \<and> obj_ref_of rv = sid") apply clarsimp apply (frule cte_wp_tcb_cap_valid) apply simp+ apply (clarsimp simp:valid_mdb_def reply_master_revocable_def) apply (drule_tac x = "obj_ref_of rv" in spec) apply (drule_tac x = "tcb_cnode_index 2" in spec) apply (drule_tac x = rv in spec) apply (drule iffD1[OF cte_wp_at_caps_of_state])+ apply clarsimp apply (frule cte_wp_tcb_cap_valid) apply (clarsimp simp :cte_wp_at_def tcb_cap_valid_def st_tcb_at_def obj_at_def is_master_reply_cap_def split:cap.splits)+ apply (wp get_cap_cte_wp_at_rv) apply (clarsimp simp:cte_wp_at_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>rv s. is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) rv) (sid, tcb_cnode_index 2)) s \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. (cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) rv) (sid, tcb_cnode_index 2)) s \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s; is_master_reply_cap rv \<and> obj_ref_of rv = sid\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; valid_mdb s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; valid_mdb s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; valid_mdb s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 3. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 4. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; valid_mdb s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); \<forall>a b cap. caps_of_state s (a, b) = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s (a, b); reply_mdb (cdt s) (caps_of_state s)\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); \<forall>b cap. caps_of_state s (obj_ref_of rv, b) = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s (obj_ref_of rv, b)\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); \<forall>cap. caps_of_state s (obj_ref_of rv, tcb_cnode_index 2) = Some cap \<longrightarrow> is_master_reply_cap cap \<longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (obj_ref_of rv, tcb_cnode_index 2) s; tcb_at (obj_ref_of rv) s; valid_objs s; cte_wp_at ((=) rv) (obj_ref_of rv, tcb_cnode_index 2) s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); caps_of_state s (obj_ref_of rv, tcb_cnode_index 2) = Some rv \<longrightarrow> is_master_reply_cap rv \<longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>tcb_at (obj_ref_of rv) s; valid_objs s; is_master_reply_cap rv; sid = obj_ref_of rv; tcb_cap_valid rv (obj_ref_of rv, tcb_cnode_index 2) s; mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s); untyped_mdb (cdt s) (caps_of_state s); descendants_inc (cdt s) (caps_of_state s); no_mloop (cdt s); untyped_inc (cdt s) (caps_of_state s); ut_revocable (is_original_cap s) (caps_of_state s); irq_revocable (is_original_cap s) (caps_of_state s); reply_mdb (cdt s) (caps_of_state s); caps_of_state s (obj_ref_of rv, tcb_cnode_index 2) = Some rv \<longrightarrow> is_master_reply_cap rv \<longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2); \<exists>cap. caps_of_state s (obj_ref_of rv, tcb_cnode_index 2) = Some cap \<and> rv \<noteq> cap.NullCap; \<exists>cap. caps_of_state s (obj_ref_of rv, tcb_cnode_index 2) = Some cap \<and> rv = cap\<rbrakk> \<Longrightarrow> is_original_cap s (obj_ref_of rv, tcb_cnode_index 2)
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 2. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<And>rv s. \<lbrakk>cte_wp_at (\<lambda>c. rv \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s; valid_mdb s; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s; tcb_cap_valid rv (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> is_master_reply_cap rv \<and> obj_ref_of rv = sid
 3. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>r. cte_wp_at (\<lambda>c. r \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid, tcb_cnode_index 2)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid, tcb_cnode_index 2) and valid_mdb) s \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) s \<and> valid_mdb s \<and> tcb_at sid s \<and> valid_objs s \<and> cte_wp_at (\<lambda>cap. cap = cap) (sid, tcb_cnode_index 2) s proof (prove)
goal:
No subgoals!