theory Untyped_DR

lemma retype_region_dcorres:
  "dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv'
                       \<and> rv' = retype_addrs ptr type n us)
       \<top>
  (\<lambda>s. pspace_no_overlap_range_cover ptr sz s \<and> invs s
  \<and> range_cover ptr sz (obj_bits_api type us) n
  \<and> (type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us)
  \<and> (type = Structures_A.CapTableObject \<longrightarrow> us \<noteq> 0))
  (Untyped_D.retype_region
  us (translate_object_type type) (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)))
  (Retype_A.retype_region ptr n us type dev)" supply if_cong[cong] apply (simp add: retype_region_def Untyped_D.retype_region_def
              split del: if_split) apply (clarsimp simp:when_def generate_object_ids_def bind_assoc
                  split del:if_split) apply (simp add:retype_addrs_fold split del:if_split) apply (case_tac "type = Structures_A.Untyped") apply (rule corres_guard_imp) apply (simp add:translate_object_type_def) apply (intro conjI impI ballI | simp)+ apply (simp add:gets_fold_into_modify retype_addrs_fold retype_region_ext_def modify_modify
                   create_objects_def) apply (rule dcorres_expand_pfx) apply clarsimp apply (rule corres_guard_imp) apply (rule corres_split) apply (rule_tac r = dc and Q = \<top> and Q' = "(=) s'" in corres_guard_imp) apply (clarsimp simp: transform_def bind_def simpler_modify_def corres_underlying_def
           transform_current_thread_def transform_cdt_def transform_asid_table_def) apply (rule ext) apply (clarsimp simp:foldr_upd_app_if foldr_fun_upd_value restrict_map_def map_add_def
                              transform_objects_def retype_transform_obj_ref_def image_def) apply (subgoal_tac "idle_thread s' \<notin> set (retype_addrs ptr type n us)") apply (subgoal_tac "type = Structures_A.CapTableObject \<longrightarrow> us \<noteq> 0") apply (clarsimp simp:transform_default_object translate_object_type_not_untyped) defer apply clarsimp apply (frule invs_valid_idle,clarsimp simp:valid_idle_def pred_tcb_at_def obj_at_def) apply (erule(3) pspace_no_overlapC) apply clarsimp apply simp apply assumption apply (rule corres_trivial) apply simp apply wp+ apply fastforce apply simp apply (case_tac type, simp_all add:translate_object_type_def) apply (rename_tac aobject_type) apply (case_tac aobject_type,simp_all) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> us \<noteq> 0)) (Untyped_D.retype_region us (translate_object_type type) (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (Retype_A.retype_region ptr n us type dev) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> us \<noteq> 0)) (Untyped_D.retype_region us (translate_object_type type) (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (Retype_A.retype_region ptr n us type dev) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- when (type \<noteq> apiobject_type.Untyped) (do kh <- gets kheap;
y <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type us)) [0..<n]) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type us)) [0..<n]) kh))
od);
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type us)) [0..<n])
od) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type us)) [0..<n]) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type us)) [0..<n]) kh))
od else return ();
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type us)) [0..<n])
od) proof (prove)
goal (1 subgoal):
 1. dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od else return ();
return (retype_addrs ptr type n us)
od) proof (prove)
goal (2 subgoals):
 1. type = apiobject_type.Untyped \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od else return ();
return (retype_addrs ptr type n us)
od)
 2. type \<noteq> apiobject_type.Untyped \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od else return ();
return (retype_addrs ptr type n us)
od) proof (prove)
goal (4 subgoals):
 1. type = apiobject_type.Untyped \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) ?Q5 ?Q'5 (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od else return ();
return (retype_addrs ptr type n us)
od)
 2. \<And>s. \<lbrakk>type = apiobject_type.Untyped; True\<rbrakk> \<Longrightarrow> ?Q5 s
 3. \<And>s. \<lbrakk>type = apiobject_type.Untyped; pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)\<rbrakk> \<Longrightarrow> ?Q'5 s
 4. type \<noteq> apiobject_type.Untyped \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od else return ();
return (retype_addrs ptr type n us)
od) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>type = apiobject_type.Untyped; True\<rbrakk> \<Longrightarrow> ?Q5 s
 2. \<And>s. \<lbrakk>type = apiobject_type.Untyped; pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)\<rbrakk> \<Longrightarrow> ?Q'5 s
 3. type \<noteq> apiobject_type.Untyped \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us) \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- if translate_object_type type \<noteq> UntypedType then do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od else return ();
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- if type \<noteq> apiobject_type.Untyped then do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od else return ();
return (retype_addrs ptr type n us)
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- do current_domain <- gets cdl_current_domain;
create_objects (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us)) (Types_D.default_object (translate_object_type type) us current_domain)
od;
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 2. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (do y <- modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>);
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s));
return (retype_addrs ptr type n us)
od)
 2. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; s = transform s'; True; pspace_no_overlap (up_aligned_area ptr sz) s' \<and> invs s' \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) ((=) s) ((=) s') (do y <- modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>);
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s));
return (retype_addrs ptr type n us)
od)
 2. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (2 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) ((=) (transform s')) ((=) s') (do y <- modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>);
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s));
return (retype_addrs ptr type n us)
od)
 2. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (4 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?Q27 s') (?Q'27 s') (do y <- modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>);
return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))
od) (do y <- modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s));
return (retype_addrs ptr type n us)
od)
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> ?Q27 s' s
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> ?Q'27 s' s
 4. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (7 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> dcorres (?r'31 s') (?P31 s') (?P'31 s') (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>)) (modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)))
 2. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?r'31 s' y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 3. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 4. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 5. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 6. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 7. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (9 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> dcorres dc (\<lambda>_. True) ((=) s') (modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>)) (modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)))
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (9 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s')) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s'))) (retype_addrs ptr type n us) (ekheap s')) s')) = (\<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cur_domain s') else transform_objects s' x)
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (9 subgoals):
 1. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> transform_objects (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s')) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s'))) (retype_addrs ptr type n us) (ekheap s')) s')) x = (if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cur_domain s') else transform_objects s' x)
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (9 subgoals):
 1. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> (x \<in> set (retype_addrs ptr type n us) \<longrightarrow> (x \<noteq> idle_thread s' \<longrightarrow> Some (transform_object (machine_state s') x (default_ext type (cur_domain s')) (Retype_A.default_object type dev us)) = Types_D.default_object (translate_object_type type) us (cur_domain s')) \<and> (x = idle_thread s' \<longrightarrow> idle_thread s' \<in> set (retype_addrs ptr type n us) \<longrightarrow> None = Types_D.default_object (translate_object_type type) us (cur_domain s'))) \<and> (x \<notin> set (retype_addrs ptr type n us) \<longrightarrow> x = idle_thread s' \<longrightarrow> idle_thread s' \<in> set (retype_addrs ptr type n us) \<longrightarrow> None = Types_D.default_object (translate_object_type type) us (cur_domain s'))
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (10 subgoals):
 1. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> (x \<in> set (retype_addrs ptr type n us) \<longrightarrow> (x \<noteq> idle_thread s' \<longrightarrow> Some (transform_object (machine_state s') x (default_ext type (cur_domain s')) (Retype_A.default_object type dev us)) = Types_D.default_object (translate_object_type type) us (cur_domain s')) \<and> (x = idle_thread s' \<longrightarrow> idle_thread s' \<in> set (retype_addrs ptr type n us) \<longrightarrow> None = Types_D.default_object (translate_object_type type) us (cur_domain s'))) \<and> (x \<notin> set (retype_addrs ptr type n us) \<longrightarrow> x = idle_thread s' \<longrightarrow> idle_thread s' \<in> set (retype_addrs ptr type n us) \<longrightarrow> None = Types_D.default_object (translate_object_type type) us (cur_domain s'))
 2. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> idle_thread s' \<notin> set (retype_addrs ptr type n us)
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 5. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 7. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 9. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 10. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (11 subgoals):
 1. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us); type = CapTableObject \<longrightarrow> us \<noteq> 0\<rbrakk> \<Longrightarrow> (x \<in> set (retype_addrs ptr type n us) \<longrightarrow> (x \<noteq> idle_thread s' \<longrightarrow> Some (transform_object (machine_state s') x (default_ext type (cur_domain s')) (Retype_A.default_object type dev us)) = Types_D.default_object (translate_object_type type) us (cur_domain s')) \<and> (x = idle_thread s' \<longrightarrow> idle_thread s' \<in> set (retype_addrs ptr type n us) \<longrightarrow> None = Types_D.default_object (translate_object_type type) us (cur_domain s'))) \<and> (x \<notin> set (retype_addrs ptr type n us) \<longrightarrow> x = idle_thread s' \<longrightarrow> idle_thread s' \<in> set (retype_addrs ptr type n us) \<longrightarrow> None = Types_D.default_object (translate_object_type type) us (cur_domain s'))
 2. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0
 3. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> idle_thread s' \<notin> set (retype_addrs ptr type n us)
 4. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 5. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 6. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 7. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 8. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 9. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 10. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0
 2. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> idle_thread s' \<notin> set (retype_addrs ptr type n us)
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 4. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 5. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 7. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 9. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 10. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od) proof (prove)
goal (10 subgoals):
 1. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> idle_thread s' \<notin> set (retype_addrs ptr type n us)
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 10. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (10 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<in> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> False
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 10. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (10 subgoals):
 1. \<And>s' tcb. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread_ptr \<in> set (retype_addrs ptr type n us); idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> False
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 10. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (10 subgoals):
 1. \<And>s' tcb. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread_ptr \<in> set (retype_addrs ptr type n us); idle_thread s' = idle_thread_ptr; kheap s' idle_thread_ptr = Some (TCB tcb); idle (tcb_state tcb); tcb_bound_notification tcb = None; valid_arch_idle (tcb_iarch tcb)\<rbrakk> \<Longrightarrow> valid_pspace s'
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 4. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 6. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 8. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 9. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 10. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (9 subgoals):
 1. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P31 s' s\<rbrakk> \<Longrightarrow> True
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 3. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 4. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 5. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 6. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 7. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 8. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 9. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (8 subgoals):
 1. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; ?P'31 s' s\<rbrakk> \<Longrightarrow> s' = s
 2. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 3. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 4. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 5. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 6. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> (?P'31 s' and ?Q'31 s') s
 7. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 8. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (7 subgoals):
 1. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (?R31 s' y) (?R'31 s' ya) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 2. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>?R31 s'\<rbrace>
 3. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>?R'31 s'\<rbrace>
 4. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 5. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'31 s') s
 6. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 7. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (7 subgoals):
 1. \<And>s' y ya. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; dc y ya\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>_. True) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (return (retype_addrs ptr type n us))
 2. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>\<lambda>y _. True\<rbrace>
 3. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>\<lambda>ya _. True\<rbrace>
 4. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 5. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'31 s') s
 6. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 7. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (6 subgoals):
 1. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q31 s'\<rbrace> modify (\<lambda>s. s\<lparr>cdl_objects := \<lambda>x. if {x} \<in> retype_transform_obj_ref type us ` set (retype_addrs ptr type n us) then Types_D.default_object (translate_object_type type) us (cdl_current_domain s) else cdl_objects s x\<rparr>) \<lbrace>\<lambda>y _. True\<rbrace>
 2. \<And>s'. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us\<rbrakk> \<Longrightarrow> \<lbrace>?Q'31 s'\<rbrace> modify (\<lambda>s. update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) (kheap s)) (ekheap_update (\<lambda>_. foldr (\<lambda>p ekh. ekh(p := default_ext type (cur_domain s))) (retype_addrs ptr type n us) (ekheap s)) s)) \<lbrace>\<lambda>ya _. True\<rbrace>
 3. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and ?Q31 s') s
 4. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and ?Q'31 s') s
 5. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 6. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (4 subgoals):
 1. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; transform s' = s\<rbrakk> \<Longrightarrow> (?P31 s' and (\<lambda>s. True)) s
 2. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and (\<lambda>s. True)) s
 3. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 4. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (3 subgoals):
 1. \<And>s' s. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; s' = s\<rbrakk> \<Longrightarrow> ((=) s' and (\<lambda>s. True)) s
 2. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 3. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (2 subgoals):
 1. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type = UntypedType\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' \<and> rv' = retype_addrs ptr type n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api type us) n \<and> (type = CapTableObject \<longrightarrow> 0 < us)) (return (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr type n us) type;
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object type dev us)) (retype_addrs ptr type n us) kh))
od;
return (retype_addrs ptr type n us)
od)
 2. \<And>s' x. \<lbrakk>type \<noteq> apiobject_type.Untyped; translate_object_type type \<noteq> UntypedType; pspace_no_overlap (up_aligned_area ptr sz) s'; invs s'; range_cover ptr sz (obj_bits_api type us) n; type = CapTableObject \<longrightarrow> 0 < us; idle_thread s' \<notin> set (retype_addrs ptr type n us)\<rbrakk> \<Longrightarrow> type = CapTableObject \<longrightarrow> us \<noteq> 0 proof (prove)
goal (1 subgoal):
 1. \<And>x6. \<lbrakk>(case x6 of SmallPageObj \<Rightarrow> FrameType 12 | LargePageObj \<Rightarrow> FrameType 16 | SectionObj \<Rightarrow> FrameType 20 | SuperSectionObj \<Rightarrow> FrameType 24 | PageTableObj \<Rightarrow> PageTableType | PageDirectoryObj \<Rightarrow> PageDirectoryType | ASIDPoolObj \<Rightarrow> AsidPoolType) = UntypedType; type = ArchObject x6\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref (ArchObject x6) us) rv' \<and> rv' = retype_addrs ptr (ArchObject x6) n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api (ArchObject x6) us) n) (return (map (retype_transform_obj_ref (ArchObject x6) us) (retype_addrs ptr (ArchObject x6) n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr (ArchObject x6) n us) (ArchObject x6);
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object (ArchObject x6) dev us)) (retype_addrs ptr (ArchObject x6) n us) kh))
od;
return (retype_addrs ptr (ArchObject x6) n us)
od) proof (prove)
goal (1 subgoal):
 1. \<And>aobject_type. \<lbrakk>(case aobject_type of SmallPageObj \<Rightarrow> FrameType 12 | LargePageObj \<Rightarrow> FrameType 16 | SectionObj \<Rightarrow> FrameType 20 | SuperSectionObj \<Rightarrow> FrameType 24 | PageTableObj \<Rightarrow> PageTableType | PageDirectoryObj \<Rightarrow> PageDirectoryType | ASIDPoolObj \<Rightarrow> AsidPoolType) = UntypedType; type = ArchObject aobject_type\<rbrakk> \<Longrightarrow> dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref (ArchObject aobject_type) us) rv' \<and> rv' = retype_addrs ptr (ArchObject aobject_type) n us) (\<lambda>_. True) (\<lambda>s. pspace_no_overlap (up_aligned_area ptr sz) s \<and> invs s \<and> range_cover ptr sz (obj_bits_api (ArchObject aobject_type) us) n) (return (map (retype_transform_obj_ref (ArchObject aobject_type) us) (retype_addrs ptr (ArchObject aobject_type) n us))) (do y <- do kh <- gets kheap;
y <- retype_region_ext (retype_addrs ptr (ArchObject aobject_type) n us) (ArchObject aobject_type);
modify (update_kheap (foldr (\<lambda>p kh. kh(p \<mapsto> Retype_A.default_object (ArchObject aobject_type) dev us)) (retype_addrs ptr (ArchObject aobject_type) n us) kh))
od;
return (retype_addrs ptr (ArchObject aobject_type) n us)
od) proof (prove)
goal:
No subgoals!