theory ArchAcc_AI

lemma lookup_pt_slot_ptes_aligned_valid:
  "\<lbrace>valid_vspace_objs and valid_arch_state
    and equal_kernel_mappings and pspace_aligned
    and valid_global_objs
    and \<exists>\<rhd> pd and page_directory_at pd
    and K (is_aligned vptr 16)\<rbrace>
  lookup_pt_slot pd vptr
  \<lbrace>\<lambda>r s. is_aligned r 6 \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. pte_at (x + r) s)\<rbrace>, -" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp|wpc)+ apply (clarsimp simp: lookup_pd_slot_def Let_def) apply (simp add: pd_shifting_at) apply (frule (2) valid_vspace_objsD) apply (clarsimp simp: ) subgoal for s _ _ x apply (prop_tac "page_table_at (ptrFromPAddr x) s") subgoal apply (bspec "(ucast (pd + (vptr >> 20 << 2) && mask pd_bits >> 2))";clarsimp) apply (frule kernel_mapping_slots_empty_pdeI) apply ((simp add: obj_at_def pte_at_def;fail)+)[4] by (clarsimp simp: pde_ref_def valid_global_pts_def valid_arch_state_def second_level_tables_def) apply (rule conjI) apply (rule is_aligned_add) apply (rule is_aligned_weaken, erule(1) is_aligned_pt) apply (simp add: pt_bits_def pageBits_def) apply (rule is_aligned_shiftl) apply (rule is_aligned_andI1) apply (rule is_aligned_shiftr, simp) apply clarsimp by (erule(1) pte_at_aligned_vptr, simp+) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_arch_state and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K (is_aligned vptr 16)\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>r s. is_aligned r 6 \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. pte_at (x + r) s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_vspace_objs and valid_arch_state and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and (\<lambda>y. is_aligned vptr 16)\<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>r s. is_aligned r 6 \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. pte_at (x + r) s)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_vspace_objs and valid_arch_state and equal_kernel_mappings and pspace_aligned and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and (\<lambda>y. is_aligned vptr 16)) 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> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s)) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda) (pd + (vptr >> 20 << 2) && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda) pd s; pda (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr x) s
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr x) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr x) s proof (prove)
goal (5 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> kheap s ?p9 = Some (ArchObj (PageDirectory ?pd9))
 4. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x9 \<in> kernel_mapping_slots
 5. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots; (\<forall>r. pde_ref (?pd9 ?x9) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (?pd9 ?x9)\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr x) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2) \<in> kernel_mapping_slots; (\<forall>r. pde_ref (pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2))) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)))\<rbrakk> \<Longrightarrow> typ_at (AArch APageTable) (ptrFromPAddr x) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 \<and> (\<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s) proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) 6
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 3. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (3 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> pt_bits
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 3. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) (6 - 2)
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (2 subgoals):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) (6 - 2)
 2. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> \<forall>xa\<in>set [0 , 4 .e. 0x3C]. pte_at (xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>xc. \<lbrakk>valid_vspace_objs s; valid_arch_state s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; (ref_ \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 16; ako_at (PageDirectory pda_) pd s; pda_ (UCAST(32 \<rightarrow> 12) (pd + (vptr >> 20 << 2) && mask pd_bits >> 2)) = PageTablePDE x xa_ xb_; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda_ x) s; typ_at (AArch APageTable) (ptrFromPAddr x) s; xc \<in> set [0 , 4 .e. 0x3C]\<rbrakk> \<Longrightarrow> pte_at (xc + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) s proof (prove)
goal:
No subgoals!