theory CSpace1_R

lemma setUntypedCapAsFull_caps_contained:
  assumes preserve:"\<And>m m'. mdb_inv_preserve m m' \<Longrightarrow> mdb_inv_preserve (Q m) (Q m')"
  shows
 "\<lbrace>\<lambda>s. P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrace>
setUntypedCapAsFull (cteCap srcCTE) cap src
 \<lbrace>\<lambda>r s. P (caps_contained' (Q (ctes_of s)))\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits,intro conjI impI) apply (wp updateCapFreeIndex_caps_contained) apply (clarsimp simp:cte_wp_at_ctes_of preserve)+ apply wp apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>r s. P (caps_contained' (Q (ctes_of s)))\<rbrace> proof (prove)
goal (2 subgoals):
 1. isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) \<lbrace>\<lambda>r s. P (caps_contained' (Q (ctes_of s)))\<rbrace>
 2. capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrace> return () \<lbrace>\<lambda>r s. P (caps_contained' (Q (ctes_of s)))\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>m m'. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap; mdb_inv_preserve m m'\<rbrakk> \<Longrightarrow> mdb_inv_preserve (Q m) (Q m')
 2. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap; P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrakk> \<Longrightarrow> P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE \<and> isUntypedCap (cteCap c)) src s
 3. capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_contained' (Q (ctes_of s))) \<and> cte_wp_at' (\<lambda>c. c = srcCTE) src s\<rbrace> return () \<lbrace>\<lambda>r s. P (caps_contained' (Q (ctes_of s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap \<Longrightarrow> \<lbrace>\<lambda>s. P (caps_contained' (Q (ctes_of s))) \<and> ctes_of s src = Some srcCTE\<rbrace> return () \<lbrace>\<lambda>r s. P (caps_contained' (Q (ctes_of s)))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap; P (caps_contained' (Q (ctes_of s))) \<and> ctes_of s src = Some srcCTE\<rbrakk> \<Longrightarrow> P (caps_contained' (Q (ctes_of s))) proof (prove)
goal:
No subgoals!