theory Untyped_DR

lemma generate_object_ids_exec:
  notes [simp del] = order_class.Icc_eq_Icc
  shows
  "dcorres r P P' (f  (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g
   \<Longrightarrow> dcorres r  P
  (K ((ty = Structures_A.Untyped \<longrightarrow> (untyped_min_bits \<le> us))
   \<and> range_cover ptr sz (obj_bits_api ty us) n
   \<and> is_aligned ptr (obj_bits_api ty us)
   \<and> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range )
  and (pspace_no_overlap_range_cover ptr sz) and valid_pspace and valid_idle and P')
  (do
    t \<leftarrow> generate_object_ids n (translate_object_type ty) free_range;
    f t
  od) g" apply (clarsimp simp: generate_object_ids_def bind_assoc) apply (rule dcorres_absorb_get_l) apply (rule corres_guard_imp) apply (rule_tac x = "(map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))"
                    in select_pick_corres_asm[rotated]) apply (rule corres_symb_exec_l) apply (rule_tac F = "rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)"
                        in corres_gen_asm) apply clarify apply assumption apply (clarsimp simp:return_def exs_valid_def) apply (rule hoare_vcg_if_split) apply (wp|simp)+ apply (intro conjI impI) apply (clarsimp simp:distinct_map distinct_retype_addrs) apply (clarsimp simp:inj_on_def) apply (clarsimp simp:retype_transform_obj_ref_def split: if_split_asm) apply (frule range_cover.sz(1)) apply (drule(1) retype_addrs_aligned[where sz = sz]) apply (clarsimp simp:word_bits_def) apply (erule range_cover.sz) apply (drule(1) retype_addrs_aligned[where sz = sz]) apply (clarsimp simp:word_bits_def) apply (erule range_cover.sz) apply (subst (asm) range_eq) apply (clarsimp simp: obj_bits_api_def) apply simp apply (clarsimp simp:retype_transform_obj_ref_def split:if_splits) apply (frule range_cover.sz(1)) apply (drule(1) retype_addrs_aligned[where sz = sz]) apply (clarsimp simp:word_bits_def) apply (erule range_cover.sz) apply (drule(1) retype_addrs_aligned[where sz = sz]) apply (clarsimp simp:word_bits_def) apply (erule range_cover.sz) apply (clarsimp simp:obj_bits_api_def order_class.Icc_eq_Icc) apply (drule_tac x = b in neg_mask_mono_le[where n = us]) apply (drule_tac x = a in neg_mask_mono_le[where n = us]) apply (clarsimp simp: neg_mask_add_2p_helper dest!: range_cover_sz') apply (clarsimp) apply (intro conjI) apply (clarsimp simp:retype_transform_obj_ref_def) apply (rule is_aligned_no_overflow) apply (drule(1) retype_addrs_aligned[where sz = sz]) apply (clarsimp simp:word_bits_def dest!:range_cover.sz(1)) apply (erule range_cover.sz) apply (simp add:obj_bits_api_def) apply (erule(2) subset_trans[OF retype_transform_ref_subseteq_strong]) apply (rule retype_transform_obj_ref_available) apply simp+ apply (clarsimp simp:retype_transform_obj_ref_def translate_object_type_def) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g \<Longrightarrow> dcorres r P (K ((ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') (generate_object_ids n (translate_object_type ty) free_range >>= f) g proof (prove)
goal (1 subgoal):
 1. dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g \<Longrightarrow> dcorres r P ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') (do x <- get;
x <- select {xa. distinct xa \<and> (\<forall>a\<in>set xa. \<forall>b\<in>set xa. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set xa. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects x -` {Some cdl_object.Untyped}) \<and> n = length xa};
(if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) x else return x) >>= f
od) g proof (prove)
goal (1 subgoal):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> dcorres r ((=) (transform s')) ((=) s') (do x <- select {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x};
(if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) x else return x) >>= f
od) g proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> dcorres r (?Q8 s') (?Q'8 s') (do x <- select {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x};
(if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) x else return x) >>= f
od) g
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'8 s' s proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> dcorres r (?Q8 s') (?Q'8 s') ((if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) >>= f) g
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'8 s' s proof (prove)
goal (7 subgoals):
 1. \<And>s' rv. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> dcorres r (?Q13 s' rv) (?Q'8 s') (f rv) g
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; ?Q8 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s'\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>?Q13 s'\<rbrace>
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; False\<rbrakk> \<Longrightarrow> no_fail (?Q8 s') (if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)))
 5. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'8 s' s proof (prove)
goal (7 subgoals):
 1. \<And>s' rv. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)\<rbrakk> \<Longrightarrow> dcorres r (?P18 s' rv) (?Q'8 s') (f rv) g
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; ?Q8 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s'\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>\<lambda>rv. ?P18 s' rv and (\<lambda>s. rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))\<rbrace>
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; False\<rbrakk> \<Longrightarrow> no_fail (?Q8 s') (if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)))
 5. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'8 s' s proof (prove)
goal (7 subgoals):
 1. \<And>s' rv. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); P' s'; valid_idle s'; valid_pspace s'; pspace_no_overlap (up_aligned_area ptr sz) s'; ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range\<rbrakk> \<Longrightarrow> dcorres r (?P18 s' (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) (?Q'8 s') (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; ?Q8 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s'\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>\<lambda>rv. ?P18 s' rv and (\<lambda>s. rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))\<rbrace>
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; False\<rbrakk> \<Longrightarrow> no_fail (?Q8 s') (if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)))
 5. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> ?Q'8 s' s proof (prove)
goal (6 subgoals):
 1. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; ?Q8 s' s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s'\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>\<lambda>rv. P and (\<lambda>s. rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))\<rbrace>
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; False\<rbrakk> \<Longrightarrow> no_fail (?Q8 s') (if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)))
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> \<lbrace>?Q8 s'\<rbrace> if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>\<lambda>rv. P and (\<lambda>s. rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))\<rbrace>
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; False\<rbrakk> \<Longrightarrow> no_fail (?Q8 s') (if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)))
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> ?Q8 s' s
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; translate_object_type ty \<noteq> UntypedType\<rbrakk> \<Longrightarrow> \<lbrace>?Q33 s'\<rbrace> return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>\<lambda>rv. P and (\<lambda>s. rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))\<rbrace>
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; \<not> translate_object_type ty \<noteq> UntypedType\<rbrakk> \<Longrightarrow> \<lbrace>?R33 s'\<rbrace> return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<lbrace>\<lambda>rv. P and (\<lambda>s. rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))\<rbrace>
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; False\<rbrakk> \<Longrightarrow> no_fail (\<lambda>s. (translate_object_type ty \<noteq> UntypedType \<longrightarrow> ?Q33 s' s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> ?R33 s' s)) (if translate_object_type ty \<noteq> UntypedType then return $ map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) else return (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)))
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'\<rbrakk> \<Longrightarrow> map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) \<in> {x. distinct x \<and> (\<forall>a\<in>set x. \<forall>b\<in>set x. a \<noteq> b \<longrightarrow> a \<inter> b = {}) \<and> (\<forall>y\<in>set x. y \<noteq> {} \<and> y \<subseteq> free_range \<and> y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}) \<and> n = length x}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> ?Q33 s' s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> ?R33 s' s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> distinct (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) \<and> (\<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}) \<and> (\<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped})
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> distinct (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> inj_on (retype_transform_obj_ref ty us) (set (retype_addrs ptr ty n us))
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; x \<in> set (retype_addrs ptr ty n us); y \<in> set (retype_addrs ptr ty n us); retype_transform_obj_ref ty us x = retype_transform_obj_ref ty us y\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; x \<in> set (retype_addrs ptr apiobject_type.Untyped n us); y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; x \<in> set (retype_addrs ptr apiobject_type.Untyped n us); y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (7 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 3. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 5. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 2. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (7 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 3. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us); is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 5. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 2. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us); is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {x..x + 2 ^ us - 1} = {y..y + 2 ^ us - 1}; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us); is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s' x y. \<lbrakk>sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us); is_aligned y (obj_bits_api apiobject_type.Untyped us); dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> x \<le> x + 2 ^ us - 1
 2. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; x = y \<and> x + 2 ^ us - 1 = y + 2 ^ us - 1; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us); is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' x y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; x = y \<and> x + 2 ^ us - 1 = y + 2 ^ us - 1; sz < LENGTH(32); is_aligned x (obj_bits_api apiobject_type.Untyped us); is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> x = y
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>a\<in>set (retype_addrs ptr ty n us). \<forall>b\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us a \<noteq> retype_transform_obj_ref ty us b \<longrightarrow> retype_transform_obj_ref ty us a \<inter> retype_transform_obj_ref ty us b = {}
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; a \<in> set (retype_addrs ptr apiobject_type.Untyped n us); b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; a \<in> set (retype_addrs ptr apiobject_type.Untyped n us); b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 3. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> False
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 2. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> False
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; b \<in> set (retype_addrs ptr apiobject_type.Untyped n us); {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 3. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us); is_aligned b (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> False
 4. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 2. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us); is_aligned b (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> False
 3. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; {a..a + 2 ^ us - 1} \<noteq> {b..b + 2 ^ us - 1}; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; a \<le> a + 2 ^ us - 1; b \<le> b + 2 ^ us - 1; sz < LENGTH(32); is_aligned a (obj_bits_api apiobject_type.Untyped us); is_aligned b (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz us n; is_aligned ptr us; {ptr..ptr + word_of_nat n * 2 ^ us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; a \<noteq> b; a \<le> b + 2 ^ us - 1; b \<le> a + 2 ^ us - 1; sz < 32; is_aligned a us; is_aligned b us\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz us n; is_aligned ptr us; {ptr..ptr + word_of_nat n * 2 ^ us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; a \<noteq> b; a \<le> b + 2 ^ us - 1; sz < 32; is_aligned a us; is_aligned b us; b && ~~ mask us \<le> a + 2 ^ us - 1 && ~~ mask us\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' a b. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz us n; is_aligned ptr us; {ptr..ptr + word_of_nat n * 2 ^ us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; a \<noteq> b; sz < 32; is_aligned a us; is_aligned b us; b && ~~ mask us \<le> a + 2 ^ us - 1 && ~~ mask us; a && ~~ mask us \<le> b + 2 ^ us - 1 && ~~ mask us\<rbrakk> \<Longrightarrow> False
 2. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (3 subgoals):
 1. \<And>s'. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'\<rbrakk> \<Longrightarrow> \<forall>y\<in>set (retype_addrs ptr ty n us). retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (3 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<noteq> {} \<and> retype_transform_obj_ref ty us y \<subseteq> free_range \<and> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<noteq> {}
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> y \<le> y + 2 ^ us - 1
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); y \<in> set (retype_addrs ptr apiobject_type.Untyped n us); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> is_aligned y us
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (7 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> sz < word_bits
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> is_aligned y us
 4. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 5. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (6 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped\<rbrakk> \<Longrightarrow> obj_bits_api apiobject_type.Untyped us \<le> sz
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> is_aligned y us
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 4. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 6. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (5 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref apiobject_type.Untyped us) (retype_addrs ptr apiobject_type.Untyped n us))) g; P (transform s'); untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api apiobject_type.Untyped us) n; is_aligned ptr (obj_bits_api apiobject_type.Untyped us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api apiobject_type.Untyped us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'; ty = apiobject_type.Untyped; is_aligned y (obj_bits_api apiobject_type.Untyped us)\<rbrakk> \<Longrightarrow> is_aligned y us
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 5. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (4 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> free_range
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 4. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (3 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> cdl_objects (transform s') -` {Some cdl_object.Untyped}
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 3. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (8 subgoals):
 1. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area (?ptr174 s' y) (?sz174 s' y)) (?s'174 s' y)
 2. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> transform s' = transform (?s'174 s' y)
 3. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> valid_pspace (?s'174 s' y)
 4. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> valid_idle (?s'174 s' y)
 5. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> range_cover (?ptr174 s' y) (?sz174 s' y) (obj_bits_api ty us) (?n174 s' y)
 6. \<And>s' y. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); y \<in> set (retype_addrs ptr ty n us); ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us; range_cover ptr sz (obj_bits_api ty us) n; is_aligned ptr (obj_bits_api ty us); {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range; pspace_no_overlap (up_aligned_area ptr sz) s'; valid_pspace s'; valid_idle s'; P' s'\<rbrakk> \<Longrightarrow> y \<in> set (retype_addrs (?ptr174 s' y) ty (?n174 s' y) us)
 7. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; transform s' = s\<rbrakk> \<Longrightarrow> (translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s) \<and> (\<not> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (P and (\<lambda>s. map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us) = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) s)
 8. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (2 subgoals):
 1. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P s; (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range \<and> pspace_no_overlap (up_aligned_area ptr sz) s' \<and> valid_pspace s' \<and> valid_idle s' \<and> P' s'; transform s' = s\<rbrakk> \<Longrightarrow> translate_object_type ty \<noteq> UntypedType \<longrightarrow> (\<forall>x\<in>set (retype_addrs ptr ty n us). {pick (retype_transform_obj_ref ty us x)} = retype_transform_obj_ref ty us x)
 2. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal (1 subgoal):
 1. \<And>s' s. \<lbrakk>dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g; P (transform s'); ((\<lambda>y. (ty = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> is_aligned ptr (obj_bits_api ty us) \<and> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and valid_idle and P') s'; s' = s\<rbrakk> \<Longrightarrow> P' s proof (prove)
goal:
No subgoals!