theory ArchVSpaceEntries_AI

lemma create_mapping_entries_safe[wp]:
  "\<lbrace>\<exists>\<rhd>pd and K (vmsz_aligned vptr sz) and K (is_aligned pd pd_bits)
          and K (vptr < kernel_base)
          and valid_vspace_objs and pspace_aligned and
          (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits))\<rbrace>
      create_mapping_entries ptr vptr sz rights attrib pd
   \<lbrace>\<lambda>entries. case entries of (Inl (SmallPagePTE _ _ _, [_])) \<Rightarrow> \<top>
                  | (Inl (SmallPagePTE _ _ _, _)) \<Rightarrow> \<bottom>
                  | (Inl (LargePagePTE _ _ _, [])) \<Rightarrow> \<bottom>
                  | (Inr (SectionPDE _ _ _ _, [_])) \<Rightarrow> \<top>
                  | (Inr (SectionPDE _ _ _ _, _)) \<Rightarrow> \<bottom>
                  | (Inr (SuperSectionPDE _ _ _, [])) \<Rightarrow> \<bottom>
                  | _ \<Rightarrow> page_inv_entries_pre entries\<rbrace>,-" apply (cases sz, simp_all add: largePagePTE_offsets_def superSectionPDE_offsets_def) defer 2 apply (wp | simp)+ apply (simp split:list.split) apply (subgoal_tac "lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C") apply (clarsimp simp:upto_enum_def not_less upto_enum_step_def
      page_inv_entries_pre_def Let_def) apply (clarsimp simp:upto_enum_step_def upto_enum_def
                     map_eq_Cons_conv upt_eq_Cons_conv) apply (drule_tac x = "lookup_pd_slot pd vptr" in spec) apply (subst (asm) upto_0_to_n2) apply simp apply clarsimp apply (drule lookup_pd_slot_aligned_6) apply (simp add:pd_bits_def pageBits_def) apply simp apply clarsimp apply (erule is_aligned_no_wrap'[OF lookup_pd_slot_aligned_6]) apply (simp add:pd_bits pageBits_def) apply simp apply (wp get_pde_wp | simp add:lookup_pt_slot_def | wpc)+ apply (clarsimp simp:upto_enum_def upto_enum_step_def
    page_inv_entries_pre_def Let_def ) apply (drule_tac ref = refa in valid_vspace_objsD) apply (simp add:obj_at_def) apply simp apply (simp) apply (drule_tac x = "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2)"
    in bspec) apply simp apply (erule(1) less_kernel_base_mapping_slots) apply (clarsimp simp:not_less[symmetric] split:list.splits) apply (clarsimp simp:page_inv_entries_pre_def
    Let_def upto_enum_step_def upto_enum_def) apply (subst (asm) upto_0_to_n2) apply simp apply (clarsimp simp:not_less[symmetric]) apply (subgoal_tac
    "(\<exists>xa xb. pda (ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2))
     = pde.PageTablePDE x xa xb)
     \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6") apply clarsimp apply clarsimp apply (rule aligned_add_aligned) apply (erule(1) pt_aligned) apply (rule is_aligned_shiftl[OF is_aligned_andI1]) apply (rule is_aligned_shiftr) apply (simp add:vmsz_aligned_def) apply simp 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 K (vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> create_mapping_entries ptr vptr sz rights attrib pd \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMSmallPage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (SmallPagePTE ptr (attrib - {Global, ParityEnabled}) rights, [p]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, -
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, -
 3. sz = ARMSection \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMSection) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> returnOk (Inr (SectionPDE ptr (attrib - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, -
 4. sz = ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMSuperSection) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attrib - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. sz = ARMSmallPage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMSmallPage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (SmallPagePTE ptr (attrib - {Global, ParityEnabled}) rights, [p]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, -
 2. sz = ARMSection \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMSection) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> returnOk (Inr (SectionPDE ptr (attrib - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, -
 3. sz = ARMSuperSection \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMSuperSection) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attrib - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, -
 4. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> (case map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inr (SuperSectionPDE ptr (attrib - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))) s
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>x21 x22. map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C] = x21 # x22 \<longrightarrow> page_inv_entries_pre (Inr (SuperSectionPDE ptr (attrib - {Global}) rights, x21 # x22)) s)
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s); lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C\<rbrakk> \<Longrightarrow> [0 , 4 .e. 0x3C] \<noteq> [] \<and> (\<forall>x21 x22. map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C] = x21 # x22 \<longrightarrow> page_inv_entries_pre (Inr (SuperSectionPDE ptr (attrib - {Global}) rights, x21 # x22)) s)
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x21 x22 ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> (x22 = [] \<longrightarrow> map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] \<noteq> [x21]) \<and> (x22 \<noteq> [] \<longrightarrow> map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] = x21 # x22 \<longrightarrow> (\<exists>p. is_aligned p 6 \<and> x21 # x22 = map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]))
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; \<forall>p. is_aligned p 6 \<longrightarrow> lookup_pd_slot pd vptr # map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16] \<noteq> map ((\<lambda>x. x + p) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; is_aligned (lookup_pd_slot pd vptr) 6 \<longrightarrow> lookup_pd_slot pd vptr # map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16] \<noteq> map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16]\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> 0 < 16
 2. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; is_aligned (lookup_pd_slot pd vptr) 6 \<longrightarrow> lookup_pd_slot pd vptr # map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16] \<noteq> map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) (0 # [1..<16])\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 4. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; is_aligned (lookup_pd_slot pd vptr) 6 \<longrightarrow> lookup_pd_slot pd vptr # map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [Suc 0..<16] \<noteq> map ((\<lambda>x. x + lookup_pd_slot pd vptr) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) (0 # [1..<16])\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; \<not> is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; \<not> is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> is_aligned (?pd74 s ref refa) 14
 2. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; \<not> is_aligned (lookup_pd_slot pd vptr) 6; is_aligned (lookup_pd_slot (?pd74 s ref refa) vptr) 6\<rbrakk> \<Longrightarrow> False
 3. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 4. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; \<not> is_aligned (lookup_pd_slot pd vptr) 6; is_aligned (lookup_pd_slot pd vptr) 6\<rbrakk> \<Longrightarrow> False
 2. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>sz = ARMSuperSection; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMSuperSection \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; (ref \<rhd> pd) s; vmsz_aligned vptr ARMSuperSection; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vptr \<le> lookup_pd_slot pd vptr + 0x3C
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> is_aligned pd 14
 2. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 3. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref refa. \<lbrakk>sz = ARMSuperSection; (ref \<rhd> pd) s; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> 0x3C < 2 ^ 6
 2. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. sz = ARMLargePage \<Longrightarrow> \<lbrace>(\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and (\<lambda>y. vmsz_aligned vptr ARMLargePage) and (\<lambda>y. is_aligned pd pd_bits) and (\<lambda>y. vptr < kernel_base) and valid_vspace_objs and pspace_aligned and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>entries. case entries of Inl (InvalidPTE, xc) \<Rightarrow> page_inv_entries_pre entries | Inl (LargePagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (LargePagePTE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inl (SmallPagePTE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inl (SmallPagePTE x xa xb, [xca]) \<Rightarrow> \<lambda>_. True | Inl (SmallPagePTE x xa xb, xca # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, []) \<Rightarrow> \<lambda>_. False | Inr (SectionPDE x xa xb xc, [xda]) \<Rightarrow> \<lambda>_. True | Inr (SectionPDE x xa xb xc, xda # aa # lista) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, []) \<Rightarrow> \<lambda>_. False | Inr (SuperSectionPDE x xa xb, a # list) \<Rightarrow> page_inv_entries_pre entries | Inr (_, xd) \<Rightarrow> page_inv_entries_pre entries\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>sz = ARMLargePage; (\<exists>ref. (ref \<rhd> pd) s) \<and> vmsz_aligned vptr ARMLargePage \<and> is_aligned pd pd_bits \<and> vptr < kernel_base \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>ref. (ref \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s)\<rbrakk> \<Longrightarrow> \<forall>pda. ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s \<longrightarrow> (\<forall>x. (\<exists>xa xb. pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb) \<longrightarrow> (case map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; (refa \<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> ako_at (?ao164 s pda ref refa x xa xb) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s
 2. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 3. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (?ao164 s pda ref refa x xa xb) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> valid_vspace_objs s
 2. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref refa x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_vspace_obj (PageDirectory pda) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; \<forall>x\<in>- kernel_mapping_slots. valid_pde (pda x) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> 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>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb\<rbrakk> \<Longrightarrow> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; valid_pde (pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2))) s\<rbrakk> \<Longrightarrow> (case map ((\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) \<circ> ((\<lambda>x. x * 4) \<circ> toEnum)) [0..<16] of [] \<Rightarrow> \<lambda>_. False | a # list \<Rightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C]))) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb z zs. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; [0..<16] = z # zs\<rbrakk> \<Longrightarrow> page_inv_entries_pre (Inl (LargePagePTE ptr (attrib - {Global, ParityEnabled}) rights, map (\<lambda>xa. xa + (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2))) [0 , 4 .e. 0x3C])) s proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb z zs. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; [0..<16] = z # zs\<rbrakk> \<Longrightarrow> zs \<noteq> [] \<and> (zs \<noteq> [] \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb z zs. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 0 < 16
 2. \<And>s pda ref x xa xb z zs. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; 0 # [1..<16] = z # zs\<rbrakk> \<Longrightarrow> zs \<noteq> [] \<and> (zs \<noteq> [] \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb z zs. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; 0 # [1..<16] = z # zs\<rbrakk> \<Longrightarrow> zs \<noteq> [] \<and> (zs \<noteq> [] \<longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6) proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s; (\<exists>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\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6
 2. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>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 proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> (\<exists>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 proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x + ((vptr >> 12) && 0xFF << 2)) 6 proof (prove)
goal (3 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (ptrFromPAddr x) (?n193 s pda ref x xa xb)
 2. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 3. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> ?n193 s pda ref x xa xb proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned ((vptr >> 12) && 0xFF << 2) 6
 2. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> 10 proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned (vptr >> 12) (6 - 2)
 2. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> 10 proof (prove)
goal (2 subgoals):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> is_aligned vptr (6 - 2 + 12)
 2. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> 10 proof (prove)
goal (1 subgoal):
 1. \<And>s pda ref x xa xb. \<lbrakk>sz = ARMLargePage; (ref \<rhd> pd) s; vmsz_aligned vptr ARMLargePage; is_aligned pd pd_bits; vptr < kernel_base; valid_vspace_objs s; pspace_aligned s; ako_at (PageDirectory pda) (lookup_pd_slot pd vptr && ~~ mask pd_bits) s; pda (UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vptr && mask pd_bits >> 2)) = PageTablePDE x xa xb; typ_at (AArch APageTable) (ptrFromPAddr x) s\<rbrakk> \<Longrightarrow> 6 \<le> 10 proof (prove)
goal:
No subgoals!