theory Untyped_R

lemma createNewCaps_ranges:
  "\<lbrace>\<lambda>s. range_cover ptr sz (APIType_capBits ty us) n \<and> 0<n \<rbrace>
  createNewCaps ty ptr n us d
  \<lbrace>\<lambda>rv s. distinct_sets (map capRange rv)\<rbrace>" apply (rule hoare_assume_pre) apply (rule hoare_chain) apply (rule createNewCaps_range_helper) apply fastforce apply (clarsimp simp: distinct_sets_prop distinct_prop_map) apply (rule distinct_prop_distinct) apply simp apply (clarsimp simp: capRange_def simp del: Int_atLeastAtMost
                  dest!: less_two_pow_divD) apply (rule aligned_neq_into_no_overlap[simplified field_simps]) apply (rule notI) apply (erule(3) ptr_add_distinct_helper) apply (simp add:range_cover_def word_bits_def) apply (erule range_cover.range_cover_n_le(1)) apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]) apply (rule is_aligned_add_multI[OF _ le_refl refl]) apply (simp add:range_cover_def)+ apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]) apply (rule is_aligned_add_multI[OF _ le_refl refl]) apply (simp add:range_cover_def)+ done

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