theory CSpace_R

lemma updateFreeIndex_forward_valid_mdb':
  "\<lbrace>\<lambda>s. valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap
          \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) o cteCap) src s\<rbrace>
   updateFreeIndex src idx
   \<lbrace>\<lambda>r s. valid_mdb' s\<rbrace>" apply (simp add: valid_mdb'_def updateFreeIndex_def
                   updateTrackedFreeIndex_def getSlotCap_def) apply (wp updateCapFreeIndex_valid_mdb_ctes getCTE_wp' | simp)+ apply clarsimp apply (frule(1) CSpace1_R.ctes_of_valid) apply (clarsimp simp: cte_wp_at_ctes_of del: subsetI) apply (rule usableUntypedRange_mono2,
    auto simp add: isCap_simps valid_cap_simps' capAligned_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb' s \<and> valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) src s\<rbrace> updateFreeIndex src idx \<lbrace>\<lambda>r. valid_mdb'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_mdb_ctes (ctes_of s) \<and> valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) src s\<rbrace> do y <- do cte <- getCTE src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cte <- getCTE src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) (cteCap cte))
od \<lbrace>\<lambda>r s. valid_mdb_ctes (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_mdb_ctes (ctes_of s) \<and> valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) src s \<Longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) src s \<longrightarrow> usableUntypedRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) \<subseteq> usableUntypedRange (cteCap cte) \<and> isUntypedCap (cteCap cte) \<and> cte_wp_at' (\<lambda>c. cteCap c = cteCap cte) src s) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) src s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) src s\<rbrakk> \<Longrightarrow> usableUntypedRange (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) \<subseteq> usableUntypedRange (cteCap ctea) \<and> isUntypedCap (cteCap ctea) \<and> cte_wp_at' (\<lambda>c. cteCap c = cteCap ctea) src s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap) \<circ> cteCap) src s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) src s; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> usableUntypedRange (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) \<subseteq> usableUntypedRange (cteCap ctea) \<and> isUntypedCap (cteCap ctea) \<and> cte_wp_at' (\<lambda>c. cteCap c = cteCap ctea) src s proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_mdb_ctes (ctes_of s); valid_objs' s; ctes_of s src = Some cte; valid_cap' (cteCap cte) s; isUntypedCap (cteCap cte); capFreeIndex (cteCap cte) \<le> idx; idx \<le> 2 ^ capBlockSize (cteCap cte)\<rbrakk> \<Longrightarrow> usableUntypedRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) \<subseteq> usableUntypedRange (cteCap cte) proof (prove)
goal:
No subgoals!