theory Untyped_R

lemma createNewCaps_caps_overlap_reserved_ret':
  "\<lbrace>\<lambda>s. caps_overlap_reserved'
          {ptr..ptr + of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and>
        pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and>
        0 < n \<and> range_cover ptr sz (APIType_capBits ty us) n\<rbrace>
   createNewCaps ty ptr n us d
   \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) s\<rbrace>" apply (rule hoare_name_pre_state) apply (clarsimp simp:valid_def) apply (frule use_valid[OF _ createNewCaps_range_helper]) apply fastforce apply clarsimp apply (erule use_valid[OF _ createNewCaps_caps_overlap_reserved']) apply (intro conjI,simp_all) apply (erule caps_overlap_reserved'_subseteq) apply (drule(1) range_cover_subset) apply simp apply (clarsimp simp: ptr_add_def capRange_def
                  simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                            Int_atLeastAtMost atLeastatMost_empty_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits ty us) n\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr sz s \<and> 0 < n \<and> range_cover ptr sz (APIType_capBits ty us) n \<Longrightarrow> \<lbrace>(=) s\<rbrace> createNewCaps ty ptr n us d \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. caps_overlap_reserved' (capRange y) 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; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; range_cover ptr sz (APIType_capBits ty us) n\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (capRange y) 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; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; range_cover ptr sz (APIType_capBits ty us) n\<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; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; range_cover ptr sz (APIType_capBits ty us) n; \<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> caps_overlap_reserved' (capRange y) 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; caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; 0 < n; range_cover ptr sz (APIType_capBits ty us) n; \<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> caps_overlap_reserved' (capRange y) b proof (prove)
goal (1 subgoal):
 1. \<And>s b capfn x. \<lbrakk>(map (capfn \<circ> (\<lambda>p. ptr_add ptr (p * 2 ^ APIType_capBits ty us))) [0..<n], b) \<in> fst (createNewCaps ty ptr n us d s); caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; x < n\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us)))) b proof (prove)
goal (1 subgoal):
 1. \<And>s b capfn x. \<lbrakk>caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; x < n\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us)))) s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> pspace_no_overlap' ptr (?sz28 s b capfn x) s \<and> 0 < n \<and> range_cover ptr (?sz28 s b capfn x) (APIType_capBits ty us) n proof (prove)
goal (1 subgoal):
 1. \<And>s capfn x. \<lbrakk>caps_overlap_reserved' {ptr..ptr + word_of_nat n * 2 ^ APIType_capBits ty us - 1} s; pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; x < n\<rbrakk> \<Longrightarrow> caps_overlap_reserved' (capRange (capfn (ptr_add ptr (x * 2 ^ APIType_capBits ty us)))) s proof (prove)
goal (1 subgoal):
 1. \<And>s capfn x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (APIType_capBits ty us) n; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; 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 capfn x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; x < n\<rbrakk> \<Longrightarrow> n \<noteq> 0
 2. \<And>s capfn x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; 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 capfn x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; \<forall>p. capClass (capfn p) = PhysicalClass \<and> global.capUntypedPtr (capfn p) = p \<and> capBits (capfn p) = APIType_capBits ty us; 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!