theory ArchArch_AI

lemma create_mapping_entries_parent_for_refs:
  "\<lbrace>invs and \<exists>\<rhd> pd and page_directory_at pd
           and K (is_aligned pd pd_bits) and K (vmsz_aligned vptr pgsz)
           and K (vptr < kernel_base)\<rbrace>
    create_mapping_entries ptr vptr pgsz
                 rights attribs pd
   \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -" apply (rule hoare_gen_asmE)+ apply (cases pgsz, simp_all add: vmsz_aligned_def largePagePTE_offsets_def
                                   superSectionPDE_offsets_def) apply (rule hoare_pre) apply wp apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to) apply (elim exEI) apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def) apply simp apply (rule hoare_pre) apply wp apply (rule hoare_post_imp_R) apply (rule lookup_pt_slot_cap_to_multiple1) apply (elim conjE exEI cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
                           subset_iff p_0x3C_shift map_up_enum_0x3C) apply simp apply (rule hoare_pre, wp) apply (clarsimp dest!:vs_lookup_pages_vs_lookupI) apply (drule valid_vs_lookupD, clarsimp) apply (simp, elim exEI) apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def
                         lookup_pd_slot_def Let_def) apply (subst pd_shifting, simp add: pd_bits_def pageBits_def) apply (clarsimp simp: vs_cap_ref_def
                  split: cap.split_asm arch_cap.split_asm option.split_asm) apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def
                dest!: caps_of_state_valid_cap split:if_splits)[3] apply (frule(1) caps_of_state_valid) apply (clarsimp simp:valid_cap_def obj_at_def) apply (simp add:is_cap_simps) apply (rule hoare_pre, wp) apply (clarsimp dest!:vs_lookup_pages_vs_lookupI) apply (drule valid_vs_lookupD, clarsimp) apply (simp, elim exEI) apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def) apply (rule conjI) apply (simp add: subset_eq) apply (clarsimp simp: lookup_pd_slot_add_eq) apply (clarsimp simp: vs_cap_ref_def
                 split: cap.split_asm arch_cap.split_asm option.split_asm) apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def
             dest!: caps_of_state_valid_cap split:if_splits)[3] apply (frule(1) caps_of_state_valid) apply (clarsimp simp:valid_cap_def obj_at_def) apply (simp add:is_cap_simps) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd and K (is_aligned pd pd_bits) and K (vmsz_aligned vptr pgsz) and K (vptr < kernel_base)\<rbrace> create_mapping_entries ptr vptr pgsz rights attribs pd \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; vmsz_aligned vptr pgsz; is_aligned pd pd_bits\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> create_mapping_entries ptr vptr pgsz rights attribs pd \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (SmallPagePTE ptr (attribs - {Global, ParityEnabled}) rights, [p]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage\<rbrakk> \<Longrightarrow> \<lbrace>?P'7\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (SmallPagePTE ptr (attribs - {Global, ParityEnabled}) rights, [p]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> ?P'7 s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 5. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage\<rbrakk> \<Longrightarrow> \<lbrace>?P'15\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>p a. \<exists>aa b. cte_wp_at (parent_for_refs (Inl (SmallPagePTE ptr (attribs - {Global, ParityEnabled}) rights, [p]))) (aa, b) a\<rbrace>, -
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> ?P'15 s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 5. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>rv s. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inl (SmallPagePTE ptr (attribs - {Global, ParityEnabled}) rights, [rv]))) (a, b) s
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)) s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 5. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<And>rv s x xa. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; \<exists>cap. caps_of_state s (x, xa) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrakk> \<Longrightarrow> cte_wp_at (parent_for_refs (Inl (SmallPagePTE ptr (attribs - {Global, ParityEnabled}) rights, [rv]))) (x, xa) s
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)) s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 5. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 12; is_aligned pd pd_bits; pgsz = ARMSmallPage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base)) s
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>?P'33\<rbrace> doE p <- lookup_error_on_failure False (lookup_pt_slot pd vptr);
returnOk (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))
odE \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> ?P'33 s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>?P'41\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>p a. \<exists>aa b. cte_wp_at (parent_for_refs (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + p) [0 , 4 .e. 0x3C]))) (aa, b) a\<rbrace>, -
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> ?P'41 s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (5 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage\<rbrakk> \<Longrightarrow> \<lbrace>?P'41\<rbrace> lookup_pt_slot pd vptr \<lbrace>?Q'44\<rbrace>, -
 2. \<And>rv s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; ?Q'44 rv s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C]))) (a, b) s
 3. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> ?P'41 s
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 5. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>rv s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; is_aligned rv 6 \<and> (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s)\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C]))) (a, b) s
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)) s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (4 subgoals):
 1. \<And>rv s x xa c. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; is_aligned rv 6; is_pt_cap c; cap_asid c \<noteq> None; (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c\<rbrakk> \<Longrightarrow> parent_for_refs (Inl (LargePagePTE ptr (attribs - {Global, ParityEnabled}) rights, map (\<lambda>x. x + rv) [0 , 4 .e. 0x3C])) c
 2. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)) s
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 4. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 16; is_aligned pd pd_bits; pgsz = ARMLargePage; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> True \<and> (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)) s
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr]))) (a, b) s
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr]))) (a, b) s
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr]))) (a, b) s
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref x xa. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; \<exists>cap. caps_of_state s (x, xa) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> cte_wp_at (parent_for_refs (Inr (SectionPDE ptr (attribs - {Global}) 0 rights, [lookup_pd_slot pd vptr]))) (x, xa) s
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> pd + (vptr >> 20 << 2) && ~~ mask pd_bits \<in> obj_refs cap \<and> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y)
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> pd \<in> obj_refs cap \<and> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y)
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (6 subgoals):
 1. \<And>s x xa x12a. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (ASIDPoolCap pd x12a))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x xa x31 x33 x34. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageCap x31 pd x33 x34 None)); (case x34 of ARMSmallPage \<Rightarrow> None | _ \<Rightarrow> None) = Some ref\<rbrakk> \<Longrightarrow> False
 3. \<And>s ref x xa x31 x33 x34 a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageCap x31 pd x33 x34 (Some (a, b)))); (case x34 of ARMSection \<Rightarrow> Some [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] | ARMSuperSection \<Rightarrow> Some [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] | _ \<Rightarrow> Some [VSRef ((b >> 12) && mask 8) (Some APageTable), VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) = Some ref\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageCap x31 pd x33 x34 (Some (a, b))))
 4. \<And>s x xa a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap pd (Some (a, b))))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageTableCap pd (Some (a, b))))
 5. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2)))
 6. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap pd (Some (a, b))))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageTableCap pd (Some (a, b))))
 2. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2)))
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (3 subgoals):
 1. \<And>s x xa a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap pd (Some (a, b)))); s \<turnstile> ArchObjectCap (PageTableCap pd (Some (a, b)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageTableCap pd (Some (a, b))))
 2. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2)))
 3. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (2 subgoals):
 1. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 20; is_aligned pd pd_bits; pgsz = ARMSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2)))
 2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection\<rbrakk> \<Longrightarrow> \<lbrace>invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd\<rbrace> returnOk (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C])) \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, - proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; (invs and (\<lambda>s. \<exists>ref. (ref \<rhd> pd) s) and typ_at (AArch APageDirectory) pd) s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; (ref \<unrhd> pd) s\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; \<exists>slot cap. caps_of_state s slot = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> \<exists>a b. cte_wp_at (parent_for_refs (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))) (a, b) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref x xa. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; \<exists>cap. caps_of_state s (x, xa) = Some cap \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> cte_wp_at (parent_for_refs (Inr (SuperSectionPDE ptr (attribs - {Global}) rights, map (\<lambda>x. x + lookup_pd_slot pd vptr) [0 , 4 .e. 0x3C]))) (x, xa) s proof (prove)
goal (1 subgoal):
 1. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pd_bits) ` (\<lambda>x. x + lookup_pd_slot pd vptr) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs cap \<and> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> (\<lambda>x. x && ~~ mask pd_bits) ` (\<lambda>x. x + lookup_pd_slot pd vptr) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs cap
 2. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y) proof (prove)
goal (2 subgoals):
 1. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> \<forall>x\<in>set [0 , 4 .e. 0x3C]. x + lookup_pd_slot pd vptr && ~~ mask pd_bits \<in> obj_refs cap
 2. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y) proof (prove)
goal (1 subgoal):
 1. \<And>s ref x xa cap. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some cap; pd \<in> obj_refs cap; vs_cap_ref cap = Some ref\<rbrakk> \<Longrightarrow> is_pd_cap cap \<and> (\<exists>y. cap_asid cap = Some y) proof (prove)
goal (5 subgoals):
 1. \<And>s x xa x12a. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (ASIDPoolCap pd x12a))\<rbrakk> \<Longrightarrow> False
 2. \<And>s ref x xa x31 x33 x34. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageCap x31 pd x33 x34 None)); (case x34 of ARMSmallPage \<Rightarrow> None | _ \<Rightarrow> None) = Some ref\<rbrakk> \<Longrightarrow> False
 3. \<And>s ref x xa x31 x33 x34 a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageCap x31 pd x33 x34 (Some (a, b)))); (case x34 of ARMSection \<Rightarrow> Some [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] | ARMSuperSection \<Rightarrow> Some [VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None] | _ \<Rightarrow> Some [VSRef ((b >> 12) && mask 8) (Some APageTable), VSRef (b >> 20) (Some APageDirectory), VSRef (a && mask local.asid_low_bits) (Some AASIDPool), VSRef (UCAST(7 \<rightarrow> 32) (asid_high_bits_of a)) None]) = Some ref\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageCap x31 pd x33 x34 (Some (a, b))))
 4. \<And>s x xa a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap pd (Some (a, b))))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageTableCap pd (Some (a, b))))
 5. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap pd (Some (a, b))))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageTableCap pd (Some (a, b))))
 2. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2))) proof (prove)
goal (2 subgoals):
 1. \<And>s x xa a b. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageTableCap pd (Some (a, b)))); s \<turnstile> ArchObjectCap (PageTableCap pd (Some (a, b)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageTableCap pd (Some (a, b))))
 2. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa x2. \<lbrakk>vptr < kernel_base; is_aligned vptr 24; is_aligned pd pd_bits; pgsz = ARMSuperSection; invs s; typ_at (AArch APageDirectory) pd s; caps_of_state s (x, xa) = Some (ArchObjectCap (PageDirectoryCap pd (Some x2)))\<rbrakk> \<Longrightarrow> is_pd_cap (ArchObjectCap (PageDirectoryCap pd (Some x2))) proof (prove)
goal:
No subgoals!