theory Retype_R

lemma corres_retype:
  assumes         not_zero: "n \<noteq> 0"
  and         aligned: "is_aligned ptr (objBitsKO ko + gbits)"
  and    obj_bits_api: "obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits"
  and              tp: "APIType_map2 ty \<in> no_gs_types"
  and              ko: "makeObjectKO dev ty = Some ko"
  and             orr: "obj_bits_api (APIType_map2 ty) us \<le> sz \<Longrightarrow>
                        obj_relation_retype (default_object (APIType_map2 ty) dev us) ko"
  and           cover: "range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n"
  shows "corres (=)
  (\<lambda>s. valid_pspace s \<and> pspace_no_overlap_range_cover ptr sz s
     \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s)
  (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s
       \<and> (\<exists>val. ko = injectKO val))
  (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)" apply (rule corres_guard_imp) apply (rule_tac F = "(\<exists>val. ko = injectKO val)" in corres_gen_asm2) apply (erule exE) apply (rule corres_rel_imp) apply (rule corres_retype'[where g=id and ty=ty and sz = sz,OF not_zero aligned _ _ _ ko
           ,simplified update_gs_id[OF tp] modify_id_return,simplified]) using assms apply (simp_all add: objBits_def no_gs_types_def) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (\<lambda>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val)) (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val) \<Longrightarrow> ?Q' s proof (prove)
goal (3 subgoals):
 1. \<exists>val. ko = injectKO val \<Longrightarrow> corres (=) ?Q ?P'4 (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val) \<Longrightarrow> (?P'4 and (\<lambda>s. \<exists>val. ko = injectKO val)) s proof (prove)
goal (3 subgoals):
 1. \<And>val. ko = injectKO val \<Longrightarrow> corres (=) ?Q ?P'4 (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)
 2. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q s
 3. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val) \<Longrightarrow> (?P'4 and (\<lambda>s. \<exists>val. ko = injectKO val)) s proof (prove)
goal (4 subgoals):
 1. \<And>val. ko = injectKO val \<Longrightarrow> corres (?r'8 val) ?Q ?P'4 (retype_region2 ptr n us (APIType_map2 ty) dev) (createObjects ptr n ko gbits)
 2. \<And>val x y. \<lbrakk>ko = injectKO val; ?r'8 val x y\<rbrakk> \<Longrightarrow> x = y
 3. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> ?Q s
 4. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val) \<Longrightarrow> (?P'4 and (\<lambda>s. \<exists>val. ko = injectKO val)) s proof (prove)
goal (8 subgoals):
 1. \<And>val. ko = injectKO val \<Longrightarrow> obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits
 2. \<And>val. ko = injectKO val \<Longrightarrow> (sz < obj_bits_api (APIType_map2 ty) us) = (sz < objBitsKO ko + gbits)
 3. \<And>val. \<lbrakk>ko = injectKO val; APIType_map2 ty = Structures_A.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 4. \<And>val. \<lbrakk>ko = injectKO val; obj_bits_api (APIType_map2 ty) us \<le> sz\<rbrakk> \<Longrightarrow> obj_relation_retype (default_object (APIType_map2 ty) dev us) ko
 5. \<And>val. ko = injectKO val \<Longrightarrow> range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n
 6. \<And>val x y. \<lbrakk>ko = injectKO val; y = x\<rbrakk> \<Longrightarrow> x = y
 7. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s
 8. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val) \<Longrightarrow> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>s. \<exists>val. ko = injectKO val)) s proof (prove)
using this:
n \<noteq> 0
is_aligned ptr (objBitsKO ko + gbits)
obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits
APIType_map2 ty \<in> no_gs_types
makeObjectKO dev ty = Some ko
obj_bits_api (APIType_map2 ty) us \<le> sz \<Longrightarrow> obj_relation_retype (default_object (APIType_map2 ty) dev us) ko
range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n

goal (8 subgoals):
 1. \<And>val. ko = injectKO val \<Longrightarrow> obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits
 2. \<And>val. ko = injectKO val \<Longrightarrow> (sz < obj_bits_api (APIType_map2 ty) us) = (sz < objBitsKO ko + gbits)
 3. \<And>val. \<lbrakk>ko = injectKO val; APIType_map2 ty = Structures_A.apiobject_type.CapTableObject\<rbrakk> \<Longrightarrow> 0 < us
 4. \<And>val. \<lbrakk>ko = injectKO val; obj_bits_api (APIType_map2 ty) us \<le> sz\<rbrakk> \<Longrightarrow> obj_relation_retype (default_object (APIType_map2 ty) dev us) ko
 5. \<And>val. ko = injectKO val \<Longrightarrow> range_cover ptr sz (obj_bits_api (APIType_map2 ty) us) n
 6. \<And>val x y. \<lbrakk>ko = injectKO val; y = x\<rbrakk> \<Longrightarrow> x = y
 7. \<And>s. valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s \<Longrightarrow> valid_pspace s \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_mdb s \<and> valid_etcbs s \<and> valid_list s
 8. \<And>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val) \<Longrightarrow> ((\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s) and (\<lambda>s. \<exists>val. ko = injectKO val)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> (\<exists>val. ko = injectKO val); 0 < n; is_aligned ptr (objBitsKO ko + gbits); obj_bits_api (APIType_map2 ty) us = objBitsKO ko + gbits; APIType_map2 ty \<noteq> Structures_A.apiobject_type.CapTableObject \<and> APIType_map2 ty \<noteq> ArchObject SmallPageObj \<and> APIType_map2 ty \<noteq> ArchObject LargePageObj \<and> APIType_map2 ty \<noteq> ArchObject SectionObj \<and> APIType_map2 ty \<noteq> ArchObject SuperSectionObj; makeObjectKO dev ty = Some ko; objBitsKO ko + gbits \<le> sz \<Longrightarrow> obj_relation_retype (default_object (APIType_map2 ty) dev us) ko; range_cover ptr sz (objBitsKO ko + gbits) n\<rbrakk> \<Longrightarrow> \<exists>val. ko = injectKO val proof (prove)
goal:
No subgoals!