theory Untyped_AI

lemma cte_wp_at_caps_descendants_range_inI:
  "\<lbrakk> invs s;cte_wp_at (\<lambda>c. c = UntypedCap dev (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 s" apply (frule invs_mdb) apply (frule(1) le_mask_le_2p) apply (clarsimp simp: descendants_range_in_def cte_wp_at_caps_of_state ) apply (frule(1) descendants_of_cte_at) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (drule untyped_cap_descendants_range[rotated]) apply simp+ apply (simp add: invs_valid_pspace) apply (clarsimp simp: cte_wp_at_caps_of_state) 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. c = UntypedCap dev (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 s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = UntypedCap dev (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 s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>invs s; cte_wp_at (\<lambda>c. c = UntypedCap dev (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 s proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); cte_wp_at (\<lambda>_. True) (a, b) s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state s (a, b) = Some cap \<and> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>invs s; caps_of_state s cref = Some (UntypedCap dev (ptr && ~~ mask sz) sz idx); idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (5 subgoals):
 1. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> is_untyped_cap (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> valid_mdb s
 3. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> ?q11 a b cap \<in> descendants_of cref (cdt s)
 4. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> valid_pspace s
 5. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; cte_wp_at (\<lambda>c. cap_range c \<inter> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}) (?q11 a b cap) s\<rbrakk> \<Longrightarrow> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (2 subgoals):
 1. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> valid_pspace s
 2. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; cte_wp_at (\<lambda>c. cap_range c \<inter> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}) (a, b) s\<rbrakk> \<Longrightarrow> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; cte_wp_at (\<lambda>c. cap_range c \<inter> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) = {}) (a, b) s\<rbrakk> \<Longrightarrow> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; cap_range cap \<inter> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> cap_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<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>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; 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>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; 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>a b cap. \<lbrakk>invs s; idx \<le> unat (ptr && mask sz); sz < word_bits; valid_mdb s; idx < 2 ^ sz; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr && mask sz proof (prove)
goal:
No subgoals!