theory Untyped_R

lemma updateFreeIndex_updateCap_descendants_range_in':
  "\<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and>
        descendants_range_in' S slot (ctes_of s)\<rbrace>
   updateCap slot (capFreeIndex_update (\<lambda>_. index) cap)
   \<lbrace>\<lambda>r s. descendants_range_in' S slot (ctes_of s)\<rbrace>" apply (rule hoare_pre) apply (wp descendants_range_in_lift'
     [where Q'="\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap" and
       Q = "\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap "] ) apply (wp updateFreeIndex_descendants_of') apply (clarsimp simp: cte_wp_at_ctes_of swp_def isCap_simps) apply (simp add:updateCap_def) apply (wp setCTE_weak_cte_wp_at getCTE_wp) apply (fastforce simp:cte_wp_at_ctes_of isCap_simps) apply (clarsimp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s)\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. descendants_range_in' S slot (ctes_of s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. descendants_range_in' S slot (ctes_of s)\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>P. \<lbrace>\<lambda>s. (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> P (swp descendants_of' (null_filter' (ctes_of s)))\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r s. P (swp descendants_of' (null_filter' (ctes_of s)))\<rbrace>
 2. \<And>P p. \<lbrace>\<lambda>s. (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p\<rbrace>
 3. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> descendants_range_in' S slot (ctes_of s) proof (prove)
goal (3 subgoals):
 1. \<And>P s. (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> P (swp descendants_of' (null_filter' (ctes_of s))) \<Longrightarrow> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (K idx') cap) slot s \<and> isUntypedCap cap \<and> P (swp descendants_of' (null_filter' (ctes_of s)))
 2. \<And>P p. \<lbrace>\<lambda>s. (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p\<rbrace>
 3. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> descendants_range_in' S slot (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<And>P p. \<lbrace>\<lambda>s. (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s\<rbrace> updateCap slot (capFreeIndex_update (\<lambda>_. index) cap) \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> descendants_range_in' S slot (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<And>P p. \<lbrace>\<lambda>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s\<rbrace> do cte <- getCTE slot;
setCTE slot (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap) cte)
od \<lbrace>\<lambda>r. cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p\<rbrace>
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> descendants_range_in' S slot (ctes_of s) proof (prove)
goal (2 subgoals):
 1. \<And>P p s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s \<Longrightarrow> cte_wp_at' (\<lambda>_. True) slot s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) slot s \<and> (if p = slot then P (capRange (cteCap (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. index) cap) cte))) else cte_wp_at' (\<lambda>c. P (capRange (cteCap c))) p s))
 2. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> descendants_range_in' S slot (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap \<and> descendants_range_in' S slot (ctes_of s) \<Longrightarrow> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> (cte_wp_at' (\<lambda>c. cteCap c = cap) slot s \<and> isUntypedCap cap) \<and> descendants_range_in' S slot (ctes_of s) proof (prove)
goal:
No subgoals!