theory Retype_AC

lemma retype_region_post_retype_invs_spec:
  "\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz
         and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}
         and region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1}
         and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s)
         and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us)
         and K (range_cover ptr sz (obj_bits_api ty us) n) \<rbrace>
   retype_region ptr n us ty dev
   \<lbrace>\<lambda>rv. post_retype_invs ty rv\<rbrace>" apply (rule hoare_pre) apply (wp retype_region_post_retype_invs) apply (clarsimp simp del: split_paired_Ex) apply (frule valid_cap_range_untyped[OF invs_valid_objs],simp) apply fastforce done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s) and K (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api ty us) n)\<rbrace> retype_region ptr n us ty dev \<lbrace>post_retype_invs ty\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> retype_region ptr n us ty dev \<lbrace>post_retype_invs ty\<rbrace>
 2. \<And>s. (invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s) and K (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api ty us) n)) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and caps_no_overlap ptr sz and pspace_no_overlap (up_aligned_area ptr sz) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s) and K (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr sz (obj_bits_api ty us) n)) s \<Longrightarrow> (invs and caps_no_overlap ptr ?sz4 and pspace_no_overlap (up_aligned_area ptr ?sz4) and caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} and region_in_kernel_window {ptr..(ptr && ~~ mask ?sz4) + 2 ^ ?sz4 - 1} and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz4 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and K (ty = CapTableObject \<longrightarrow> 0 < us) and K (range_cover ptr ?sz4 (obj_bits_api ty us) n)) s proof (prove)
goal (1 subgoal):
 1. \<And>s idx. \<lbrakk>invs s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s; ty = CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> \<Longrightarrow> caps_no_overlap ptr ?sz4 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz4) s \<and> region_in_kernel_window {ptr..(ptr && ~~ mask ?sz4) + 2 ^ ?sz4 - 1} s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz4 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> range_cover ptr ?sz4 (obj_bits_api ty us) n proof (prove)
goal (1 subgoal):
 1. \<And>s idx. \<lbrakk>invs s; caps_no_overlap ptr sz s; pspace_no_overlap (up_aligned_area ptr sz) s; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} s; region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s; ty = CapTableObject \<longrightarrow> 0 < us; range_cover ptr sz (obj_bits_api ty us) n; cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s\<rbrakk> \<Longrightarrow> caps_no_overlap ptr ?sz4 s \<and> pspace_no_overlap (up_aligned_area ptr ?sz4) s \<and> region_in_kernel_window {ptr..(ptr && ~~ mask ?sz4) + 2 ^ ?sz4 - 1} s \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr ?sz4 \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> range_cover ptr ?sz4 (obj_bits_api ty us) n proof (prove)
goal:
No subgoals!