theory Untyped_R

lemma createNewCaps_range_helper2:
  "\<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace>
     createNewCaps tp ptr n us d
   \<lbrace>\<lambda>rv s. \<forall>cp \<in> set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_strengthen_post) apply (rule createNewCaps_range_helper) apply (clarsimp simp: capRange_def ptr_add_def word_unat_power[symmetric]
                  simp del: atLeastatMost_subset_iff
                 dest!: less_two_pow_divD) apply (rule conjI) apply (rule is_aligned_no_overflow) apply (rule is_aligned_add_multI [OF _ _ refl]) apply (fastforce simp:range_cover_def) apply simp apply (rule range_subsetI) apply (rule machine_word_plus_mono_right_split[OF range_cover.range_cover_compare]) apply (assumption)+ apply (simp add:range_cover_def word_bits_def) apply (frule range_cover_cell_subset) apply (erule of_nat_mono_maybe[rotated]) apply (drule (1) range_cover.range_cover_n_less ) apply (clarsimp) apply (erule impE) apply (simp add:range_cover_def) apply (rule is_aligned_no_overflow) apply (rule is_aligned_add_multI[OF _ le_refl refl]) apply (fastforce simp:range_cover_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv s. \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n \<Longrightarrow> \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> createNewCaps tp ptr n us d \<lbrace>\<lambda>rv s. \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n \<Longrightarrow> \<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n\<rbrace> createNewCaps tp ptr n us d \<lbrace>?Q2 s\<rbrace>
 2. \<And>s rv sa. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n; ?Q2 s rv sa\<rbrakk> \<Longrightarrow> \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s rv sa. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n \<and> 0 < n; \<exists>capfn. rv = map capfn (map (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits tp us)) [0..<n]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us)\<rbrakk> \<Longrightarrow> \<forall>cp\<in>set rv. capRange cp \<noteq> {} \<and> capRange cp \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<and> {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 2 ^ APIType_capBits tp us) (APIType_capBits tp us)
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (3 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> is_aligned ptr (?m25 capfn x)
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> APIType_capBits tp us \<le> ?m25 capfn x
 3. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> APIType_capBits tp us \<le> APIType_capBits tp us
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (1 subgoal):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (4 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> range_cover ptr (?sz39 capfn x) (APIType_capBits tp us) (?n40 capfn x)
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> x < ?n40 capfn x
 3. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ?sz39 capfn x < word_bits
 4. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ?x44 capfn x < word_of_nat n
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; {ptr + ?x44 capfn x * 2 ^ APIType_capBits tp us..ptr + ?x44 capfn x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us\<rbrakk> \<Longrightarrow> n < 2 ^ LENGTH(32)
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; {ptr + word_of_nat x * 2 ^ APIType_capBits tp us..ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<and> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<and> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>is_aligned ptr (APIType_capBits tp us) \<and> sz < 32 \<and> APIType_capBits tp us \<le> sz \<and> n + unat (ptr && mask sz >> APIType_capBits tp us) \<le> 2 ^ (sz - APIType_capBits tp us); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<and> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>is_aligned ptr (APIType_capBits tp us) \<and> sz < 32 \<and> APIType_capBits tp us \<le> sz \<and> n + unat (ptr && mask sz >> APIType_capBits tp us) \<le> 2 ^ (sz - APIType_capBits tp us); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 2 ^ APIType_capBits tp us) (APIType_capBits tp us)
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<and> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (2 subgoals):
 1. \<And>capfn x. \<lbrakk>is_aligned ptr (APIType_capBits tp us) \<and> sz < 32 \<and> APIType_capBits tp us \<le> sz \<and> n + unat (ptr && mask sz >> APIType_capBits tp us) \<le> 2 ^ (sz - APIType_capBits tp us); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n\<rbrakk> \<Longrightarrow> is_aligned ptr (APIType_capBits tp us)
 2. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<and> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal (1 subgoal):
 1. \<And>capfn x. \<lbrakk>range_cover ptr sz (APIType_capBits tp us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits tp us; x < n; ptr \<le> ptr + word_of_nat x * 2 ^ APIType_capBits tp us \<and> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ APIType_capBits tp us + 2 ^ APIType_capBits tp us - 1 \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1 proof (prove)
goal:
No subgoals!