theory ArchAcc_AI

lemma lookup_pt_slot_non_empty:
  "\<lbrace>valid_vspace_objs and \<exists>\<rhd> pd and page_directory_at pd and pspace_aligned
  and K (is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace>
  lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. [rv , rv + 4 .e. rv + 0x3C] \<noteq> []\<rbrace>, -" apply (simp add:lookup_pt_slot_def) apply (wp get_pde_wp| wpc | clarsimp)+ apply (simp add:valid_vspace_objs_def) apply (drule_tac x = "(lookup_pd_slot pd vptr && ~~ mask pd_bits)" in spec) apply (erule impE) apply (subst lookup_pd_slot_eq) apply (clarsimp simp: obj_at_def) apply (drule_tac p = pd in pspace_alignedD) apply simp apply (simp add:obj_bits_def pageBits_def pd_bits_def) apply fastforce apply (drule spec) apply (erule(1) impE) apply (clarsimp simp:) apply (drule_tac x = "(ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2))" in bspec) apply (drule less_kernel_base_mapping_slots) apply (clarsimp simp: obj_at_def) apply (drule_tac p = pd in pspace_alignedD) apply simp apply (simp add:obj_bits_def pageBits_def pd_bits_def) apply simp apply (clarsimp simp: obj_at_def) apply (drule_tac p = "(ptrFromPAddr x)" in pspace_alignedD) apply simp apply (drule arg_cong[where f = length]) apply (subst (asm) length_upto_enum_step) apply (rule_tac sz = 6 in is_aligned_no_wrap'[rotated]) apply simp apply (erule aligned_add_aligned) apply (rule is_aligned_shiftl) apply (rule is_aligned_andI1[OF is_aligned_shiftr]) apply simp apply (simp add:word_bits_conv) apply (simp add:word_bits_conv) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and pspace_aligned and K (is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. [rv , rv + 4 .e. rv + 0x3C] \<noteq> []\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and pspace_aligned and (\<lambda>y. is_aligned vptr 16 \<and> vptr < kernel_base)\<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. [rv , rv + 4 .e. rv + 0x3C] \<noteq> []\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>valid_vspace_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>\<forall>p. (\<exists>rs. (rs \<rhd> p) s) \<longrightarrow> (\<forall>ao. ako_at ao p s \<longrightarrow> valid_vspace_obj ao s); (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; (\<exists>rs. (rs \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) \<longrightarrow> (\<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb rs. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> pd) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> pd) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; is_aligned pd (obj_bits (ArchObj (PageDirectory pdaa)))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> pd) s
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; is_aligned pd (obj_bits (ArchObj (PageDirectory pdaa)))\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> pd) s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> \<exists>rs. (rs \<rhd> pd) s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>ao. ako_at ao (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj ao s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; ako_at (?ao82 s pda ref x xa xb) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> valid_vspace_obj (?ao82 s pda ref x xa xb) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> - kernel_mapping_slots
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> is_aligned (?pd90 s pda ref x xa xb) pd_bits
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; UCAST(32 \<rightarrow> 12) (lookup_pd_slot (?pd90 s pda ref x xa xb) vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> - kernel_mapping_slots
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> is_aligned (?pd90 s pda ref x xa xb) pd_bits
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; UCAST(32 \<rightarrow> 12) (lookup_pd_slot (?pd90 s pda ref x xa xb) vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> - kernel_mapping_slots
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; is_aligned pd (obj_bits (ArchObj (PageDirectory pdaa)))\<rbrakk> \<Longrightarrow> is_aligned (?pd90 s pda ref x xa xb) pd_bits
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; UCAST(32 \<rightarrow> 12) (lookup_pd_slot (?pd90 s pda ref x xa xb) vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> - kernel_mapping_slots
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; is_aligned pd (obj_bits (ArchObj (PageDirectory pdaa)))\<rbrakk> \<Longrightarrow> is_aligned (?pd90 s pda ref x xa xb) pd_bits
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; UCAST(32 \<rightarrow> 12) (lookup_pd_slot (?pd90 s pda ref x xa xb) vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> - kernel_mapping_slots
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> - kernel_mapping_slots
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; 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; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; kheap s pd = Some (ArchObj (PageDirectory pdaa)); kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable pt))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = []; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); length [ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) , ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 .e. ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C] = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) \<le> ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 3. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt)))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> 6 \<le> obj_bits (ArchObj (PageTable pt))
 3. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) (6 - 2)
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> 6 \<le> obj_bits (ArchObj (PageTable pt))
 3. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> is_aligned vptr (6 - 2 + 12)
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> 6 \<le> obj_bits (ArchObj (PageTable pt))
 3. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa))\<rbrakk> \<Longrightarrow> 6 \<le> obj_bits (ArchObj (PageTable pt))
 2. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb pdaa pt. \<lbrakk>(ref \<rhd> pd) s; pspace_aligned s; is_aligned vptr 16; vptr < kernel_base; kheap s (lookup_pd_slot pd vptr && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; kheap s pd = Some (ArchObj (PageDirectory pdaa)); is_aligned (ptrFromPAddr x) (obj_bits (ArchObj (PageTable pt))); unat ((ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 0x3C - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) div (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2) + 4 - (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)))) + 1 = length []\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!