theory Syscall_R

lemma deleteCallerCap_nonz_cap:
  "\<lbrace>ex_nonz_cap_to' p and tcb_at' t and valid_objs'\<rbrace>
      deleteCallerCap t
   \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>" apply (simp add: deleteCallerCap_def getSlotCap_def getThreadCallerSlot_map
                    locateSlot_conv ) apply (rule hoare_pre) apply (wp cteDeleteOne_reply_cap_to'' getCTE_wp') apply clarsimp apply (frule_tac offs="tcb_cnode_index 3" in tcb_at_cte_at_map) apply (clarsimp simp: tcb_cap_cases_def) apply (auto simp: ex_nonz_cap_to'_def isCap_simps cte_wp_at_ctes_of) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p and tcb_at' t and valid_objs'\<rbrace> deleteCallerCap t \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>ex_nonz_cap_to' p and tcb_at' t and valid_objs'\<rbrace> do cte <- getCTE (cte_map (t, tcb_cnode_index 3));
y <- assert (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do cte <- getCTE (cte_map (t, tcb_cnode_index 3));
y <- assert (isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap);
cteDeleteOne (cte_map (t, tcb_cnode_index 3))
od \<lbrace>\<lambda>rv. ex_nonz_cap_to' p\<rbrace>
 2. \<And>s. (ex_nonz_cap_to' p and tcb_at' t and valid_objs') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (ex_nonz_cap_to' p and tcb_at' t and valid_objs') s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s \<longrightarrow> isReplyCap (cteCap cte) \<or> cteCap cte = capability.NullCap \<longrightarrow> (ex_nonz_cap_to' p and cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> isNullCap (cteCap c)) (cte_map (t, tcb_cnode_index 3))) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>ex_nonz_cap_to' p s; tcb_at' t s; valid_objs' s; cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s\<rbrakk> \<Longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> cteCap c = capability.NullCap) (cte_map (t, tcb_cnode_index 3)) s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> cteCap c = capability.NullCap) (cte_map (t, tcb_cnode_index 3)) s) proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>ex_nonz_cap_to' p s; tcb_at' t s; valid_objs' s; cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s\<rbrakk> \<Longrightarrow> tcb_cnode_index 3 \<in> dom tcb_cap_cases
 2. \<And>s cte. \<lbrakk>ex_nonz_cap_to' p s; tcb_at' t s; valid_objs' s; cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s; cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s\<rbrakk> \<Longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> cteCap c = capability.NullCap) (cte_map (t, tcb_cnode_index 3)) s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> cteCap c = capability.NullCap) (cte_map (t, tcb_cnode_index 3)) s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>ex_nonz_cap_to' p s; tcb_at' t s; valid_objs' s; cte_wp_at' ((=) cte) (cte_map (t, tcb_cnode_index 3)) s; cte_wp_at' (\<lambda>_. True) (cte_map (t, tcb_cnode_index 3)) s\<rbrakk> \<Longrightarrow> (isReplyCap (cteCap cte) \<longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> cteCap c = capability.NullCap) (cte_map (t, tcb_cnode_index 3)) s) \<and> (cteCap cte = capability.NullCap \<longrightarrow> cte_wp_at' (\<lambda>c. isReplyCap (cteCap c) \<or> cteCap c = capability.NullCap) (cte_map (t, tcb_cnode_index 3)) s) proof (prove)
goal:
No subgoals!