theory CSpace1_R

lemma setUntypedCapAsFull_cte_wp_at:
  "\<lbrace>cte_wp_at' ((=) srcCTE) slot and
    (\<lambda>s. cte_wp_at' (\<lambda>c. P c) dest s \<and> dest \<noteq> slot \<or>
         dest = slot \<and> cte_wp_at' (\<lambda>c. P (CTE (maskedAsFull (cteCap c) c')
                                              (cteMDBNode c))) slot s) \<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) c' slot
   \<lbrace>\<lambda>r s. cte_wp_at' (\<lambda>c. P c) dest s\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def cte_wp_at_ctes_of split:if_splits) apply (case_tac "dest = slot") apply (intro conjI impI) apply (clarsimp simp:updateCap_def) apply (wp getCTE_wp) apply (clarsimp simp:maskedAsFull_def cte_wp_at_ctes_of cteCap_update_simps) apply wp apply (case_tac srcCTE) apply (fastforce simp:maskedAsFull_def cte_wp_at_ctes_of) apply (intro conjI impI) apply (clarsimp simp:updateCap_def | wp setCTE_weak_cte_wp_at getCTE_wp)+ apply (simp add:cte_wp_at'_def) apply (clarsimp simp:updateCap_def | wp setCTE_weak_cte_wp_at getCTE_wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. cte_wp_at' P dest s \<and> dest \<noteq> slot \<or> dest = slot \<and> cte_wp_at' (\<lambda>c. P (CTE (maskedAsFull (cteCap c) c') (cteMDBNode c))) slot s)\<rbrace> setUntypedCapAsFull (cteCap srcCTE) c' slot \<lbrace>\<lambda>r. cte_wp_at' P dest\<rbrace> proof (prove)
goal (1 subgoal):
 1. (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (2 subgoals):
 1. dest = slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>)
 2. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest = slot; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>
 2. \<lbrakk>dest = slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>
 3. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>dest = slot; isUntypedCap (cteCap srcCTE); isUntypedCap c'; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. \<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte)))\<rbrace> do cte <- getCTE slot;
setCTE slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) cte)
od \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s slot = Some cte \<and> P cte\<rbrace>
 2. \<lbrakk>dest = slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>
 3. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>dest = slot; isUntypedCap (cteCap srcCTE); isUntypedCap c'; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; (cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. \<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte)))) s\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (\<exists>ctea. ((ctes_of s)(slot \<mapsto> cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) cte)) slot = Some ctea \<and> P ctea))
 2. \<lbrakk>dest = slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>
 3. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dest = slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>
 2. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>dest = slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'; (cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))) s\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s dest = Some cte \<and> P cte
 2. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<And>s x1 x2. \<lbrakk>dest = slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'; (cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))) s; srcCTE = CTE x1 x2\<rbrakk> \<Longrightarrow> \<exists>cte. ctes_of s dest = Some cte \<and> P cte
 2. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (1 subgoal):
 1. dest \<noteq> slot \<Longrightarrow> (isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c' \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c') \<longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>dest \<noteq> slot; isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c' \<and> capPtr (cteCap srcCTE) = capPtr c' \<and> capBlockSize (cteCap srcCTE) = capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c')) (cteCap srcCTE)) \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace>
 2. \<lbrakk>dest \<noteq> slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s cte. \<lbrakk>dest \<noteq> slot; isUntypedCap (cteCap srcCTE); isUntypedCap c'; capPtr (cteCap srcCTE) = capPtr c'; capBlockSize (cteCap srcCTE) = capBlockSize c'; cte_wp_at' ((=) srcCTE) slot s; ctes_of s dest = Some cte; P cte; cte_wp_at' (\<lambda>_. True) slot s\<rbrakk> \<Longrightarrow> \<exists>cte. cte_wp_at' ((=) cte) slot s
 2. \<lbrakk>dest \<noteq> slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrakk>dest \<noteq> slot; capPtr (cteCap srcCTE) = capPtr c' \<longrightarrow> isUntypedCap c' \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c'\<rbrakk> \<Longrightarrow> \<lbrace>cte_wp_at' ((=) srcCTE) slot and (\<lambda>s. (\<exists>cte. ctes_of s dest = Some cte \<and> P cte) \<and> dest \<noteq> slot \<or> dest = slot \<and> (\<exists>cte. ctes_of s slot = Some cte \<and> P (CTE (maskedAsFull (cteCap cte) c') (cteMDBNode cte))))\<rbrace> return () \<lbrace>\<lambda>r s. \<exists>cte. ctes_of s dest = Some cte \<and> P cte\<rbrace> proof (prove)
goal:
No subgoals!