theory ArchAcc_AI

lemma lookup_pt_slot_looks_up [wp]:
  "\<lbrace>ref \<rhd> pd and K (is_aligned pd 14 \<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>pt_slot. (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref) \<rhd> (pt_slot && ~~ mask pt_bits)\<rbrace>, -" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp|wpc)+ apply clarsimp apply (rule vs_lookup_step, assumption) apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting pd_shifting_dual) apply (rule exI, rule conjI, assumption) subgoal for s _ x apply (prop_tac "ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x") apply (prop_tac "is_aligned (ptrFromPAddr x) 10") 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 invs_def valid_state_def valid_pspace_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)+)[4] apply (clarsimp simp: pde_ref_def second_level_tables_def) apply (erule is_aligned_global_pt[unfolded pt_bits_def pageBits_def, simplified]) apply simp+ apply (subgoal_tac "(vptr >> 12) && 0xFF << 2 < 2 ^ 10") apply (subst is_aligned_add_or, (simp add: pt_bits_def pageBits_def)+) apply (subst word_ao_dist) apply (subst mask_out_sub_mask [where x="(vptr >> 12) && 0xFF << 2"]) apply (subst less_mask_eq, simp) apply (subst is_aligned_neg_mask_eq, simp) apply (clarsimp simp: valid_arch_state_def valid_global_pts_def) apply (rule shiftl_less_t2n, simp) apply (rule and_mask_less'[where n=8, unfolded mask_def, simplified], (simp )+) apply (subst shiftl_shiftr_id) apply (simp add: word_bits_def)+ apply word_bitwise apply (subst (asm) shiftl_shiftr_id) apply (simp add: word_bits_def)+ apply word_bitwise apply (erule vs_refs_pdI) apply (erule kernel_base_kernel_mapping_slots) apply (intro allI impI) apply (simp add: nth_shiftr) apply (rule bang_big[simplified]) by (simp add: word_size) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>ref \<rhd> pd and K (is_aligned pd 14 \<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>pt_slot. (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref) \<rhd> (pt_slot && ~~ mask pt_bits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>ref \<rhd> pd and (\<lambda>y. is_aligned pd 14 \<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>pt_slot. (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref) \<rhd> (pt_slot && ~~ mask pt_bits)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (ref \<rhd> pd and (\<lambda>y. is_aligned pd 14 \<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> ((VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref) \<rhd> (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 x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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> ((VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref) \<rhd> (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits)) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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> ((ref, pd), VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory) # ref, ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_lookup1 s proof (prove)
goal (1 subgoal):
 1. \<And>s pda x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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\<rbrakk> \<Longrightarrow> \<exists>ko. ko_at ko pd s \<and> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs ko proof (prove)
goal (1 subgoal):
 1. \<And>s pda x xa xb. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; valid_vspace_obj (PageDirectory pda_) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; valid_pde (pda_ (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 4. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa_ xb_; valid_pde (pda_ (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 4. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (4 subgoals):
 1. \<And>pt. \<lbrakk>is_aligned pd 14; 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) (vptr >> 20 << 2 >> 2)) = PageTablePDE x xa_ xb_; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 4. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (4 subgoals):
 1. \<And>pt. \<lbrakk>is_aligned pd 14; vptr < kernel_base; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; pda_ (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 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. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 4. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (7 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> kheap s ?p31 = Some (ArchObj (PageDirectory ?pd31))
 4. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x31 \<in> kernel_mapping_slots
 5. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots; (\<forall>r. pde_ref (?pd31 ?x31) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (?pd31 ?x31)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 6. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 7. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<notin> - kernel_mapping_slots; (\<forall>r. pde_ref (pda_ (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2))) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pda_ (UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2)))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; ptrFromPAddr x \<in> set (arm_global_pts (arch_state s)); valid_pde_mappings (PageTablePDE x xa_ xb_)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa_ xb_)\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<lbrakk>is_aligned pd 14; 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_; UCAST(32 \<rightarrow> 12) (vptr >> 20 << 2 >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa_ xb_)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 4. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10; (vptr >> 12) && 0xFF << 2 < 2 ^ 10\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10; (vptr >> 12) && 0xFF << 2 < 0x400\<rbrakk> \<Longrightarrow> (ptrFromPAddr x || ((vptr >> 12) && 0xFF << 2)) && ~~ mask 10 = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10; (vptr >> 12) && 0xFF << 2 < 0x400\<rbrakk> \<Longrightarrow> ptrFromPAddr x && ~~ mask 10 || ((vptr >> 12) && 0xFF << 2) && ~~ mask 10 = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10; (vptr >> 12) && 0xFF << 2 < 0x400\<rbrakk> \<Longrightarrow> ptrFromPAddr x && ~~ mask 10 || ((vptr >> 12) && 0xFF << 2) - (((vptr >> 12) && 0xFF << 2) && mask 10) = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10; (vptr >> 12) && 0xFF << 2 < 0x400\<rbrakk> \<Longrightarrow> ptrFromPAddr x && ~~ mask 10 || ((vptr >> 12) && 0xFF << 2) - ((vptr >> 12) && 0xFF << 2) = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10; (vptr >> 12) && 0xFF << 2 < 0x400\<rbrakk> \<Longrightarrow> ptrFromPAddr x || ((vptr >> 12) && 0xFF << 2) - ((vptr >> 12) && 0xFF << 2) = ptrFromPAddr x
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF << 2 < 2 ^ 10
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> (vptr >> 12) && 0xFF < 0x100
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; is_aligned (ptrFromPAddr x) 10\<rbrakk> \<Longrightarrow> 10 < LENGTH(32)
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20 << 2 >> 2) (Some APageDirectory), ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; 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. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> vptr >> 20 < 2 ^ (LENGTH(32) - 2)
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> vptr >> 20 < 0x40000000
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x; (ref \<rhd> pd) s; is_aligned pd 14; 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\<rbrakk> \<Longrightarrow> 2 < LENGTH(32)
 2. \<lbrakk>ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x; (ref \<rhd> pd) s; is_aligned pd 14; 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\<rbrakk> \<Longrightarrow> vptr >> 20 < 2 ^ (LENGTH(32) - 2)
 3. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x; (ref \<rhd> pd) s; is_aligned pd 14; 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\<rbrakk> \<Longrightarrow> vptr >> 20 < 0x40000000
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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_; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> (VSRef (vptr >> 20) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pda_)) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (vptr >> 20) \<notin> kernel_mapping_slots
 2. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> (vptr >> 20) !! n proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x\<rbrakk> \<Longrightarrow> \<forall>n\<ge>12. n < 32 \<longrightarrow> \<not> (vptr >> 20) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x; 12 \<le> n; n < 32\<rbrakk> \<Longrightarrow> \<not> (vptr >> 20) !! n proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x; 12 \<le> n; n < 32\<rbrakk> \<Longrightarrow> \<not> vptr !! (20 + n) proof (prove)
goal (1 subgoal):
 1. \<And>n. \<lbrakk>(ref \<rhd> pd) s; is_aligned pd 14; 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; ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) && ~~ mask pt_bits = ptrFromPAddr x; 12 \<le> n; n < 32\<rbrakk> \<Longrightarrow> size vptr \<le> 20 + n proof (prove)
goal:
No subgoals!