theory ArchAcc_AI

lemma create_mapping_entries_valid [wp]:
  "\<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs
   and equal_kernel_mappings and valid_global_objs
   and \<exists>\<rhd> pd and page_directory_at pd and
    K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and>
       (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24)) \<rbrace>
  create_mapping_entries base vptr sz vm_rights attrib pd
  \<lbrace>\<lambda>m. valid_mapping_entries m\<rbrace>, -" apply (cases sz) apply (rule hoare_pre) apply (wp|simp add: valid_mapping_entries_def largePagePTE_offsets_def)+ apply clarsimp apply (erule (1) page_directory_pde_at_lookupI) apply (rule hoare_pre) apply (clarsimp simp add: valid_mapping_entries_def) apply wp apply (simp add: lookup_pd_slot_def Let_def) apply (prop_tac "is_aligned pd 14") apply (clarsimp simp: obj_at_def add.commute invs_def valid_state_def valid_pspace_def pspace_aligned_def) apply (drule bspec, blast) apply (clarsimp simp: a_type_def split: kernel_object.splits arch_kernel_obj.splits if_split_asm) apply (clarsimp simp: superSectionPDE_offsets_def) apply (clarsimp simp: upto_enum_step_def word_shift_by_2) apply (clarsimp simp: pde_at_def) apply (simp add: add.commute add.left_commute) apply (subst add_mask_lower_bits) apply (simp add: pd_bits_def pageBits_def) apply (clarsimp simp: pd_bits_def pageBits_def) apply (subst (asm) word_plus_and_or_coroll) prefer 2 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth p_le_0xF_helper word_bits_def) apply (drule test_bit_size)+ apply (simp add: word_size) apply (rule word_eqI) apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth p_le_0xF_helper word_bits_def) apply (frule_tac w=vptr in test_bit_size) apply (simp add: word_size) apply (thin_tac "All _") subgoal for \<dots> n apply (spec "18+n") by simp apply (clarsimp simp: a_type_simps) apply (rule aligned_add_aligned is_aligned_shiftl_self
                 | simp add: word_bits_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 3. sz = ARMSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>?P'1\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSmallPage; (pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))) s\<rbrakk> \<Longrightarrow> ?P'1 s
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 4. sz = ARMSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 5. sz = ARMSuperSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>sz = ARMSection; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; typ_at (AArch APageDirectory) pd s; (ref \<rhd> pd) s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s
 2. sz = ARMSuperSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>?P'55\<rbrace> create_mapping_entries base vptr sz vm_rights attrib pd \<lbrace>valid_mapping_entries\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))) s\<rbrakk> \<Longrightarrow> ?P'55 s proof (prove)
goal (2 subgoals):
 1. sz = ARMSuperSection \<Longrightarrow> \<lbrace>?P'55\<rbrace> returnOk (Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDE_offsets)) \<lbrace>\<lambda>m. case m of Inl (InvalidPTE, x) \<Rightarrow> \<lambda>_. True | Inl (_, x) \<Rightarrow> \<lambda>s. \<forall>p\<in>set x. pte_at p s | Inr (InvalidPDE, x) \<Rightarrow> \<lambda>_. True | Inr (PageTablePDE xa xaa xb, x) \<Rightarrow> \<lambda>_. False | Inr (_, x) \<Rightarrow> \<lambda>s. \<forall>p\<in>set x. pde_at p s\<rbrace>, -
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))) s\<rbrakk> \<Longrightarrow> ?P'55 s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; (pspace_aligned and valid_arch_state and valid_vspace_objs and equal_kernel_mappings and valid_global_objs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24))) s\<rbrakk> \<Longrightarrow> (case Inr (SuperSectionPDE base (attrib - {Global}) vm_rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) superSectionPDE_offsets) of Inl (InvalidPTE, x) \<Rightarrow> \<lambda>_. True | Inl (_, x) \<Rightarrow> \<lambda>s. \<forall>p\<in>set x. pte_at p s | Inr (InvalidPDE, x) \<Rightarrow> \<lambda>_. True | Inr (PageTablePDE xa xaa xb, x) \<Rightarrow> \<lambda>_. False | Inr (_, x) \<Rightarrow> \<lambda>s. \<forall>p\<in>set x. pde_at p s) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned vptr 24\<rbrakk> \<Longrightarrow> \<forall>p\<in>set superSectionPDE_offsets. pde_at (p + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned vptr 24\<rbrakk> \<Longrightarrow> is_aligned pd 14
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned vptr 24; is_aligned pd 14\<rbrakk> \<Longrightarrow> \<forall>p\<in>set superSectionPDE_offsets. pde_at (p + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; \<forall>x\<in>dom (kheap s). is_aligned x (obj_bits (the (kheap s x))); valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda))\<rbrakk> \<Longrightarrow> is_aligned pd 14
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned vptr 24; is_aligned pd 14\<rbrakk> \<Longrightarrow> \<forall>p\<in>set superSectionPDE_offsets. pde_at (p + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (2 subgoals):
 1. \<And>s ref pda. \<lbrakk>sz = ARMSuperSection; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; is_aligned vptr 24; kheap s pd = Some (ArchObj (PageDirectory pda)); is_aligned pd (obj_bits (the (kheap s pd)))\<rbrakk> \<Longrightarrow> is_aligned pd 14
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned vptr 24; is_aligned pd 14\<rbrakk> \<Longrightarrow> \<forall>p\<in>set superSectionPDE_offsets. pde_at (p + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; pspace_aligned s \<and> valid_arch_state s \<and> valid_vspace_objs s \<and> equal_kernel_mappings s \<and> valid_global_objs s \<and> (\<exists>ref. (ref \<rhd> pd) s) \<and> typ_at (AArch APageDirectory) pd s \<and> is_aligned vptr 24; is_aligned pd 14\<rbrakk> \<Longrightarrow> \<forall>p\<in>set superSectionPDE_offsets. pde_at (p + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>s p ref. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; p \<in> set [0 , 4 .e. 0x3C]; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24\<rbrakk> \<Longrightarrow> pde_at (p + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> pde_at ((x << 2) + (pd + (vptr >> 20 << 2))) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) ((x << 2) + (pd + (vptr >> 20 << 2)) && ~~ mask pd_bits) s \<and> is_aligned ((x << 2) + (pd + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) (pd + ((x << 2) + (vptr >> 20 << 2)) && ~~ mask pd_bits) s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> is_aligned pd pd_bits
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < LENGTH(32) \<longrightarrow> \<not> ((x << 2) + (vptr >> 20 << 2)) !! n'
 3. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> \<forall>n'\<ge>pd_bits. n' < LENGTH(32) \<longrightarrow> \<not> ((x << 2) + (vptr >> 20 << 2)) !! n'
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32; ((x << 2) + (vptr >> 20 << 2)) !! n'\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> (x << 2) && (vptr >> 20 << 2) = 0
 2. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32; ((x << 2) || (vptr >> 20 << 2)) !! n'\<rbrakk> \<Longrightarrow> False
 3. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32; ((x << 2) || (vptr >> 20 << 2)) !! n'\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> (x << 2) && (vptr >> 20 << 2) = 0
 3. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; \<forall>n<14. \<not> pd !! n; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x !! n'; 14 \<le> n'; n' < 32; vptr !! (18 + n')\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> (x << 2) && (vptr >> 20 << 2) = 0
 3. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (3 subgoals):
 1. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; \<forall>n<14. \<not> pd !! n; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x !! n'; 14 \<le> n'; n' < 32; 18 + n' < size vptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> (x << 2) && (vptr >> 20 << 2) = 0
 3. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n'. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> (x << 2) && (vptr >> 20 << 2) = 0
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n' n. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF; 14 \<le> n'; n' < 32\<rbrakk> \<Longrightarrow> n < size ((x << 2) && (vptr >> 20 << 2)) \<longrightarrow> ((x << 2) && (vptr >> 20 << 2)) !! n = 0 !! n
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n' n. \<lbrakk>sz = ARMSuperSection; \<forall>n<14. \<not> pd !! n; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x !! n'; 14 \<le> n'; n' < 32; n < 32; 2 \<le> n; x !! (n - 2); vptr !! (18 + n)\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n' n. \<lbrakk>sz = ARMSuperSection; \<forall>n<14. \<not> pd !! n; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x !! n'; 14 \<le> n'; n' < 32; n < 32; 2 \<le> n; x !! (n - 2); vptr !! (18 + n); 18 + n < size vptr\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n' n. \<lbrakk>sz = ARMSuperSection; \<forall>n<14. \<not> pd !! n; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x !! n'; 14 \<le> n'; n' < 32; 2 \<le> n; x !! (n - 2); vptr !! (18 + n); n < 14\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (2 subgoals):
 1. \<And>s ref x n' n. \<lbrakk>sz = ARMSuperSection; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x !! n'; 14 \<le> n'; n' < 32; 2 \<le> n; x !! (n - 2); vptr !! (18 + n); n < 14\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = ARMSuperSection; pspace_aligned s_; valid_arch_state s_; valid_vspace_objs s_; equal_kernel_mappings s_; valid_global_objs s_; (ref_ \<rhd> pd) s_; typ_at (AArch APageDirectory) pd s_; \<forall>n<24. \<not> vptr !! n; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x_ !! n'; 14 \<le> n'_; n'_ < 32; 2 \<le> n; x_ !! (n - 2); vptr !! (18 + n); n < 14\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<lbrakk>sz = ARMSuperSection; pspace_aligned s_; valid_arch_state s_; valid_vspace_objs s_; equal_kernel_mappings s_; valid_global_objs s_; (ref_ \<rhd> pd) s_; typ_at (AArch APageDirectory) pd s_; \<forall>n'\<ge>4. n' < 32 \<longrightarrow> \<not> x_ !! n'; 14 \<le> n'_; n'_ < 32; 2 \<le> n; x_ !! (n - 2); vptr !! (18 + n); n < 14; 18 + n < 24 \<longrightarrow> \<not> vptr !! (18 + n)\<rbrakk> \<Longrightarrow> False proof (prove)
goal (1 subgoal):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> typ_at (AArch APageDirectory) pd s \<and> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal (1 subgoal):
 1. \<And>s ref x. \<lbrakk>sz = ARMSuperSection; is_aligned pd 14; pspace_aligned s; valid_arch_state s; valid_vspace_objs s; equal_kernel_mappings s; valid_global_objs s; (ref \<rhd> pd) s; typ_at (AArch APageDirectory) pd s; is_aligned vptr 24; x \<le> 0xF\<rbrakk> \<Longrightarrow> is_aligned (pd + ((x << 2) + (vptr >> 20 << 2))) 2 proof (prove)
goal:
No subgoals!