theory Retype_R

lemma valid_cap'_range_no_overlap:
  "\<lbrakk>untypedRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; s \<turnstile>' c;
    valid_pspace' s; pspace_no_overlap' ptr sz s;
    range_cover ptr sz (objBitsKO val) n\<rbrakk>
   \<Longrightarrow> s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val)
                           (new_cap_addrs n ptr val) (ksPSpace s)\<rparr> \<turnstile>' c" apply (cases c; simp add: valid_cap'_def cte_wp_at_obj_cases' valid_pspace'_def retype_obj_at_disj'
                       split: zombie_type.split_asm
                       del: Int_atLeastAtMost)[1] apply (rename_tac arch_capability) apply (case_tac arch_capability;
          simp add: retype_obj_at_disj' typ_at_to_obj_at_arches
                    page_table_at'_def page_directory_at'_def) apply (fastforce simp: typ_at_to_obj_at_arches retype_obj_at_disj') apply (rename_tac word nat1 nat2) apply (clarsimp simp:valid_untyped'_def retype_ko_wp_at'
        simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff) apply (frule aligned_untypedRange_non_empty) apply (simp add:isCap_simps) apply (intro conjI impI) apply (intro allI) apply (drule_tac x = ptr' in spec) apply (rule ccontr) apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                             Int_atLeastAtMost atLeastatMost_empty_iff) apply (erule disjE) apply (drule(2) disjoint_subset2 [OF obj_range'_subset]) apply (drule(1) disjoint_subset2[OF psubset_imp_subset]) apply (simp add: Int_absorb ptr_add_def p_assoc_help
                del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                     Int_atLeastAtMost atLeastatMost_empty_iff) apply (drule(1) obj_range'_subset) apply (drule_tac A'=" {word + of_nat nat2..word + 2 ^ nat1 - 1}" in disjoint_subset[rotated]) apply clarsimp apply (rule is_aligned_no_wrap') apply (fastforce simp:capAligned_def) apply (erule of_nat_less_pow_32) apply (simp add:capAligned_def) apply (drule(1) disjoint_subset2) apply blast apply (intro allI) apply (drule_tac x = ptr' in spec) apply (rule ccontr) apply (clarsimp simp del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                            Int_atLeastAtMost atLeastatMost_empty_iff) apply (drule(2) disjoint_subset2 [OF obj_range'_subset]) apply (drule(1) disjoint_subset2) apply (simp add: Int_absorb ptr_add_def p_assoc_help
              del: atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
                   Int_atLeastAtMost atLeastatMost_empty_iff) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>untypedRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; valid_cap' c s; valid_pspace' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n\<rbrakk> \<Longrightarrow> valid_cap' c (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>x8. \<lbrakk>capAligned (capability.ArchObjectCap x8) \<and> (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
 2. \<And>x101 x102 x103 x104. \<lbrakk>{x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>arch_capability. \<lbrakk>capAligned (capability.ArchObjectCap arch_capability) \<and> (case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
 2. \<And>x101 x102 x103 x104. \<lbrakk>{x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (2 subgoals):
 1. \<And>arch_capability x31 x32 x33 x34 x35. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<and> x32 \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize x34 - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (x32 + p * 2 ^ pageBits) s) \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase); valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> (x31 \<longrightarrow> (\<forall>p<2 ^ (pageBitsForSize x34 - pageBits). obj_at' (\<lambda>_. True) (x32 + p * 2 ^ pageBits) s \<or> x32 + p * 2 ^ pageBits \<in> set (new_cap_addrs n ptr val) \<and> (\<exists>ko. projectKO_opt val = Some ko))) \<and> (\<not> x31 \<longrightarrow> (\<forall>p<2 ^ (pageBitsForSize x34 - pageBits). obj_at' (\<lambda>_. True) (x32 + p * 2 ^ pageBits) s \<or> x32 + p * 2 ^ pageBits \<in> set (new_cap_addrs n ptr val) \<and> (\<exists>ko. projectKO_opt val = Some ko)))
 2. \<And>x101 x102 x103 x104. \<lbrakk>{x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x101 x102 x103 x104. \<lbrakk>{x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; capAligned (capability.UntypedCap x101 word nat1 nat2) \<and> valid_untyped' x101 word nat1 nat2 s \<and> word \<noteq> 0 \<and> minUntypedSizeBits \<le> nat1 \<and> nat1 \<le> maxUntypedSizeBits \<and> nat2 \<le> 2 ^ nat1 \<and> is_aligned (word_of_nat nat2) minUntypedSizeBits; valid_objs' s \<and> pspace_aligned' s \<and> pspace_distinct' s \<and> no_0_obj' s \<and> valid_mdb' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2\<rbrakk> \<Longrightarrow> valid_untyped' x101 word nat1 nat2 (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits\<rbrakk> \<Longrightarrow> (nat2 < 2 ^ nat1 \<longrightarrow> (\<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s))) \<and> (nat2 = 2 ^ nat1 \<longrightarrow> (\<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s))) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits\<rbrakk> \<Longrightarrow> isUntypedCap (capability.UntypedCap x101 word nat1 nat2)
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}\<rbrakk> \<Longrightarrow> (nat2 < 2 ^ nat1 \<longrightarrow> (\<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s))) \<and> (nat2 = 2 ^ nat1 \<longrightarrow> (\<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s))) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}\<rbrakk> \<Longrightarrow> (nat2 < 2 ^ nat1 \<longrightarrow> (\<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s))) \<and> (nat2 = 2 ^ nat1 \<longrightarrow> (\<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s))) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 < 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s)
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 < 2 ^ nat1\<rbrakk> \<Longrightarrow> (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s)
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s\<rbrakk> \<Longrightarrow> (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s)
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; \<not> ((ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<and> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} = {}) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s))\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val \<or> obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val; {word..word + 2 ^ nat1 - 1} \<inter> obj_range' ptr' val = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); {word..word + 2 ^ nat1 - 1} \<inter> obj_range' ptr' val = {}; {word..word + 2 ^ nat1 - 1} \<inter> {word..word + 2 ^ nat1 - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<subseteq> {word..word + 2 ^ nat1 - 1}
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; word \<le> word + 2 ^ nat1 - 1; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; word + word_of_nat nat2 \<le> word + 2 ^ nat1 - 1\<rbrakk> \<Longrightarrow> word \<le> word + word_of_nat nat2
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (4 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; word \<le> word + 2 ^ nat1 - 1; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; word + word_of_nat nat2 \<le> word + 2 ^ nat1 - 1\<rbrakk> \<Longrightarrow> is_aligned word (?sz149 x101 word nat1 nat2 ptr')
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; word \<le> word + 2 ^ nat1 - 1; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; word + word_of_nat nat2 \<le> word + 2 ^ nat1 - 1\<rbrakk> \<Longrightarrow> word_of_nat nat2 < 2 ^ ?sz149 x101 word nat1 nat2 ptr'
 3. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 4. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; word \<le> word + 2 ^ nat1 - 1; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; word + word_of_nat nat2 \<le> word + 2 ^ nat1 - 1\<rbrakk> \<Longrightarrow> word_of_nat nat2 < 2 ^ nat1
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (3 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; word \<le> word + 2 ^ nat1 - 1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; word + word_of_nat nat2 \<le> word + 2 ^ nat1 - 1\<rbrakk> \<Longrightarrow> nat1 < word_bits
 2. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 3. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (2 subgoals):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (word_of_nat nat2) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; nat2 < 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); obj_range' ptr' val \<inter> {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<noteq> {}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; {word + word_of_nat nat2..word + 2 ^ nat1 - 1} \<inter> obj_range' ptr' val = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> \<forall>ptr'. (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1\<rbrakk> \<Longrightarrow> (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s\<rbrakk> \<Longrightarrow> (ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s) proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 nat2 ptr'. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 nat2; capAligned (capability.UntypedCap x101 word nat1 nat2); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; nat2 \<le> 2 ^ nat1; is_aligned (word_of_nat nat2) minUntypedSizeBits; untypedRange (capability.UntypedCap x101 word nat1 nat2) \<noteq> {}; nat2 = 2 ^ nat1; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> (if nat2 < 2 ^ nat1 then {word + word_of_nat nat2..word + 2 ^ nat1 - 1} else {}) \<noteq> {}) ptr' s; \<not> ((ptr' \<in> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' val) \<and> (ptr' \<notin> set (new_cap_addrs n ptr val) \<longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 ptr' x. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; c = capability.UntypedCap x101 word nat1 (2 ^ nat1); capAligned (capability.UntypedCap x101 word nat1 (2 ^ nat1)); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (2 ^ nat1) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); {word..word + 2 ^ nat1 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 ptr' x. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 (2 ^ nat1); capAligned (capability.UntypedCap x101 word nat1 (2 ^ nat1)); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (2 ^ nat1) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); {word..word + 2 ^ nat1 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val; {word..word + 2 ^ nat1 - 1} \<inter> obj_range' ptr' val = {}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>x101 word nat1 ptr' x. \<lbrakk>{word..word + 2 ^ nat1 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; pspace_no_overlap' ptr sz s; c = capability.UntypedCap x101 word nat1 (2 ^ nat1); capAligned (capability.UntypedCap x101 word nat1 (2 ^ nat1)); valid_objs' s; pspace_aligned' s; word \<noteq> 0; pspace_distinct' s; minUntypedSizeBits \<le> nat1; no_0_obj' s; valid_mdb' s; nat1 \<le> maxUntypedSizeBits; is_aligned (2 ^ nat1) minUntypedSizeBits; {word..word + 2 ^ nat1 - 1} \<noteq> {}; \<not> ko_wp_at' (\<lambda>ko. {word..word + 2 ^ nat1 - 1} \<subset> obj_range' ptr' ko) ptr' s; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; {word..word + 2 ^ nat1 - 1} \<inter> obj_range' ptr' val = {}; {word..word + 2 ^ nat1 - 1} \<inter> {word..word + 2 ^ nat1 - 1} = {}\<rbrakk> \<Longrightarrow> x \<in> {word..word + 2 ^ nat1 - 1} proof (prove)
goal:
No subgoals!