theory Untyped_AI

lemma retype_region_distinct_sets:
  "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) n)\<rbrace>
  retype_region ptr n us tp dev
  \<lbrace>\<lambda>rv s. distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs rv))\<rbrace>" apply (simp add: distinct_sets_prop) apply (rule hoare_gen_asm[where P'="\<top>", simplified]) apply (rule hoare_strengthen_post [OF retype_region_ret]) apply (rule distinct_prop_prefixE [rotated]) apply (rule map_snd_zip_prefix_help [unfolded less_eq_list_def]) apply (clarsimp simp: retype_addrs_def distinct_prop_map) apply (rule distinct_prop_distinct) apply simp apply (subgoal_tac  "of_nat y * (2::machine_word) ^ obj_bits_api tp us \<noteq> of_nat x * 2 ^ obj_bits_api tp us") apply (case_tac tp) defer apply (simp add:cap_range_def ptr_add_def)+ apply (clarsimp simp: ptr_add_def word_unat_power[symmetric]
                      shiftl_t2n[simplified mult.commute, symmetric]) apply (erule(2) of_nat_shift_distinct_helper[where 'a=machine_word_len and n = "obj_bits_api tp us"]) apply simp apply (simp add:range_cover_def) apply (erule range_cover.range_cover_n_le) apply (clarsimp simp: add_diff_eq[symmetric]
                  simp del: Int_atLeastAtMost
                  dest!: less_two_pow_divD) apply (simp add: obj_bits_api_def ptr_add_def shiftl_t2n[simplified mult.commute, symmetric] del: Int_atLeastAtMost) apply (rule aligned_neq_into_no_overlap) apply simp apply (simp_all add:range_cover_def shiftl_t2n mult.commute) apply (rule is_aligned_add_multI[OF _ le_refl refl]) apply (simp add:range_cover_def)+ 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>K (range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. distinct_sets (map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs rv))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>y. range_cover ptr sz (obj_bits_api tp us) n\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. distinct_prop (\<lambda>x y. x \<inter> y = {}) (map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs rv))\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api tp us) n \<Longrightarrow> \<lbrace>\<lambda>_. True\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. distinct_prop (\<lambda>x y. x \<inter> y = {}) (map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs rv))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs rv)) proof (prove)
goal (2 subgoals):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> prefix (map (\<lambda>tup. cap_range (default_cap tp (snd tup) us dev)) (zip xs rv)) (?ys5 rv s)
 2. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (?ys5 rv s) proof (prove)
goal (1 subgoal):
 1. \<And>rv s. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> distinct_prop (\<lambda>x y. x \<inter> y = {}) (map (\<lambda>x. cap_range (default_cap tp x us dev)) rv) proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api tp us) n \<Longrightarrow> distinct_prop (\<lambda>x y. cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}) [0..<n] proof (prove)
goal (2 subgoals):
 1. range_cover ptr sz (obj_bits_api tp us) n \<Longrightarrow> distinct [0..<n]
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = TCBObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 3. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = EndpointObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 4. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = NotificationObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 5. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = CapTableObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 6. \<And>x y x6. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = ArchObject x6\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 7. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us proof (prove)
goal (7 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = TCBObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = EndpointObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 3. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = NotificationObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 4. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = CapTableObject\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 5. \<And>x y x6. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = ArchObject x6\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {}
 6. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us
 7. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x < n; y < n; x \<noteq> y\<rbrakk> \<Longrightarrow> word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x < n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> False
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (4 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> word_of_nat x << obj_bits_api tp us = word_of_nat y << obj_bits_api tp us
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> obj_bits_api tp us < LENGTH(32)
 3. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - obj_bits_api tp us)
 4. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> obj_bits_api tp us < LENGTH(32)
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - obj_bits_api tp us)
 3. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; y < n; x \<noteq> y; word_of_nat y << obj_bits_api tp us = word_of_nat x << obj_bits_api tp us\<rbrakk> \<Longrightarrow> n \<le> 2 ^ (LENGTH(32) - obj_bits_api tp us)
 2. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; x \<in> set [0..<n]; y \<in> set [0..<n]; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api tp us \<noteq> word_of_nat x * 2 ^ obj_bits_api tp us; tp = Untyped\<rbrakk> \<Longrightarrow> cap_range (default_cap tp (ptr_add ptr (x * 2 ^ obj_bits_api tp us)) us dev) \<inter> cap_range (default_cap tp (ptr_add ptr (y * 2 ^ obj_bits_api tp us)) us dev) = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz (obj_bits_api Untyped us) n; x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ obj_bits_api Untyped us \<noteq> word_of_nat x * 2 ^ obj_bits_api Untyped us; tp = Untyped\<rbrakk> \<Longrightarrow> {ptr_add ptr (x * 2 ^ obj_bits_api Untyped us)..ptr_add ptr (x * 2 ^ obj_bits_api Untyped us) + (2 ^ us - 1)} \<inter> {ptr_add ptr (y * 2 ^ obj_bits_api Untyped us)..ptr_add ptr (y * 2 ^ obj_bits_api Untyped us) + (2 ^ us - 1)} = {} proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>range_cover ptr sz us n; x < n; y < n; x \<noteq> y; word_of_nat y << us \<noteq> word_of_nat x << us; tp = Untyped\<rbrakk> \<Longrightarrow> {ptr + (word_of_nat x << us)..ptr + (word_of_nat x << us) + (2 ^ us - 1)} \<inter> {ptr + (word_of_nat y << us)..ptr + (word_of_nat y << us) + (2 ^ us - 1)} = {} proof (prove)
goal (3 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz us n; x < n; y < n; x \<noteq> y; word_of_nat y << us \<noteq> word_of_nat x << us; tp = Untyped\<rbrakk> \<Longrightarrow> ptr + (word_of_nat x << us) \<noteq> ptr + (word_of_nat y << us)
 2. \<And>x y. \<lbrakk>range_cover ptr sz us n; x < n; y < n; x \<noteq> y; word_of_nat y << us \<noteq> word_of_nat x << us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat x << us)) us
 3. \<And>x y. \<lbrakk>range_cover ptr sz us n; x < n; y < n; x \<noteq> y; word_of_nat y << us \<noteq> word_of_nat x << us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat y << us)) us proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>range_cover ptr sz us n; x < n; y < n; x \<noteq> y; word_of_nat y << us \<noteq> word_of_nat x << us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat x << us)) us
 2. \<And>x y. \<lbrakk>range_cover ptr sz us n; x < n; y < n; x \<noteq> y; word_of_nat y << us \<noteq> word_of_nat x << us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + (word_of_nat y << us)) us proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr us \<and> sz < 32 \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ us \<noteq> word_of_nat x * 2 ^ us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 2 ^ us) us
 2. \<And>x y. \<lbrakk>is_aligned ptr us \<and> sz < 32 \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ us \<noteq> word_of_nat x * 2 ^ us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat y * 2 ^ us) us proof (prove)
goal (2 subgoals):
 1. \<And>x y. \<lbrakk>is_aligned ptr us \<and> sz < 32 \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ us \<noteq> word_of_nat x * 2 ^ us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned ptr us
 2. \<And>x y. \<lbrakk>is_aligned ptr us \<and> sz < 32 \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ us \<noteq> word_of_nat x * 2 ^ us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat y * 2 ^ us) us proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_aligned ptr us \<and> sz < 32 \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ us \<noteq> word_of_nat x * 2 ^ us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat y * 2 ^ us) us proof (prove)
goal (1 subgoal):
 1. \<And>x y. \<lbrakk>is_aligned ptr us \<and> sz < 32 \<and> us \<le> sz \<and> n + unat (ptr && mask sz >> us) \<le> 2 ^ (sz - us); x < n; y < n; x \<noteq> y; word_of_nat y * 2 ^ us \<noteq> word_of_nat x * 2 ^ us; tp = Untyped\<rbrakk> \<Longrightarrow> is_aligned ptr us proof (prove)
goal:
No subgoals!