theory Untyped_R

lemma updateFreeIndex_valid_pspace_no_overlap':
  "\<lbrace>\<lambda>s. valid_pspace' s \<and>
        (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and>
        cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) o cteCap) src s)
        \<and> is_aligned (of_nat idx :: word32) minUntypedSizeBits \<and>
        descendants_of' src (ctes_of s) = {}\<rbrace>
     updateFreeIndex src idx
   \<lbrace>\<lambda>r s. valid_pspace' s\<rbrace>" apply (clarsimp simp:valid_pspace'_def updateFreeIndex_def
     updateTrackedFreeIndex_def) apply (rule hoare_pre) apply (rule hoare_vcg_conj_lift) apply (clarsimp simp:updateCap_def getSlotCap_def) apply (wp getCTE_wp | simp)+ apply (wp updateFreeIndex_mdb_simple' getCTE_wp'
       | simp add: getSlotCap_def)+ apply (clarsimp simp:cte_wp_at_ctes_of valid_pspace'_def) apply (case_tac cte,simp add:isCap_simps) apply (frule(1) ctes_of_valid_cap') apply (clarsimp simp: valid_cap_simps' capAligned_def
                        pspace_no_overlap_valid_untyped') done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_pspace' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}\<rbrace> updateFreeIndex src idx \<lbrace>\<lambda>r. valid_pspace'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {}\<rbrace> do y <- do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>r s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do y <- do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>r s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s\<rbrace>
 2. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3\<rbrace> do y <- do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>rv. valid_objs'\<rbrace>
 2. \<lbrace>?P'3\<rbrace> do y <- do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s\<rbrace>
 3. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> ?P3 s \<and> ?P'3 s proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P3\<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>rv. valid_objs'\<rbrace>
 2. \<lbrace>?P'3\<rbrace> do y <- do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od;
cap <- getSlotCap src;
updateCap src (capFreeIndex_update (\<lambda>_. idx) cap)
od \<lbrace>\<lambda>rv s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s\<rbrace>
 3. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> ?P3 s \<and> ?P'3 s proof (prove)
goal (4 subgoals):
 1. \<And>cap. \<lbrace>?P'30 () cap\<rbrace> updateCap src (capFreeIndex_update (\<lambda>_. idx) cap) \<lbrace>\<lambda>rv. valid_mdb'\<rbrace>
 2. \<And>y. \<lbrace>?B24 y\<rbrace> getSlotCap src \<lbrace>\<lambda>cap s. pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> ?P'30 y cap s\<rbrace>
 3. \<lbrace>?P'3\<rbrace> do cap <- getSlotCap src;
y <- modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange cap of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> gsUntypedZeroRanges ks - {r}\<rparr>);
modify (\<lambda>ks. ks\<lparr>gsUntypedZeroRanges := case untypedZeroRange (capFreeIndex_update (\<lambda>_. idx) cap) of None \<Rightarrow> gsUntypedZeroRanges ks | Some r \<Rightarrow> insert r (gsUntypedZeroRanges ks)\<rparr>)
od \<lbrace>?B24\<rbrace>
 4. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (cte_wp_at' (\<lambda>_. True) 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> (\<exists>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>) \<and> (cte_wp_at' (\<lambda>_. True) 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> (\<exists>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>) \<and> (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>))))))) \<and> ?P'3 s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s \<and> (\<exists>ptr sz. pspace_no_overlap' ptr sz s \<and> idx \<le> 2 ^ sz \<and> cte_wp_at' ((\<lambda>c. isUntypedCap c \<and> capPtr c = ptr \<and> capBlockSize c = sz) \<circ> cteCap) src s) \<and> is_aligned (word_of_nat idx) minUntypedSizeBits \<and> descendants_of' src (ctes_of s) = {} \<Longrightarrow> (cte_wp_at' (\<lambda>_. True) src s \<longrightarrow> (\<exists>cte. cte_wp_at' ((=) cte) src s) \<and> (\<exists>cte. cte_wp_at' ((=) cte) src s \<and> (\<exists>cte. cte_wp_at' ((=) cte) src s) \<and> valid_cap' (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) s)) \<and> ((\<exists>cte. cte_wp_at' ((=) cte) src s) \<longrightarrow> (\<forall>cte. cte_wp_at' ((=) cte) src s \<longrightarrow> pspace_no_overlap' (capPtr (cteCap cte)) (capBlockSize (cteCap cte)) s \<and> valid_pspace' s \<and> cte_wp_at' (\<lambda>c. \<exists>idx'. cteCap c = capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) src s \<and> isUntypedCap (cteCap cte))) proof (prove)
goal (1 subgoal):
 1. \<And>s cte. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' (capPtr (cteCap cte)) (capBlockSize (cteCap cte)) s; idx \<le> 2 ^ capBlockSize (cteCap cte); ctes_of s src = Some cte; isUntypedCap (cteCap cte)\<rbrakk> \<Longrightarrow> valid_cap' (capFreeIndex_update (\<lambda>_. idx) (cteCap cte)) s \<and> (\<exists>idx'. cteCap cte = capFreeIndex_update (\<lambda>_. idx') (cteCap cte)) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x1 x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' (capPtr x1) (capBlockSize x1) s; idx \<le> 2 ^ capBlockSize x1; ctes_of s src = Some (CTE x1 x2); \<exists>d v0 v1 f. x1 = capability.UntypedCap d v0 v1 f; cte = CTE x1 x2\<rbrakk> \<Longrightarrow> valid_cap' (capFreeIndex_update (\<lambda>_. idx) x1) s \<and> (\<exists>idx'. x1 = capFreeIndex_update (\<lambda>_. idx') x1) proof (prove)
goal (1 subgoal):
 1. \<And>s cte x1 x2. \<lbrakk>valid_objs' s; pspace_aligned' s; pspace_distinct' s; no_0_obj' s; valid_mdb' s; is_aligned (word_of_nat idx) minUntypedSizeBits; descendants_of' src (ctes_of s) = {}; pspace_no_overlap' (capPtr x1) (capBlockSize x1) s; idx \<le> 2 ^ capBlockSize x1; ctes_of s src = Some (CTE x1 x2); \<exists>d v0 v1 f. x1 = capability.UntypedCap d v0 v1 f; cte = CTE x1 x2; valid_cap' x1 s\<rbrakk> \<Longrightarrow> valid_cap' (capFreeIndex_update (\<lambda>_. idx) x1) s \<and> (\<exists>idx'. x1 = capFreeIndex_update (\<lambda>_. idx') x1) proof (prove)
goal:
No subgoals!