theory VSpace_R

lemma checkMappingPPtr_corres:
  "corres (dc \<oplus> dc)
            ((case slotptr of Inl ptr \<Rightarrow> pte_at ptr | Inr ptr \<Rightarrow> pde_at ptr) and
             (\<lambda>s. (case slotptr of Inl ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz)
                   | Inr ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz))))
            (pspace_aligned' and pspace_distinct')
      (throw_on_false v (check_mapping_pptr pptr sz slotptr))
      (checkMappingPPtr pptr sz slotptr)" apply (rule corres_gen_asm) apply (simp add: throw_on_false_def liftE_bindE check_mapping_pptr_def
                   checkMappingPPtr_def) apply (cases slotptr, simp_all add: liftE_bindE) apply (rule corres_guard_imp) apply (rule corres_split[OF getObject_PTE_corres']) apply (rule corres_trivial) subgoal by (cases sz,
         auto simp add: is_aligned_mask[symmetric]
         is_aligned_shiftr pg_entry_align_def
         unlessE_def returnOk_def pte_relation_aligned_def
         split: ARM_A.pte.split if_splits ARM_H.pte.split ) apply wp+ apply simp apply (simp add:is_aligned_mask[symmetric] is_aligned_shiftr pg_entry_align_def) apply (rule corres_guard_imp) apply (rule corres_split[OF getObject_PDE_corres']) apply (rule corres_trivial) subgoal by (cases sz,
         auto simp add: is_aligned_mask[symmetric]
         is_aligned_shiftr pg_entry_align_def
         unlessE_def returnOk_def pde_relation_aligned_def
         split: ARM_A.pde.split if_splits ARM_H.pde.split ) apply wp+ apply simp+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres (dc \<oplus> dc) ((case slotptr of Inl ptr \<Rightarrow> pte_at ptr | Inr ptr \<Rightarrow> pde_at ptr) and (\<lambda>s. case slotptr of Inl ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz) | Inr ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz))) (pspace_aligned' and pspace_distinct') (throw_on_false v (check_mapping_pptr pptr sz slotptr)) (checkMappingPPtr pptr sz slotptr) proof (prove)
goal (1 subgoal):
 1. case slotptr of Inl ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz) | Inr ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz) \<Longrightarrow> corres (dc \<oplus> dc) (case slotptr of Inl ptr \<Rightarrow> pte_at ptr | Inr ptr \<Rightarrow> pde_at ptr) (pspace_aligned' and pspace_distinct') (throw_on_false v (check_mapping_pptr pptr sz slotptr)) (checkMappingPPtr pptr sz slotptr) proof (prove)
goal (1 subgoal):
 1. case slotptr of Inl ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz) | Inr ptr \<Rightarrow> is_aligned ptr (pg_entry_align sz) \<Longrightarrow> corres (dc \<oplus> dc) (case slotptr of Inl ptr \<Rightarrow> pte_at ptr | Inr ptr \<Rightarrow> pde_at ptr) (pspace_aligned' and pspace_distinct') (do va <- case slotptr of Inl ptePtr \<Rightarrow> do pte <- get_pte ptePtr;
return $ case pte of ARM_A.InvalidPTE \<Rightarrow> False | ARM_A.LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMLargePage | ARM_A.SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSmallPage
od | Inr pdePtr \<Rightarrow> do pde <- get_pde pdePtr;
return $ case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False
od;
unlessE va (throwError v)
od) (case slotptr of Inl pt \<Rightarrow> doE pte <- withoutFailure $ getObject pt;
case (pte, sz) of (ARM_H.InvalidPTE, b) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.LargePagePTE base x xa xb xc, ARMLargePage) \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.LargePagePTE base x xa xb xc, _) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.SmallPagePTE base x xa xb xc, ARMSmallPage) \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.SmallPagePTE base x xa xb xc, _) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot
odE | Inr pd \<Rightarrow> doE pde <- withoutFailure $ getObject pd;
case (pde, sz) of (ARM_H.SectionPDE base x xa xb xc xd xe, ARMSection) \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.SectionPDE base x xa xb xc xd xe, _) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.SuperSectionPDE base x xa xb xc xd, ARMSuperSection) \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | (ARM_H.SuperSectionPDE base x xa xb xc xd, _) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | (_, b) \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot
odE) proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pte_at a) (pspace_aligned' and pspace_distinct') (do pte <- get_pte a;
unlessE (case pte of ARM_A.InvalidPTE \<Rightarrow> False | ARM_A.LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMLargePage | ARM_A.SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSmallPage) (throwError v)
od) (getObject a >>= ARM_H.case_pte (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc. case sz of ARMLargePage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc. case sz of ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot))
 2. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (4 subgoals):
 1. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (?Q3 a) (?Q'3 a) (do pte <- get_pte a;
unlessE (case pte of ARM_A.InvalidPTE \<Rightarrow> False | ARM_A.LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMLargePage | ARM_A.SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSmallPage) (throwError v)
od) (getObject a >>= ARM_H.case_pte (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc. case sz of ARMLargePage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc. case sz of ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot))
 2. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_at a s\<rbrakk> \<Longrightarrow> ?Q3 a s
 3. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'3 a s
 4. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (6 subgoals):
 1. \<And>a pte rv'. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_relation_aligned (a >> 2) pte rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (?R7 a pte) (?R'7 a rv') (unlessE (case pte of ARM_A.InvalidPTE \<Rightarrow> False | ARM_A.LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMLargePage | ARM_A.SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSmallPage) (throwError v)) (case rv' of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case sz of ARMLargePage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SmallPagePTE base x xa xb xc \<Rightarrow> case sz of ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)
 2. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a\<rbrace> get_pte a \<lbrace>?R7 a\<rbrace>
 3. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a\<rbrace> getObject a \<lbrace>?R'7 a\<rbrace>
 4. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_at a s\<rbrakk> \<Longrightarrow> (pte_at a and ?Q7 a) s
 5. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'7 a) s
 6. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (6 subgoals):
 1. \<And>a pte rv'. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_relation_aligned (a >> 2) pte rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (unlessE (case pte of ARM_A.InvalidPTE \<Rightarrow> False | ARM_A.LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMLargePage | ARM_A.SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSmallPage) (throwError v)) (case rv' of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case sz of ARMLargePage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SmallPagePTE base x xa xb xc \<Rightarrow> case sz of ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)
 2. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a\<rbrace> get_pte a \<lbrace>\<lambda>pte _. True\<rbrace>
 3. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a\<rbrace> getObject a \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_at a s\<rbrakk> \<Longrightarrow> (pte_at a and ?Q7 a) s
 5. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'7 a) s
 6. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned a_ (pg_entry_align sz); slotptr = Inl a_; pte_relation_aligned (a_ >> 2) pte_ rv'_\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (unlessE (case pte_ of ARM_A.InvalidPTE \<Rightarrow> False | ARM_A.LargePagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMLargePage | ARM_A.SmallPagePTE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSmallPage) (throwError v)) (case rv'_ of ARM_H.InvalidPTE \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.LargePagePTE base x xa xb xc \<Rightarrow> case sz of ARMLargePage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SmallPagePTE base x xa xb xc \<Rightarrow> case sz of ARMSmallPage \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) proof (prove)
goal (5 subgoals):
 1. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>?Q7 a\<rbrace> get_pte a \<lbrace>\<lambda>pte _. True\<rbrace>
 2. \<And>a. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a\<rbrakk> \<Longrightarrow> \<lbrace>?Q'7 a\<rbrace> getObject a \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_at a s\<rbrakk> \<Longrightarrow> (pte_at a and ?Q7 a) s
 4. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'7 a) s
 5. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (3 subgoals):
 1. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; pte_at a s\<rbrakk> \<Longrightarrow> (pte_at a and (\<lambda>_. True)) s
 2. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s
 3. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (2 subgoals):
 1. \<And>a s. \<lbrakk>is_aligned a (pg_entry_align sz); slotptr = Inl a; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s
 2. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (1 subgoal):
 1. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (pde_at b) (pspace_aligned' and pspace_distinct') (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) proof (prove)
goal (3 subgoals):
 1. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (?Q20 b) (?Q'20 b) (do pde <- get_pde b;
unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)
od) (getObject b >>= ARM_H.case_pde (throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>word1 bool word2. throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd xe. case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) (\<lambda>base x xa xb xc xd. case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot))
 2. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_at b s\<rbrakk> \<Longrightarrow> ?Q20 b s
 3. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> ?Q'20 b s proof (prove)
goal (5 subgoals):
 1. \<And>b pde rv'. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_relation_aligned (b >> 2) pde rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (?R24 b pde) (?R'24 b rv') (unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)) (case rv' of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SuperSectionPDE base x xa xb xc xd \<Rightarrow> case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)
 2. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 b\<rbrace> get_pde b \<lbrace>?R24 b\<rbrace>
 3. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 b\<rbrace> getObject b \<lbrace>?R'24 b\<rbrace>
 4. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_at b s\<rbrakk> \<Longrightarrow> (pde_at b and ?Q24 b) s
 5. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'24 b) s proof (prove)
goal (5 subgoals):
 1. \<And>b pde rv'. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_relation_aligned (b >> 2) pde rv'\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (unlessE (case pde of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)) (case rv' of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SuperSectionPDE base x xa xb xc xd \<Rightarrow> case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)
 2. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 b\<rbrace> get_pde b \<lbrace>\<lambda>pde _. True\<rbrace>
 3. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 b\<rbrace> getObject b \<lbrace>\<lambda>rv' _. True\<rbrace>
 4. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_at b s\<rbrakk> \<Longrightarrow> (pde_at b and ?Q24 b) s
 5. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'24 b) s proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_aligned b_ (pg_entry_align sz); slotptr = Inr b_; pde_relation_aligned (b_ >> 2) pde_ rv'_\<rbrakk> \<Longrightarrow> corres (dc \<oplus> dc) (\<lambda>_. True) (\<lambda>_. True) (unlessE (case pde_ of ARM_A.SectionPDE x xa xb xc \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSection | ARM_A.SuperSectionPDE x xa xb \<Rightarrow> x = addrFromPPtr pptr \<and> sz = ARMSuperSection | _ \<Rightarrow> False) (throwError v)) (case rv'_ of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case sz of ARMSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | ARM_H.SuperSectionPDE base x xa xb xc xd \<Rightarrow> case sz of ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot) proof (prove)
goal (4 subgoals):
 1. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>?Q24 b\<rbrace> get_pde b \<lbrace>\<lambda>pde _. True\<rbrace>
 2. \<And>b. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b\<rbrakk> \<Longrightarrow> \<lbrace>?Q'24 b\<rbrace> getObject b \<lbrace>\<lambda>rv' _. True\<rbrace>
 3. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_at b s\<rbrakk> \<Longrightarrow> (pde_at b and ?Q24 b) s
 4. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and ?Q'24 b) s proof (prove)
goal (2 subgoals):
 1. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; pde_at b s\<rbrakk> \<Longrightarrow> (pde_at b and (\<lambda>_. True)) s
 2. \<And>b s. \<lbrakk>is_aligned b (pg_entry_align sz); slotptr = Inr b; (pspace_aligned' and pspace_distinct') s\<rbrakk> \<Longrightarrow> (pspace_aligned' and pspace_distinct' and (\<lambda>_. True)) s proof (prove)
goal:
No subgoals!