theory Retype_R

lemma valid_untyped'_helper:
  assumes valid : "valid_cap' c s"
  and  cte_at : "cte_wp_at' (\<lambda>cap. cteCap cap = c) q s"
  and  cover  : "range_cover ptr sz (objBitsKO val) n"
  and  range  : "caps_no_overlap'' ptr sz s"
  and  pres   : "isUntypedCap c \<longrightarrow> usableUntypedRange c \<inter>  {ptr..ptr + of_nat n * 2 ^ objBitsKO val - 1} = {}"
  shows "\<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<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 - note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff assume pn : "pspace_aligned' s" "pspace_distinct' s"
  and   no_overlap: "pspace_no_overlap' ptr sz s" show ?thesis using pn pres no_overlap valid cover cte_wp_at_ctes_of[THEN iffD1,OF cte_at]
        caps_no_overlapD''[OF cte_at range] apply (clarsimp simp:valid_cap'_def retype_ko_wp_at') apply (case_tac "cteCap cte"; simp add: valid_cap'_def cte_wp_at_obj_cases'
                                valid_pspace'_def retype_obj_at_disj'
                         split: zombie_type.split_asm) 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 split del: if_splits) apply (fastforce simp: typ_at_to_obj_at_arches retype_obj_at_disj') unfolding valid_untyped'_def apply (intro allI) apply (rule ccontr) apply clarify using cover[unfolded range_cover_def] apply (clarsimp simp:isCap_simps retype_ko_wp_at' split:if_split_asm) apply (thin_tac "\<forall>x. Q x" for Q) apply (frule aligned_untypedRange_non_empty) apply (simp add:isCap_simps) apply (elim disjE) apply (frule(1) obj_range'_subset) apply (erule impE) apply (drule(1) psubset_subset_trans) apply (drule Int_absorb1[OF psubset_imp_subset]) apply (drule aligned_untypedRange_non_empty) apply (simp add:isCap_simps) apply (simp add:Int_ac) apply (drule(1) subset_trans) apply blast apply (frule(1) obj_range'_subset_strong) apply (drule(1) non_disjoing_subset) apply blast apply (thin_tac "\<forall>x. Q x" for Q) apply (frule aligned_untypedRange_non_empty) apply (simp add:isCap_simps) apply (frule(1) obj_range'_subset) apply (drule(1) subset_trans) apply (erule impE) apply clarsimp apply blast apply blast done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<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 (state)
goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<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 (state)
this:
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)

goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<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 (state)
this:
pspace_aligned' s
pspace_distinct' s
pspace_no_overlap' ptr sz s

goal (1 subgoal):
 1. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s\<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 (1 subgoal):
 1. 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)
using this:
pspace_aligned' s
pspace_distinct' s
isUntypedCap c \<longrightarrow> usableUntypedRange c \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}
pspace_no_overlap' ptr sz s
valid_cap' c s
range_cover ptr sz (objBitsKO val) n
\<exists>cte. ctes_of s q = Some cte \<and> cteCap cte = c
untypedRange c \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange c

goal (1 subgoal):
 1. 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 (1 subgoal):
 1. \<And>cte. \<lbrakk>pspace_aligned' s; pspace_distinct' s; isUntypedCap (cteCap cte) \<longrightarrow> usableUntypedRange (cteCap cte) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; untypedRange (cteCap cte) \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> untypedRange (cteCap cte); capAligned (cteCap cte); case cteCap cte of capability.ThreadCap r \<Rightarrow> tcb_at' r s | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r s | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r s | capability.Zombie r b n \<Rightarrow> n \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r s | ZombieCNode n \<Rightarrow> n \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask n)) s)) | capability.ArchObjectCap (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 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (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) | capability.ArchObjectCap (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) | capability.ArchObjectCap (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) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r s | capability.UntypedCap d r n f \<Rightarrow> valid_untyped' d r n f s \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> n \<and> n \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ n \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) s) | _ \<Rightarrow> True; ctes_of s q = Some cte; c = cteCap cte\<rbrakk> \<Longrightarrow> case cteCap cte of capability.ThreadCap r \<Rightarrow> tcb_at' r (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) | capability.NotificationCap r badge x y \<Rightarrow> ntfn_at' r (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) | capability.IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | capability.EndpointCap r badge x y z t \<Rightarrow> ep_at' r (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) | capability.Zombie r b na \<Rightarrow> na \<le> zombieCTEs b \<and> zBits b < word_bits \<and> (case b of ZombieTCB \<Rightarrow> tcb_at' r (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) | ZombieCNode na \<Rightarrow> na \<noteq> 0 \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask na)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>))) | capability.ArchObjectCap (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 | capability.ArchObjectCap arch_capability.ASIDControlCap \<Rightarrow> True | capability.ArchObjectCap (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) | capability.ArchObjectCap (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) | capability.ArchObjectCap (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) | capability.ReplyCap r m x \<Rightarrow> tcb_at' r (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) | capability.UntypedCap d r na f \<Rightarrow> valid_untyped' d r na f (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>) \<and> r \<noteq> 0 \<and> minUntypedSizeBits \<le> na \<and> na \<le> maxUntypedSizeBits \<and> f \<le> 2 ^ na \<and> is_aligned (word_of_nat f) minUntypedSizeBits | capability.CNodeCap r bits guard guard_sz \<Rightarrow> bits \<noteq> 0 \<and> bits + guard_sz \<le> word_bits \<and> guard && mask guard_sz = guard \<and> (\<forall>addr. real_cte_at' (r + 2 ^ cteSizeBits * (addr && mask bits)) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)) | _ \<Rightarrow> True proof (prove)
goal (2 subgoals):
 1. \<And>cte x8. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.ArchObjectCap x8); 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); ctes_of s q = Some cte; c = capability.ArchObjectCap x8; cteCap cte = 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>cte x101 x102 x103 x104. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = 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>cte arch_capability. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.ArchObjectCap arch_capability); 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); ctes_of s q = Some cte; c = capability.ArchObjectCap arch_capability; cteCap cte = 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>cte x101 x102 x103 x104. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = 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>cte arch_capability x31 x32 x33 x34 x35. \<lbrakk>pspace_aligned' s; pspace_distinct' s; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); 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); ctes_of s q = Some cte; c = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35); arch_capability = arch_capability.PageCap x31 x32 x33 x34 x35\<rbrakk> \<Longrightarrow> \<forall>p<2 ^ (pageBitsForSize x34 - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (x32 + p * 2 ^ pageBits) (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)
 2. \<And>cte x101 x102 x103 x104. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = 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>cte x101 x102 x103 x104. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = 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>cte x101 x102 x103 x104. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); (\<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' (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>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); (\<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' (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>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); (\<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' 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; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; \<not> \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; x104 \<le> 2 ^ x103; is_aligned (word_of_nat x104) minUntypedSizeBits; \<not> False; ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
using this:
(is_aligned ptr (objBitsKO val) \<and> sz < LENGTH(32)) \<and> objBitsKO val \<le> sz \<and> n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val)

goal (1 subgoal):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; (if x104 < 2 ^ x103 then {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} else {}) \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; x104 \<le> 2 ^ x103; is_aligned (word_of_nat x104) minUntypedSizeBits; \<not> False; ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> usableUntypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}) ptr' (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko \<or> obj_range' ptr' ko \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val \<or> obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val \<or> obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val \<or> obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> isUntypedCap (capability.UntypedCap x101 x102 x103 x104)
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val \<or> obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}; untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val \<or> obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}; untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 4. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subset> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 4. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> {x102..x102 + 2 ^ x103 - 1} = {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 4. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (5 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> {x102..x102 + 2 ^ x103 - 1} = {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> isUntypedCap (capability.UntypedCap x101 x102 x103 x104)
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> {x102..x102 + 2 ^ x103 - 1} = {x102..x102 + 2 ^ x103 - 1}; untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}\<rbrakk> \<Longrightarrow> {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 3. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 4. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 5. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (4 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<inter> {x102..x102 + 2 ^ x103 - 1} = {x102..x102 + 2 ^ x103 - 1}; untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}\<rbrakk> \<Longrightarrow> {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 4. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (3 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' val; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; obj_range' ptr' val \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 3. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 x104 ptr'. \<lbrakk>pspace_aligned' s; pspace_distinct' s; x104 < 2 ^ x103; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<inter> {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} = {}; pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 x104); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 x104; cteCap cte = capability.UntypedCap x101 x102 x103 x104; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (word_of_nat x104) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); untypedRange (capability.UntypedCap x101 x102 x103 x104) \<noteq> {}; obj_range' ptr' val \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}; {ptr..ptr + word_of_nat n * 2 ^ objBitsKO val - 1} \<inter> {x102 + word_of_nat x104..x102 + 2 ^ x103 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); \<forall>ptr'. \<not> ko_wp_at' (\<lambda>ko. {x102..x102 + 2 ^ x103 - 1} \<subset> obj_range' ptr' ko) ptr' s; x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val\<rbrakk> \<Longrightarrow> isUntypedCap (capability.UntypedCap x101 x102 x103 (2 ^ x103))
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); {x102..x102 + 2 ^ x103 - 1} \<subseteq> obj_range' ptr' val; x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {} \<longrightarrow> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}\<rbrakk> \<Longrightarrow> {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<noteq> {}
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (2 subgoals):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; {x102..x102 + 2 ^ x103 - 1} \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> False
 2. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal (1 subgoal):
 1. \<And>cte x101 x102 x103 ptr' x. \<lbrakk>pspace_aligned' s; pspace_distinct' s; is_aligned ptr (objBitsKO val); sz < 32; objBitsKO val \<le> sz; n + unat (ptr && mask sz >> objBitsKO val) \<le> 2 ^ (sz - objBitsKO val); pspace_no_overlap' ptr sz s; range_cover ptr sz (objBitsKO val) n; capAligned (capability.UntypedCap x101 x102 x103 (2 ^ x103)); ctes_of s q = Some cte; c = capability.UntypedCap x101 x102 x103 (2 ^ x103); cteCap cte = capability.UntypedCap x101 x102 x103 (2 ^ x103); x102 \<noteq> 0; minUntypedSizeBits \<le> x103; x103 \<le> maxUntypedSizeBits; is_aligned (2 ^ x103) minUntypedSizeBits; ptr' \<in> set (new_cap_addrs n ptr val); x \<in> obj_range' ptr' val; untypedRange (capability.UntypedCap x101 x102 x103 (2 ^ x103)) \<noteq> {}; obj_range' ptr' val \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {x102..x102 + 2 ^ x103 - 1} \<subseteq> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1}; {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} \<subseteq> {x102..x102 + 2 ^ x103 - 1}\<rbrakk> \<Longrightarrow> x \<in> {x102..x102 + 2 ^ x103 - 1} proof (prove)
goal:
No subgoals! proof (state)
this:
valid_cap' c (s\<lparr>ksPSpace := foldr (\<lambda>addr. data_map_insert addr val) (new_cap_addrs n ptr val) (ksPSpace s)\<rparr>)

goal:
No subgoals!