theory CSpace_R

lemma setUntypedCapAsFull_sizes[wp]:
  "\<lbrace>\<lambda>s. valid_cap_sizes' sz (ctes_of s) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace>
    setUntypedCapAsFull (cteCap srcCTE) cap src
  \<lbrace>\<lambda>rv s. valid_cap_sizes' sz (ctes_of s)\<rbrace>" apply (clarsimp simp:valid_cap_sizes'_def setUntypedCapAsFull_def split del:if_splits) apply (rule hoare_pre) apply (wp updateCap_ctes_of_wp | wps)+ 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_cap_sizes' sz (ctes_of s) \<and> cte_wp_at' ((=) srcCTE) src s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>rv s. valid_cap_sizes' sz (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> sz) \<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>rv s. \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> sz\<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>rv s. \<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> sz\<rbrace>
 2. \<And>s. (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> sz) \<and> cte_wp_at' ((=) srcCTE) src s \<Longrightarrow> ?Q6 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> sz) \<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>cte\<in>ran (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)))). 2 ^ capBits (cteCap cte) \<le> sz)) \<and> (\<not> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap) \<longrightarrow> (\<forall>cte\<in>ran (ctes_of s). 2 ^ capBits (cteCap cte) \<le> sz)) proof (prove)
goal (1 subgoal):
 1. \<And>s y ya. \<lbrakk>\<forall>y\<in>dom (ctes_of s). 2 ^ capBits (cteCap (the (ctes_of s y))) \<le> sz; 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> 2 ^ capBits (cteCap ya) \<le> sz 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; 2 ^ capBits (cteCap (the (ctes_of s y))) \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ capBits (cteCap ya) \<le> sz 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; 2 ^ capBits (cteCap (the (ctes_of s y))) \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ capBits (cteCap ya) \<le> sz 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; 2 ^ capBits (cteCap (the (ctes_of s y))) \<le> sz\<rbrakk> \<Longrightarrow> 2 ^ capBits (cteCap ya) \<le> sz proof (prove)
goal:
No subgoals!