theory ArchAInvsPre

lemma some_get_page_info_umapsD:
  "\<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r);
    (\<exists>\<rhd> pd_ref) s; p \<notin> kernel_mappings; valid_vspace_objs s; pspace_aligned s;
    valid_asid_table (arm_asid_table (arch_state s)) s; valid_objs s\<rbrakk>
   \<Longrightarrow> (\<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and>
             data_at sz (ptrFromPAddr b) s)" apply (clarsimp simp: get_page_info_def get_pd_entry_def get_arch_obj_def
                        kernel_mappings_slots_eq
                 split: option.splits Structures_A.kernel_object.splits
                        arch_kernel_obj.splits) apply (frule (1) valid_vspace_objsD[rotated 2]) apply (simp add: obj_at_def) apply (simp add: valid_vspace_obj_def) apply (drule bspec, simp) apply (simp split: pde.splits) apply (rename_tac rs pd pt_ref rights w) apply (subgoal_tac
        "((rs, pd_ref) \<rhd>1
          (VSRef (ucast (ucast (p >> 20))) (Some APageDirectory) # rs,
           ptrFromPAddr pt_ref)) s") prefer 2 apply (rule vs_lookup1I[rotated 2], simp) apply (simp add: obj_at_def) apply (simp add: vs_refs_def pde_ref_def image_def graph_of_def) apply (rule exI, rule conjI, simp+) apply (frule (1) vs_lookup_step) apply (drule (2) stronger_vspace_objsD[where ref="x # xs" for x xs]) apply clarsimp apply (case_tac ao, simp_all add: a_type_simps obj_at_def )[1] apply (simp add: get_pt_info_def get_pt_entry_def) apply (drule_tac x="(ucast ((p >> 12) && mask 8))" in spec) apply (clarsimp simp: obj_at_def split: pte.splits,intro exI conjI,simp_all)[1] apply (frule obj_bits_data_at) apply (clarsimp simp: pspace_aligned_def data_at_def) apply (drule_tac x = "(ptrFromPAddr b)" in  bspec ) apply (fastforce simp: obj_at_def) apply (clarsimp dest!: is_aligned_ptrFromPAddrD) apply (frule (1) data_at_aligned) apply (intro exI conjI, simp_all add: pageBits_def is_aligned_ptrFromPAddrD)[1] apply (simp add: get_pt_info_def get_pt_entry_def) apply (frule obj_bits_data_at) apply (intro exI conjI, simp_all add: pageBits_def)[1] apply (clarsimp simp: pspace_aligned_def data_at_def) apply (drule_tac x = "(ptrFromPAddr b)" in  bspec) apply (fastforce simp: obj_at_def) apply (clarsimp dest!: is_aligned_ptrFromPAddrD) apply (frule obj_bits_data_at) apply (intro exI conjI, simp_all add: pageBits_def)[1] apply (clarsimp simp: pspace_aligned_def data_at_def) apply (drule_tac x = "(ptrFromPAddr b)" in  bspec) apply (fastforce simp: obj_at_def) apply (clarsimp dest!: is_aligned_ptrFromPAddrD) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>get_page_info (\<lambda>obj. get_arch_obj (kheap s obj)) pd_ref p = Some (b, a, attr, r); \<exists>ref. (ref \<rhd> pd_ref) s; p \<notin> kernel_mappings; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>(ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (2 subgoals):
 1. \<And>ref x3. \<lbrakk>(ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s\<rbrakk> \<Longrightarrow> ako_at (?ao102 ref x3) pd_ref s
 2. \<And>ref x3. \<lbrakk>(ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; valid_vspace_obj (?ao102 ref x3) s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>(ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; valid_vspace_obj (PageDirectory x3) s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>(ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; \<forall>x\<in>- kernel_mapping_slots. valid_pde (x3 x) s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>(ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); (case x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) of InvalidPDE \<Rightarrow> None | PageTablePDE pa x xa \<Rightarrow> get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj xa) \<Rightarrow> Some xa | Some _ \<Rightarrow> None) (ptrFromPAddr pa) p | SectionPDE base attrs x rights \<Rightarrow> Some (base, 20, attrs, rights) | SuperSectionPDE base attrs rights \<Rightarrow> Some (base, 24, attrs, rights)) = Some (b, a, attr, r); UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; valid_pde (x3 (UCAST(32 \<rightarrow> 12) (p >> 20))) s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>ref x3 x21 x22 x23. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr x21) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE x21 x22 x23; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr x21) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s
 2. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (5 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> ko_at (?ko139 rs pd pt_ref rights w) pd_ref s
 2. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> (VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory), ptrFromPAddr pt_ref) \<in> vs_refs (?ko139 rs pd pt_ref rights w)
 3. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 5. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> (VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory), ptrFromPAddr pt_ref) \<in> vs_refs (ArchObj (PageDirectory pd))
 2. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r)\<rbrakk> \<Longrightarrow> \<exists>a. a \<notin> kernel_mapping_slots \<and> (a \<notin> kernel_mapping_slots \<longrightarrow> (case pd a of PageTablePDE ptr x z \<Rightarrow> Some (ptrFromPAddr ptr) | _ \<Rightarrow> None) = Some (ptrFromPAddr pt_ref) \<and> UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20)) = UCAST(12 \<rightarrow> 32) a)
 2. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(?'b138 \<rightarrow> 32) (UCAST(32 \<rightarrow> ?'b138) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; ((VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs) \<rhd> ptrFromPAddr pt_ref) s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>rs pd pt_ref rights w. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; \<exists>ao. ako_at ao (ptrFromPAddr pt_ref) s \<and> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>rs pd pt_ref rights w ao. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch APageTable) (ptrFromPAddr pt_ref) s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; ako_at ao (ptrFromPAddr pt_ref) s; valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w ao x2. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); \<forall>x. valid_pte (x2 x) s; ao = PageTable x2\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w ao x2. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; (case x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); \<forall>x. valid_pte (x2 x) s; ao = PageTable x2\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w ao x2. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; (case x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) of InvalidPTE \<Rightarrow> None | LargePagePTE base attrs rights \<Rightarrow> Some (base, 16, attrs, rights) | SmallPagePTE base attrs rights \<Rightarrow> Some (base, 12, attrs, rights)) = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); ao = PageTable x2; valid_pte (x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8))) s\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (5 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMLargePage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16\<rbrakk> \<Longrightarrow> is_aligned b 16
 2. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 5. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (5 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMLargePage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16; obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize ARMLargePage\<rbrakk> \<Longrightarrow> is_aligned b 16
 2. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 5. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (5 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); typ_at (AArch (AUserData ARMLargePage)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMLargePage)) (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16; obj_bits (the (kheap s (ptrFromPAddr b))) = 16\<rbrakk> \<Longrightarrow> is_aligned b 16
 2. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 5. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (6 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); typ_at (AArch (AUserData ARMLargePage)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMLargePage)) (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16; obj_bits (the (kheap s (ptrFromPAddr b))) = 16\<rbrakk> \<Longrightarrow> ptrFromPAddr b \<in> dom (kheap s)
 2. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); typ_at (AArch (AUserData ARMLargePage)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMLargePage)) (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16; obj_bits (the (kheap s (ptrFromPAddr b))) = 16; is_aligned (ptrFromPAddr b) (obj_bits (the (kheap s (ptrFromPAddr b))))\<rbrakk> \<Longrightarrow> is_aligned b 16
 3. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 5. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 6. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (5 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); typ_at (AArch (AUserData ARMLargePage)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMLargePage)) (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = LargePagePTE b attr r; a = 16; obj_bits (the (kheap s (ptrFromPAddr b))) = 16; is_aligned (ptrFromPAddr b) (obj_bits (the (kheap s (ptrFromPAddr b))))\<rbrakk> \<Longrightarrow> is_aligned b 16
 2. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 5. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (4 subgoals):
 1. \<And>rs pd pt_ref rights w x2. \<lbrakk>((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (PageTable x2)); data_at ARMSmallPage (ptrFromPAddr b) s; UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; x2 (UCAST(32 \<rightarrow> 8) ((p >> 12) && mask 8)) = SmallPagePTE b attr r; a = 12; is_aligned (ptrFromPAddr b) (pageBitsForSize ARMSmallPage)\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 12 \<and> is_aligned b 12 \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 4. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>rs pd pt_ref rights w ao x41 x42. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; (if x41 then ADeviceData x42 else AUserData x42) = APageTable; (rs \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory pd)); pd (UCAST(32 \<rightarrow> 12) (p >> 20)) = PageTablePDE pt_ref rights w; get_pt_info (\<lambda>obj. case kheap s obj of None \<Rightarrow> None | Some (ArchObj x) \<Rightarrow> Some x | Some _ \<Rightarrow> None) (ptrFromPAddr pt_ref) p = Some (b, a, attr, r); ((rs, pd_ref), VSRef (UCAST(12 \<rightarrow> 32) (UCAST(32 \<rightarrow> 12) (p >> 20))) (Some APageDirectory) # rs, ptrFromPAddr pt_ref) \<in> vs_lookup1 s; kheap s (ptrFromPAddr pt_ref) = Some (ArchObj (DataPage x41 x42)); ao = DataPage x41 x42\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = a \<and> is_aligned b a \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (2 subgoals):
 1. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (2 subgoals):
 1. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20; obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize ARMSection\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 20 \<and> is_aligned b 20 \<and> data_at sz (ptrFromPAddr b) s
 2. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (2 subgoals):
 1. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20; obj_bits (the (kheap s (ptrFromPAddr b))) = 20\<rbrakk> \<Longrightarrow> is_aligned b 20
 2. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (2 subgoals):
 1. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20; obj_bits (the (kheap s (ptrFromPAddr b))) = 20\<rbrakk> \<Longrightarrow> is_aligned b 20
 2. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (3 subgoals):
 1. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20; obj_bits (the (kheap s (ptrFromPAddr b))) = 20\<rbrakk> \<Longrightarrow> ptrFromPAddr b \<in> dom (kheap s)
 2. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20; obj_bits (the (kheap s (ptrFromPAddr b))) = 20; is_aligned (ptrFromPAddr b) (obj_bits (the (kheap s (ptrFromPAddr b))))\<rbrakk> \<Longrightarrow> is_aligned b 20
 3. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (2 subgoals):
 1. \<And>ref x3 x33. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SectionPDE b attr x33 r; a = 20; obj_bits (the (kheap s (ptrFromPAddr b))) = 20; is_aligned (ptrFromPAddr b) (obj_bits (the (kheap s (ptrFromPAddr b))))\<rbrakk> \<Longrightarrow> is_aligned b 20
 2. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24; obj_bits (the (kheap s (ptrFromPAddr b))) = pageBitsForSize ARMSuperSection\<rbrakk> \<Longrightarrow> \<exists>sz. pageBitsForSize sz = 24 \<and> is_aligned b 24 \<and> data_at sz (ptrFromPAddr b) s proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; pspace_aligned s; valid_asid_table (asid_table s) s; valid_objs s; data_at ARMSuperSection (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24; obj_bits (the (kheap s (ptrFromPAddr b))) = 24\<rbrakk> \<Longrightarrow> is_aligned b 24 proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSuperSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSuperSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24; obj_bits (the (kheap s (ptrFromPAddr b))) = 24\<rbrakk> \<Longrightarrow> is_aligned b 24 proof (prove)
goal (2 subgoals):
 1. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSuperSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSuperSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24; obj_bits (the (kheap s (ptrFromPAddr b))) = 24\<rbrakk> \<Longrightarrow> ptrFromPAddr b \<in> dom (kheap s)
 2. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSuperSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSuperSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24; obj_bits (the (kheap s (ptrFromPAddr b))) = 24; is_aligned (ptrFromPAddr b) (obj_bits (the (kheap s (ptrFromPAddr b))))\<rbrakk> \<Longrightarrow> is_aligned b 24 proof (prove)
goal (1 subgoal):
 1. \<And>ref x3. \<lbrakk>UCAST(32 \<rightarrow> 12) (p >> 20) \<notin> kernel_mapping_slots; valid_vspace_objs s; valid_asid_table (asid_table s) s; valid_objs s; typ_at (AArch (AUserData ARMSuperSection)) (ptrFromPAddr b) s \<or> typ_at (AArch (ADeviceData ARMSuperSection)) (ptrFromPAddr b) s; (ref \<rhd> pd_ref) s; kheap s pd_ref = Some (ArchObj (PageDirectory x3)); x3 (UCAST(32 \<rightarrow> 12) (p >> 20)) = SuperSectionPDE b attr r; a = 24; obj_bits (the (kheap s (ptrFromPAddr b))) = 24; is_aligned (ptrFromPAddr b) (obj_bits (the (kheap s (ptrFromPAddr b))))\<rbrakk> \<Longrightarrow> is_aligned b 24 proof (prove)
goal:
No subgoals!