theory Untyped_AI

lemma valid_untyped_cap_inc:
  "\<lbrakk>s \<turnstile> UntypedCap dev (ptr&&~~ mask sz) sz idx;
    idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n\<rbrakk>
   \<Longrightarrow> s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz
                          (unat ((ptr && mask sz) + of_nat n * 2 ^ sb))" apply (clarsimp simp: valid_cap_def cap_aligned_def valid_untyped_def simp del: usable_untyped_range.simps) apply (intro conjI allI impI) apply (elim allE conjE impE) apply simp apply simp apply (erule disjoint_subset[rotated]) apply (frule(1) le_mask_le_2p[OF _
                     range_cover.sz(1)[where 'a=machine_word_len, folded word_bits_def]]) apply clarsimp apply (rule word_plus_mono_right) apply (rule word_of_nat_le) apply (simp add: unat_of_nat_eq[where 'a=machine_word_len] range_cover_unat field_simps) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask[OF le_refl]]) apply (simp add: word_less_nat_alt) apply (simp add: range_cover_unat range_cover.unat_of_nat_shift shiftl_t2n field_simps) apply (subst add.commute) apply (simp add: range_cover.range_cover_compare_bound) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz idx; idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n\<rbrakk> \<Longrightarrow> s \<turnstile> UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> (\<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<inter> obj_range p obj = {}) \<and> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<inter> obj_range p obj = {}
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (4 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> kheap s (?p16 p obj) = Some (?obj17 p obj)
 2. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range (?p16 p obj) (?obj17 p obj) \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 3. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range (?p16 p obj) (?obj17 p obj) \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range (?p16 p obj) (?obj17 p obj) = {}\<rbrakk> \<Longrightarrow> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<inter> obj_range p obj = {}
 4. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<inter> obj_range p obj = {}
 3. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}\<rbrakk> \<Longrightarrow> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<inter> obj_range p obj = {}
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<subseteq> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz\<rbrakk> \<Longrightarrow> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz (unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb))) \<subseteq> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx)
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + word_of_nat idx \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb)
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> word_of_nat idx \<le> (ptr && mask sz) + word_of_nat n * 2 ^ sb
 2. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb)
 3. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (3 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> idx \<le> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb)
 2. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb)
 3. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb)
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (2 subgoals):
 1. \<And>p obj. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; untyped_min_bits \<le> sz; ptr && ~~ mask sz \<noteq> 0; kheap s p = Some obj; obj_range p obj \<inter> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}; obj_range p obj \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2 ^ sz - 1}; idx < 2 ^ sz; unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) < 2 ^ sz; (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat n * 2 ^ sb < 2 ^ sz
 2. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> usable_untyped_range (UntypedCap dev (ptr && ~~ mask sz) sz idx) \<inter> obj_range p obj = {}; untyped_min_bits \<le> sz; idx \<le> 2 ^ sz; ptr && ~~ mask sz \<noteq> 0\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat n * 2 ^ sb) \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> unat (ptr && mask sz) + n * 2 ^ sb \<le> 2 ^ sz proof (prove)
goal (1 subgoal):
 1. \<lbrakk>idx \<le> unat (ptr && mask sz); range_cover ptr sz sb n; sz < word_bits; \<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> n * 2 ^ sb + unat (ptr && mask sz) \<le> 2 ^ sz proof (prove)
goal:
No subgoals!