theory CSpace1_R

lemma setUntypedCapAsFull_ctes:
 "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and>
   P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))
  \<rbrace>
 setUntypedCapAsFull (cteCap srcCTE) cap src
 \<lbrace>\<lambda>r s. P (ctes_of s)\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits,intro conjI impI) apply (wp updateCap_ctes_of_wp) apply (clarsimp simp:isCap_simps max_free_index_def maskedAsFull_def) apply wp apply (clarsimp simp:isCap_simps cte_wp_at_ctes_of
    max_free_index_def maskedAsFull_def split:if_splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrace> setUntypedCapAsFull (cteCap srcCTE) cap src \<lbrace>\<lambda>r s. P (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. cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE)) \<lbrace>\<lambda>r s. P (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. cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrace> return () \<lbrace>\<lambda>r s. P (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>isUntypedCap (cteCap srcCTE) \<and> isUntypedCap cap \<and> capPtr (cteCap srcCTE) = capPtr cap \<and> capBlockSize (cteCap srcCTE) = capBlockSize cap; cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize cap)) (cteCap srcCTE))))
 2. capPtr (cteCap srcCTE) = capPtr cap \<longrightarrow> isUntypedCap cap \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize cap \<Longrightarrow> \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrace> return () \<lbrace>\<lambda>r s. P (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. cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrace> return () \<lbrace>\<lambda>r s. P (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; cte_wp_at' (\<lambda>c. c = srcCTE) src s \<and> P (modify_map (ctes_of s) src (cteCap_update (\<lambda>_. maskedAsFull (cteCap srcCTE) cap)))\<rbrakk> \<Longrightarrow> P (ctes_of s) proof (prove)
goal:
No subgoals!