theory CSpace_AI

lemma mdb_cte_at_set_untyped_cap_as_full:
  assumes localcong:"\<And>a cap. P (cap\<lparr>free_index:= a\<rparr>) = P cap"
  shows "
  \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace>
  set_untyped_cap_as_full src_cap cap src
  \<lbrace>\<lambda>rv s'. mdb_cte_at (swp (cte_wp_at P) s') (cdt s') \<rbrace>" apply (clarsimp simp:set_untyped_cap_as_full_def split del:if_split) apply (rule hoare_pre) apply (wp set_cap_mdb_cte_at) apply clarsimp apply (unfold mdb_cte_at_def) apply (intro conjI impI,elim allE domE ranE impE,simp) apply (clarsimp simp:cte_wp_at_caps_of_state cong:local.localcong) apply (elim allE ranE impE,simp) apply (clarsimp simp:cte_wp_at_caps_of_state cong:local.localcong) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> set_untyped_cap_as_full src_cap cap src \<lbrace>\<lambda>rv s'. mdb_cte_at (swp (cte_wp_at P) s') (cdt s')\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s\<rbrace> if 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 then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>rv s'. mdb_cte_at (swp (cte_wp_at P) s') (cdt s')\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> if 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 then set_cap (max_free_index_update src_cap) src else return () \<lbrace>\<lambda>rv s'. mdb_cte_at (swp (cte_wp_at P) s') (cdt s')\<rbrace>
 2. \<And>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> cte_wp_at ((=) src_cap) src s \<Longrightarrow> (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> mdb_cte_at (swp (cte_wp_at P) s) (cdt s) \<and> (src \<in> dom (cdt s) \<union> ran (cdt s) \<longrightarrow> P (max_free_index_update src_cap))) \<and> (\<not> (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> mdb_cte_at (swp (cte_wp_at P) s) (cdt s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>mdb_cte_at (swp (cte_wp_at P) s) (cdt s); cte_wp_at ((=) src_cap) src s; 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> (src \<in> dom (cdt s) \<longrightarrow> P (max_free_index_update src_cap)) \<and> (src \<in> ran (cdt s) \<longrightarrow> P (max_free_index_update src_cap)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> swp (cte_wp_at P) s p \<and> swp (cte_wp_at P) s c; cte_wp_at ((=) src_cap) src s; 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> (src \<in> dom (cdt s) \<longrightarrow> P (max_free_index_update src_cap)) \<and> (src \<in> ran (cdt s) \<longrightarrow> P (max_free_index_update src_cap)) proof (prove)
goal (2 subgoals):
 1. \<And>s r. \<lbrakk>cte_wp_at ((=) src_cap) src s; 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; cdt s src = Some r; swp (cte_wp_at P) s r \<and> swp (cte_wp_at P) s src\<rbrakk> \<Longrightarrow> P (max_free_index_update src_cap)
 2. \<And>s. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> swp (cte_wp_at P) s p \<and> swp (cte_wp_at P) s c; cte_wp_at ((=) src_cap) src s; 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; src \<in> ran (cdt s)\<rbrakk> \<Longrightarrow> P (max_free_index_update src_cap) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>p c. cdt s c = Some p \<longrightarrow> swp (cte_wp_at P) s p \<and> swp (cte_wp_at P) s c; cte_wp_at ((=) src_cap) src s; 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; src \<in> ran (cdt s)\<rbrakk> \<Longrightarrow> P (max_free_index_update src_cap) proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>cte_wp_at ((=) src_cap) src s; 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; cdt s x = Some src; swp (cte_wp_at P) s src \<and> swp (cte_wp_at P) s x\<rbrakk> \<Longrightarrow> P (max_free_index_update src_cap) proof (prove)
goal:
No subgoals!