theory Detype_R

lemma valid_cap':
    "\<And>p c. \<lbrakk> s \<turnstile>' c; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s;
             capRange c \<inter> {base .. base + (2 ^ bits - 1)} = {} \<rbrakk> \<Longrightarrow> state' \<turnstile>' c" apply (subgoal_tac "capClass c = PhysicalClass \<longrightarrow> capUntypedPtr c \<in> capRange c") apply (subgoal_tac "capClass c = PhysicalClass \<longrightarrow>
                        capUntypedPtr c \<notin> {base .. base + (2 ^ bits - 1)}") apply (frule valid_cap_ctes_pre) apply (case_tac c, simp_all add: valid_cap'_def replycap_argument
                                del: atLeastAtMost_iff
                              split: zombie_type.split_asm) apply (simp add: field_simps del: atLeastAtMost_iff) apply blast apply (rename_tac arch_capability) apply (case_tac arch_capability,
             simp_all add: ARM_H.capUntypedPtr_def
                           page_table_at'_def page_directory_at'_def
                           shiftl_t2n
                      del: atLeastAtMost_iff)[1] apply (rename_tac word vmrights vmpage_size option) apply (subgoal_tac "\<forall>p < 2 ^ (pageBitsForSize vmpage_size - pageBits).
                               word + p * 2 ^ pageBits \<in> capRange c") apply blast apply (clarsimp simp: capRange_def capAligned_def) apply (frule word_less_power_trans2,
               rule pbfs_atleast_pageBits, simp add: word_bits_def) apply (rule context_conjI) apply (erule(1) is_aligned_no_wrap') apply (simp only: add_diff_eq[symmetric]) apply (rule word_plus_mono_right) apply simp apply (erule is_aligned_no_overflow') apply (simp add: field_simps pteBits_def del: atLeastAtMost_iff) apply blast apply (simp add: field_simps pdeBits_def del: atLeastAtMost_iff) apply blast apply (simp add: valid_untyped'_def) apply (simp add: field_simps del: atLeastAtMost_iff) apply blast apply blast apply (clarsimp simp: capAligned_capUntypedPtr) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> valid_cap' c state' proof (prove)
goal (2 subgoals):
 1. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> valid_cap' c state'
 2. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits\<rbrakk> \<Longrightarrow> valid_cap' c state'
 2. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 3. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits; case c of capability.Zombie ref ZombieTCB n \<Rightarrow> True | capability.Zombie ref (ZombieCNode bits) n \<Rightarrow> \<forall>x. ref + (x && mask bits) * 2 ^ cteSizeBits \<in> capRange c | capability.ArchObjectCap (arch_capability.PageTableCap ref data) \<Rightarrow> \<forall>x<0x100. ref + x * 2 ^ pteBits \<in> capRange c | capability.ArchObjectCap (arch_capability.PageDirectoryCap ref data) \<Rightarrow> \<forall>x<0x1000. ref + x * 2 ^ pdeBits \<in> capRange c | capability.ArchObjectCap _ \<Rightarrow> True | capability.CNodeCap ref bits g gs \<Rightarrow> \<forall>x. ref + (x && mask bits) * 2 ^ cteSizeBits \<in> capRange c | _ \<Rightarrow> True\<rbrakk> \<Longrightarrow> valid_cap' c state'
 2. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 3. \<And>p c. \<lbrakk>valid_cap' c s; cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (6 subgoals):
 1. \<And>p c x71 x72 x73 x2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie x71 (ZombieCNode x2) x73) p s; capRange (capability.Zombie x71 (ZombieCNode x2) x73) \<inter> base_bits = {}; x71 \<in> capRange (capability.Zombie x71 (ZombieCNode x2) x73); x71 \<notin> base_bits; \<forall>x. x71 + (x && mask x2) * 2 ^ cteSizeBits \<in> capRange (capability.Zombie x71 (ZombieCNode x2) x73); c = capability.Zombie x71 (ZombieCNode x2) x73; x72 = ZombieCNode x2; capAligned (capability.Zombie x71 (ZombieCNode x2) x73) \<and> x73 \<le> 2 ^ x2 \<and> objBits undefined + x2 < word_bits \<and> 0 < x2 \<and> (\<forall>addr. real_cte_at' (x71 + 2 ^ cteSizeBits * (addr && mask x2)) s)\<rbrakk> \<Longrightarrow> \<forall>addr. x71 + 2 ^ cteSizeBits * (addr && mask x2) \<notin> base_bits
 2. \<And>p c x8. \<lbrakk>capAligned (capability.ArchObjectCap x8) \<and> (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) p s; capRange (capability.ArchObjectCap x8) \<inter> base_bits = {}; acapClass x8 = PhysicalClass \<longrightarrow> Arch.capUntypedPtr x8 \<in> capRange (capability.ArchObjectCap x8); acapClass x8 = PhysicalClass \<longrightarrow> Arch.capUntypedPtr x8 \<notin> base_bits; case x8 of arch_capability.PageTableCap ref data \<Rightarrow> \<forall>x<0x100. ref + x * 2 ^ pteBits \<in> capRange c | arch_capability.PageDirectoryCap ref data \<Rightarrow> \<forall>x<0x1000. ref + x * 2 ^ pdeBits \<in> capRange c | _ \<Rightarrow> True; c = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool state' \<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) state') \<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 state' \<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 state' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
 3. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 4. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (6 subgoals):
 1. \<And>p c x71 x72 x73 x2. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.Zombie x71 (ZombieCNode x2) x73) p s; capRange (capability.Zombie x71 (ZombieCNode x2) x73) \<inter> {base..base + 2 ^ bits - 1} = {}; x71 \<in> capRange (capability.Zombie x71 (ZombieCNode x2) x73); x71 \<notin> {base..base + 2 ^ bits - 1}; \<forall>x. x71 + (x && mask x2) * 2 ^ cteSizeBits \<in> capRange (capability.Zombie x71 (ZombieCNode x2) x73); c = capability.Zombie x71 (ZombieCNode x2) x73; x72 = ZombieCNode x2; capAligned (capability.Zombie x71 (ZombieCNode x2) x73) \<and> x73 \<le> 2 ^ x2 \<and> x2 + objBits undefined < word_bits \<and> 0 < x2 \<and> (\<forall>addr. real_cte_at' (x71 + (addr && mask x2) * 2 ^ cteSizeBits) s)\<rbrakk> \<Longrightarrow> \<forall>addr. x71 + (addr && mask x2) * 2 ^ cteSizeBits \<notin> {base..base + 2 ^ bits - 1}
 2. \<And>p c x8. \<lbrakk>capAligned (capability.ArchObjectCap x8) \<and> (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) p s; capRange (capability.ArchObjectCap x8) \<inter> base_bits = {}; acapClass x8 = PhysicalClass \<longrightarrow> Arch.capUntypedPtr x8 \<in> capRange (capability.ArchObjectCap x8); acapClass x8 = PhysicalClass \<longrightarrow> Arch.capUntypedPtr x8 \<notin> base_bits; case x8 of arch_capability.PageTableCap ref data \<Rightarrow> \<forall>x<0x100. ref + x * 2 ^ pteBits \<in> capRange c | arch_capability.PageDirectoryCap ref data \<Rightarrow> \<forall>x<0x1000. ref + x * 2 ^ pdeBits \<in> capRange c | _ \<Rightarrow> True; c = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool state' \<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) state') \<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 state' \<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 state' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
 3. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 4. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c x8. \<lbrakk>capAligned (capability.ArchObjectCap x8) \<and> (case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap x8) p s; capRange (capability.ArchObjectCap x8) \<inter> base_bits = {}; acapClass x8 = PhysicalClass \<longrightarrow> Arch.capUntypedPtr x8 \<in> capRange (capability.ArchObjectCap x8); acapClass x8 = PhysicalClass \<longrightarrow> Arch.capUntypedPtr x8 \<notin> base_bits; case x8 of arch_capability.PageTableCap ref data \<Rightarrow> \<forall>x<0x100. ref + x * 2 ^ pteBits \<in> capRange c | arch_capability.PageDirectoryCap ref data \<Rightarrow> \<forall>x<0x1000. ref + x * 2 ^ pdeBits \<in> capRange c | _ \<Rightarrow> True; c = capability.ArchObjectCap x8\<rbrakk> \<Longrightarrow> case x8 of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool state' \<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) state') \<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 state' \<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 state' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
 2. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 3. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 4. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c arch_capability. \<lbrakk>capAligned (capability.ArchObjectCap arch_capability) \<and> (case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool s \<and> is_aligned asid local.asid_low_bits \<and> asid \<le> 2 ^ local.asid_bits - 1 | arch_capability.ASIDControlCap \<Rightarrow> True | arch_capability.PageCap d ref rghts sz mapdata \<Rightarrow> ref \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize sz - pageBits). typ_at' (if d then UserDataDeviceT else UserDataT) (ref + p * 2 ^ pageBits) s) \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vmsz_aligned' ref sz \<and> ref < pptrBase) | arch_capability.PageTableCap ref mapdata \<Rightarrow> page_table_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> ref < pptrBase) | arch_capability.PageDirectoryCap ref mapdata \<Rightarrow> page_directory_at' ref s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap arch_capability) p s; capRange (capability.ArchObjectCap arch_capability) \<inter> base_bits = {}; acapClass arch_capability = PhysicalClass \<longrightarrow> Arch.capUntypedPtr arch_capability \<in> capRange (capability.ArchObjectCap arch_capability); acapClass arch_capability = PhysicalClass \<longrightarrow> Arch.capUntypedPtr arch_capability \<notin> base_bits; case arch_capability of arch_capability.PageTableCap ref data \<Rightarrow> \<forall>x<0x100. ref + x * 2 ^ pteBits \<in> capRange c | arch_capability.PageDirectoryCap ref data \<Rightarrow> \<forall>x<0x1000. ref + x * 2 ^ pdeBits \<in> capRange c | _ \<Rightarrow> True; c = capability.ArchObjectCap arch_capability\<rbrakk> \<Longrightarrow> case arch_capability of arch_capability.ASIDPoolCap pool asid \<Rightarrow> asid_pool_at' pool state' \<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) state') \<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 state' \<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 state' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1)
 2. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 3. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 4. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p c arch_capability x31 x32 x33 x34 x35. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<and> x32 \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize x34 - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (x32 + p * 2 ^ pageBits) s) \<and> (case x35 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref x34 \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) p s; capRange (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)) \<inter> base_bits = {}; x32 \<in> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 x32 x33 x34 x35)); x32 \<notin> base_bits; c = 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). x32 + p * 2 ^ pageBits \<notin> base_bits
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p c arch_capability x31 word vmrights vmpage_size option. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<and> word \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s) \<and> (case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<inter> base_bits = {}; word \<in> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)); word \<notin> base_bits; c = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option); arch_capability = arch_capability.PageCap x31 word vmrights vmpage_size option\<rbrakk> \<Longrightarrow> \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). word + p * 2 ^ pageBits \<notin> base_bits
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (8 subgoals):
 1. \<And>p c arch_capability x31 word vmrights vmpage_size option. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<and> word \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s) \<and> (case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<inter> base_bits = {}; word \<in> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)); word \<notin> base_bits; c = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option); arch_capability = arch_capability.PageCap x31 word vmrights vmpage_size option; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). word + p * 2 ^ pageBits \<in> capRange c\<rbrakk> \<Longrightarrow> \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). word + p * 2 ^ pageBits \<notin> base_bits
 2. \<And>p c arch_capability x31 word vmrights vmpage_size option. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<and> word \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s) \<and> (case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<inter> base_bits = {}; word \<in> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)); word \<notin> base_bits; c = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option); arch_capability = arch_capability.PageCap x31 word vmrights vmpage_size option\<rbrakk> \<Longrightarrow> \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). word + p * 2 ^ pageBits \<in> capRange c
 3. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 4. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 5. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 6. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 8. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p c arch_capability x31 word vmrights vmpage_size option. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<and> word \<noteq> 0 \<and> (\<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s) \<and> (case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) \<inter> base_bits = {}; word \<in> capRange (capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)); word \<notin> base_bits; c = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option); arch_capability = arch_capability.PageCap x31 word vmrights vmpage_size option\<rbrakk> \<Longrightarrow> \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). word + p * 2 ^ pageBits \<in> capRange c
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + 2 ^ pageBitsForSize vmpage_size - 1; base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits)\<rbrakk> \<Longrightarrow> word \<le> word + pa * 2 ^ pageBits \<and> word + pa * 2 ^ pageBits \<le> word + 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + 2 ^ pageBitsForSize vmpage_size - 1; base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size\<rbrakk> \<Longrightarrow> word \<le> word + pa * 2 ^ pageBits \<and> word + pa * 2 ^ pageBits \<le> word + 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (8 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + 2 ^ pageBitsForSize vmpage_size - 1; base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size\<rbrakk> \<Longrightarrow> word \<le> word + pa * 2 ^ pageBits
 2. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + 2 ^ pageBitsForSize vmpage_size - 1; base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; word \<le> word + pa * 2 ^ pageBits\<rbrakk> \<Longrightarrow> word + pa * 2 ^ pageBits \<le> word + 2 ^ pageBitsForSize vmpage_size - 1
 3. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 4. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 5. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 6. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 8. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + 2 ^ pageBitsForSize vmpage_size - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + 2 ^ pageBitsForSize vmpage_size - 1; base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; word \<le> word + pa * 2 ^ pageBits\<rbrakk> \<Longrightarrow> word + pa * 2 ^ pageBits \<le> word + 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + (2 ^ pageBitsForSize vmpage_size - 1) \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1); base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; word \<le> word + pa * 2 ^ pageBits\<rbrakk> \<Longrightarrow> word + pa * 2 ^ pageBits \<le> word + (2 ^ pageBitsForSize vmpage_size - 1)
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (8 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + (2 ^ pageBitsForSize vmpage_size - 1) \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1); base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; word \<le> word + pa * 2 ^ pageBits\<rbrakk> \<Longrightarrow> pa * 2 ^ pageBits \<le> 2 ^ pageBitsForSize vmpage_size - 1
 2. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + (2 ^ pageBitsForSize vmpage_size - 1) \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1); base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; word \<le> word + pa * 2 ^ pageBits\<rbrakk> \<Longrightarrow> word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1)
 3. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 4. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 5. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 6. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 8. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (7 subgoals):
 1. \<And>p x31 word vmrights vmpage_size option pa. \<lbrakk>cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageCap x31 word vmrights vmpage_size option)) p s; word \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> word + (2 ^ pageBitsForSize vmpage_size - 1) \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1); base \<le> word \<longrightarrow> \<not> word \<le> base + (2 ^ bits - 1); is_aligned word (pageBitsForSize vmpage_size); pageBitsForSize vmpage_size < word_bits; word \<noteq> 0; \<forall>p<2 ^ (pageBitsForSize vmpage_size - pageBits). typ_at' (if x31 then UserDataDeviceT else UserDataT) (word + p * 2 ^ pageBits) s; case option of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> vmsz_aligned' ref vmpage_size \<and> ref < pptrBase; pa < 2 ^ (pageBitsForSize vmpage_size - pageBits); pa * 2 ^ pageBits < 2 ^ pageBitsForSize vmpage_size; word \<le> word + pa * 2 ^ pageBits\<rbrakk> \<Longrightarrow> word \<le> word + (2 ^ pageBitsForSize vmpage_size - 1)
 2. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 3. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 4. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 5. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 7. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (6 subgoals):
 1. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + 4 * y) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> base_bits = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> base_bits; \<forall>x<0x100. x41 + x * 2 ^ pteBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + 4 * y \<notin> base_bits
 2. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 3. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 4. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (6 subgoals):
 1. \<And>p c arch_capability x41 x42. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<and> is_aligned x41 ptBits \<and> (\<forall>y<0x100. pte_at' (x41 + y * 4) s) \<and> (case x42 of None \<Rightarrow> True | Some (asid, ref) \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits \<and> ref < pptrBase); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) p s; capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)) \<inter> {base..base + 2 ^ bits - 1} = {}; x41 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); x41 \<notin> {base..base + 2 ^ bits - 1}; \<forall>x<0x100. x41 + x * 4 \<in> capRange (capability.ArchObjectCap (arch_capability.PageTableCap x41 x42)); c = capability.ArchObjectCap (arch_capability.PageTableCap x41 x42); arch_capability = arch_capability.PageTableCap x41 x42\<rbrakk> \<Longrightarrow> \<forall>y<0x100. x41 + y * 4 \<notin> {base..base + 2 ^ bits - 1}
 2. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 3. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 4. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 6. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + 4 * y) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> base_bits = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> base_bits; \<forall>x<0x1000. x51 + x * 2 ^ pdeBits \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + 4 * y \<notin> base_bits
 2. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 3. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 4. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (5 subgoals):
 1. \<And>p c arch_capability x51 x52. \<lbrakk>capAligned (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<and> is_aligned x51 pdBits \<and> (\<forall>y<0x1000. pde_at' (x51 + y * 4) s) \<and> (case x52 of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid < 2 ^ local.asid_bits); cte_wp_at' (\<lambda>cte. cteCap cte = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) p s; capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)) \<inter> {base..base + 2 ^ bits - 1} = {}; x51 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); x51 \<notin> {base..base + 2 ^ bits - 1}; \<forall>x<0x1000. x51 + x * 4 \<in> capRange (capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52)); c = capability.ArchObjectCap (arch_capability.PageDirectoryCap x51 x52); arch_capability = arch_capability.PageDirectoryCap x51 x52\<rbrakk> \<Longrightarrow> \<forall>y<0x1000. x51 + y * 4 \<notin> {base..base + 2 ^ bits - 1}
 2. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 3. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 4. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 5. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (4 subgoals):
 1. \<And>p c x101 x102 x103 x104. \<lbrakk>capAligned (capability.UntypedCap x101 x102 x103 x104) \<and> valid_untyped' x101 x102 x103 x104 s \<and> x102 \<noteq> 0 \<and> minUntypedSizeBits \<le> x103 \<and> x103 \<le> maxUntypedSizeBits \<and> x104 \<le> 2 ^ x103 \<and> is_aligned (word_of_nat x104) minUntypedSizeBits; cte_wp_at' (\<lambda>cte. cteCap cte = capability.UntypedCap x101 x102 x103 x104) p s; x102 \<le> base + (2 ^ bits - 1) \<longrightarrow> base \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> x102 \<le> x102 + 2 ^ x103 - 1 \<longrightarrow> \<not> base \<le> base + (2 ^ bits - 1); x102 \<in> {x102..x102 + 2 ^ x103 - 1}; x102 \<notin> base_bits; c = capability.UntypedCap x101 x102 x103 x104\<rbrakk> \<Longrightarrow> valid_untyped' x101 x102 x103 x104 state'
 2. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 3. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 4. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + 2 ^ cteSizeBits * (addr && mask x112)) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> base_bits = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> base_bits; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + 2 ^ cteSizeBits * (addr && mask x112) \<notin> base_bits
 2. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 3. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (3 subgoals):
 1. \<And>p c x111 x112 x113 x114. \<lbrakk>capAligned (capability.CNodeCap x111 x112 x113 x114) \<and> 0 < x112 \<and> x112 + x114 \<le> word_bits \<and> x113 && mask x114 = x113 \<and> (\<forall>addr. real_cte_at' (x111 + (addr && mask x112) * 2 ^ cteSizeBits) s); cte_wp_at' (\<lambda>cte. cteCap cte = capability.CNodeCap x111 x112 x113 x114) p s; capRange (capability.CNodeCap x111 x112 x113 x114) \<inter> {base..base + 2 ^ bits - 1} = {}; x111 \<in> capRange (capability.CNodeCap x111 x112 x113 x114); x111 \<notin> {base..base + 2 ^ bits - 1}; \<forall>x. x111 + (x && mask x112) * 2 ^ cteSizeBits \<in> capRange (capability.CNodeCap x111 x112 x113 x114); c = capability.CNodeCap x111 x112 x113 x114\<rbrakk> \<Longrightarrow> \<forall>addr. x111 + (addr && mask x112) * 2 ^ cteSizeBits \<notin> {base..base + 2 ^ bits - 1}
 2. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 3. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (2 subgoals):
 1. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}; capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<notin> base_bits
 2. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal (1 subgoal):
 1. \<And>p c. \<lbrakk>capAligned c \<and> (case c 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); cte_wp_at' (\<lambda>cte. cteCap cte = c) p s; capRange c \<inter> base_bits = {}\<rbrakk> \<Longrightarrow> capClass c = PhysicalClass \<longrightarrow> global.capUntypedPtr c \<in> capRange c proof (prove)
goal:
No subgoals!