theory CSpace_AI

lemma set_untyped_cap_as_full_has_reply_cap:
  "\<lbrace>\<lambda>s. (has_reply_cap t s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. (has_reply_cap t s)\<rbrace>" apply (clarsimp simp:has_reply_cap_def is_reply_cap_to_def) apply (wp hoare_vcg_ex_lift) apply (wp set_untyped_cap_as_full_cte_wp_at) apply (clarsimp simp:cte_wp_at_caps_of_state) apply (rule_tac x = a in exI) apply (rule_tac x = b in exI) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. has_reply_cap t s \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. has_reply_cap t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<exists>a b. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>a b. \<lbrace>?P2 a b\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b)\<rbrace>
 2. \<And>s. (\<exists>a b. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<exists>x xa. ?P2 x xa s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<exists>a b. cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (a, b) s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> \<exists>x xa. ((x, xa) \<noteq> src \<and> cte_wp_at (\<lambda>cap. \<exists>rights. cap = ReplyCap t False rights) (x, xa) s \<or> (x, xa) = src \<and> cte_wp_at (\<lambda>a. \<exists>rights. masked_as_full a cap = ReplyCap t False rights) src s) \<and> cte_wp_at ((=) src_cap) src s proof (prove)
goal (1 subgoal):
 1. \<And>s a b rights. \<lbrakk>caps_of_state s src = Some src_cap; caps_of_state s (a, b) = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>x xa. (x, xa) \<noteq> src \<and> (\<exists>cap. caps_of_state s (x, xa) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> (x, xa) = src \<and> (\<exists>rights. masked_as_full src_cap cap = ReplyCap t False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s a b rights. \<lbrakk>caps_of_state s src = Some src_cap; caps_of_state s (a, b) = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> \<exists>x. (a, x) \<noteq> src \<and> (\<exists>cap. caps_of_state s (a, x) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> (a, x) = src \<and> (\<exists>rights. masked_as_full src_cap cap = ReplyCap t False rights) proof (prove)
goal (1 subgoal):
 1. \<And>s a b rights. \<lbrakk>caps_of_state s src = Some src_cap; caps_of_state s (a, b) = Some (ReplyCap t False rights)\<rbrakk> \<Longrightarrow> (a, b) \<noteq> src \<and> (\<exists>cap. caps_of_state s (a, b) = Some cap \<and> (\<exists>rights. cap = ReplyCap t False rights)) \<or> (a, b) = src \<and> (\<exists>rights. masked_as_full src_cap cap = ReplyCap t False rights) proof (prove)
goal:
No subgoals!