theory Arch_R

lemma resolve_vaddr_valid_mapping_size:
  "\<lbrace> valid_vs_lookup and pspace_aligned and valid_vspace_objs and page_directory_at pd
                 and (\<exists>\<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits))
                 and valid_objs and K (vaddr < kernel_base) \<rbrace>
    resolve_vaddr pd vaddr \<lbrace> \<lambda>rv s. case rv of None \<Rightarrow> True
    | Some (a, b) \<Rightarrow> \<exists>p cap. caps_of_state s p = Some cap
        \<and> (case cap of cap.ArchObjectCap c \<Rightarrow> is_page_cap c | _ \<Rightarrow> False)
        \<and> cap_bits cap = pageBitsForSize a \<rbrace> " apply (simp add: resolve_vaddr_def) apply (rule hoare_seq_ext[OF _ get_master_pde_sp]) apply (rule hoare_pre) apply (wp get_master_pte_wp | wpc
     | simp add: lookup_pt_slot_no_fail_def)+ apply (clarsimp simp: obj_at_def) apply (frule(1) pspace_alignedD, simp) apply (drule_tac y=pd_bits in is_aligned_weaken, simp add: pd_bits_def pageBits_def) apply (frule valid_vspace_objsD, simp add: obj_at_def lookup_pd_slot_eq, simp) apply (simp add: lookup_pd_slot_eq less_kernel_base_mapping_slots) apply (drule bspec, simp) apply (rule conjI) apply clarsimp apply (drule vs_lookup_step) apply (rule vs_lookup1I, simp add: obj_at_def) apply (erule(1) vs_refs_pdI2) apply simp apply (drule sym[where s=pd]) apply (simp add: lookup_pd_slot_eq) apply (frule(1) is_aligned_pt) apply (frule is_aligned_weaken[where x=pt_bits and y=10]) apply (simp add: pt_bits_def pageBits_def) apply (simp add: vaddr_segment_nonsense3) apply (frule valid_vspace_objsD, simp add: obj_at_def, simp) apply (drule vs_lookup_pages_vs_lookupI) apply (rule conjI) apply (clarsimp simp:) apply (drule_tac x="ucast (pt_slot' && mask pt_bits >> 2)" in spec) apply (drule vs_lookup_pages_step) apply (rule vs_lookup_pages1I, simp add: obj_at_def) apply (erule vs_refs_pages_pt_largeI) apply simp apply (drule(1) valid_vs_lookupD) apply simp apply (erule exEI)+ apply (clarsimp simp: vs_cap_ref_def split: cap.split_asm arch_cap.split_asm
           option.split_asm vmpage_size.split_asm) apply (frule(1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
                   split: if_split_asm) apply (clarsimp simp: vaddr_segment_nonsense4) apply (drule_tac x="ucast (pt_slot' && mask pt_bits >> 2)" in spec) apply (drule vs_lookup_pages_step) apply (rule vs_lookup_pages1I, simp add: obj_at_def) apply (erule vs_refs_pages_pt_smallI) apply simp apply (drule(1) valid_vs_lookupD) apply simp apply (erule exEI)+ apply (clarsimp simp: vs_cap_ref_def split: cap.split_asm arch_cap.split_asm
          option.split_asm vmpage_size.split_asm) apply (frule(1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
                  split: if_split_asm) apply (drule vs_lookup_pages_vs_lookupI) apply (rule conjI) apply clarsimp apply (drule vs_lookup_pages_step) apply (rule vs_lookup_pages1I, simp add: obj_at_def) apply (erule(1) vs_refs_pages_pd_sectionI) apply simp apply (drule(1) valid_vs_lookupD) apply simp apply (erule exEI)+ apply (clarsimp simp: vs_cap_ref_def split: cap.split_asm arch_cap.split_asm
          option.split_asm vmpage_size.split_asm) apply (frule(1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
                   split: if_split_asm) apply (frule(1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
                  split: if_split_asm) apply clarsimp apply (drule vs_lookup_pages_step) apply (rule vs_lookup_pages1I, simp add: obj_at_def) apply (erule(1) vs_refs_pages_pd_supersectionI) apply simp apply (drule(1) valid_vs_lookupD) apply simp apply (erule exEI)+ apply (clarsimp simp: vs_cap_ref_def
                 split: cap.split_asm arch_cap.split_asm
                        option.split_asm vmpage_size.split_asm) apply (frule(1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
                  split: if_split_asm) apply (frule(1) caps_of_state_valid_cap) apply (clarsimp simp: valid_cap_def obj_at_def data_at_def a_type_simps
                 split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s) and valid_objs and K (vaddr < kernel_base)\<rbrace> resolve_vaddr pd vaddr \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some (a, b) \<Rightarrow> \<exists>p cap. caps_of_state s p = Some cap \<and> (case cap of cap.ArchObjectCap c \<Rightarrow> is_page_cap c | _ \<Rightarrow> False) \<and> cap_bits cap = pageBitsForSize a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vs_lookup and pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s) and valid_objs and (\<lambda>y. vaddr < kernel_base)\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) >>= ARM_A.case_pde (return None) (\<lambda>t x xa. get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f)))) (\<lambda>f x xa xb. return (Some (ARMSection, f))) (\<lambda>f x xa. return (Some (ARMSuperSection, f))) \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some (a, b) \<Rightarrow> \<exists>aa b cap. caps_of_state s (aa, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = pageBitsForSize a\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>\<lambda>s. (valid_vs_lookup and pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s) and valid_objs and (\<lambda>y. vaddr < kernel_base)) s \<and> (\<exists>pda pd_slot'. ako_at (PageDirectory pda) (lookup_pd_slot pd vaddr && ~~ mask pd_bits) s \<and> pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits \<and> (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots) \<and> pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = x)\<rbrace> case x of ARM_A.InvalidPDE \<Rightarrow> return None | ARM_A.PageTablePDE t x xa \<Rightarrow> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f))) | ARM_A.SectionPDE f x xa xb \<Rightarrow> return (Some (ARMSection, f)) | ARM_A.SuperSectionPDE f x xa \<Rightarrow> return (Some (ARMSuperSection, f)) \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some (a, b) \<Rightarrow> \<exists>aa b cap. caps_of_state s (aa, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = pageBitsForSize a\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>?Q8 x\<rbrace> case x of ARM_A.InvalidPDE \<Rightarrow> return None | ARM_A.PageTablePDE t x xa \<Rightarrow> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f))) | ARM_A.SectionPDE f x xa xb \<Rightarrow> return (Some (ARMSection, f)) | ARM_A.SuperSectionPDE f x xa \<Rightarrow> return (Some (ARMSuperSection, f)) \<lbrace>\<lambda>rv s. case rv of None \<Rightarrow> True | Some (a, b) \<Rightarrow> \<exists>aa b cap. caps_of_state s (aa, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = pageBitsForSize a\<rbrace>
 2. \<And>x s. (valid_vs_lookup and pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s) and valid_objs and (\<lambda>y. vaddr < kernel_base)) s \<and> (\<exists>pda pd_slot'. ako_at (PageDirectory pda) (lookup_pd_slot pd vaddr && ~~ mask pd_bits) s \<and> pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits \<and> (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots) \<and> pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = x) \<Longrightarrow> ?Q8 x s proof (prove)
goal (1 subgoal):
 1. \<And>x s. valid_vs_lookup s \<and> pspace_aligned s \<and> valid_vspace_objs s \<and> typ_at (AArch APageDirectory) pd s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s) \<and> valid_objs s \<and> vaddr < kernel_base \<and> (\<exists>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vaddr && ~~ mask pd_bits) s \<and> (\<exists>pd_slot'. pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits \<and> (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots) \<and> pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = x)) \<Longrightarrow> (\<forall>xa. (\<exists>xb xc. x = ARM_A.PageTablePDE xa xb xc) \<longrightarrow> (\<forall>pt pt_slot'. ako_at (PageTable pt) (ptrFromPAddr xa + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) s \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr xa + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>xa xb xc xd. x = ARM_A.SectionPDE xa xb xc xd) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>xa xb xc. x = ARM_A.SuperSectionPDE xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; kheap s (lookup_pd_slot pd vaddr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; kheap s (lookup_pd_slot pd vaddr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots; is_aligned pd 14\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; kheap s (lookup_pd_slot pd vaddr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots; is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; kheap s (lookup_pd_slot pd vaddr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pdaa)); pd_slot' && ~~ mask pd_bits = lookup_pd_slot pd vaddr && ~~ mask pd_bits; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<in> kernel_mapping_slots \<longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<in> kernel_mapping_slots; is_aligned pd pd_bits; valid_vspace_obj (PageDirectory pdaa) s\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pdaa x) s\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> (\<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))) \<and> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> \<forall>x. (\<exists>xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb) \<longrightarrow> (\<forall>pt pt_slot'. kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)) \<and> pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits \<longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> (pd_slot' && ~~ mask pd_bits)) s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> ((ref, pd_slot' && ~~ mask pd_bits), ?ref'132 s ref pda pd_slot' x xa xb pt pt_slot', ?p'132 s ref pda pd_slot' x xa xb pt pt_slot') \<in> vs_lookup1 s
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; (?ref'132 s ref pda pd_slot' x xa xb pt pt_slot' \<rhd> ?p'132 s ref pda pd_slot' x xa xb pt pt_slot') s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (4 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> (?r135 s ref pda pd_slot' x xa xb pt pt_slot', ?p'132 s ref pda pd_slot' x xa xb pt pt_slot') \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> ?ref'132 s ref pda pd_slot' x xa xb pt pt_slot' = ?r135 s ref pda pd_slot' x xa xb pt pt_slot' # ref
 3. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; (?ref'132 s ref pda pd_slot' x xa xb pt pt_slot' \<rhd> ?p'132 s ref pda pd_slot' x xa xb pt pt_slot') s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 4. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits\<rbrakk> \<Longrightarrow> ?ref'132 s ref pda pd_slot' x xa xb pt pt_slot' = VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; (?ref'132 s ref pda pd_slot' x xa xb pt pt_slot' \<rhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits\<rbrakk> \<Longrightarrow> 10 \<le> pt_bits
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<rhd> ptrFromPAddr x) s; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)) \<and> ((\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12))
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16)
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; \<forall>x. valid_pte (pt x) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (4 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref, ptrFromPAddr x), ?ref'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe, ?p'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) \<in> vs_lookup_pages1 s
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; (?ref'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe \<unrhd> ?p'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 3. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 4. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (5 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> (?r176 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe, ?p'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) \<in> vs_refs_pages (ArchObj (PageTable pt))
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> ?ref'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe = ?r176 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 3. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; (?ref'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe \<unrhd> ?p'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 4. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 5. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (4 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> ?ref'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe = VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; (?ref'173 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe \<unrhd> ptrFromPAddr xc) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 3. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 4. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; ((VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr xc) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> ptrFromPAddr xc \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; data_at ARMLargePage (ptrFromPAddr xc) s; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> ptrFromPAddr xc \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 16
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe xf xg xh. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; data_at ARMLargePage (ptrFromPAddr xc) s; caps_of_state s (xf, xg) = Some xh \<and> ptrFromPAddr xc \<in> obj_refs xh \<and> vs_cap_ref xh = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> caps_of_state s (xf, xg) = Some xh \<and> (case xh of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits xh = 16
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pd_slot' x xa xb pt pt_slot' xc xd xe xf xg x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; data_at ARMLargePage (ptrFromPAddr xc) s; caps_of_state s (xf, xg) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr xc) x33 ARMSmallPage (Some (a, b)))); (b >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pd_slot' x xa xb pt pt_slot' xc xd xe xf xg x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.LargePagePTE xc xd xe; data_at ARMLargePage (ptrFromPAddr xc) s; caps_of_state s (xf, xg) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr xc) x33 ARMSmallPage (Some (a, b)))); (b >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr xc) x33 ARMSmallPage (Some (a, b)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; pd_slot' && ~~ mask pd_bits = pd; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; valid_vspace_obj (PageTable pt) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12)
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; \<forall>x. valid_pte (pt x) s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref, ptrFromPAddr x), ?ref'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe, ?p'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) \<in> vs_lookup_pages1 s
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; (?ref'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe \<unrhd> ?p'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (4 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> (?r508 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe, ?p'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) \<in> vs_refs_pages (ArchObj (PageTable pt))
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> ?ref'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe = ?r508 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 3. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; (?ref'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe \<unrhd> ?p'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 4. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s\<rbrakk> \<Longrightarrow> ?ref'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe = VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 2. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; (?ref'505 s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe \<unrhd> ptrFromPAddr xc) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; ((VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr xc) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; valid_pte (pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> ptrFromPAddr xc \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; data_at ARMSmallPage (ptrFromPAddr xc) s; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> ptrFromPAddr xc \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 12
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb pt pt_slot' xc xd xe xf xg xh. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; data_at ARMSmallPage (ptrFromPAddr xc) s; caps_of_state s (xf, xg) = Some xh \<and> ptrFromPAddr xc \<in> obj_refs xh \<and> vs_cap_ref xh = Some (VSRef (UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2))) (Some APageTable) # VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> caps_of_state s (xf, xg) = Some xh \<and> (case xh of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits xh = 12
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pd_slot' x xa xb pt pt_slot' xc xd xe xf xg x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; data_at ARMSmallPage (ptrFromPAddr xc) s; caps_of_state s (xf, xg) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr xc) x33 ARMLargePage (Some (a, b)))); (b >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pd_slot' x xa xb pt pt_slot' xc xd xe xf xg x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; typ_at (AArch APageTable) (ptrFromPAddr x) s; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); pt_slot' && ~~ mask pt_bits = ptrFromPAddr x; is_aligned (ptrFromPAddr x) pt_bits; is_aligned (ptrFromPAddr x) 10; pd = pd_slot' && ~~ mask pd_bits; pt (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)) = ARM_A.SmallPagePTE xc xd xe; data_at ARMSmallPage (ptrFromPAddr xc) s; caps_of_state s (xf, xg) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr xc) x33 ARMLargePage (Some (a, b)))); (b >> 12) && mask 8 = UCAST(8 \<rightarrow> 32) (UCAST(32 \<rightarrow> 8) (pt_slot' && mask pt_bits >> 2)); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr xc) x33 ARMLargePage (Some (a, b)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> ((\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)) \<and> ((\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24)) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb xc. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20)
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; (ref \<unrhd> (pd_slot' && ~~ mask pd_bits)) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc\<rbrakk> \<Longrightarrow> ((ref, pd_slot' && ~~ mask pd_bits), ?ref'841 s ref pda pd_slot' x xa xb xc, ?p'841 s ref pda pd_slot' x xa xb xc) \<in> vs_lookup_pages1 s
 2. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; (?ref'841 s ref pda pd_slot' x xa xb xc \<unrhd> ?p'841 s ref pda pd_slot' x xa xb xc) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (4 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc\<rbrakk> \<Longrightarrow> (?r844 s ref pda pd_slot' x xa xb xc, ?p'841 s ref pda pd_slot' x xa xb xc) \<in> vs_refs_pages (ArchObj (PageDirectory pda))
 2. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc\<rbrakk> \<Longrightarrow> ?ref'841 s ref pda pd_slot' x xa xb xc = ?r844 s ref pda pd_slot' x xa xb xc # ref
 3. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; (?ref'841 s ref pda pd_slot' x xa xb xc \<unrhd> ?p'841 s ref pda pd_slot' x xa xb xc) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 4. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc\<rbrakk> \<Longrightarrow> ?ref'841 s ref pda pd_slot' x xa xb xc = VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 2. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; (?ref'841 s ref pda pd_slot' x xa xb xc \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; \<exists>slot cap. caps_of_state s slot = Some cap \<and> ptrFromPAddr x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> ptrFromPAddr x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 20
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb xc xd xe xf. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some xf \<and> ptrFromPAddr x \<in> obj_refs xf \<and> vs_cap_ref xf = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> caps_of_state s (xd, xe) = Some xf \<and> (case xf of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits xf = 20
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pd_slot' x xa xb xc xd xe x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr x) x33 ARMSuperSection (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda pd_slot' x xa xb xc xd xe a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (3 subgoals):
 1. \<And>s pda pd_slot' x xa xb xc xd xe x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr x) x33 ARMSuperSection (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr x) x33 ARMSuperSection (Some (a, b)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda pd_slot' x xa xb xc xd xe a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 3. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pd_slot' x xa xb xc xd xe a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (2 subgoals):
 1. \<And>s pda pd_slot' x xa xb xc xd xe a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SectionPDE x xa xb xc; caps_of_state s (xd, xe) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pdaa pd_slot'. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s pd = Some (ArchObj (PageDirectory pdaa)); valid_objs s; vaddr < kernel_base; pda = pdaa; pd_slot' && ~~ mask pd_bits = pd; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; is_aligned pd pd_bits; valid_pde (pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> (\<exists>x xa xb. pdaa (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb) \<longrightarrow> (\<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; (ref \<unrhd> (pd_slot' && ~~ mask pd_bits)) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb\<rbrakk> \<Longrightarrow> ((ref, pd_slot' && ~~ mask pd_bits), ?ref'1178 s ref pda pd_slot' x xa xb, ?p'1178 s ref pda pd_slot' x xa xb) \<in> vs_lookup_pages1 s
 2. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; (?ref'1178 s ref pda pd_slot' x xa xb \<unrhd> ?p'1178 s ref pda pd_slot' x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb\<rbrakk> \<Longrightarrow> (?r1181 s ref pda pd_slot' x xa xb, ?p'1178 s ref pda pd_slot' x xa xb) \<in> vs_refs_pages (ArchObj (PageDirectory pda))
 2. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb\<rbrakk> \<Longrightarrow> ?ref'1178 s ref pda pd_slot' x xa xb = ?r1181 s ref pda pd_slot' x xa xb # ref
 3. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; (?ref'1178 s ref pda pd_slot' x xa xb \<unrhd> ?p'1178 s ref pda pd_slot' x xa xb) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb\<rbrakk> \<Longrightarrow> ?ref'1178 s ref pda pd_slot' x xa xb = VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref
 2. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; (?ref'1178 s ref pda pd_slot' x xa xb \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref) \<unrhd> ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; \<exists>slot cap. caps_of_state s slot = Some cap \<and> ptrFromPAddr x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pd_slot' x xa xb. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> ptrFromPAddr x \<in> obj_refs cap \<and> vs_cap_ref cap = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> (case cap of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits cap = 24 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda pd_slot' x xa xb xc xd xe. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some xe \<and> ptrFromPAddr x \<in> obj_refs xe \<and> vs_cap_ref xe = Some (VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))) (Some APageDirectory) # ref)\<rbrakk> \<Longrightarrow> caps_of_state s (xc, xd) = Some xe \<and> (case xe of cap.ArchObjectCap x \<Rightarrow> is_page_cap x | _ \<Rightarrow> False) \<and> cap_bits xe = 24 proof (prove)
goal (2 subgoals):
 1. \<And>s pda pd_slot' x xa xb xc xd x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr x) x33 ARMSection (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda pd_slot' x xa xb xc xd a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda pd_slot' x xa xb xc xd x31 x33 a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some (cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr x) x33 ARMSection (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap x31 (ptrFromPAddr x) x33 ARMSection (Some (a, b)))\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda pd_slot' x xa xb xc xd a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda pd_slot' x xa xb xc xd a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda pd_slot' x xa xb xc xd a b. \<lbrakk>valid_vs_lookup s; pspace_aligned s; valid_vspace_objs s; kheap s (pd_slot' && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); valid_objs s; vaddr < kernel_base; UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2) \<notin> kernel_mapping_slots; data_at ARMSuperSection (ptrFromPAddr x) s; pd = pd_slot' && ~~ mask pd_bits; pda (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)) = ARM_A.SuperSectionPDE x xa xb; caps_of_state s (xc, xd) = Some (cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))); b >> 20 = UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (pd_slot' && mask pd_bits >> 2)); s \<turnstile> cap.ArchObjectCap (arch_cap.PageTableCap (ptrFromPAddr x) (Some (a, b)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!