theory Retype_R

lemma retype_region2_ext_retype_region:
  "(retype_region ptr numObjects o_bits type dev :: (obj_ref list, det_ext) s_monad)
 = (do ptrs \<leftarrow> retype_region2 ptr numObjects o_bits type dev;
       retype_region2_extra_ext ptrs type;
       return ptrs
    od)" apply (clarsimp simp: retype_region_def retype_region2_def when_def bind_assoc) apply safe defer apply (simp add: retype_region2_extra_ext_def) apply (subst retype_region_ext_modify_kheap_futz'[simplified bind_assoc]) apply (subst retype_region2_ext_retype_region_ext_futz[symmetric]) apply (simp add: bind_assoc) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. retype_region ptr numObjects o_bits type dev = do ptrs <- retype_region2 ptr numObjects o_bits type dev;
retype_region2_extra_ext ptrs type;
return ptrs
od proof (prove)
goal (1 subgoal):
 1. (type \<noteq> Structures_A.apiobject_type.Untyped \<longrightarrow> do x <- gets kheap;
xa <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od = do x <- gets kheap;
xa <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od) \<and> (type = Structures_A.apiobject_type.Untyped \<longrightarrow> return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects]) = do y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects]) Structures_A.apiobject_type.Untyped;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects])
od) proof (prove)
goal (2 subgoals):
 1. type \<noteq> Structures_A.apiobject_type.Untyped \<Longrightarrow> do x <- gets kheap;
xa <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od = do x <- gets kheap;
xa <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od
 2. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects]) = do y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects]) Structures_A.apiobject_type.Untyped;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects])
od proof (prove)
goal (2 subgoals):
 1. type = Structures_A.apiobject_type.Untyped \<Longrightarrow> return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects]) = do y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects]) Structures_A.apiobject_type.Untyped;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api Structures_A.apiobject_type.Untyped o_bits)) [0..<numObjects])
od
 2. type \<noteq> Structures_A.apiobject_type.Untyped \<Longrightarrow> do x <- gets kheap;
xa <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od = do x <- gets kheap;
xa <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od proof (prove)
goal (1 subgoal):
 1. type \<noteq> Structures_A.apiobject_type.Untyped \<Longrightarrow> do x <- gets kheap;
xa <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od = do x <- gets kheap;
xa <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
y <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od proof (prove)
goal (1 subgoal):
 1. type \<noteq> Structures_A.apiobject_type.Untyped \<Longrightarrow> do x <- gets kheap;
xa <- retype_region_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od = do x <- gets kheap;
xa <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
xa <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od proof (prove)
goal (1 subgoal):
 1. type \<noteq> Structures_A.apiobject_type.Untyped \<Longrightarrow> do x <- gets kheap;
xa <- do _ <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type
od;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od = do x <- gets kheap;
xa <- retype_region2_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
xa <- retype_region2_extra_ext (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) type;
y <- modify (kheap_update (\<lambda>y. foldr (\<lambda>p kh. kh(p \<mapsto> default_object type dev o_bits)) (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects]) x));
return (map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api type o_bits)) [0..<numObjects])
od proof (prove)
goal:
No subgoals!