theory KHeap_DR

lemma get_tcb_reply_cap_wp_obj_ref:
    "\<lbrace>tcb_at sid and valid_objs and cte_wp_at ((\<noteq>) cap.NullCap) (sid,tcb_cnode_index 2) \<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2)
    \<lbrace>\<lambda>rv s. (obj_ref_of rv = sid) \<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 tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"]) apply clarsimp apply (frule cte_wp_tcb_cap_valid) apply simp+ 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)\<rbrace> CSpaceAcc_A.get_cap (sid, tcb_cnode_index 2) \<lbrace>\<lambda>rv s. obj_ref_of rv = sid\<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 tcb_at sid and valid_objs and cte_wp_at ((=) rv) (sid, tcb_cnode_index 2)) s \<Longrightarrow> 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)\<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 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; tcb_at sid s; valid_objs s; cte_wp_at ((=) rv) (sid, tcb_cnode_index 2) s\<rbrakk> \<Longrightarrow> 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)\<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 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; 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; 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> 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)\<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 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; 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> 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)\<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 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)\<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 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)) s \<Longrightarrow> cte_wp_at (\<lambda>cap. cap \<noteq> cap.NullCap) (sid, tcb_cnode_index 2) 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!