theory Untyped_R

lemma cte_wp_at_caps_descendants_range_inI':
  "\<lbrakk>invs' s; cte_wp_at' (\<lambda>c. (cteCap c) = capability.UntypedCap
                                            d (ptr && ~~ mask sz) sz idx) cref s;
    idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk>
   \<Longrightarrow> descendants_range_in' {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}
         cref (ctes_of s)" apply (frule invs_mdb') apply (frule(1) le_mask_le_2p) apply (clarsimp simp: descendants_range_in'_def cte_wp_at_ctes_of) apply (drule untypedCap_descendants_range'[rotated]) apply (simp add: isCap_simps)+ apply (simp add: invs_valid_pspace') apply (clarsimp simp: cte_wp_at_ctes_of) apply (erule disjoint_subset2[rotated]) apply clarsimp apply (rule le_plus'[OF word_and_le2]) apply simp apply (erule word_of_nat_le) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs' s; cte_wp_at' (\<lambda>c. cteCap c = capability.UntypedCap d (ptr && ~~ mask sz) sz idx) cref s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> descendants_range_in' {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); ctes_of s cref = Some cte; cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> capRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (5 subgoals):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> isUntypedCap (cteCap cte)
 2. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> valid_mdb' s
 3. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> ?q14 p' cte c n \<in> descendants_of' cref (ctes_of s)
 4. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> valid_pspace' s
 5. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> usableUntypedRange (cteCap cte) = {}) (?q14 p' cte c n) s\<rbrakk> \<Longrightarrow> capRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> valid_pspace' s
 2. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> usableUntypedRange (cteCap cte) = {}) p' s\<rbrakk> \<Longrightarrow> capRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); cte_wp_at' (\<lambda>c. capRange (cteCap c) \<inter> usableUntypedRange (cteCap cte) = {}) p' s\<rbrakk> \<Longrightarrow> capRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); capRange c \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n)\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr - (ptr && ~~ mask sz) proof (prove)
goal (1 subgoal):
 1. \<And>p' cte c n. \<lbrakk>invs' s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb' s; idx < 2 ^ sz; p' \<in> descendants_of' cref (ctes_of s); cteCap cte = capability.UntypedCap d (ptr && ~~ mask sz) sz idx; ctes_of s p' = Some (CTE c n); ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr && mask sz proof (prove)
goal:
No subgoals!