theory ArchVSpace_AI

lemma lookup_pt_slot_is_aligned:
  "\<lbrace>(\<exists>\<rhd> pd) and K (vmsz_aligned vptr sz) and K (is_aligned pd pd_bits)
    and valid_arch_state and valid_vspace_objs and equal_kernel_mappings
    and pspace_aligned and valid_global_objs\<rbrace>
     lookup_pt_slot pd vptr
   \<lbrace>\<lambda>rv s. is_aligned rv (pg_entry_align sz)\<rbrace>,-" apply (simp add: lookup_pt_slot_def) apply (wp get_pde_wp | wpc)+ apply (clarsimp simp: lookup_pd_slot_pd) apply (frule(2) valid_vspace_objsD[rotated]) apply simp apply (rule is_aligned_add) apply (case_tac "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots") apply (frule kernel_mapping_slots_empty_pdeI) apply (simp add: obj_at_def)+ apply clarsimp apply (erule_tac x="ptrFromPAddr x" in allE) apply (simp add: pde_ref_def second_level_tables_def) apply (erule is_aligned_weaken[OF is_aligned_global_pt]) apply ((simp add: invs_psp_aligned invs_vspace_objs invs_arch_state
                        pg_entry_align_def pt_bits_def pageBits_def
                 split: vmpage_size.split)+)[3] apply (drule_tac x="ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2)" in bspec, simp) apply (clarsimp simp: obj_at_def a_type_def) apply (simp split: Structures_A.kernel_object.split_asm if_split_asm
                     arch_kernel_obj.split_asm) apply (erule is_aligned_weaken[OF pspace_alignedD], simp) apply (simp add: obj_bits_def pg_entry_align_def  split: vmpage_size.splits) apply (rule is_aligned_shiftl) apply (rule is_aligned_andI1) apply (rule is_aligned_shiftr) apply (case_tac sz) apply (clarsimp simp: vmsz_aligned_def pg_entry_align_def
                    elim!: is_aligned_weaken  split: vmpage_size.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (vmsz_aligned vptr sz) and K (is_aligned pd pd_bits) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. is_aligned rv (pg_entry_align sz)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr sz) and (\<lambda>y. is_aligned pd pd_bits) and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and pspace_aligned and valid_global_objs\<rbrace> liftE (get_pde (lookup_pd_slot pd vptr)) >>=E case_pde (throwError (MissingCapability 20)) (\<lambda>ptab x xa. returnOk (ptrFromPAddr ptab + ((vptr >> 12) && 0xFF << 2))) (\<lambda>word1 set1 word2 set2. throwError (MissingCapability 20)) (\<lambda>word set1 set2. throwError (MissingCapability 20)) \<lbrace>\<lambda>rv s. is_aligned rv (pg_entry_align sz)\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. ((\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr sz) and (\<lambda>y. is_aligned pd pd_bits) 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> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (pg_entry_align sz)) \<and> (\<forall>x xa xb xc. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SectionPDE x xa xb xc \<longrightarrow> True) \<and> (\<forall>x xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = SuperSectionPDE x xa xb \<longrightarrow> True) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (pg_entry_align sz) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) (pg_entry_align sz) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && 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)) (pg_entry_align sz) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && 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) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (7 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_global_objs s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> kheap s (?p72 s pda ref x xa xb) = Some (ArchObj (PageDirectory (?pd72 s pda ref x xa xb)))
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots\<rbrakk> \<Longrightarrow> ?x72 s pda ref x xa xb \<in> kernel_mapping_slots
 5. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; (\<forall>r. pde_ref (?pd72 s pda ref x xa xb (?x72 s pda ref x xa xb)) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (?pd72 s pda ref x xa xb (?x72 s pda ref x xa xb))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 6. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 7. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; (\<forall>r. pde_ref (PageTablePDE x xa xb) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s))) \<and> valid_pde_mappings (PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; \<forall>r. pde_ref (PageTablePDE x xa xb) = Some r \<longrightarrow> r \<in> set (second_level_tables (arch_state s)); valid_pde_mappings (PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa xb); pde_ref (PageTablePDE x xa xb) = Some (ptrFromPAddr x) \<longrightarrow> ptrFromPAddr x \<in> set (second_level_tables (arch_state s))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa xb); ptrFromPAddr x \<in> set (arm_global_pts (arch_state s))\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (5 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> pspace_aligned s
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> valid_arch_state s
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots; valid_pde_mappings (PageTablePDE x xa xb)\<rbrakk> \<Longrightarrow> pg_entry_align sz \<le> pt_bits
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 5. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb ko. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x) = Some ko; (case ko of CNode sz cspace \<Rightarrow> if well_formed_cnode_n sz cspace then ACapTable sz else AGarbage (cte_level_bits + sz) | TCB tcb \<Rightarrow> ATCB | Endpoint endpoint \<Rightarrow> AEndpoint | Notification notification \<Rightarrow> ANTFN | ArchObj ao \<Rightarrow> AArch (case ao of ASIDPool f \<Rightarrow> AASIDPool | PageTable pt \<Rightarrow> APageTable | PageDirectory pd \<Rightarrow> APageDirectory | DataPage dev sz \<Rightarrow> if dev then ADeviceData sz else AUserData sz)) = AArch APageTable\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb ko x5 x2. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; kheap s (ptrFromPAddr x) = Some (ArchObj (PageTable x2)); ko = ArchObj (PageTable x2); x5 = PageTable x2\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (pg_entry_align sz)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb ko x5 x2. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; pspace_aligned s; valid_global_objs s; kheap s pd = Some (ArchObj (PageDirectory pda)); pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots; ko = ArchObj (PageTable x2); x5 = PageTable x2\<rbrakk> \<Longrightarrow> pg_entry_align sz \<le> obj_bits (ArchObj (PageTable x2))
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) (pg_entry_align sz) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF) (pg_entry_align sz - 2) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) (pg_entry_align sz - 2) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> is_aligned vptr (pg_entry_align sz - 2 + 12) proof (prove)
goal (4 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; sz = ARMSmallPage\<rbrakk> \<Longrightarrow> is_aligned vptr (pg_entry_align sz - 2 + 12)
 2. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; sz = ARMLargePage\<rbrakk> \<Longrightarrow> is_aligned vptr (pg_entry_align sz - 2 + 12)
 3. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; sz = ARMSection\<rbrakk> \<Longrightarrow> is_aligned vptr (pg_entry_align sz - 2 + 12)
 4. \<And>s pda ref x xa xb. \<lbrakk>(ref \<rhd> pd) s; vmsz_aligned vptr sz; is_aligned pd pd_bits; valid_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) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s; sz = ARMSuperSection\<rbrakk> \<Longrightarrow> is_aligned vptr (pg_entry_align sz - 2 + 12) proof (prove)
goal:
No subgoals!