theory Retype_AI

lemma retype_region_global_refs_disjoint:
  "\<lbrace>(\<lambda>s::'state_ext state. {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> global_refs s = {})
            and K (range_cover ptr sz (obj_bits_api apiobject_type obits) n)\<rbrace>
     retype_region ptr n obits apiobject_type dev
   \<lbrace>\<lambda>r s. global_refs s \<inter> set r = {}\<rbrace>" apply (rule hoare_gen_asm) apply (rule hoare_lift_Pf3[where f=global_refs]) apply (rule hoare_assume_pre) apply (clarsimp simp: Int_commute) apply (rule hoare_chain) apply(rule retype_region_ret) apply simp apply (erule disjoint_subset2[rotated]) apply (rule subsetI, simp only: mask_in_range[symmetric]) apply (clarsimp simp: ptr_add_def) apply (intro conjI) apply (rule machine_word_plus_mono_right_split[where sz = sz]) apply (erule(1) range_cover.range_cover_compare) apply (simp add:range_cover_def word_bits_def) apply (subst p_assoc_help) apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz"]) apply (subst add.commute) apply (subst add.assoc) apply (rule word_plus_mono_right) apply (simp add:word_le_nat_alt) apply (rule le_trans[OF unat_plus_gt]) apply (subst unat_minus_one[OF power_not_zero]) apply (simp add:range_cover_def) apply (frule(1) range_cover.range_cover_compare) apply (clarsimp simp:range_cover_def le_m1_iff_lt power_not_zero nat_le_Suc_less_imp) apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask,OF le_refl ]) apply (simp add:range_cover_def) apply (simp add:range_cover_def) apply wp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> global_refs s = {}) and K (range_cover ptr sz (obj_bits_api apiobject_type obits) n)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>r s. global_refs s \<inter> set r = {}\<rbrace> proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> global_refs s = {}\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>r s. global_refs s \<inter> set r = {}\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> x = {}\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>a b. x \<inter> set a = {}\<rbrace>
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> x = {}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> x = {}\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>a b. x \<inter> set a = {}\<rbrace>
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. True\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>a b. x \<inter> set a = {}\<rbrace>
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> \<lbrace>?P10 x\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>?Q10 x\<rbrace>
 2. \<And>x s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; True\<rbrakk> \<Longrightarrow> ?P10 x s
 3. \<And>x rv s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; ?Q10 x rv s\<rbrakk> \<Longrightarrow> x \<inter> set rv = {}
 4. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; True\<rbrakk> \<Longrightarrow> True
 2. \<And>x rv s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api apiobject_type obits)) [0..<n]\<rbrakk> \<Longrightarrow> x \<inter> set rv = {}
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x rv s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api apiobject_type obits)) [0..<n]\<rbrakk> \<Longrightarrow> x \<inter> set rv = {}
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x rv s. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api apiobject_type obits)) [0..<n]\<rbrakk> \<Longrightarrow> set rv \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x rv s xa. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; rv = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api apiobject_type obits)) [0..<n]; xa \<in> set (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api apiobject_type obits)) [0..<n])\<rbrakk> \<Longrightarrow> xa \<in> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<and> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr \<le> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) < 2 ^ sz
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> sz < word_bits
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 4. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + (ptr && ~~ mask sz) + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + (ptr && mask sz) + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> (ptr && ~~ mask sz) + ((ptr && mask sz) + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> (ptr && mask sz) + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits \<le> 2 ^ sz - 1
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> unat ((ptr && mask sz) + word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) \<le> unat (2 ^ sz - 1)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) \<le> unat (2 ^ sz - 1)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> sz < LENGTH(32)
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) \<le> unat (2 ^ sz) - 1
 3. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 4. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) \<le> unat (2 ^ sz) - 1
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n; unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) < 2 ^ sz\<rbrakk> \<Longrightarrow> unat (ptr && mask sz) + unat (word_of_nat x * 2 ^ obj_bits_api apiobject_type obits) \<le> unat (2 ^ sz) - 1
 2. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 3. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> (ptr && ~~ mask sz) + (2 ^ sz - 1)
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrakk>range_cover ptr sz (obj_bits_api apiobject_type obits) n; x < n\<rbrakk> \<Longrightarrow> 2 ^ sz - 1 < 2 ^ sz
 2. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. range_cover ptr sz (obj_bits_api apiobject_type obits) n \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>P. is_aligned ptr (obj_bits_api apiobject_type obits) \<and> sz < 32 \<and> obj_bits_api apiobject_type obits \<le> sz \<and> n + unat (ptr && mask sz >> obj_bits_api apiobject_type obits) \<le> 2 ^ (sz - obj_bits_api apiobject_type obits) \<Longrightarrow> \<lbrace>\<lambda>s. P (global_refs s)\<rbrace> retype_region ptr n obits apiobject_type dev \<lbrace>\<lambda>_ s. P (global_refs s)\<rbrace> proof (prove)
goal:
No subgoals!