theory CSpace_R

lemma updateFreeIndex_forward_valid_objs':
  "\<lbrace>\<lambda>s. valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap
          \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap
          \<and> is_aligned (of_nat idx :: word32) minUntypedSizeBits) o cteCap) src s\<rbrace>
   updateFreeIndex src idx
   \<lbrace>\<lambda>r s. valid_objs' s\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def updateCap_def getSlotCap_def) apply (wp getCTE_wp') apply clarsimp apply (frule(1) CSpace1_R.ctes_of_valid) apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps capAligned_def
                        valid_cap_simps' is_aligned_weaken[OF is_aligned_triv]) apply (clarsimp simp add: valid_untyped'_def
                  simp del: usableUntypedRange.simps) apply (erule allE, erule notE, erule ko_wp_at'_weakenE) apply (rule disjCI2, simp only: simp_thms) apply (rule notI, erule notE, erule disjoint_subset2[rotated]) apply (rule usableUntypedRange_mono1, simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap \<and> is_aligned (word_of_nat idx) minUntypedSizeBits) \<circ> cteCap) src s\<rbrace> updateFreeIndex src idx \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap \<and> is_aligned (word_of_nat idx) minUntypedSizeBits) \<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;
ctea <- getCTE src;
setCTE src (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) ctea)
od \<lbrace>\<lambda>r. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap \<and> is_aligned (word_of_nat idx) minUntypedSizeBits) \<circ> cteCap) src s \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) src s \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) src (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) \<longrightarrow> (\<forall>cteb. cte_wp_at' ((=) cteb) src (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>) \<longrightarrow> (valid_objs' and valid_cap' (cteCap (cteCap_update (\<lambda>_. capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) cteb))) (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>) | Some r \<Rightarrow> insert r (gsUntypedZeroRanges (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}\<rparr>))\<rparr>))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap \<and> is_aligned (word_of_nat idx) minUntypedSizeBits) \<circ> cteCap) src s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) src s\<rbrakk> \<Longrightarrow> valid_cap' (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte ctea. \<lbrakk>valid_objs' s; cte_wp_at' ((\<lambda>cap. isUntypedCap cap \<and> capFreeIndex cap \<le> idx \<and> idx \<le> 2 ^ capBlockSize cap \<and> is_aligned (word_of_nat idx) minUntypedSizeBits) \<circ> cteCap) src s; cte_wp_at' ((=) cte) src s; cte_wp_at' ((=) ctea) src s; valid_cap' (cteCap cte) s\<rbrakk> \<Longrightarrow> valid_cap' (capFreeIndex_update (\<lambda>_. idx) (cteCap ctea)) s proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f. \<lbrakk>valid_objs' s; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; f \<le> idx; idx \<le> 2 ^ v1; is_aligned (word_of_nat idx) minUntypedSizeBits; is_aligned v0 v1; v1 < word_bits; valid_untyped' d v0 v1 f s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits\<rbrakk> \<Longrightarrow> valid_untyped' d v0 v1 idx s proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f ptr'. \<lbrakk>valid_objs' s; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; f \<le> idx; idx \<le> 2 ^ v1; is_aligned (word_of_nat idx) minUntypedSizeBits; is_aligned v0 v1; v1 < word_bits; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {}) ptr' s; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; ko_wp_at' (\<lambda>ko. {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 idx) \<noteq> {}) ptr' s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f ptr' ko. \<lbrakk>valid_objs' s; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; f \<le> idx; idx \<le> 2 ^ v1; is_aligned (word_of_nat idx) minUntypedSizeBits; is_aligned v0 v1; v1 < word_bits; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 idx) \<noteq> {}\<rbrakk> \<Longrightarrow> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f ptr' ko. \<lbrakk>valid_objs' s; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; f \<le> idx; idx \<le> 2 ^ v1; is_aligned (word_of_nat idx) minUntypedSizeBits; is_aligned v0 v1; v1 < word_bits; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 idx) \<noteq> {}; \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap d v0 v1 f) \<noteq> {} proof (prove)
goal (1 subgoal):
 1. \<And>s cte d v0 v1 f ptr' ko. \<lbrakk>valid_objs' s; ctes_of s src = Some cte; cteCap cte = capability.UntypedCap d v0 v1 f; f \<le> idx; idx \<le> 2 ^ v1; is_aligned (word_of_nat idx) minUntypedSizeBits; is_aligned v0 v1; v1 < word_bits; v0 \<noteq> 0; minUntypedSizeBits \<le> v1; v1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat f) minUntypedSizeBits; \<not> {v0..v0 + 2 ^ v1 - 1} \<subset> obj_range' ptr' ko\<rbrakk> \<Longrightarrow> usableUntypedRange (capability.UntypedCap d v0 v1 idx) \<subseteq> usableUntypedRange (capability.UntypedCap d v0 v1 f) proof (prove)
goal:
No subgoals!