theory Untyped_AI

lemma cte_wp_at_pspace_no_overlapI:
  "\<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> pspace_no_overlap_range_cover ptr sz s" apply (clarsimp simp: cte_wp_at_caps_of_state) apply (frule caps_of_state_valid_cap) apply (simp add: invs_valid_objs) apply (clarsimp simp: valid_cap_def valid_untyped_def) apply (unfold pspace_no_overlap_def) apply (intro allI impI) apply (drule spec)+ apply (erule(1) impE) apply (simp only: obj_range_def[symmetric] p_assoc_help[symmetric]) apply (frule(1) le_mask_le_2p) apply (rule ccontr) apply (erule impE) apply (rule ccontr) apply simp apply (drule disjoint_subset2[rotated,
      where B'="{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"]) apply clarsimp apply (rule word_and_le2) apply simp apply clarsimp apply (drule_tac A'="{ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}"
        in disjoint_subset[rotated]) apply clarsimp apply (rule le_plus'[OF word_and_le2]) apply simp apply (erule word_of_nat_le) apply blast 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> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (1 subgoal):
 1. \<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\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (2 subgoals):
 1. \<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\<rbrakk> \<Longrightarrow> valid_objs s
 2. \<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; s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (1 subgoal):
 1. \<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; s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (1 subgoal):
 1. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr sz) s proof (prove)
goal (1 subgoal):
 1. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> \<forall>x ko. kheap s x = Some ko \<longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; kheap s (?p12 x ko) = Some (?obj14 x ko) \<longrightarrow> obj_range (?p12 x ko) (?obj14 x ko) \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range (?p12 x ko) (?obj14 x ko) \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range (?p12 x ko) (?obj14 x ko) = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> {x..x + (2 ^ obj_bits ko - 1)} \<inter> up_aligned_area ptr sz = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; \<not> obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> ptr
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<and> (if idx < 2 ^ sz then {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} else {}) \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {(ptr && ~~ mask sz) + word_of_nat idx..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> ptr
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr - (ptr && ~~ mask sz)
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; ptr \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> ptr && mask sz
 2. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x ko. \<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; cap_aligned (UntypedCap dev (ptr && ~~ mask sz) sz idx); untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s x = Some ko; idx < 2 ^ sz; obj_range x ko \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range x ko \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> obj_range x ko = {}\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!