theory Untyped_R

lemma createNewCaps_descendants_range_ret':
 "\<lbrace>\<lambda>s.  (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n)
        \<and> pspace_aligned' s \<and> pspace_distinct' s
        \<and> pspace_no_overlap' ptr sz s
        \<and> descendants_range_in' {ptr..ptr + of_nat n * 2^(APIType_capBits ty us) - 1} cref (ctes_of s)\<rbrace>
   createNewCaps ty ptr n us d
  \<lbrace> \<lambda>rv s. \<forall>y\<in>set rv. descendants_range' y cref (ctes_of s)\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp: valid_def) apply (frule use_valid[OF _ createNewCaps_range_helper]) apply simp apply (erule use_valid[OF _ createNewCaps_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_ctes_of) apply (erule disjoint_subset2[rotated]) apply (drule(1) range_cover_subset) apply simp apply (simp add:capRange_def ptr_add_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s)\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. descendants_range' y cref (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. (range_cover ptr sz (APIType_capBits ty us) n \<and> 0 < n) \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s) \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. descendants_range' y cref (ctes_of s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<lbrakk>(a, b) \<in> fst (createNewCaps ty ptr n us d s); y \<in> set a; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s)\<rbrakk> \<Longrightarrow> descendants_range' y cref (ctes_of b) proof (prove)
goal (2 subgoals):
 1. \<And>s a b y. \<lbrakk>(a, b) \<in> fst (createNewCaps ty ptr n us d s); y \<in> set a; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s)\<rbrakk> \<Longrightarrow> range_cover ptr (?sz16 s a b y) (APIType_capBits ty us) n \<and> 0 < n
 2. \<And>s a b y. \<lbrakk>(a, b) \<in> fst (createNewCaps ty ptr n us d s); y \<in> set a; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s); \<exists>capfn. a = map capfn (map (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<n]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> descendants_range' y cref (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<lbrakk>(a, b) \<in> fst (createNewCaps ty ptr n us d s); y \<in> set a; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s); \<exists>capfn. a = map capfn (map (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<n]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> descendants_range' y cref (ctes_of b) proof (prove)
goal (1 subgoal):
 1. \<And>s a b y. \<lbrakk>y \<in> set a; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s); \<exists>capfn. a = map capfn (map (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits ty us)) [0..<n]) \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> descendants_range' y cref (ctes_of s) \<and> range_cover ptr (?sz20 s a b y) (APIType_capBits ty us) n \<and> n \<noteq> 0 \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz20 s a b y) s proof (prove)
goal (1 subgoal):
 1. \<And>s a y. \<lbrakk>y \<in> set a; range_cover ptr sz (APIType_capBits ty us) n; 0 < n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; descendants_range_in' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} cref (ctes_of s); \<exists>capfn. a = map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits ty us))) [0..<n] \<and> (\<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us)\<rbrakk> \<Longrightarrow> descendants_range' y cref (ctes_of s) proof (prove)
goal (1 subgoal):
 1. \<And>s p' capfn c na x. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>p'\<in>descendants_of' cref (ctes_of s). \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} = {}; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n\<rbrakk> \<Longrightarrow> capRange c \<inter> capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us))) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s p' capfn c na x. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n; \<forall>c. (\<exists>n. ctes_of s p' = Some (CTE c n)) \<longrightarrow> capRange c \<inter> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us))) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s p' capfn c na x. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n; capRange c \<inter> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} = {}\<rbrakk> \<Longrightarrow> capRange c \<inter> capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us))) = {} proof (prove)
goal (1 subgoal):
 1. \<And>s p' capfn c na x. \<lbrakk>range_cover ptr sz (APIType_capBits ty us) n; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n\<rbrakk> \<Longrightarrow> capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us))) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} proof (prove)
goal (2 subgoals):
 1. \<And>s p' capfn c na x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s p' capfn c na x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n; {ptr + word_of_nat x * 2 ^ APIType_capBits ty us..ptr + word_of_nat x * 2 ^ APIType_capBits ty us + 2 ^ APIType_capBits ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1}\<rbrakk> \<Longrightarrow> capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us))) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} proof (prove)
goal (1 subgoal):
 1. \<And>s p' capfn c na x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; p' \<in> descendants_of' cref (ctes_of s); \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; ctes_of s p' = Some (CTE c na); x < n; {ptr + word_of_nat x * 2 ^ APIType_capBits ty us..ptr + word_of_nat x * 2 ^ APIType_capBits ty us + 2 ^ APIType_capBits ty us - 1} \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1}\<rbrakk> \<Longrightarrow> capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us))) \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} proof (prove)
goal:
No subgoals!