theory Untyped_AI

lemma retype_region_ranges:
  "\<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. cap_range (default_cap tp y us dev) \<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) apply (frule use_valid[OF _ retype_region_ranges']) apply (fastforce simp: cte_wp_at_caps_of_state) apply (drule(1) bspec) apply (drule(1) subsetD) apply (rule_tac A = "{x..y}" for x y in subsetD[rotated]) apply assumption apply simp apply (erule subset_trans[OF range_cover_subset']) apply (frule use_valid[OF _ retype_region_ret]) apply simp apply fastforce apply (clarsimp simp: is_cap_simps) apply (erule order_trans[OF word_and_le2]) 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. cap_range (default_cap tp y us dev) \<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> cap_range (default_cap tp y us dev) \<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> cap_range (default_cap tp y us dev) \<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> cap_range (default_cap tp y us dev) \<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> cap_range (default_cap tp y us dev) \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev)\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev)\<rbrakk> \<Longrightarrow> K (range_cover ptr (?sz31 s a b y cap x) (obj_bits_api tp us) n) s
 2. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); \<forall>y\<in>set a. cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); \<forall>y\<in>set a. cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); x \<in> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> x \<in> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); x \<in> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> x \<in> {?xa46 s a b y cap x..?ya46 s a b y cap x}
 2. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); x \<in> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> {?xa46 s a b y cap x..?ya46 s a b y cap x} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); x \<in> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask (cap_bits cap)) + 2 ^ cap_bits cap - 1} \<subseteq> untyped_range cap proof (prove)
goal (3 subgoals):
 1. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> True
 2. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1; a = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> n \<noteq> 0
 3. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask (cap_bits cap)) + 2 ^ cap_bits cap - 1} \<subseteq> untyped_range cap proof (prove)
goal (2 subgoals):
 1. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1; a = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api tp us)) [0..<n]\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask (cap_bits cap)) + 2 ^ cap_bits cap - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y cap x. \<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; is_untyped_cap cap; obj_ref_of cap = ptr && ~~ mask (cap_bits cap); sz = cap_bits cap; caps_of_state b p = Some cap; x \<in> cap_range (default_cap tp y us dev); ptr \<le> x \<and> x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1\<rbrakk> \<Longrightarrow> {ptr..(ptr && ~~ mask (cap_bits cap)) + 2 ^ cap_bits cap - 1} \<subseteq> untyped_range cap proof (prove)
goal (1 subgoal):
 1. \<And>s a b y x xa deva f. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us tp dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr sz) s; caps_of_state s p = Some (UntypedCap deva (ptr && ~~ mask sz) sz f); valid_pspace s; caps_of_state b p = Some (UntypedCap deva (ptr && ~~ mask sz) sz f); x \<in> cap_range (default_cap tp y us dev); ptr \<le> x; x \<le> ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1; ptr \<le> xa; xa \<le> (ptr && ~~ mask sz) + 2 ^ sz - 1\<rbrakk> \<Longrightarrow> ptr && ~~ mask sz \<le> xa proof (prove)
goal:
No subgoals!