theory CSpace_R

lemma setUntypedCapAsFull_valid_refs'[wp]:
  "\<lbrace>\<lambda>s. valid_refs' R (ctes_of s) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) cap src
   \<lbrace>\<lambda>yb s. valid_refs' R (ctes_of s)\<rbrace>" apply (clarsimp simp:valid_refs'_def setUntypedCapAsFull_def split del:if_splits) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp) apply (clarsimp simp:ran_dom) apply (drule_tac x = y in bspec) apply (drule_tac a = y in domI) apply (simp add:modify_map_dom) apply (clarsimp simp:modify_map_def cte_wp_at_ctes_of
    isCap_simps split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_refs' R (ctes_of s) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>yb s. valid_refs' R (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>c\<in>ran (ctes_of s). R \<inter> capRange (cteCap c) = {}) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace> if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) else return () \<lbrace>\<lambda>yb s. \<forall>c\<in>ran (ctes_of s). R \<inter> capRange (cteCap c) = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q6\<rbrace> if isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap then updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) else return () \<lbrace>\<lambda>yb s. \<forall>c\<in>ran (ctes_of s). R \<inter> capRange (cteCap c) = {}\<rbrace>
 2. \<And>s. (\<forall>c\<in>ran (ctes_of s). R \<inter> capRange (cteCap c) = {}) \<and> cte_wp_at' ((=) srcCTE) src s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>c\<in>ran (ctes_of s). R \<inter> capRange (cteCap c) = {}) \<and> cte_wp_at' ((=) srcCTE) src s \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<longrightarrow> (\<forall>c\<in>ran (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)))). R \<inter> capRange (cteCap c) = {})) \<and> (\<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<longrightarrow> (\<forall>c\<in>ran (ctes_of s). R \<inter> capRange (cteCap c) = {})) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya. \<lbrakk>\<forall>y\<in>dom (ctes_of s). R \<inter> capRange (cteCap (the (ctes_of s y))) = {}; cte_wp_at' ((=) srcCTE) src s; modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))) y = Some ya; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap\<rbrakk> \<Longrightarrow> R \<inter> capRange (cteCap ya) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s y ya. \<lbrakk>cte_wp_at' ((=) srcCTE) src s; modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))) y = Some ya; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap\<rbrakk> \<Longrightarrow> y \<in> dom (ctes_of s)
 2. \<And>s y ya. \<lbrakk>cte_wp_at' ((=) srcCTE) src s; modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))) y = Some ya; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap; R \<inter> capRange (cteCap (the (ctes_of s y))) = {}\<rbrakk> \<Longrightarrow> R \<inter> capRange (cteCap ya) = {} proof (prove)
goal (2 subgoals):
 1. \<And>s y ya. \<lbrakk>cte_wp_at' ((=) srcCTE) src s; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap; y \<in> dom (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))))\<rbrakk> \<Longrightarrow> y \<in> dom (ctes_of s)
 2. \<And>s y ya. \<lbrakk>cte_wp_at' ((=) srcCTE) src s; modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))) y = Some ya; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap; R \<inter> capRange (cteCap (the (ctes_of s y))) = {}\<rbrakk> \<Longrightarrow> R \<inter> capRange (cteCap ya) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s y ya. \<lbrakk>cte_wp_at' ((=) srcCTE) src s; modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))) y = Some ya; isUntypedCap (cteCap srcCTE); isUntypedCap cap; capPtr (cteCap srcCTE) = capPtr cap; capBlockSize (cteCap srcCTE) = capBlockSize cap; R \<inter> capRange (cteCap (the (ctes_of s y))) = {}\<rbrakk> \<Longrightarrow> R \<inter> capRange (cteCap ya) = {} proof (prove)
goal:
No subgoals!