theory Untyped_AI

lemma retype_region_descendants_range_ret:
  "\<lbrace>\<lambda>s. (range_cover ptr sz (obj_bits_api ty us) n)
    \<and> pspace_no_overlap_range_cover ptr sz s
    \<and> valid_pspace s
    \<and> range_cover ptr sz (obj_bits_api ty us) n
    \<and> descendants_range_in {ptr..ptr + of_nat n * 2^(obj_bits_api ty us) - 1} cref s
  \<rbrace>
  retype_region ptr n us ty dev
          \<lbrace>\<lambda>rv (s::'state_ext state). \<forall>y\<in>set rv. descendants_range (default_cap ty y us dev) cref s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: valid_def) apply (frule retype_region_ret[unfolded valid_def,simplified,THEN spec,THEN bspec]) apply (clarsimp) apply (rename_tac x) apply (erule use_valid[OF _ retype_region_descendants_range]) apply (intro conjI,simp_all) apply (clarsimp simp: descendants_range_def descendants_range_in_def) apply (drule(1) bspec) apply (clarsimp simp: cte_wp_at_caps_of_state) apply (erule disjoint_subset2[rotated]) apply (frule(1) range_cover_subset) apply simp apply (erule subset_trans[rotated]) apply (subgoal_tac "ptr + of_nat x * 2 ^ obj_bits_api ty us
          \<le> ptr + of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1") prefer 2 apply (rule is_aligned_no_overflow) apply (rule is_aligned_add_multI) apply (fastforce simp: range_cover_def)+ apply (auto simp add: cap_range_def2 ptr_add_def obj_bits_api_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. range_cover ptr sz (obj_bits_api ty us) n \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. descendants_range (default_cap ty y us dev) cref s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. range_cover ptr sz (obj_bits_api ty us) n \<and> pspace_no_overlap (up_aligned_area ptr sz) s \<and> valid_pspace s \<and> range_cover ptr sz (obj_bits_api ty us) n \<and> descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s \<Longrightarrow> \<lbrace>(=) s\<rbrace> retype_region ptr n us ty dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. descendants_range (default_cap ty y us dev) cref s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us ty dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s\<rbrakk> \<Longrightarrow> descendants_range (default_cap ty y us dev) cref b proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<lbrakk>(a, b) \<in> fst (retype_region ptr n us ty dev s); y \<in> set a; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s; case (a, b) of (r, s') \<Rightarrow> r = map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n]\<rbrakk> \<Longrightarrow> descendants_range (default_cap ty y us dev) cref b proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>(map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n], b) \<in> fst (retype_region ptr n us ty dev s); pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s; x < n\<rbrakk> \<Longrightarrow> descendants_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) cref b proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>(map (\<lambda>p. ptr_add ptr (p * 2 ^ obj_bits_api ty us)) [0..<n], b) \<in> fst (retype_region ptr n us ty dev s); pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s; x < n\<rbrakk> \<Longrightarrow> descendants_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) cref b proof (prove)
goal (1 subgoal):
 1. \<And>s b x. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s; x < n\<rbrakk> \<Longrightarrow> descendants_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) cref s \<and> pspace_no_overlap (up_aligned_area ptr (?sz21 s b x)) s \<and> valid_pspace s \<and> range_cover ptr (?sz21 s b x) (obj_bits_api ty us) n proof (prove)
goal (1 subgoal):
 1. \<And>s x. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; descendants_range_in {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} cref s; x < n\<rbrakk> \<Longrightarrow> descendants_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) cref s proof (prove)
goal (1 subgoal):
 1. \<And>s x a b. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; \<forall>p'\<in>descendants_of cref (cdt s). cte_wp_at (\<lambda>c. cap_range c \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}) p' s; x < n; (a, b) \<in> descendants_of cref (cdt s)\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) = {}) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s x a b. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); cte_wp_at (\<lambda>c. cap_range c \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}) (a, b) s\<rbrakk> \<Longrightarrow> cte_wp_at (\<lambda>c. cap_range c \<inter> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) = {}) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; cap_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} = {}\<rbrakk> \<Longrightarrow> cap_range cap \<inter> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1}\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1}
 2. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1 proof (prove)
goal (2 subgoals):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1
 2. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> is_aligned (ptr + word_of_nat x * 2 ^ obj_bits_api ty us) (obj_bits_api ty us)
 2. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (4 subgoals):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> is_aligned ptr (?m44 s x a b cap)
 2. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> obj_bits_api ty us \<le> ?m44 s x a b cap
 3. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap\<rbrakk> \<Longrightarrow> obj_bits_api ty us = obj_bits_api ty us
 4. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s x a b cap. \<lbrakk>pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; range_cover ptr sz (obj_bits_api ty us) n; x < n; (a, b) \<in> descendants_of cref (cdt s); caps_of_state s (a, b) = Some cap; ptr + word_of_nat x * 2 ^ obj_bits_api ty us \<le> ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1\<rbrakk> \<Longrightarrow> cap_range (default_cap ty (ptr_add ptr (x * 2 ^ obj_bits_api ty us)) us dev) \<subseteq> {ptr + word_of_nat x * 2 ^ obj_bits_api ty us..ptr + word_of_nat x * 2 ^ obj_bits_api ty us + 2 ^ obj_bits_api ty us - 1} proof (prove)
goal:
No subgoals!