theory Retype_IF

lemma retype_region_reads_respects_g:
  "reads_respects_g aag l
     ((\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and>
                 (idx \<le> unat (ptr && mask sz) \<or> pspace_no_overlap_range_cover ptr sz s)) and
      invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects))
     (retype_region ptr num_objects o_bits type dev)" apply (rule equiv_valid_guard_imp[OF reads_respects_g[OF retype_region_reads_respects]]) apply (rule doesnt_touch_globalsI) apply (rule hoare_weaken_pre[OF retype_region_globals_equiv]) apply simp apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. reads_equiv_valid_g_inv (affects_equiv aag l) aag ((\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> pspace_no_overlap (up_aligned_area ptr sz) s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) (retype_region ptr num_objects o_bits type dev) proof (prove)
goal (2 subgoals):
 1. doesnt_touch_globals ?Q1 (retype_region ptr num_objects o_bits type dev)
 2. \<And>s. ((\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> pspace_no_overlap (up_aligned_area ptr sz) s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>globals_equiv st and ?Q1\<rbrace> retype_region ptr num_objects o_bits type dev \<lbrace>\<lambda>_. globals_equiv st\<rbrace>
 2. \<And>s. ((\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> pspace_no_overlap (up_aligned_area ptr sz) s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (2 subgoals):
 1. \<And>st s. (globals_equiv st and ?Q1) s \<Longrightarrow> (globals_equiv st and invs and (\<lambda>s. \<exists>i. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask (?sz8 st)) (?sz8 st) i) (?slot8 st) s \<and> (i \<le> unat (ptr && mask (?sz8 st)) \<or> pspace_no_overlap (up_aligned_area ptr (?sz8 st)) s)) and K (range_cover ptr (?sz8 st) (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) s
 2. \<And>s. ((\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> pspace_no_overlap (up_aligned_area ptr sz) s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) s \<Longrightarrow> ((\<lambda>_. True) and ?Q1) s proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>idx. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask sz) sz idx) slot s \<and> (idx \<le> unat (ptr && mask sz) \<or> pspace_no_overlap (up_aligned_area ptr sz) s)) and invs and K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. invs s \<and> (\<exists>i. cte_wp_at (\<lambda>c. c = UntypedCap dev (ptr && ~~ mask ?sz16) ?sz16 i) ?slot12 s \<and> (i \<le> unat (ptr && mask ?sz16) \<or> pspace_no_overlap (up_aligned_area ptr ?sz16) s)) \<and> range_cover ptr ?sz16 (obj_bits_api type o_bits) num_objects \<and> 0 < num_objects)) s proof (prove)
goal:
No subgoals!