theory CSpace1_R

lemma setUntypedCapAsFull_pspace_aligned[wp]:
  "\<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace>
   setUntypedCapAsFull (cteCap srcCTE) c slot
   \<lbrace>\<lambda>r. pspace_aligned'\<rbrace>" apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits) apply (intro conjI impI) apply (clarsimp simp:valid_def) apply (drule updateCap_stuff) apply simp apply (wp|clarsimp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> setUntypedCapAsFull (cteCap srcCTE) c slot \<lbrace>\<lambda>r. pspace_aligned'\<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>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)) \<lbrace>\<lambda>r. pspace_aligned'\<rbrace>) \<and> ((capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c) \<longrightarrow> \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. pspace_aligned'\<rbrace>) proof (prove)
goal (2 subgoals):
 1. isUntypedCap (cteCap srcCTE) \<and> isUntypedCap c \<and> capPtr (cteCap srcCTE) = capPtr c \<and> capBlockSize (cteCap srcCTE) = capBlockSize c \<Longrightarrow> \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)) \<lbrace>\<lambda>r. pspace_aligned'\<rbrace>
 2. capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c \<Longrightarrow> \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. pspace_aligned'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>isUntypedCap (cteCap srcCTE); isUntypedCap c; capPtr (cteCap srcCTE) = capPtr c; capBlockSize (cteCap srcCTE) = capBlockSize c; ((), b) \<in> fst (updateCap slot (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)) s); pspace_aligned' s; cte_wp_at' ((=) srcCTE) slot s\<rbrakk> \<Longrightarrow> pspace_aligned' b
 2. capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c \<Longrightarrow> \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. pspace_aligned'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s b. \<lbrakk>isUntypedCap (cteCap srcCTE); isUntypedCap c; capPtr (cteCap srcCTE) = capPtr c; capBlockSize (cteCap srcCTE) = capBlockSize c; pspace_aligned' s; cte_wp_at' ((=) srcCTE) slot s; ctes_of b = modify_map (ctes_of s) slot (cteCap_update (K (capFreeIndex_update (\<lambda>_. max_free_index (capBlockSize c)) (cteCap srcCTE)))) \<and> gsUserPages b = gsUserPages s \<and> gsCNodes b = gsCNodes s \<and> ksMachineState b = ksMachineState s \<and> ksWorkUnitsCompleted b = ksWorkUnitsCompleted s \<and> ksCurThread b = ksCurThread s \<and> ksIdleThread b = ksIdleThread s \<and> ksReadyQueues b = ksReadyQueues s \<and> ksSchedulerAction b = ksSchedulerAction s \<and> ksArchState b = ksArchState s \<and> (pspace_aligned' s \<longrightarrow> pspace_aligned' b) \<and> (pspace_distinct' s \<longrightarrow> pspace_distinct' b)\<rbrakk> \<Longrightarrow> pspace_aligned' b
 2. capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c \<Longrightarrow> \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. pspace_aligned'\<rbrace> proof (prove)
goal (1 subgoal):
 1. capPtr (cteCap srcCTE) = capPtr c \<longrightarrow> isUntypedCap c \<longrightarrow> isUntypedCap (cteCap srcCTE) \<longrightarrow> capBlockSize (cteCap srcCTE) \<noteq> capBlockSize c \<Longrightarrow> \<lbrace>pspace_aligned' and cte_wp_at' ((=) srcCTE) slot\<rbrace> return () \<lbrace>\<lambda>r. pspace_aligned'\<rbrace> proof (prove)
goal:
No subgoals!