theory Untyped_AI

lemma (in Untyped_AI_arch) retype_region_caps_reserved:
  "\<lbrace>cte_wp_at (is_untyped_cap) p and caps_overlap_reserved {ptr..ptr + of_nat (n * 2 ^ obj_bits_api tp us) - 1}
  and K (range_cover ptr sz (obj_bits_api tp us) n) and pspace_no_overlap_range_cover ptr sz and valid_pspace \<rbrace>
  retype_region ptr n us tp dev
 \<lbrace>\<lambda>rv (s::('state_ext::state_ext) state). \<forall>y\<in>set rv. cte_wp_at (\<lambda>a. untyped_range (default_cap tp y us dev) \<inter> usable_untyped_range a = {}) p s\<rbrace>" apply (clarsimp simp: valid_def cte_wp_at_caps_of_state) apply (frule use_valid[OF _ retype_region_ranges']) apply fastforce apply (drule(1) bspec) 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 caps_overlap_reserved_def) apply (drule bspec) apply fastforce apply (clarsimp simp: cap_range_def) apply blast done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>cte_wp_at is_untyped_cap p and caps_overlap_reserved {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1} and K (range_cover ptr sz (obj_bits_api tp us) n) and pspace_no_overlap (up_aligned_area ptr sz) and valid_pspace\<rbrace> retype_region ptr n us tp dev \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. cte_wp_at (\<lambda>a. untyped_range (default_cap tp y us dev) \<inter> usable_untyped_range a = {}) 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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s\<rbrakk> \<Longrightarrow> K (range_cover ptr (?sz18 s a b y cap) (obj_bits_api tp us) n) 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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; \<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> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; \<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> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> range_cover ptr (?sz27 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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}\<rbrakk> \<Longrightarrow> pspace_no_overlap (up_aligned_area ptr (?sz27 s a b y cap)) s \<and> cte_wp_at ((=) cap) (?ptr27 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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}; cte_wp_at ((=) cap) (?ptr27 s a b y cap) b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}\<rbrakk> \<Longrightarrow> cte_wp_at ((=) cap) (?ptr27 s a b y cap) 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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}; cte_wp_at ((=) cap) (?ptr27 s a b y cap) b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_overlap_reserved {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} s; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat (n * 2 ^ obj_bits_api tp us) - 1}; cte_wp_at ((=) cap) p b\<rbrakk> \<Longrightarrow> \<exists>cap. caps_of_state b p = Some cap \<and> untyped_range (default_cap tp y us dev) \<inter> usable_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; \<forall>cap\<in>ran (caps_of_state s). is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} = {}; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}; caps_of_state b p = Some cap\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}; caps_of_state b p = Some cap\<rbrakk> \<Longrightarrow> ?cap32 s a b y cap \<in> ran (caps_of_state 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; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}; caps_of_state b p = Some cap; is_untyped_cap (?cap32 s a b y cap) \<longrightarrow> usable_untyped_range (?cap32 s a b y cap) \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} = {}\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; cap_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}; caps_of_state b p = Some cap; is_untyped_cap cap \<longrightarrow> usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} = {}\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp y us dev) \<inter> usable_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; caps_of_state s p = Some cap; is_untyped_cap cap; range_cover ptr sz (obj_bits_api tp us) n; pspace_no_overlap (up_aligned_area ptr sz) s; valid_pspace s; caps_of_state b p = Some cap; usable_untyped_range cap \<inter> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1} = {}; untyped_range (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}; obj_refs (default_cap tp y us dev) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ obj_bits_api tp us - 1}\<rbrakk> \<Longrightarrow> untyped_range (default_cap tp y us dev) \<inter> usable_untyped_range cap = {} proof (prove)
goal:
No subgoals!