theory VSpace_C

lemma checkMappingPPtr_pde_ccorres:
  assumes pre:
    "\<And>pde \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pde'. cslift s (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation pde pde')
                            \<and> (\<sigma>, s) \<in> rf_sr}
           call1;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip;;
           call3;; Cond U return_void_C Skip
       {s. (\<sigma>, s) \<in> rf_sr \<and> (isSectionPDE pde \<and> pgsz = ARMSection
                                \<or> isSuperSectionPDE pde \<and> pgsz = ARMSuperSection)
                 \<and> pdeFrame pde = addrFromPPtr pptr},
       {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSectionPDE pde \<and> pgsz = ARMSection
                                \<or> isSuperSectionPDE pde \<and> pgsz = ARMSuperSection)
                 \<and> pdeFrame pde = addrFromPPtr pptr)}"
  shows
  "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc
       \<top> UNIV [SKIP]
     (checkMappingPPtr pptr pgsz (Inr pde_ptr))
     (call1;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip;;
      call3;; Cond U return_void_C Skip)" apply (simp add: checkMappingPPtr_def liftE_bindE) apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. UNIV", OF _ _ getObject_ko_at, simplified]) apply (rule stronger_ccorres_guard_imp) apply (rule ccorres_from_vcg_might_throw[where P=\<top>]) apply (rule allI) apply (rule conseqPost, rule conseqPre, rule_tac \<sigma>1=\<sigma> and pde1=rv in pre) apply clarsimp apply (erule CollectE, assumption) apply (fold_subgoals (prefix))[2] subgoal by (auto simp: in_monad Bex_def isSectionPDE_def isSuperSectionPDE_def
                         split: pde.split vmpage_size.split) apply (wp empty_fail_getObject | simp)+ apply (erule cmap_relationE1[OF rf_sr_cpde_relation]) apply (erule ko_at_projectKO_opt) apply simp apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def pdeBits_def)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (\<lambda>_. True) UNIV [SKIP] (checkMappingPPtr pptr pgsz (Inr pde_ptr)) (call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T return_void_C SKIP;;
call3;;
Cond U return_void_C SKIP) proof (prove)
goal (1 subgoal):
 1. ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (\<lambda>_. True) UNIV [SKIP] (getObject pde_ptr >>= 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 pgsz of local.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 pgsz of local.ARMSuperSection \<Rightarrow> unlessE (base = addrFromPPtr pptr) $ throw Fault_H.lookup_failure.InvalidRoot | _ \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot)) (call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T return_void_C SKIP;;
call3;;
Cond U return_void_C SKIP) proof (prove)
goal (5 subgoals):
 1. \<And>rv. ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (ko_at' rv pde_ptr) UNIV [SKIP] (case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) (call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T return_void_C SKIP;;
call3;;
Cond U return_void_C SKIP)
 2. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 4. \<And>v. 1 < 2 ^ objBits v
 5. empty_fail (getObject pde_ptr) proof (prove)
goal (7 subgoals):
 1. \<And>rv. ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (?Q21 rv) (?Q'21 rv) [SKIP] (case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) (call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T return_void_C SKIP;;
call3;;
Cond U return_void_C SKIP)
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> ?Q21 rv s
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pde_ptr) proof (prove)
goal (7 subgoals):
 1. \<And>rv. \<forall>\<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> ?Q'21 rv \<and> (\<sigma>, s) \<in> rf_sr} call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T return_void_C SKIP;;
call3;;
Cond U return_void_C SKIP {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)},{s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)}
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pde_ptr) proof (prove)
goal (7 subgoals):
 1. \<And>rv \<sigma>. \<Gamma>\<turnstile> {s. True \<and> s \<in> ?Q'21 rv \<and> (\<sigma>, s) \<in> rf_sr} call1;;
Cond S return_void_C SKIP;;
call2;;
Cond T return_void_C SKIP;;
call3;;
Cond U return_void_C SKIP {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)},{s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)}
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pde_ptr) proof (prove)
goal (9 subgoals):
 1. \<And>rv \<sigma>. {s. True \<and> s \<in> ?Q'21 rv \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. True \<and> (\<exists>pde'. cslift s (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde') \<and> (\<sigma>, s) \<in> rf_sr}
 2. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)}
 3. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)}
 4. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 5. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 6. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 8. \<And>v. 1 < 2 ^ objBits v
 9. empty_fail (getObject pde_ptr) proof (prove)
goal (9 subgoals):
 1. \<And>rv \<sigma> x. \<lbrakk>x \<in> ?Q'21 rv; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>pde'. cslift x (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'
 2. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)}
 3. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)}
 4. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 5. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> ?Q'21 rv
 6. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 8. \<And>v. 1 < 2 ^ objBits v
 9. empty_fail (getObject pde_ptr) proof (prove)
goal (8 subgoals):
 1. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)}
 2. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)}
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 4. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> {x. \<exists>pde'. cslift x (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'}
 5. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 7. \<And>v. 1 < 2 ^ objBits v
 8. empty_fail (getObject pde_ptr) proof (prove)
goal (7 subgoals):
 1. \<And>rv \<sigma>. {s. (\<sigma>, s) \<in> rf_sr \<and> (isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)} &&& {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSectionPDE rv \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)}
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 3. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> {x. \<exists>pde'. cslift x (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'}
 4. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 6. \<And>v. 1 < 2 ^ objBits v
 7. empty_fail (getObject pde_ptr) proof (prove)
goal (1 subgoal):
 1. {s. (\<sigma>_, s) \<in> rf_sr \<and> (isSectionPDE rv_ \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv_ \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv_ = addrFromPPtr pptr} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv_ of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>_). (\<sigma>', s) \<in> rf_sr \<and> inr_rrel dc rv (xfdc s)} &&& {s. (\<sigma>_, s) \<in> rf_sr \<and> \<not> ((isSectionPDE rv_ \<and> pgsz = Wellformed_C.ARMSection \<or> isSuperSectionPDE rv_ \<and> pgsz = Wellformed_C.ARMSuperSection) \<and> pdeFrame rv_ = addrFromPPtr pptr)} \<subseteq> {s. \<exists>(rv, \<sigma>')\<in>fst ((case rv_ of ARM_H.SectionPDE base x xa xb xc xd xe \<Rightarrow> case pgsz of local.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 pgsz of local.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) \<sigma>_). (\<sigma>', s) \<in> rf_sr \<and> inl_rrel dc rv (xfdc s)} proof (prove)
goal (6 subgoals):
 1. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> True
 2. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; s' \<in> UNIV; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> s' \<in> {x. \<exists>pde'. cslift x (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'}
 3. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 5. \<And>v. 1 < 2 ^ objBits v
 6. empty_fail (getObject pde_ptr) proof (prove)
goal (5 subgoals):
 1. \<And>rv s s'. \<lbrakk>ko_at' rv pde_ptr s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> \<exists>pde'. cslift s' (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'
 2. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 4. \<And>v. 1 < 2 ^ objBits v
 5. empty_fail (getObject pde_ptr) proof (prove)
goal (6 subgoals):
 1. \<And>rv s s'. ko_at' rv pde_ptr s \<Longrightarrow> map_to_pdes (ksPSpace s) (?x3 rv s s') = Some (?y3 rv s s')
 2. \<And>rv s s' y'. \<lbrakk>ko_at' rv pde_ptr s; map_to_pdes (ksPSpace s) (?x3 rv s s') = Some (?y3 rv s s'); cpde_relation (?y3 rv s s') y'; cslift s' (pde_Ptr (?x3 rv s s')) = Some y'\<rbrakk> \<Longrightarrow> \<exists>pde'. cslift s' (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'
 3. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 5. \<And>v. 1 < 2 ^ objBits v
 6. empty_fail (getObject pde_ptr) proof (prove)
goal (5 subgoals):
 1. \<And>rv s s' y'. \<lbrakk>ko_at' rv pde_ptr s; map_to_pdes (ksPSpace s) pde_ptr = Some rv; cpde_relation rv y'; cslift s' (pde_Ptr pde_ptr) = Some y'\<rbrakk> \<Longrightarrow> \<exists>pde'. cslift s' (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation rv pde'
 2. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 4. \<And>v. 1 < 2 ^ objBits v
 5. empty_fail (getObject pde_ptr) proof (prove)
goal (4 subgoals):
 1. \<And>s. \<lbrace>(=) s\<rbrace> getObject pde_ptr \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>q n ko. loadObject pde_ptr q n ko = loadObject_default pde_ptr q n ko
 3. \<And>v. 1 < 2 ^ objBits v
 4. empty_fail (getObject pde_ptr) proof (prove)
goal:
No subgoals!