theory CSpace_AI

lemma set_untyped_cap_as_full_unique_reply_caps:
  "\<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
   set_untyped_cap_as_full src_cap cap src
   \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace>" apply (simp add: unique_reply_caps_def set_untyped_cap_as_full_def) apply (rule conjI) apply clarify apply wp apply (clarsimp simp: is_cap_simps) apply wpsimp by blast

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. unique_reply_caps (caps_of_state s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s. unique_reply_caps (caps_of_state s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. (is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace>) \<and> ((obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace>) proof (prove)
goal (2 subgoals):
 1. is_untyped_cap src_cap \<and> is_untyped_cap cap \<and> obj_ref_of src_cap = obj_ref_of cap \<and> cap_bits_untyped src_cap = cap_bits_untyped cap \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace>
 2. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_cap (max_free_index_update src_cap) src \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace>
 2. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>is_untyped_cap src_cap; is_untyped_cap cap; obj_ref_of src_cap = obj_ref_of cap; cap_bits_untyped src_cap = cap_bits_untyped cap; (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrakk> \<Longrightarrow> \<forall>a b aa ba t. (\<exists>R. ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. ((caps_of_state s)(src \<mapsto> max_free_index_update src_cap)) (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba
 2. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace> proof (prove)
goal (1 subgoal):
 1. (obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap) \<longrightarrow> \<lbrace>\<lambda>s. (\<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> return () \<lbrace>\<lambda>rv s. \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b aa ba t R R'. \<lbrakk>obj_ref_of src_cap = obj_ref_of cap \<longrightarrow> is_untyped_cap cap \<longrightarrow> is_untyped_cap src_cap \<longrightarrow> cap_bits_untyped src_cap \<noteq> cap_bits_untyped cap; \<forall>a b aa ba t. (\<exists>R. caps_of_state s (a, b) = Some (ReplyCap t False R)) \<longrightarrow> (\<exists>R'. caps_of_state s (aa, ba) = Some (ReplyCap t False R')) \<longrightarrow> a = aa \<and> b = ba; cte_wp_at ((=) src_cap) src s; caps_of_state s (a, b) = Some (ReplyCap t False R); caps_of_state s (aa, ba) = Some (ReplyCap t False R')\<rbrakk> \<Longrightarrow> a = aa \<and> b = ba