theory ArchAcc_AI

lemma lookup_pt_slot_reachable2 [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>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. (\<exists>\<rhd> (x + rv && ~~ mask pt_bits)) s\<rbrace>, -" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp|wpc)+ 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 (subgoal_tac "ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x") prefer 2 apply (subgoal_tac "is_aligned (ptrFromPAddr x) 10") prefer 2 apply (drule (2) valid_vspace_objsD) apply clarsimp apply (erule_tac x="ucast (vptr >> 20 << 2 >> 2)" in ballE) apply (thin_tac "obj_at P x s" for P x)+ apply (clarsimp simp: obj_at_def 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 (frule kernel_mapping_slots_empty_pdeI) apply (simp add: obj_at_def)+ apply clarsimp apply (erule_tac x="ptrFromPAddr x" in allE) apply (clarsimp simp: pde_ref_def second_level_tables_def) apply (rule is_aligned_global_pt[unfolded pt_bits_def pageBits_def, simplified]) apply simp+ 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 (rule conjI, rule refl) 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) 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>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (x + rv && ~~ 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>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (x + rv && ~~ 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>xa\<in>set [0 , 4 .e. 0x3C]. \<exists>ref. (ref \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ 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 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) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> \<exists>ref. (ref \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ 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) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> (?ref66 s pda ref x xa xb xc \<rhd> (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ 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) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> ((ref, pd), ?ref66 s pda ref x xa xb xc, xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_lookup1 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at ko pd s \<and> (\<exists>r. ?ref66 s pda ref x xa xb xc = r # ref \<and> (r, xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs ko) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> \<exists>r. ?ref66 s pda ref x xa xb xc = r # ref \<and> (r, xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; valid_pde (pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; valid_pde (pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb xc pt. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (4 subgoals):
 1. \<And>s pda x xa xb xc pt. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; 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 x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (7 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> kheap s (?p108 s pda x xa xb xc) = Some (ArchObj (PageDirectory (?pd108 s pda x xa xb xc)))
 4. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x108 s pda x xa xb xc \<in> kernel_mapping_slots
 5. \<And>s pda x xa xb xc. \<lbrakk>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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots; (\<forall>r. pde_ref (?pd108 s pda x xa xb xc (?x108 s pda x xa xb xc)) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (?pd108 s pda x xa xb xc (?x108 s pda x xa xb xc))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 6. \<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x
 7. \<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; (\<forall>r. pde_ref (PageTablePDE x xb xc) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (PageTablePDE x xb xc)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; \<forall>r. pde_ref (PageTablePDE x xb xc) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s)); valid_pde_mappings (PageTablePDE x xb xc)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xb xc); pde_ref (PageTablePDE x xb xc) = Some (ptrFromPAddr x) \<longrightarrow> ptrFromPAddr x \<in> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xb xc); ptrFromPAddr x \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (5 subgoals):
 1. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xb xc); ptrFromPAddr x \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> ptrFromPAddr x \<in> set (arm_global_pts (arch_state (?s120 s pda x xa xb xc)))
 2. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xb xc); ptrFromPAddr x \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> pspace_aligned (?s120 s pda x xa xb xc)
 3. \<And>s pda x xa xb xc. \<lbrakk>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; kheap s pd = Some (ArchObj (PageDirectory pda)); xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xb xc); ptrFromPAddr x \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> valid_arch_state (?s120 s pda x xa xb xc)
 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x
 5. \<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pt_bits. n' < LENGTH(32) \<longrightarrow> \<not> (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (2 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; is_aligned (ptrFromPAddr x) 10; 10 \<le> n'; n' < 32; (xa + ((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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xb xc 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 xb xc; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xb xc 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; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xb xc 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; 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 xb xc 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; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xb xc 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; 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 xb xc 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; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 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; \<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 xb xc 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; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (3 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; \<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 xb xc 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; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xb xc 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; 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> ?ref66 s pda ref x xa xb xc = VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; ptrFromPAddr x + (xa + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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)) 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots 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; xa \<in> set [0 , 4 .e. 0x3C]; pda (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xb xc; xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots proof (prove)
goal:
No subgoals!