theory Arch_R

lemma resolveVAddr_corres:
  "\<lbrakk> is_aligned pd pd_bits; vaddr < kernel_base \<rbrakk> \<Longrightarrow>
  corres (=) (pspace_aligned and valid_vspace_objs and page_directory_at pd
                 and (\<exists>\<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)))
                (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> vs_valid_duplicates' (ksPSpace s))
          (resolve_vaddr pd vaddr) (resolveVAddr pd vaddr)" apply (clarsimp simp: resolve_vaddr_def resolveVAddr_def) apply (rule stronger_corres_guard_imp) apply (rule_tac R="\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s"
               and R'="\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s
                           \<and> vs_valid_duplicates' (ksPSpace s)"
                in corres_split[OF get_master_pde_corres]) apply simp apply (case_tac rv, simp_all add: pde_relation'_def)[1] apply (rule corres_stateAssert_assume_stronger) apply (rule stronger_corres_guard_imp) apply (rule corres_split[OF get_master_pte_corres[OF refl]]) apply (rule corres_trivial) apply (case_tac rva, simp_all add: pte_relation'_def)[1] apply (wp get_master_pte_inv)+ apply (clarsimp simp: page_table_pte_at_lookupI) apply (clarsimp simp: page_table_pte_at_lookupI' page_table_at_state_relation) apply clarsimp apply (erule(3) page_table_at_state_relation) apply wpsimp+ apply (clarsimp simp: page_directory_pde_at_lookupI less_kernel_base_mapping_slots) apply (clarsimp simp: page_directory_pde_at_lookupI' page_directory_at_state_relation) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> corres (=) (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> vs_valid_duplicates' (ksPSpace s)) (resolve_vaddr pd vaddr) (resolveVAddr pd vaddr) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> corres (=) (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) (\<lambda>s. pspace_aligned' s \<and> pspace_distinct' s \<and> vs_valid_duplicates' (ksPSpace s)) (get_master_pde (lookup_pd_slot pd vaddr) >>= ARM_A.case_pde (return None) (\<lambda>t x xa. get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f)))) (\<lambda>f x xa xb. return (Some (ARMSection, f))) (\<lambda>f x xa. return (Some (ARMSuperSection, f)))) (getObject (lookup_pd_slot pd vaddr) >>= ARM_H.case_pde (return None) (\<lambda>table v61 v62. do y <- stateAssert (page_table_at' (ptrFromPAddr table)) [];
getObject (lookup_pt_slot_no_fail (ptrFromPAddr table) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame)))
od) (\<lambda>frame v50 v51 v52 v53 v54 v55. return (Some (ARMSection, frame))) (\<lambda>frame v56 v57 v58 v59 v60. return (Some (ARMSuperSection, frame)))) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> corres (=) ?Q ?Q' (get_master_pde (lookup_pd_slot pd vaddr) >>= ARM_A.case_pde (return None) (\<lambda>t x xa. get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f)))) (\<lambda>f x xa xb. return (Some (ARMSection, f))) (\<lambda>f x xa. return (Some (ARMSuperSection, f)))) (getObject (lookup_pd_slot pd vaddr) >>= ARM_H.case_pde (return None) (\<lambda>table v61 v62. do y <- stateAssert (page_table_at' (ptrFromPAddr table)) [];
getObject (lookup_pt_slot_no_fail (ptrFromPAddr table) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame)))
od) (\<lambda>frame v50 v51 v52 v53 v54 v55. return (Some (ARMSection, frame))) (\<lambda>frame v56 v57 v58 v59 v60. return (Some (ARMSuperSection, frame))))
 2. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q s
 3. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q' s' proof (prove)
goal (6 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> lookup_pd_slot pd vaddr = lookup_pd_slot pd vaddr
 2. \<And>rv rv'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; pde_relation' rv rv'\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. valid_pde rv s \<and> pspace_aligned s) (\<lambda>s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)) (case rv of ARM_A.InvalidPDE \<Rightarrow> return None | ARM_A.PageTablePDE t x xa \<Rightarrow> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f))) | ARM_A.SectionPDE f x xa xb \<Rightarrow> return (Some (ARMSection, f)) | ARM_A.SuperSectionPDE f x xa \<Rightarrow> return (Some (ARMSuperSection, f))) (case rv' of ARM_H.InvalidPDE \<Rightarrow> return None | ARM_H.PageTablePDE table v61 v62 \<Rightarrow> do y <- stateAssert (page_table_at' (ptrFromPAddr table)) [];
getObject (lookup_pt_slot_no_fail (ptrFromPAddr table) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame)))
od | ARM_H.SectionPDE frame v50 v51 v52 v53 v54 v55 \<Rightarrow> return (Some (ARMSection, frame)) | ARM_H.SuperSectionPDE frame v56 v57 v58 v59 v60 \<Rightarrow> return (Some (ARMSuperSection, frame)))
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 4. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; pde_relation' rv rv'\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. valid_pde rv s \<and> pspace_aligned s) (\<lambda>s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)) (case rv of ARM_A.InvalidPDE \<Rightarrow> return None | ARM_A.PageTablePDE t x xa \<Rightarrow> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr t) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f))) | ARM_A.SectionPDE f x xa xb \<Rightarrow> return (Some (ARMSection, f)) | ARM_A.SuperSectionPDE f x xa \<Rightarrow> return (Some (ARMSuperSection, f))) (case rv' of ARM_H.InvalidPDE \<Rightarrow> return None | ARM_H.PageTablePDE table v61 v62 \<Rightarrow> do y <- stateAssert (page_table_at' (ptrFromPAddr table)) [];
getObject (lookup_pt_slot_no_fail (ptrFromPAddr table) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame)))
od | ARM_H.SectionPDE frame v50 v51 v52 v53 v54 v55 \<Rightarrow> return (Some (ARMSection, frame)) | ARM_H.SuperSectionPDE frame v56 v57 v58 v59 v60 \<Rightarrow> return (Some (ARMSuperSection, frame)))
 2. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s) (\<lambda>s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)) (get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f)))) (do y <- stateAssert (page_table_at' (ptrFromPAddr x21)) [];
getObject (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame)))
od)
 2. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>s. typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s) (\<lambda>s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)) (get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f)))) (getObject (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame))))
 2. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 4. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (8 subgoals):
 1. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> corres (=) (?Q12 rv rv' x21 x22 x23) (?Q'12 rv rv' x21 x22 x23) (get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) >>= ARM_A.case_pte (return None) (\<lambda>f x xa. return (Some (ARMLargePage, f))) (\<lambda>f x xa. return (Some (ARMSmallPage, f)))) (getObject (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) >>= ARM_H.case_pte (return None) (\<lambda>frame v42 v43 v44 v45. return (Some (ARMLargePage, frame))) (\<lambda>frame v46 v47 v48 v49. return (Some (ARMSmallPage, frame))))
 2. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q12 rv rv' x21 x22 x23 s
 3. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> ?Q'12 rv rv' x21 x22 x23 s'
 4. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 5. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 6. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 7. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 8. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (10 subgoals):
 1. \<And>rv rv' x21 x22 x23 rva rv'a. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; pte_relation' rva rv'a\<rbrakk> \<Longrightarrow> corres (=) (?R16 rv rv' x21 x22 x23 rva) (?R'16 rv rv' x21 x22 x23 rv'a) (case rva of ARM_A.InvalidPTE \<Rightarrow> return None | ARM_A.LargePagePTE f x xa \<Rightarrow> return (Some (ARMLargePage, f)) | ARM_A.SmallPagePTE f x xa \<Rightarrow> return (Some (ARMSmallPage, f))) (case rv'a of ARM_H.InvalidPTE \<Rightarrow> return None | ARM_H.LargePagePTE frame v42 v43 v44 v45 \<Rightarrow> return (Some (ARMLargePage, frame)) | ARM_H.SmallPagePTE frame v46 v47 v48 v49 \<Rightarrow> return (Some (ARMSmallPage, frame)))
 2. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 rv rv' x21 x22 x23\<rbrace> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) \<lbrace>?R16 rv rv' x21 x22 x23\<rbrace>
 3. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 rv rv' x21 x22 x23\<rbrace> getObject (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) \<lbrace>?R'16 rv rv' x21 x22 x23\<rbrace>
 4. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and ?Q16 rv rv' x21 x22 x23) s
 5. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at' (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'16 rv rv' x21 x22 x23) s'
 6. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 7. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 8. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 9. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (10 subgoals):
 1. \<And>rv rv' x21 x22 x23 rva rv'a. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; pte_relation' rva rv'a\<rbrakk> \<Longrightarrow> corres (=) (\<lambda>_. True) (\<lambda>_. True) (case rva of ARM_A.InvalidPTE \<Rightarrow> return None | ARM_A.LargePagePTE f x xa \<Rightarrow> return (Some (ARMLargePage, f)) | ARM_A.SmallPagePTE f x xa \<Rightarrow> return (Some (ARMSmallPage, f))) (case rv'a of ARM_H.InvalidPTE \<Rightarrow> return None | ARM_H.LargePagePTE frame v42 v43 v44 v45 \<Rightarrow> return (Some (ARMLargePage, frame)) | ARM_H.SmallPagePTE frame v46 v47 v48 v49 \<Rightarrow> return (Some (ARMSmallPage, frame)))
 2. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 rv rv' x21 x22 x23\<rbrace> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) \<lbrace>\<lambda>rva _. True\<rbrace>
 3. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 rv rv' x21 x22 x23\<rbrace> getObject (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) \<lbrace>\<lambda>rv'a _. True\<rbrace>
 4. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and ?Q16 rv rv' x21 x22 x23) s
 5. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at' (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'16 rv rv' x21 x22 x23) s'
 6. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 7. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 8. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 9. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 10. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (9 subgoals):
 1. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q16 rv rv' x21 x22 x23\<rbrace> get_master_pte (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) \<lbrace>\<lambda>rva _. True\<rbrace>
 2. \<And>rv rv' x21 x22 x23. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23\<rbrakk> \<Longrightarrow> \<lbrace>?Q'16 rv rv' x21 x22 x23\<rbrace> getObject (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) \<lbrace>\<lambda>rv'a _. True\<rbrace>
 3. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and ?Q16 rv rv' x21 x22 x23) s
 4. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at' (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'16 rv rv' x21 x22 x23) s'
 5. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 6. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 7. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 8. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 9. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (7 subgoals):
 1. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and (\<lambda>_. True)) s
 2. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at' (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s'
 3. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 4. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 5. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 6. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 7. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (6 subgoals):
 1. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pte_at' (lookup_pt_slot_no_fail (ptrFromPAddr x21) vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s'
 2. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 4. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 6. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. \<And>rv rv' x21 x22 x23 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; rv' = ARM_H.PageTablePDE x21 (ParityEnabled \<in> x22) x23; rv = ARM_A.PageTablePDE x21 x22 x23; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s \<and> pspace_aligned s; pspace_distinct' s' \<and> pspace_aligned' s' \<and> vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 2. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (5 subgoals):
 1. \<And>x21 s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (s, s') \<in> state_relation; typ_at (AArch APageTable) (ptrFromPAddr x21) s; pspace_aligned s; pspace_distinct' s'; pspace_aligned' s'; vs_valid_duplicates' (ksPSpace s')\<rbrakk> \<Longrightarrow> page_table_at' (ptrFromPAddr x21) s'
 2. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 3. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 4. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 5. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (4 subgoals):
 1. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q4\<rbrace> get_master_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. valid_pde rv s \<and> pspace_aligned s\<rbrace>
 2. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base\<rbrakk> \<Longrightarrow> \<lbrace>?Q'4\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>_ s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s)\<rbrace>
 3. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at (lookup_pd_slot pd vaddr) and ?Q4) s
 4. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and ?Q'4) s' proof (prove)
goal (2 subgoals):
 1. \<And>s s' ref. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (s, s') \<in> state_relation; pspace_aligned s; pspace_aligned' s'; valid_vspace_objs s; pspace_distinct' s'; vs_valid_duplicates' (ksPSpace s'); typ_at (AArch APageDirectory) pd s; (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vaddr) s \<and> UCAST(32 \<rightarrow> 12) (lookup_pd_slot pd vaddr && mask pd_bits >> 2) \<notin> kernel_mapping_slots
 2. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s))) s' proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>is_aligned pd pd_bits; vaddr < kernel_base; (pspace_aligned and valid_vspace_objs and typ_at (AArch APageDirectory) pd and (\<lambda>s. \<exists>ref. (ref \<rhd> (lookup_pd_slot pd vaddr && ~~ mask pd_bits)) s)) s; pspace_aligned' s' \<and> pspace_distinct' s' \<and> vs_valid_duplicates' (ksPSpace s'); (s, s') \<in> state_relation\<rbrakk> \<Longrightarrow> (pde_at' (lookup_pd_slot pd vaddr) and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and pspace_aligned' and pspace_distinct' and (\<lambda>s. pspace_distinct' s \<and> pspace_aligned' s \<and> vs_valid_duplicates' (ksPSpace s))) s' proof (prove)
goal:
No subgoals!