theory VSpace_R

lemma pageTableMapped_corres:
  "corres (=) (valid_arch_state and valid_vspace_objs and pspace_aligned
                       and K (asid \<noteq> 0 \<and> asid \<le> mask asid_bits))
                 (pspace_aligned' and pspace_distinct' and no_0_obj')
       (page_table_mapped asid vaddr pt)
       (pageTableMapped asid vaddr pt)" apply (simp add: page_table_mapped_def pageTableMapped_def) apply (rule corres_guard_imp) apply (rule corres_split_catch) apply (rule corres_split_eqrE[OF find_pd_for_asid_corres]) apply simp apply (simp add: liftE_bindE) apply (rule corres_split[OF getObject_PDE_corres']) apply (corres_cases_both simp: pde_relation_aligned_def;
                  fastforce intro!: corres_returnOkTT
                            simp: pde_relation_aligned_def
                            split: if_split_asm) apply (wpsimp simp: lookup_pd_slot_def word_neq_0_conv)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (=) (valid_arch_state and valid_vspace_objs and pspace_aligned and K (asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (page_table_mapped asid vaddr pt) (pageTableMapped asid vaddr pt) proof (prove)
goal (1 subgoal):
 1. corres (=) (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) (pspace_aligned' and pspace_distinct' and no_0_obj') (doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None)) (doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE <catch> (\<lambda>_. return None)) proof (prove)
goal (3 subgoals):
 1. corres (=) ?Q ?Q' (doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE <catch> (\<lambda>y. return None)) (doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE <catch> (\<lambda>_. return None))
 2. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ?Q s
 3. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> ?Q' s proof (prove)
goal (6 subgoals):
 1. corres (?f4 \<oplus> (=)) ?P4 ?P'4 (doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE) (doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE)
 2. \<And>y uu_. ?f4 y uu_ \<Longrightarrow> corres (=) (?E4 y) (?E'4 uu_) (return None) (return None)
 3. \<lbrace>?Q4\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 4. \<lbrace>?Q'4\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 5. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> (?P4 and ?Q4) s
 6. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (?P'4 and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. asid = asid
 2. \<And>pd. corres (lfr \<oplus> (=)) (?R9 pd) (?R'9 pd) (liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)) (liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None))
 3. \<lbrace>?Q9\<rbrace> find_pd_for_asid asid \<lbrace>?R9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'9\<rbrace> findPDForASID asid \<lbrace>?R'9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y uu_. lfr y uu_ \<Longrightarrow> corres (=) (?E4 y) (?E'4 uu_) (return None) (return None)
 6. \<lbrace>?Q4\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 8. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid ?pd10 s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q9 and ?Q4) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'9 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>pd. corres (lfr \<oplus> (=)) (?R9 pd) (?R'9 pd) (liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)) (liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None))
 2. \<lbrace>?Q9\<rbrace> find_pd_for_asid asid \<lbrace>?R9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> findPDForASID asid \<lbrace>?R'9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y uu_. lfr y uu_ \<Longrightarrow> corres (=) (?E4 y) (?E'4 uu_) (return None) (return None)
 5. \<lbrace>?Q4\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 7. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid ?pd10 s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q9 and ?Q4) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'9 and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>pd. corres (lfr \<oplus> (=)) (?R9 pd) (?R'9 pd) (get_pde (lookup_pd_slot pd vaddr) >>= ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)) (getObject (lookup_pd_slot pd vaddr) >>= ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None))
 2. \<lbrace>?Q9\<rbrace> find_pd_for_asid asid \<lbrace>?R9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 3. \<lbrace>?Q'9\<rbrace> findPDForASID asid \<lbrace>?R'9\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<And>y uu_. lfr y uu_ \<Longrightarrow> corres (=) (?E4 y) (?E'4 uu_) (return None) (return None)
 5. \<lbrace>?Q4\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 7. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid ?pd10 s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q9 and ?Q4) s
 8. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'9 and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>pd rv rv'. pde_relation_aligned (lookup_pd_slot pd vaddr >> 2) rv rv' \<Longrightarrow> corres (lfr \<oplus> (=)) (?R15 pd rv) (?R'15 pd rv') (case rv of ARM_A.PageTablePDE addr x xa \<Rightarrow> returnOk (if addrFromPPtr pt = addr then Some pd else None) | _ \<Rightarrow> returnOk None) (case rv' of ARM_H.PageTablePDE pt' x xa \<Rightarrow> returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing) | _ \<Rightarrow> returnOk None)
 2. \<And>pd. \<lbrace>?Q15 pd\<rbrace> get_pde (lookup_pd_slot pd vaddr) \<lbrace>?R15 pd\<rbrace>
 3. \<And>pd. \<lbrace>?Q'15 pd\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>?R'15 pd\<rbrace>
 4. \<lbrace>?Q9\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (lookup_pd_slot pd vaddr) and ?Q15 pd\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<lbrace>?Q'9\<rbrace> findPDForASID asid \<lbrace>\<lambda>pd. pspace_aligned' and pspace_distinct' and ?Q'15 pd\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 6. \<And>y uu_. lfr y uu_ \<Longrightarrow> corres (=) (?E4 y) (?E'4 uu_) (return None) (return None)
 7. \<lbrace>?Q4\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 9. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid ?pd10 s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q9 and ?Q4) s
 10. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'9 and ?Q'4) s proof (prove)
goal (9 subgoals):
 1. \<And>pd. \<lbrace>?Q15 pd\<rbrace> get_pde (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv s. (rv = ARM_A.InvalidPDE \<longrightarrow> True \<and> True \<and> True \<and> True) \<and> (\<forall>x xa xb. rv = ARM_A.PageTablePDE x xa xb \<longrightarrow> True \<and> True \<and> True \<and> ?B'689 pd rv x xa xb s) \<and> (\<forall>x xa xb xc. rv = ARM_A.SectionPDE x xa xb xc \<longrightarrow> True \<and> True \<and> True \<and> ?B'508 pd rv x xa xb xc s) \<and> (\<forall>x xa xb. rv = ARM_A.SuperSectionPDE x xa xb \<longrightarrow> True \<and> True \<and> True \<and> True)\<rbrace>
 2. \<And>pd. \<lbrace>?Q'15 pd\<rbrace> getObject (lookup_pd_slot pd vaddr) \<lbrace>\<lambda>rv' s. ((rv' = ARM_H.InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. rv' = ARM_H.PageTablePDE x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe xf. rv' = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rv' = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> True)) \<and> ((rv' = ARM_H.InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. rv' = ARM_H.PageTablePDE x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe xf. rv' = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rv' = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> ?Q693 pd rv' x xa xb xc xd xe s)) \<and> ((rv' = ARM_H.InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. rv' = ARM_H.PageTablePDE x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe xf. rv' = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rv' = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> ?Q512 pd rv' x xa xb xc xd xe s)) \<and> (rv' = ARM_H.InvalidPDE \<longrightarrow> True) \<and> (\<forall>x xa xb. rv' = ARM_H.PageTablePDE x xa xb \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe xf. rv' = ARM_H.SectionPDE x xa xb xc xd xe xf \<longrightarrow> True) \<and> (\<forall>x xa xb xc xd xe. rv' = ARM_H.SuperSectionPDE x xa xb xc xd xe \<longrightarrow> True)\<rbrace>
 3. \<lbrace>?Q9\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. pde_at (lookup_pd_slot pd vaddr) and ?Q15 pd\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 4. \<lbrace>?Q'9\<rbrace> findPDForASID asid \<lbrace>\<lambda>pd. pspace_aligned' and pspace_distinct' and ?Q'15 pd\<rbrace>, \<lbrace>\<lambda>_ _. True\<rbrace>
 5. \<And>y uu_. lfr y uu_ \<Longrightarrow> corres (=) (?E4 y) (?E'4 uu_) (return None) (return None)
 6. \<lbrace>?Q4\<rbrace> doE pd <- find_pd_for_asid asid;
liftE (get_pde (lookup_pd_slot pd vaddr)) >>=E ARM_A.case_pde (returnOk None) (\<lambda>addr x xa. returnOk (if addrFromPPtr pt = addr then Some pd else None)) (\<lambda>word1 set1 word2 set2. returnOk None) (\<lambda>word set1 set2. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E4\<rbrace>
 7. \<lbrace>?Q'4\<rbrace> doE pd <- findPDForASID asid;
liftE (getObject (lookup_pd_slot pd vaddr)) >>=E ARM_H.case_pde (returnOk None) (\<lambda>pt' x xa. returnOk (if pt' = addrFromPPtr pt then Just pd else Nothing)) (\<lambda>word1 bool1 word2 bool2 bool3 bool4 vmrights. returnOk None) (\<lambda>word bool1 bool2 bool3 bool4 vmrights. returnOk None)
odE \<lbrace>\<lambda>_ _. True\<rbrace>, \<lbrace>?E'4\<rbrace>
 8. \<And>s. (valid_arch_state and valid_vspace_objs and pspace_aligned and (\<lambda>y. asid \<noteq> 0 \<and> asid \<le> mask local.asid_bits)) s \<Longrightarrow> ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid ?pd10 s) and valid_vspace_objs and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits) and ?Q9 and ?Q4) s
 9. \<And>s. (pspace_aligned' and pspace_distinct' and no_0_obj') s \<Longrightarrow> (pspace_aligned' and pspace_distinct' and no_0_obj' and ?Q'9 and ?Q'4) s proof (prove)
goal:
No subgoals!