theory ArchRetype_AI

lemma valid_cap:
  assumes cap:
    "(s::'state_ext state) \<turnstile> cap \<and> untyped_range cap \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} = {}"
  shows "s' \<turnstile> cap" proof - note blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff
        Int_atLeastAtMost atLeastatMost_empty_iff have cover':"range_cover ptr sz (obj_bits (default_object ty dev us)) n" using cover tyunt by (clarsimp simp: obj_bits_dev_irr) show ?thesis using cap apply (case_tac cap) unfolding valid_cap_def apply (simp_all add: valid_cap_def obj_at_pres cte_at_pres
                              split: option.split_asm arch_cap.split_asm
                                     option.splits) apply (clarsimp simp add: valid_untyped_def ps_def s'_def) apply (intro conjI) apply clarsimp apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) apply (simp add: Int_ac p_assoc_help[symmetric]) apply simp apply clarsimp apply (drule disjoint_subset [OF retype_addrs_obj_range_subset [OF _ cover' tyunt]]) apply (simp add: Int_ac p_assoc_help[symmetric]) apply simp using cover tyunt apply (simp add: obj_bits_api_def2 split: Structures_A.apiobject_type.splits) apply clarsimp+ apply (fastforce elim!: obj_at_pres)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> cap proof (state)
goal (1 subgoal):
 1. s' \<turnstile> cap proof (state)
this:
(?i \<in> {?l..?u}) = (?l \<le> ?i \<and> ?i \<le> ?u)
({?a..?b} \<subseteq> {?c..?d}) = (\<not> ?a \<le> ?b \<or> ?c \<le> ?a \<and> ?b \<le> ?d)
(?i \<in> {?l..<?u}) = (?l \<le> ?i \<and> ?i < ?u)
{?a..?b} \<inter> {?c..?d} = {max ?a ?c..min ?b ?d}
({?a..?b} = {}) = (\<not> ?a \<le> ?b)

goal (1 subgoal):
 1. s' \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. range_cover ptr sz (obj_bits (default_object ty dev us)) n proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n
ty \<noteq> Untyped

goal (1 subgoal):
 1. range_cover ptr sz (obj_bits (default_object ty dev us)) n proof (state)
this:
range_cover ptr sz (obj_bits (default_object ty dev us)) n

goal (1 subgoal):
 1. s' \<turnstile> cap proof (prove)
goal (1 subgoal):
 1. s' \<turnstile> cap proof (prove)
using this:
s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}

goal (1 subgoal):
 1. s' \<turnstile> cap proof (prove)
goal (12 subgoals):
 1. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = NullCap\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 2. \<And>x21 x22 x23 x24. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 3. \<And>x31 x32 x33. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 4. \<And>x41 x42 x43. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 5. \<And>x51 x52 x53. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 6. \<And>x61 x62 x63. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 7. \<And>x7. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 8. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = DomainCap\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 9. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = IRQControlCap\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
 10. \<And>x10. \<lbrakk>s \<turnstile> cap \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> s' \<turnstile> cap
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = NullCap\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 2. \<And>x21 x22 x23 x24. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 3. \<And>x31 x32 x33. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = EndpointCap x31 x32 x33\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 4. \<And>x41 x42 x43. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = NotificationCap x41 x42 x43\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 5. \<And>x51 x52 x53. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = ReplyCap x51 x52 x53\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 6. \<And>x61 x62 x63. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = CNodeCap x61 x62 x63\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 7. \<And>x7. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = ThreadCap x7\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 8. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = DomainCap\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 9. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = IRQControlCap\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
 10. \<And>x10. \<lbrakk>(cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s | NotificationCap r badge rights \<Rightarrow> ntfn_at r s \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s else typ_at (AArch (AUserData sz)) r s) \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)) \<and> untyped_range cap \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = IRQHandlerCap x10\<rbrakk> \<Longrightarrow> cap_aligned cap \<and> (case cap of UntypedCap dev p b f \<Rightarrow> valid_untyped cap s' \<and> untyped_min_bits \<le> b \<and> f \<le> 2 ^ b \<and> p \<noteq> 0 | EndpointCap r badge rights \<Rightarrow> ep_at r s' | NotificationCap r badge rights \<Rightarrow> ntfn_at r s' \<and> AllowGrant \<notin> rights \<and> AllowGrantReply \<notin> rights | ReplyCap r m rights \<Rightarrow> tcb_at r s' \<and> AllowWrite \<in> rights \<and> AllowRead \<notin> rights \<and> AllowGrantReply \<notin> rights | CNodeCap r bits guard \<Rightarrow> cap_table_at bits r s' \<and> bits \<noteq> 0 \<and> length guard \<le> word_bits | ThreadCap r \<Rightarrow> tcb_at r s' | IRQHandlerCap irq \<Rightarrow> irq \<le> maxIRQ | Zombie r None n \<Rightarrow> tcb_at r s' \<and> n \<le> 5 | Zombie r (Some ba) n \<Rightarrow> cap_table_at ba r s' \<and> n \<le> 2 ^ ba \<and> ba \<noteq> 0 | ArchObjectCap (ASIDPoolCap r as) \<Rightarrow> typ_at (AArch AASIDPool) r s' \<and> is_aligned as local.asid_low_bits \<and> as \<le> 2 ^ local.asid_bits - 1 | ArchObjectCap ASIDControlCap \<Rightarrow> True | ArchObjectCap (PageCap dev r rghts sz mapdata) \<Rightarrow> (if dev then typ_at (AArch (ADeviceData sz)) r s' else typ_at (AArch (AUserData sz)) r s') \<and> rghts \<in> valid_vm_rights \<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 < kernel_base) | ArchObjectCap (PageTableCap r mapdata) \<Rightarrow> typ_at (AArch APageTable) r s' \<and> (case mapdata of None \<Rightarrow> True | Some (asid, vref) \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1 \<and> vref < kernel_base \<and> is_aligned vref (pageBitsForSize ARMSection)) | ArchObjectCap (PageDirectoryCap r mapdata) \<Rightarrow> typ_at (AArch APageDirectory) r s' \<and> (case mapdata of None \<Rightarrow> True | Some asid \<Rightarrow> 0 < asid \<and> asid \<le> 2 ^ local.asid_bits - 1) | _ \<Rightarrow> True)
A total of 12 subgoals... proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap_aligned (UntypedCap x21 x22 x23 x24) \<and> valid_untyped (UntypedCap x21 x22 x23 x24) s \<and> untyped_min_bits \<le> x23 \<and> x24 \<le> 2 ^ x23 \<and> x22 \<noteq> 0 \<and> {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; cap = UntypedCap x21 x22 x23 x24\<rbrakk> \<Longrightarrow> valid_untyped (UntypedCap x21 x22 x23 x24) s'
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 4. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> (x24 < 2 ^ x23 \<longrightarrow> (\<forall>p. (p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p (default_object ty dev us) = {}) \<and> (p \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p obj = {})))) \<and> (x24 = 2 ^ x23 \<longrightarrow> (\<forall>p. p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1}))
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 4. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> x24 < 2 ^ x23 \<longrightarrow> (\<forall>p. (p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p (default_object ty dev us) = {}) \<and> (p \<notin> set (retype_addrs ptr ty n us) \<longrightarrow> (\<forall>obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p obj = {})))
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> x24 = 2 ^ x23 \<longrightarrow> (\<forall>p. p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1})
 3. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 4. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 5. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 p. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; x24 < 2 ^ x23; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> x24 = 2 ^ x23 \<longrightarrow> (\<forall>p. p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1})
 3. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 4. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 5. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x23 x24 p. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; x24 < 2 ^ x23; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<inter> ?B128 x21 x22 x23 x24 p = {}
 2. \<And>x21 x22 x23 x24 p. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; x24 < 2 ^ x23; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<inter> ?B128 x21 x22 x23 x24 p = {}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 3. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> x24 = 2 ^ x23 \<longrightarrow> (\<forall>p. p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1})
 4. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 5. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 6. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 x24 p. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; x24 < 2 ^ x23; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} = {}\<rbrakk> \<Longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} \<inter> obj_range p (default_object ty dev us) = {}
 2. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> x24 = 2 ^ x23 \<longrightarrow> (\<forall>p. p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1})
 3. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 4. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 5. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 x24. \<lbrakk>cap = UntypedCap x21 x22 x23 x24; cap_aligned (UntypedCap x21 x22 x23 x24); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1} \<and> (if x24 < 2 ^ x23 then {x22 + word_of_nat x24..x22 + 2 ^ x23 - 1} else {}) \<inter> obj_range p obj = {}; untyped_min_bits \<le> x23; x24 \<le> 2 ^ x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}\<rbrakk> \<Longrightarrow> x24 = 2 ^ x23 \<longrightarrow> (\<forall>p. p \<in> set (retype_addrs ptr ty n us) \<longrightarrow> obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p (default_object ty dev us) \<subseteq> {x22..x22 + 2 ^ x23 - 1})
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 4. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 p x. \<lbrakk>cap = UntypedCap x21 x22 x23 (2 ^ x23); cap_aligned (UntypedCap x21 x22 x23 (2 ^ x23)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; p \<in> set (retype_addrs ptr ty n us); obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> x \<in> {x22..x22 + 2 ^ x23 - 1}
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 4. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (5 subgoals):
 1. \<And>x21 x22 x23 p x. \<lbrakk>cap = UntypedCap x21 x22 x23 (2 ^ x23); cap_aligned (UntypedCap x21 x22 x23 (2 ^ x23)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us)\<rbrakk> \<Longrightarrow> up_aligned_area ptr sz \<inter> ?B142 x21 x22 x23 p x = {}
 2. \<And>x21 x22 x23 p x. \<lbrakk>cap = UntypedCap x21 x22 x23 (2 ^ x23); cap_aligned (UntypedCap x21 x22 x23 (2 ^ x23)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<inter> ?B142 x21 x22 x23 p x = {}\<rbrakk> \<Longrightarrow> x \<in> {x22..x22 + 2 ^ x23 - 1}
 3. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 4. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 5. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (4 subgoals):
 1. \<And>x21 x22 x23 p x. \<lbrakk>cap = UntypedCap x21 x22 x23 (2 ^ x23); cap_aligned (UntypedCap x21 x22 x23 (2 ^ x23)); \<forall>p obj. kheap s p = Some obj \<longrightarrow> obj_range p obj \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {} \<longrightarrow> obj_range p obj \<subseteq> {x22..x22 + 2 ^ x23 - 1}; untyped_min_bits \<le> x23; x22 \<noteq> 0; {x22..x22 + 2 ^ x23 - 1} \<inter> {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} = {}; obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} \<noteq> {}; x \<in> obj_range p (default_object ty dev us); obj_range p (default_object ty dev us) \<inter> {x22..x22 + 2 ^ x23 - 1} = {}\<rbrakk> \<Longrightarrow> x \<in> {x22..x22 + 2 ^ x23 - 1}
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 4. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (3 subgoals):
 1. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 2. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 3. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
using this:
range_cover ptr sz (obj_bits_api ty us) n
ty \<noteq> Untyped

goal (3 subgoals):
 1. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ((\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights) \<and> (\<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base)\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 2. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 3. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (7 subgoals):
 1. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = TCBObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object TCBObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = EndpointObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object EndpointObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = NotificationObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object NotificationObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 4. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = CapTableObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object CapTableObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 5. \<And>x12 x31 x32 x33 x34 x35 x6. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; ty = ArchObject x6; range_cover ptr sz (obj_bits (default_object (ArchObject x6) False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 6. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 7. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal (7 subgoals):
 1. \<And>x31 x32 x33 x34. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 None); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 None)); ty = TCBObject; range_cover ptr sz (obj_bits (default_object TCBObject False us)) n; if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s; x33 \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s') \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s')
 2. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = EndpointObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object EndpointObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 3. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = NotificationObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object NotificationObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 4. \<And>x12 x31 x32 x33 x34 x35. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; ty = CapTableObject; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; range_cover ptr sz (obj_bits (default_object CapTableObject False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 5. \<And>x12 x31 x32 x33 x34 x35 x6. \<lbrakk>cap = ArchObjectCap (PageCap x31 x32 x33 x34 x35); cap_aligned (ArchObjectCap (PageCap x31 x32 x33 x34 x35)); x12 = PageCap x31 x32 x33 x34 x35; (\<exists>a b. x35 = Some (a, b)) \<or> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> x33 \<in> valid_vm_rights; \<forall>a b. x35 = Some (a, b) \<longrightarrow> x33 \<in> valid_vm_rights \<and> (if x31 then typ_at (AArch (ADeviceData x34)) x32 s else typ_at (AArch (AUserData x34)) x32 s) \<and> vmsz_aligned b x34 \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> b < kernel_base; ty = ArchObject x6; range_cover ptr sz (obj_bits (default_object (ArchObject x6) False us)) n\<rbrakk> \<Longrightarrow> x35 = None \<longrightarrow> (x31 \<longrightarrow> typ_at (AArch (ADeviceData x34)) x32 s' \<and> x33 \<in> valid_vm_rights) \<and> (\<not> x31 \<longrightarrow> typ_at (AArch (AUserData x34)) x32 s' \<and> x33 \<in> valid_vm_rights)
 6. \<And>x12 x41 x42. \<lbrakk>cap = ArchObjectCap (PageTableCap x41 x42); cap_aligned (ArchObjectCap (PageTableCap x41 x42)); x12 = PageTableCap x41 x42; ((\<exists>a b. x42 = Some (a, b)) \<or> typ_at (AArch APageTable) x41 s) \<and> (\<forall>a b. x42 = Some (a, b) \<longrightarrow> typ_at (AArch APageTable) x41 s \<and> b < kernel_base \<and> a < 2 ^ local.asid_bits \<and> 0 < a \<and> is_aligned b 20)\<rbrakk> \<Longrightarrow> x42 = None \<longrightarrow> typ_at (AArch APageTable) x41 s'
 7. \<And>x12 x51 x52. \<lbrakk>cap = ArchObjectCap (PageDirectoryCap x51 x52); cap_aligned (ArchObjectCap (PageDirectoryCap x51 x52)); x12 = PageDirectoryCap x51 x52; ((\<exists>y. x52 = Some y) \<or> typ_at (AArch APageDirectory) x51 s) \<and> (\<forall>x2. x52 = Some x2 \<longrightarrow> 0 < x2 \<and> typ_at (AArch APageDirectory) x51 s \<and> x2 < 2 ^ local.asid_bits)\<rbrakk> \<Longrightarrow> x52 = None \<longrightarrow> typ_at (AArch APageDirectory) x51 s' proof (prove)
goal:
No subgoals! proof (state)
this:
s' \<turnstile> cap

goal:
No subgoals!