theory Untyped_R

lemma updateFreeIndex_descendants_of2:
  " \<lbrace>\<lambda>s. cte_wp_at' (isUntypedCap o cteCap) ptr s \<and>
         P (\<lambda>y. descendants_of' y (ctes_of s))\<rbrace>
    updateFreeIndex ptr index
  \<lbrace>\<lambda>r s. P (\<lambda>y. descendants_of' y (ctes_of s))\<rbrace>" apply (simp add: updateFreeIndex_def updateTrackedFreeIndex_def getSlotCap_def) apply (wp updateFreeIndex_descendants_of'[simplified swp_def descendants_of_null_filter']
           getCTE_wp') apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (isUntypedCap \<circ> cteCap) ptr s \<and> P (\<lambda>y. descendants_of' y (ctes_of s))\<rbrace> updateFreeIndex ptr index \<lbrace>\<lambda>r s. P (\<lambda>y. descendants_of' y (ctes_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. cte_wp_at' (isUntypedCap \<circ> cteCap) ptr s \<and> P (\<lambda>y. descendants_of' y (ctes_of s))\<rbrace> do y <- do cte <- getCTE ptr;
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 ptr;
updateCap ptr (capFreeIndex_update (\<lambda>_. index) (cteCap cte))
od \<lbrace>\<lambda>r s. P (\<lambda>y. descendants_of' y (ctes_of s))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. cte_wp_at' (isUntypedCap \<circ> cteCap) ptr s \<and> P (\<lambda>y. descendants_of' y (ctes_of s)) \<Longrightarrow> \<forall>cte. cte_wp_at' ((=) cte) ptr s \<longrightarrow> (\<forall>ctea. cte_wp_at' ((=) ctea) ptr (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> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (K idx') (cteCap ctea)) ptr (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> isUntypedCap (cteCap ctea) \<and> P (\<lambda>y. descendants_of' y (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>)))) proof (prove)
goal:
No subgoals!