theory ArchAcc_AI

lemma lookup_pt_slot_reachable3 [wp]:
  "\<lbrace>\<exists>\<rhd> pd and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base)
   and valid_arch_state and valid_vspace_objs and equal_kernel_mappings
   and pspace_aligned and valid_global_objs\<rbrace>
   lookup_pt_slot pd vptr
  \<lbrace>\<lambda>p s. \<forall>x\<in>set [p, p + 4 .e. p + 0x3C]. (\<exists>\<rhd> (x && ~~ mask pt_bits)) s\<rbrace>, -" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp|wpc)+ apply (clarsimp del: ballI) apply (clarsimp simp: lookup_pd_slot_def Let_def del: ballI) apply (simp add: pd_shifting) apply (frule (2) valid_vspace_objsD) apply (clarsimp del: ballI) apply (erule_tac x="(ucast (pd + (vptr >> 20 << 2) && mask pd_bits >> 2))" in ballE) apply (clarsimp del: ballI) apply (subgoal_tac "is_aligned (ptrFromPAddr x) 10") prefer 2 apply (thin_tac "ko_at P p s" for P p)+ apply (clarsimp simp: obj_at_def add.commute add.left_commute pspace_aligned_def) apply (drule bspec, blast) apply (clarsimp simp: a_type_def split: kernel_object.splits arch_kernel_obj.splits if_split_asm) apply (subst p_0x3C_shift) apply (rule aligned_add_aligned, assumption) apply (clarsimp intro!: is_aligned_andI1 is_aligned_shiftl is_aligned_shiftr) apply simp apply clarsimp apply (rule exI) apply (rule vs_lookup_step, assumption) apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting pd_shifting_dual add.commute add.left_commute) apply (rule exI, rule conjI, assumption) apply (rule_tac x="VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory)" in exI) apply (rule conjI, rule refl) apply (subgoal_tac "ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x") prefer 2 apply (subst add_mask_lower_bits) apply (simp add: pt_bits_def pageBits_def) prefer 2 apply simp apply (clarsimp simp: pt_bits_def pageBits_def) apply (clarsimp simp: upto_enum_step_def word_shift_by_2 p_le_0xF_helper) apply (thin_tac "pda x = t" for x t) apply (subst (asm) word_plus_and_or_coroll) apply (rule word_eqI) apply (clarsimp simp: word_size word_bits_def nth_shiftr nth_shiftl is_aligned_nth word_FF_is_mask) apply (erule_tac x="n - 2" in allE) apply simp apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth word_FF_is_mask word_bits_def) apply (simp add: add.commute add.left_commute) apply (rule vs_refs_pdI) prefer 3 apply (clarsimp simp: word_ops_nth_size word_size nth_shiftr nth_shiftl) apply (drule test_bit_size) apply (simp add: word_size) apply fastforce apply (subst shiftl_shiftr_id) apply (simp add: word_bits_def)+ apply word_bitwise apply (erule kernel_base_kernel_mapping_slots) apply clarsimp apply (subst (asm) mask_add_aligned, simp add: pd_bits_def pageBits_def)+ apply (simp add: shiftr_over_and_dist) apply (subst (asm) shiftl_shiftr_id, (simp add: word_bits_conv)+, word_bitwise)+ apply (subst (asm) shiftr_mask2, (simp add: pd_bits_def pageBits_def)+)+ apply (simp add: shiftr_mask_eq[where x=vptr and n=20, unfolded word_size, simplified]) apply (drule kernel_base_kernel_mapping_slots, simp) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>p s. \<forall>x\<in>set [p , p + 4 .e. p + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>\<lambda>p s. \<forall>x\<in>set [p , p + 4 .e. p + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs) s \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb \<longrightarrow> (\<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s)) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) (pd + (vptr >> 20 << 2) && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_pde (pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pt. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_global_objs s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pt. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt)); is_aligned (ptrFromPAddr x) (obj_bits (the (kheap s (ptrFromPAddr x))))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits)) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 6 \<le> 10
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits)) s
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 6 \<le> 10
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits)) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> (?ref110 s pda ref x xa xb xc \<rhd> (xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ((ref, pd), ?ref110 s pda ref x xa xb xc, xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_lookup1 s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at ko pd s \<and> (\<exists>r. ?ref110 s pda ref x xa xb xc = r # ref \<and> (r, xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs ko)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<exists>r. ?ref110 s pda ref x xa xb xc = r # ref \<and> (r, xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ?ref110 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (5 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) pt_bits
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xc + ((vptr >> 12) && 0xFF << 2)) !! n'
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptrFromPAddr x = ptrFromPAddr x
 4. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 5. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xc + ((vptr >> 12) && 0xFF << 2)) !! n'
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptrFromPAddr x = ptrFromPAddr x
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> ptrFromPAddr x = ptrFromPAddr x
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xc + ((vptr >> 12) && 0xFF << 2)) !! n'
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xc + ((vptr >> 12) && 0xFF << 2)) !! n'
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc n'. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; 10 \<le> n'; n' < 32; (xc + ((vptr >> 12) && 0xFF << 2)) !! n'\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) + ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) + ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb n' xd. \<lbrakk>\<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'; (ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> (xd << 2) && ((vptr >> 12) && 0xFF << 2) = 0
 2. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) || ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb n' xd n. \<lbrakk>\<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'; (ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> n < size ((xd << 2) && ((vptr >> 12) && 0xFF << 2)) \<longrightarrow> ((xd << 2) && ((vptr >> 12) && 0xFF << 2)) !! n = 0 !! n
 2. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) || ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x n' xd n. \<lbrakk>\<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> xd !! n'; (ref \<rhd> pd) s; \<forall>n<14. \<not> pd !! n; \<forall>n<16. \<not> vptr !! n; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; \<forall>n<10. \<not> ptrFromPAddr x !! n; 10 \<le> n'; n' < 32; n < 32; vptr !! (10 + n); 2 \<le> n; xd !! (n - 2); n - 2 < 8\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) || ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x n' xd n. \<lbrakk>(ref \<rhd> pd) s; \<forall>n<14. \<not> pd !! n; \<forall>n<16. \<not> vptr !! n; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; \<forall>n<10. \<not> ptrFromPAddr x !! n; 10 \<le> n'; n' < 32; n < 32; vptr !! (10 + n); 2 \<le> n; xd !! (n - 2); n - 2 < 8; 4 \<le> n - 2 \<longrightarrow> n - 2 < 32 \<longrightarrow> \<not> xd !! (n - 2)\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) || ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb n' xd. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; ((xd << 2) || ((vptr >> 12) && 0xFF << 2)) !! n'; \<forall>n'\<ge>4. n' < word_bits \<longrightarrow> \<not> xd !! n'\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; ptrFromPAddr x + (xc + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda))
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x (?a162 s pda ref x xa xb xc) (?b162 s pda ref x xa xb xc)
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> kernel_mapping_slots
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> (vptr >> 20 << 2 >> 2) !! n
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> (vptr >> 20 << 2 >> 2) !! n
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x (?a162 s pda ref x xa xb xc) (?b162 s pda ref x xa xb xc)
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> kernel_mapping_slots
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc n. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x; 12 \<le> n; n < 30; vptr !! (20 + n)\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x (?a162 s pda ref x xa xb xc) (?b162 s pda ref x xa xb xc)
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> kernel_mapping_slots
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc n. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x; 12 \<le> n; n < 30; 20 + n < size vptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x (?a162 s pda ref x xa xb xc) (?b162 s pda ref x xa xb xc)
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> kernel_mapping_slots
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x (?a162 s pda ref x xa xb xc) (?b162 s pda ref x xa xb xc)
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> kernel_mapping_slots
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> kernel_mapping_slots
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> vptr >> 20 < 2 ^ (LENGTH(32) - 2)
 3. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> vptr >> 20 < 0x40000000
 2. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; is_aligned (ptrFromPAddr x) 10; xc \<in> set [0 , 4 .e. 0x3C]; xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]. \<exists>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots; xc \<in> set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) ((vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) ((vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots; xc \<in> set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) ((vptr >> 20 << 2 >> 2) && (mask pd_bits >> 2))) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) ((vptr >> 20 << 2 >> 2) && (mask pd_bits >> 2)) \<in> kernel_mapping_slots; xc \<in> set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) ((vptr >> 20) && (mask pd_bits >> 2))) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) ((vptr >> 20) && (mask pd_bits >> 2)) \<in> kernel_mapping_slots; xc \<in> set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) ((vptr >> 20) && mask 12)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) ((vptr >> 20) && mask 12) \<in> kernel_mapping_slots; xc \<in> set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; is_aligned vptr 16; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (vptr >> 20) \<in> kernel_mapping_slots; xc \<in> set [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C]\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xc && ~~ mask pt_bits)) s proof (prove)
goal:
No subgoals!