theory ArchAcc_AI

lemma create_mapping_entries_valid_slots [wp]:
  "\<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings
   and pspace_aligned and valid_global_objs
   and \<exists>\<rhd> pd and page_directory_at pd and data_at sz (ptrFromPAddr base) and
    K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base
       \<and> vm_rights \<in> valid_vm_rights)\<rbrace>
  create_mapping_entries base vptr sz vm_rights attrib pd
  \<lbrace>\<lambda>m. valid_slots m\<rbrace>, -" apply (cases sz) apply (rule hoare_pre) apply (wp lookup_pt_slot_inv | simp add: valid_slots_def)+ apply (clarsimp simp: vmsz_aligned_def pd_aligned pageBits_def) apply (rule hoare_pre) apply (simp add: valid_slots_def largePagePTE_offsets_def pd_bits_def) apply (wpsimp wp: lookup_pt_slot_inv lookup_pt_slot_non_empty
           | simp add: valid_slots_def ball_conj_distrib largePagePTE_offsets_def)+ apply (clarsimp simp: pd_aligned vmsz_aligned_def upto_enum_def upto_enum_step_def
                          is_aligned_weaken pageBits_def) apply (clarsimp simp add: valid_slots_def) apply (rule hoare_pre) apply wp apply (clarsimp simp: valid_slots_def) apply (rule conjI) apply (simp add: lookup_pd_slot_def Let_def) apply (fastforce simp: pd_shifting pd_aligned) apply (simp add: page_directory_pde_at_lookupI) apply (erule less_kernel_base_mapping_slots) apply (simp add: pd_aligned pd_bits) apply simp apply (clarsimp simp: superSectionPDE_offsets_def) apply (rule hoare_pre) apply (clarsimp simp add: valid_slots_def) apply wp apply simp apply (elim conjE) apply (thin_tac "vmsz_aligned base b" for b) apply (subgoal_tac "is_aligned pd 14") prefer 2 apply (clarsimp simp: pd_aligned) apply (clarsimp simp: upto_enum_step_def  word_shift_by_2) apply (clarsimp simp: obj_at_def pde_at_def) apply (subgoal_tac "is_aligned pd pd_bits") prefer 2 apply (simp add: pd_bits) apply (rule conjI, simp add: upto_enum_def) apply (intro allI impI) apply (subst less_kernel_base_mapping_slots_both,assumption+) apply (simp add: word_leq_minus_one_le) apply (simp add: pd_bits vmsz_aligned_def) apply (frule (1) is_aligned_lookup_pd_slot
                   [OF _ is_aligned_weaken[of _ 14 6, simplified]]) apply (subgoal_tac "(p<<2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd") prefer 2 apply (subst add.commute add.left_commute) apply (subst and_not_mask_twice[where n=6 and m=14, simplified, symmetric]) apply (subst is_aligned_add_helper[THEN conjunct2], simp) apply (rule shiftl_less_t2n) apply (rule word_less_sub_le[THEN iffD1], simp+) apply (erule lookup_pd_slot_eq[simplified pd_bits]) apply (simp add: a_type_simps) apply (subst add.commute) apply (fastforce intro!: aligned_add_aligned is_aligned_shiftl_self) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 3. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>?P'1\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSmallPage; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> ?P'1 s
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 4. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 5. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSmallPage; valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> data_at ARMSmallPage (ptrFromPAddr base) s \<and> vmsz_aligned base ARMSmallPage \<and> vmsz_aligned vptr ARMSmallPage \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> is_aligned pd 14
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 3. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. sz = ARMLargePage \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 2. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 3. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMLargePage \<Longrightarrow> \<lbrace>?P'48\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMLargePage; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> ?P'48 s
 3. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMLargePage \<Longrightarrow> \<lbrace>?P'48\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE base (attrib - {Global, ParityEnabled}) vm_rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>m. case m of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMLargePage; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> ?P'48 s
 3. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMLargePage; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMLargePage (ptrFromPAddr base) s; vmsz_aligned base ARMLargePage; vmsz_aligned vptr ARMLargePage; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> is_aligned pd 14 \<and> is_aligned vptr 16
 2. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 3. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, -
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. sz = ARMSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSection \<and> vmsz_aligned vptr ARMSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> returnOk (Inr (SectionPDE base (attrib - {Global}) 0 vm_rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>m. case m of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s\<rbrace>, -
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. sz = ARMSection \<Longrightarrow> \<lbrace>?P'102\<rbrace> returnOk (Inr (SectionPDE base (attrib - {Global}) 0 vm_rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>m. case m of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSection; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSection \<and> vmsz_aligned vptr ARMSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> ?P'102 s
 3. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSection; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSection \<and> vmsz_aligned vptr ARMSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> (case Inr (SectionPDE base (attrib - {Global}) 0 vm_rights, [lookup_pd_slot pd vptr]) of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s) s
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s
 2. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 3. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (pd + (vptr >> 20 << 2) && ~~ mask pd_bits)) s
 2. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 3. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSection (ptrFromPAddr base) s; vmsz_aligned base ARMSection; vmsz_aligned vptr ARMSection; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at sz (ptrFromPAddr base) and K (vmsz_aligned base sz \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSuperSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSuperSection \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> returnOk (Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDE_offsets)) \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSuperSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSuperSection \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)\<rbrace> returnOk (Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>valid_slots\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>?P'131\<rbrace> returnOk (Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>valid_slots\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSuperSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSuperSection \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> ?P'131 s proof (prove)
goal (2 subgoals):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>?P'131\<rbrace> returnOk (Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>m. case m of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSuperSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSuperSection \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> ?P'131 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; (valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and data_at ARMSuperSection (ptrFromPAddr base) and (\<lambda>y. vmsz_aligned base ARMSuperSection \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights)) s\<rbrakk> \<Longrightarrow> (case Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]) of Inl (pte, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s) and pte_at p) s) \<and> wellformed_pte pte \<and> valid_pte pte s | Inr (pde, xs) \<Rightarrow> \<lambda>s. xs \<noteq> [] \<and> (\<forall>p\<in>set xs. ((\<lambda>s. \<exists>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s) and pde_at p) s \<and> UCAST(32 \<rightarrow> 12) (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots) \<and> wellformed_pde pde \<and> valid_pde pde s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> pspace_aligned s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> data_at ARMSuperSection (ptrFromPAddr base) s \<and> vmsz_aligned base ARMSuperSection \<and> vmsz_aligned vptr ARMSuperSection \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>p\<in>set [0 , 4 .e. 0x3C]. (\<exists>ref. (ref \<rhd> (p + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (p + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (p + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned base ARMSuperSection; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>p\<in>set [0 , 4 .e. 0x3C]. (\<exists>ref. (ref \<rhd> (p + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (p + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (p + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>p\<in>set [0 , 4 .e. 0x3C]. (\<exists>ref. (ref \<rhd> (p + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (p + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (p + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>p\<in>set [0 , 4 .e. 0x3C]. (\<exists>ref. (ref \<rhd> (p + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (p + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (p + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> is_aligned pd 14 proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights\<rbrakk> \<Longrightarrow> is_aligned pd 14
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>p\<in>set [0 , 4 .e. 0x3C]. (\<exists>ref. (ref \<rhd> (p + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (p + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (p + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; \<exists>ref. (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>p\<in>set [0 , 4 .e. 0x3C]. (\<exists>ref. (ref \<rhd> (p + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at (p + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) (p + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; typ_at (AArch APageDirectory) pd s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s\<rbrakk> \<Longrightarrow> [0 .e. 0xF] \<noteq> [] \<and> (\<forall>p\<le>0xF. (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> pde_at ((p << 2) + lookup_pd_slot pd vptr) s \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> [0 .e. 0xF] \<noteq> [] \<and> (\<forall>p\<le>0xF. (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> [0 .e. 0xF] \<noteq> [] \<and> (\<forall>p\<le>0xF. (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)
 2. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> [0 .e. 0xF] \<noteq> [] \<and> (\<forall>p\<le>0xF. (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> [0 .e. 0xF] \<noteq> [] \<and> (\<forall>p\<le>0xF. (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots) proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> \<forall>p\<le>0xF. (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits; p \<le> 0xF\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> UCAST(32 \<rightarrow> 12) ((p << 2) + lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits; p \<le> 0xF\<rbrakk> \<Longrightarrow> p = 0 \<or> p < 2 ^ 4 \<and> vmsz_aligned vptr ARMSuperSection
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits; p \<le> 0xF\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> \<not> False proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; vmsz_aligned vptr ARMSuperSection; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd pd_bits; p \<le> 0xF\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 \<and> \<not> False proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr + (p << 2) && ~~ mask 14 = pd
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> (lookup_pd_slot pd vptr + (p << 2) && ~~ mask 6) && ~~ mask 14 = pd
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> p << 2 < 2 ^ 6
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr && ~~ mask 14 = pd
 3. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (4 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> p < 2 ^ (6 - 2)
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> 6 < LENGTH(32)
 3. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr && ~~ mask 14 = pd
 4. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr && ~~ mask 14 = pd
 2. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14)) s) \<and> (\<exists>ko. kheap s ((p << 2) + lookup_pd_slot pd vptr && ~~ mask 14) = Some ko \<and> a_type ko = AArch APageDirectory) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> pd) s) \<and> is_aligned ((p << 2) + lookup_pd_slot pd vptr) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s ref pda p. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; data_at ARMSuperSection (ptrFromPAddr base) s; is_aligned vptr 24; vptr < kernel_base; vm_rights \<in> valid_vm_rights; is_aligned pd 14; (ref \<rhd> pd) s; kheap s pd = Some (ArchObj (PageDirectory pda)); p \<le> 0xF; is_aligned (lookup_pd_slot pd vptr) 6; (p << 2) + lookup_pd_slot pd vptr && ~~ mask 14 = pd\<rbrakk> \<Longrightarrow> (\<exists>ref. (ref \<rhd> pd) s) \<and> is_aligned (lookup_pd_slot pd vptr + (p << 2)) 2 proof (prove)
goal:
No subgoals!