theory CSpace_C

lemma update_freeIndex:
  "ccorres dc xfdc
     (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = UntypedCap d p sz i) srcSlot
           and (\<lambda>_. is_aligned (of_nat i' :: word32) minUntypedSizeBits \<and> i' \<le> 2 ^ sz))
     (UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace>
           \<inter> \<lbrace>\<acute>v32 = of_nat i' >> minUntypedSizeBits\<rbrace>) []
     (updateCap srcSlot (UntypedCap d p sz i'))
     (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)" apply (rule ccorres_assume_pre, rule ccorres_guard_imp) apply (rule update_freeIndex'; clarsimp simp: cte_wp_at_ctes_of) apply (case_tac cte; clarsimp dest!: ctes_of_valid_cap' simp: valid_cap'_def) by auto

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) (UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = word_of_nat i' >> minUntypedSizeBits\<rbrace>) [] (updateCap srcSlot (capability.UntypedCap d p sz i')) (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc) proof (prove)
goal (3 subgoals):
 1. \<And>s. (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s \<Longrightarrow> ccorres dc xfdc (?Q2 s) (?Q'2 s) [] (updateCap srcSlot (capability.UntypedCap d p sz i')) (Call cap_untyped_cap_ptr_set_capFreeIndex_'proc)
 2. \<And>s sa. \<lbrakk>(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s; (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz) and (\<lambda>s'. s' = s)) sa\<rbrakk> \<Longrightarrow> ?Q2 s sa
 3. \<And>s sa. \<lbrakk>(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s; sa \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = word_of_nat i' >> minUntypedSizeBits\<rbrace>\<rbrakk> \<Longrightarrow> sa \<in> ?Q'2 s proof (prove)
goal (3 subgoals):
 1. \<And>s cte i. \<lbrakk>valid_objs' s; is_aligned (word_of_nat i') minUntypedSizeBits; i' \<le> 2 ^ sz; ctes_of s srcSlot = Some cte; cteCap cte = capability.UntypedCap d p sz i\<rbrakk> \<Longrightarrow> sz \<le> maxUntypedSizeBits
 2. \<And>s sa. \<lbrakk>(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s; (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz) and (\<lambda>s'. s' = s)) sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot sa
 3. \<And>s sa. \<lbrakk>(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s; sa \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = word_of_nat i' >> minUntypedSizeBits\<rbrace>\<rbrakk> \<Longrightarrow> sa \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = word_of_nat i' >> minUntypedSizeBits\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s sa. \<lbrakk>(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s; (valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz) and (\<lambda>s'. s' = s)) sa\<rbrakk> \<Longrightarrow> cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot sa
 2. \<And>s sa. \<lbrakk>(valid_objs' and cte_wp_at' (\<lambda>cte. \<exists>i. cteCap cte = capability.UntypedCap d p sz i) srcSlot and (\<lambda>_. is_aligned (word_of_nat i') minUntypedSizeBits \<and> i' \<le> 2 ^ sz)) s; sa \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = word_of_nat i' >> minUntypedSizeBits\<rbrace>\<rbrakk> \<Longrightarrow> sa \<in> UNIV \<inter> \<lbrace>\<acute>cap_ptr = cap_Ptr &(cte_Ptr srcSlot\<rightarrow>[''cap_C''])\<rbrace> \<inter> \<lbrace>\<acute>v32 = word_of_nat i' >> minUntypedSizeBits\<rbrace>