theory Untyped_R

lemma updateFreeIndex_caps_overlap_reserved:
  "\<lbrace>\<lambda>s. valid_pspace' s \<and> descendants_range_in' S src (ctes_of s)
        \<and> cte_wp_at' ((\<lambda>cap. S \<subseteq> untypedRange cap \<and>
            usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and>
            isUntypedCap cap) o cteCap) src s\<rbrace>
   updateFreeIndex src index
   \<lbrace>\<lambda>r s. caps_overlap_reserved' S s\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def getSlotCap_def) apply (wp updateFreeIndex_updateCap_caps_overlap_reserved getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of valid_pspace'_def) apply (clarsimp simp: valid_mdb'_def split: option.split) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> descendants_range_in' S src (ctes_of s) \<and> cte_wp_at' ((\<lambda>cap. S \<subseteq> untypedRange cap \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and> isUntypedCap cap) \<circ> cteCap) src s\<rbrace> updateFreeIndex src index \<lbrace>\<lambda>r. caps_overlap_reserved' S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> descendants_range_in' S src (ctes_of s) \<and> cte_wp_at' ((\<lambda>cap. S \<subseteq> untypedRange cap \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and> isUntypedCap 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>_. index) (cteCap cte)) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cte <- getCTE src;
updateCap src (capFreeIndex_update (\<lambda>_. index) (cteCap cte))
od \<lbrace>\<lambda>r. caps_overlap_reserved' S\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_pspace' s \<and> descendants_range_in' S src (ctes_of s) \<and> cte_wp_at' ((\<lambda>cap. S \<subseteq> untypedRange cap \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) cap) \<inter> S = {} \<and> isUntypedCap cap) \<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>_. index) (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_mdb' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. index) (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>) \<and> valid_objs' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. index) (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>) \<and> S \<subseteq> untypedRange (cteCap ctea) \<and> usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {} \<and> isUntypedCap (cteCap ctea) \<and> descendants_range_in' S src (ctes_of (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (cteCap cte) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r}, gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. index) (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>)) \<and> cte_wp_at' (\<lambda>c. cteCap c = cteCap 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>_. index) (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 ctea. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; descendants_range_in' S src (ctes_of s); S \<subseteq> untypedRange (cteCap ctea); usableUntypedRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) \<inter> S = {}; isUntypedCap (cteCap ctea); ctes_of s src = Some ctea\<rbrakk> \<Longrightarrow> valid_mdb' (s\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. index) (cteCap ctea)) of None \<Rightarrow> case untypedZeroRange (cteCap ctea) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r} | Some r \<Rightarrow> insert r (case untypedZeroRange (cteCap ctea) of None \<Rightarrow> gsUntypedZeroRanges s | Some r \<Rightarrow> gsUntypedZeroRanges s - {r})\<rparr>) proof (prove)
goal:
No subgoals!