theory Untyped_AI

lemma retype_region_ranges_obj_bits_api:
  "\<lbrace>cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz
          \<and> obj_ref_of c = ptr && ~~ mask sz) p and
    pspace_no_overlap_range_cover ptr sz and
    valid_pspace and K (range_cover ptr sz (obj_bits_api tp us) n)
   \<rbrace>
  retype_region ptr n us tp dev
   \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. cte_wp_at
           (\<lambda>c. {y .. y + 2 ^ (obj_bits_api tp us) - 1} \<subseteq> untyped_range c )
           p s\<rbrace>" apply (clarsimp simp:cte_wp_at_caps_of_state valid_def) apply (frule_tac P1 = "(=) cap" in use_valid[OF _ retype_region_cte_at_other]) apply simp apply (fastforce simp:cte_wp_at_caps_of_state) apply (clarsimp simp:cte_wp_at_caps_of_state del: subsetI) apply (frule use_valid[OF _ retype_region_ret_folded], simp+) apply (rule order_trans, erule(1) retype_addrs_range_subset) apply (clarsimp simp: is_cap_simps word_and_le2 del: subsetI) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at (\<lambda>c. is_untyped_cap c \<and> cap_bits c = sz \<and> obj_ref_of c = ptr && ~~ mask sz) p and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace and K (range_cover ptr sz (obj_bits_api tp us) n)\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. cte_wp_at (\<lambda>c. {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range c) p s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap\<rbrakk> \<Longrightarrow> range_cover ptr (?sz23 s a b y cap) (obj_bits_api tp us) n
 2. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr (?sz23 s a b y cap)) s \<and> cte_wp_at ((=) cap) (?ptr23 s a b y cap) s \<and> valid_pspace s
 3. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; cte_wp_at ((=) cap) (?ptr23 s a b y cap) b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s \<and> cte_wp_at ((=) cap) (?ptr23 s a b y cap) s \<and> valid_pspace s
 2. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; cte_wp_at ((=) cap) (?ptr23 s a b y cap) b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; cte_wp_at ((=) cap) p b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap\<rbrakk> \<Longrightarrow> {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap. \<lbrakk>(retype_addrs ptr tp n us, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set (retype_addrs ptr tp n us); pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; a = retype_addrs ptr tp n us\<rbrakk> \<Longrightarrow> {y..y + 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap. \<lbrakk>(retype_addrs ptr tp n us, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set (retype_addrs ptr tp n us); pspace_no_overlap (up_aligned_area ptr (cap_bits cap)) s; caps_of_state s p = Some cap; valid_pspace s; range_cover ptr (cap_bits cap) (obj_bits_api tp us) n; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; a = retype_addrs ptr tp n us\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask (cap_bits cap)) + 2 ^ cap_bits cap - 1} \<subseteq> untyped_range cap proof (prove)
goal:
No subgoals!